-----------------------------------------------------------------------------
-- |
-- Module      :  Finite.PowerSet
-- Maintainer  :  Felix Klein
--
-- Encodes the powerset of a finite range type.
--
-----------------------------------------------------------------------------

{-# LANGUAGE

    MultiParamTypeClasses
  , FlexibleInstances
  , FlexibleContexts
  , LambdaCase
  , MultiWayIf
  , BangPatterns

  #-}

-----------------------------------------------------------------------------

module Finite.PowerSet
  ( PowerSet
  ) where

-----------------------------------------------------------------------------

import Finite.Type
  ( T
  , (#)
  , (\#)
  , (#<<)
  , v2t
  )

import Finite.Class
  ( Finite(..)
  )

import Control.Exception
  ( assert
  )

-----------------------------------------------------------------------------

-- | Powersets are just lists of the correpsonding elements. The type
-- has only been added for clearification. Consider the corresponding
-- instance of 'Finite' for possible applications.

type PowerSet a = [a]

-----------------------------------------------------------------------------

-- | If the number of elements associated with a type is finite, then
-- it also has finite number of powersets.

instance Finite b a => Finite b (PowerSet a) where

  elements :: FiniteBounds b => T (PowerSet a) -> Int
elements =
    Int -> Int -> Int
forall {t} {t}. (Eq t, Num t, Num t) => t -> t -> t
pow2 Int
2 (Int -> Int) -> (T (PowerSet a) -> Int) -> T (PowerSet a) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T a -> Int
forall b a. (Finite b a, FiniteBounds b) => T a -> Int
elements (T a -> Int) -> (T (PowerSet a) -> T a) -> T (PowerSet a) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (T (PowerSet a) -> T a
forall {a}. T (PowerSet a) -> T a
forall b a. b -> T a
(\#) :: T (PowerSet a) -> T a)

    where
      pow2 :: t -> t -> t
pow2 !t
a !t
n = case t
n of
        t
0 -> t
1
        t
1 -> t
a
        t
_ -> t -> t -> t
pow2 (t
2t -> t -> t
forall a. Num a => a -> a -> a
*t
a) (t
nt -> t -> t
forall a. Num a => a -> a -> a
-t
1)

  index :: FiniteBounds b => PowerSet a -> Int
index = \case
    []     -> Int
0
    (a
y:PowerSet a
yr) -> (Int, Int, Int, PowerSet a) -> Int
forall {b} {b} {a}.
(Integral b, FiniteBounds b, Finite b a) =>
(b, b, Int, [a]) -> b
powsum (Int
0,Int
2,a -> Int
forall {b} {a}. (FiniteBounds b, Finite b a) => a -> Int
idx a
y,PowerSet a
yr)

    where
      idx :: a -> Int
idx a
x = a -> Int
forall b a. (Finite b a, FiniteBounds b) => a -> Int
index a
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- T a -> Int
forall b a. (Finite b a, FiniteBounds b) => T a -> Int
offset (T a -> Int) -> a -> Int
forall a b. (T a -> b) -> a -> b
#<< a
x

      powsum :: (b, b, Int, [a]) -> b
powsum !(b, b, Int, [a])
p = case (b, b, Int, [a])
p of
        (b
a,b
_,Int
0,[])   ->
          b
a b -> b -> b
forall a. Num a => a -> a -> a
+ (b
1 b -> b -> b
forall a. Num a => a -> a -> a
- (b
a b -> b -> b
forall a. Integral a => a -> a -> a
`mod` b
2))
        (b
a,b
p,Int
1,[])   ->
          b
a b -> b -> b
forall a. Num a => a -> a -> a
+ ((b
1 b -> b -> b
forall a. Num a => a -> a -> a
- ((b
a b -> b -> b
forall a. Integral a => a -> a -> a
`mod` (b
2b -> b -> b
forall a. Num a => a -> a -> a
*b
p)) b -> b -> b
forall a. Integral a => a -> a -> a
`div` b
p)) b -> b -> b
forall a. Num a => a -> a -> a
* b
p)
        (b
a,b
_,Int
0,a
x:[a]
xr) ->
          (b, b, Int, [a]) -> b
powsum (b
a b -> b -> b
forall a. Num a => a -> a -> a
+ (b
1 b -> b -> b
forall a. Num a => a -> a -> a
- (b
a b -> b -> b
forall a. Integral a => a -> a -> a
`mod` b
2)),b
2,a -> Int
forall {b} {a}. (FiniteBounds b, Finite b a) => a -> Int
idx a
x,[a]
xr)
        (b
a,b
p,Int
1,a
x:[a]
xr) ->
          (b, b, Int, [a]) -> b
powsum (b
a b -> b -> b
forall a. Num a => a -> a -> a
+ ((b
1 b -> b -> b
forall a. Num a => a -> a -> a
- ((b
a b -> b -> b
forall a. Integral a => a -> a -> a
`mod` (b
2b -> b -> b
forall a. Num a => a -> a -> a
*b
p)) b -> b -> b
forall a. Integral a => a -> a -> a
`div` b
p)) b -> b -> b
forall a. Num a => a -> a -> a
* b
p), b
2, a -> Int
forall {b} {a}. (FiniteBounds b, Finite b a) => a -> Int
idx a
x, [a]
xr)
        (b
a,b
p,Int
n,[a]
xs)   ->
          (b, b, Int, [a]) -> b
powsum (b
a,b
2b -> b -> b
forall a. Num a => a -> a -> a
*b
p,Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1,[a]
xs)

  value :: FiniteBounds b => Int -> PowerSet a
value Int
n =
    let ty :: T [a] -> T a
        ty :: forall {a}. T (PowerSet a) -> T a
ty T [a]
_ = T a
forall a. T a
(#)
        bs :: PowerSet a
bs = (Int -> a) -> [Int] -> PowerSet a
forall a b. (a -> b) -> [a] -> [b]
map (Int -> a
forall b a. (Finite b a, FiniteBounds b) => Int -> a
value (Int -> a) -> (Int -> Int) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (T a -> Int
forall b a. (Finite b a, FiniteBounds b) => T a -> Int
offset (T a -> Int) -> T a -> Int
forall a b. (a -> b) -> a -> b
$ T (PowerSet a) -> T a
forall {a}. T (PowerSet a) -> T a
ty (T (PowerSet a) -> T a) -> T (PowerSet a) -> T a
forall a b. (a -> b) -> a -> b
$ PowerSet a -> T (PowerSet a)
forall a. a -> T a
v2t PowerSet a
bs))) ([Int] -> PowerSet a) -> [Int] -> PowerSet a
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
bin Int
n
    in Bool -> PowerSet a -> PowerSet a
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< (T (PowerSet a) -> Int
forall b a. (Finite b a, FiniteBounds b) => T a -> Int
elements (T (PowerSet a) -> Int) -> PowerSet a -> Int
forall a b. (T a -> b) -> a -> b
#<< PowerSet a
bs)) PowerSet a
bs

  offset :: FiniteBounds b => T (PowerSet a) -> Int
offset = T a -> Int
forall b a. (Finite b a, FiniteBounds b) => T a -> Int
offset (T a -> Int) -> (T (PowerSet a) -> T a) -> T (PowerSet a) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (T (PowerSet a) -> T a
forall {a}. T (PowerSet a) -> T a
forall b a. b -> T a
(\#) :: T (PowerSet a) -> T a)

  values :: FiniteBounds b => [PowerSet a]
values = PowerSet a -> [PowerSet a]
forall a. [a] -> [[a]]
powerset PowerSet a
forall b a. (Finite b a, FiniteBounds b) => [a]
values

-----------------------------------------------------------------------------

-- | Converts an Int value to a list of Int values of logarithmic size
-- encoding the original value.

bin
  :: Int -> [Int]

bin :: Int -> [Int]
bin Int
x =
  let
    bin :: ([b], b, c) -> [b]
bin ([b]
a,!b
s,!c
n)
      | c
n c -> c -> Bool
forall a. Ord a => a -> a -> Bool
<= c
0         = [b] -> [b]
forall a. [a] -> [a]
reverse [b]
a
      | c
n c -> c -> c
forall a. Integral a => a -> a -> a
`mod` c
2 c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== c
1 = ([b], b, c) -> [b]
bin (b
sb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
a, b
sb -> b -> b
forall a. Num a => a -> a -> a
+b
1, c
n c -> c -> c
forall a. Integral a => a -> a -> a
`div` c
2)
      | Bool
otherwise     = ([b], b, c) -> [b]
bin ([b]
a, b
sb -> b -> b
forall a. Num a => a -> a -> a
+b
1, c
n c -> c -> c
forall a. Integral a => a -> a -> a
`div` c
2)
  in
    ([Int], Int, Int) -> [Int]
forall {c} {b}. (Integral c, Num b) => ([b], b, c) -> [b]
bin ([],Int
0,Int
x)

-----------------------------------------------------------------------------

-- | Creates the powerset of a set, for sets represented as lists. If
-- the given list is sorted, the created powerset will be sorted
-- lexographically and the elements themselve will be sorted as well.

powerset
  :: [a] -> [[a]]

powerset :: forall a. [a] -> [[a]]
powerset =
  let f :: a -> [[a]] -> [[a]]
f a
x [[a]]
a = [a
x] [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: ([a] -> [[a]] -> [[a]]) -> [[a]] -> [[a]] -> [[a]]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((:) ([a] -> [[a]] -> [[a]]) -> ([a] -> [a]) -> [a] -> [[a]] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:)) [[a]]
a [[a]]
a
  in  ([][a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
:) ([[a]] -> [[a]]) -> ([a] -> [[a]]) -> [a] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> [[a]] -> [[a]]) -> [[a]] -> [a] -> [[a]]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> [[a]] -> [[a]]
forall {a}. a -> [[a]] -> [[a]]
f []

-----------------------------------------------------------------------------