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

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

import Algebra.Boolean (BooleanAlgebra)
import Algebra.Heyting (HeytingAlgebra (..))

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

instance JoinSemiLattice (FreeBoolean a) where
  FreeBoolean f \/ FreeBoolean g = FreeBoolean (\inj -> f inj \/ g inj)

instance BoundedJoinSemiLattice (FreeBoolean a) where
  bottom = FreeBoolean (\_ -> bottom)

instance MeetSemiLattice (FreeBoolean a) where
  FreeBoolean f /\ FreeBoolean g = FreeBoolean (\inj -> f inj /\ g inj)

instance BoundedMeetSemiLattice (FreeBoolean a) where
  top = FreeBoolean (\_ -> top)

instance Lattice (FreeBoolean a)

instance BoundedLattice (FreeBoolean a)

instance HeytingAlgebra (FreeBoolean a) where
  FreeBoolean f ==> FreeBoolean g = FreeBoolean (\inj -> f inj ==> g inj)

instance BooleanAlgebra (FreeBoolean a)

type instance AlgebraType0 FreeBoolean a = ()
type instance AlgebraType  FreeBoolean a = BooleanAlgebra a
instance FreeAlgebra FreeBoolean where
  returnFree a = FreeBoolean (\inj -> inj a)
  foldMapFree f (FreeBoolean inj) = inj f

  codom  = proof
  forget = proof

instance Functor FreeBoolean where
  fmap = fmapFree

instance Applicative FreeBoolean where
  pure = returnFree
  (<*>) = ap

instance Monad FreeBoolean where
  return = returnFree
  (>>=) = bindFree