{-# LANGUAGE TypeFamilies #-}
module Algebra.Boolean.Free
  ( FreeBoolean (..)
  ) where

import           Control.Monad     (ap)
import           Algebra.Lattice   ( BoundedJoinSemiLattice (..)
                                   , BoundedMeetSemiLattice (..)
                                   , Lattice (..)
                                   )
import           Data.Algebra.Free ( AlgebraType0
                                   , AlgebraType
                                   , FreeAlgebra (..)
                                   , fmapFree
                                   , bindFree
                                   )

import           Algebra.Boolean   (Boolean)
import           Algebra.Heyting

-- |
-- Free Boolean algebra.  @'FreeAlgebra'@ instance provides all the usual
-- combinators for a free algebra.
newtype FreeBoolean a = FreeBoolean
  { FreeBoolean a -> forall h. Boolean h => (a -> h) -> h
runFreeBoolean :: forall h . Boolean h => (a -> h) -> h }

instance BoundedJoinSemiLattice (FreeBoolean a) where
  bottom :: FreeBoolean a
bottom = (forall h. Boolean h => (a -> h) -> h) -> FreeBoolean a
forall a. (forall h. Boolean h => (a -> h) -> h) -> FreeBoolean a
FreeBoolean (\a -> h
_ -> h
forall a. BoundedJoinSemiLattice a => a
bottom)

instance BoundedMeetSemiLattice (FreeBoolean a) where
  top :: FreeBoolean a
top = (forall h. Boolean h => (a -> h) -> h) -> FreeBoolean a
forall a. (forall h. Boolean h => (a -> h) -> h) -> FreeBoolean a
FreeBoolean (\a -> h
_ -> h
forall a. BoundedMeetSemiLattice a => a
top)

instance Lattice (FreeBoolean a) where
  FreeBoolean forall h. Boolean h => (a -> h) -> h
f /\ :: FreeBoolean a -> FreeBoolean a -> FreeBoolean a
/\ FreeBoolean forall h. Boolean h => (a -> h) -> h
g = (forall h. Boolean h => (a -> h) -> h) -> FreeBoolean a
forall a. (forall h. Boolean h => (a -> h) -> h) -> FreeBoolean a
FreeBoolean (\a -> h
inj -> (a -> h) -> h
forall h. Boolean h => (a -> h) -> h
f a -> h
inj h -> h -> h
forall a. Lattice a => a -> a -> a
/\ (a -> h) -> h
forall h. Boolean h => (a -> h) -> h
g a -> h
inj)
  FreeBoolean forall h. Boolean h => (a -> h) -> h
f \/ :: FreeBoolean a -> FreeBoolean a -> FreeBoolean a
\/ FreeBoolean forall h. Boolean h => (a -> h) -> h
g = (forall h. Boolean h => (a -> h) -> h) -> FreeBoolean a
forall a. (forall h. Boolean h => (a -> h) -> h) -> FreeBoolean a
FreeBoolean (\a -> h
inj -> (a -> h) -> h
forall h. Boolean h => (a -> h) -> h
f a -> h
inj h -> h -> h
forall a. Lattice a => a -> a -> a
\/ (a -> h) -> h
forall h. Boolean h => (a -> h) -> h
g a -> h
inj)

instance Heyting (FreeBoolean a) where
  FreeBoolean forall h. Boolean h => (a -> h) -> h
f ==> :: FreeBoolean a -> FreeBoolean a -> FreeBoolean a
==> FreeBoolean forall h. Boolean h => (a -> h) -> h
g = (forall h. Boolean h => (a -> h) -> h) -> FreeBoolean a
forall a. (forall h. Boolean h => (a -> h) -> h) -> FreeBoolean a
FreeBoolean (\a -> h
inj -> (a -> h) -> h
forall h. Boolean h => (a -> h) -> h
f a -> h
inj h -> h -> h
forall a. Heyting a => a -> a -> a
==> (a -> h) -> h
forall h. Boolean h => (a -> h) -> h
g a -> h
inj)

instance Boolean (FreeBoolean a)

type instance AlgebraType0 FreeBoolean a = ()
type instance AlgebraType  FreeBoolean a = Boolean a
instance FreeAlgebra FreeBoolean where
  returnFree :: a -> FreeBoolean a
returnFree a
a = (forall h. Boolean h => (a -> h) -> h) -> FreeBoolean a
forall a. (forall h. Boolean h => (a -> h) -> h) -> FreeBoolean a
FreeBoolean (\a -> h
inj -> a -> h
inj a
a)
  foldMapFree :: (a -> d) -> FreeBoolean a -> d
foldMapFree a -> d
f (FreeBoolean forall h. Boolean h => (a -> h) -> h
inj) = (a -> d) -> d
forall h. Boolean h => (a -> h) -> h
inj a -> d
f

instance Functor FreeBoolean where
  fmap :: (a -> b) -> FreeBoolean a -> FreeBoolean b
fmap = (a -> b) -> FreeBoolean a -> FreeBoolean b
forall (m :: * -> *) a b.
(FreeAlgebra m, AlgebraType0 m a, AlgebraType0 m b) =>
(a -> b) -> m a -> m b
fmapFree

instance Applicative FreeBoolean where
  pure :: a -> FreeBoolean a
pure = a -> FreeBoolean a
forall (m :: * -> *) a. FreeAlgebra m => a -> m a
returnFree
  <*> :: FreeBoolean (a -> b) -> FreeBoolean a -> FreeBoolean b
(<*>) = FreeBoolean (a -> b) -> FreeBoolean a -> FreeBoolean b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad FreeBoolean where
  return :: a -> FreeBoolean a
return = a -> FreeBoolean a
forall (m :: * -> *) a. FreeAlgebra m => a -> m a
returnFree
  >>= :: FreeBoolean a -> (a -> FreeBoolean b) -> FreeBoolean b
(>>=) = FreeBoolean a -> (a -> FreeBoolean b) -> FreeBoolean b
forall (m :: * -> *) a b.
(FreeAlgebra m, AlgebraType0 m a, AlgebraType0 m b) =>
m a -> (a -> m b) -> m b
bindFree