-----------------------------------------------------------------------------
-- |
-- 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
  , (\#)
  , (#<<)
  )

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 :: 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
. (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 :: PowerSet a -> Int
index = \case
    []     -> Int
0
    (a
y:PowerSet a
yr) -> (Int, Int, Int, PowerSet a) -> Int
forall b b a.
(?bounds::b, Integral b, Finite b a) =>
(b, b, Int, [a]) -> b
powsum (Int
0,Int
2,a -> Int
forall b a. (?bounds::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. (?bounds::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. (?bounds::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 :: Int -> PowerSet a
value Int
n =
    let 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) -> a -> Int
forall a b. (T a -> b) -> a -> b
#<< PowerSet a -> a
forall a. [a] -> a
head 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 :: 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
. (forall a. T (PowerSet a) -> T a
forall b a. b -> T a
(\#) :: T (PowerSet a) -> T a)

  values :: [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 :: ([a], a, a) -> [a]
bin ([a]
a,!a
s,!a
n)
      | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
0         = [a] -> [a]
forall a. [a] -> [a]
reverse [a]
a
      | a
n a -> a -> a
forall a. Integral a => a -> a -> a
`mod` a
2 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
1 = ([a], a, a) -> [a]
bin (a
sa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
a, a
sa -> a -> a
forall a. Num a => a -> a -> a
+a
1, a
n a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
2)
      | Bool
otherwise     = ([a], a, a) -> [a]
bin ([a]
a, a
sa -> a -> a
forall a. Num a => a -> a -> a
+a
1, a
n a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
2)
  in
    ([Int], Int, Int) -> [Int]
forall a a. (Integral a, Num a) => ([a], a, a) -> [a]
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 :: [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 (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 (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> [[a]] -> [[a]]
forall a. a -> [[a]] -> [[a]]
f []

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