{-# OPTIONS -Wall #-}
{-# OPTIONS -fwarn-simple-patterns #-}
{-# OPTIONS -fwarn-tabs #-}
{-# OPTIONS -fwarn-incomplete-record-updates #-}
{-# OPTIONS -fwarn-monomorphism-restriction #-}

{-# LANGUAGE FlexibleContexts #-}       -- no type variable in context
{-# LANGUAGE FlexibleInstances #-}      -- type vars appears more than once in head
{-# LANGUAGE MultiParamTypeClasses #-}  
{-# LANGUAGE GADTs #-}                  -- for Mu
{-# LANGUAGE TypeOperators #-}          -- for :+: and :<:
{-# LANGUAGE OverlappingInstances #-}   -- for automatic injections


module Prop where
import Prelude

-- coproduct for (* -> *)
data (f :+: g) a where
      Inl :: (f a) -> (f :+: g) a
      Inr :: (g a) -> (f :+: g) a
infixr 6 :+:

-- the coproduct of two functors is a functor
instance (Functor f, Functor g) => Functor (f :+: g) where
    fmap f (Inl x) = Inl (fmap f x)
    fmap f (Inr y) = Inr (fmap f y)

-- fixpoint
data Mu f where In {
    out :: f (Mu f)
    }  :: Mu f

-- catamorphism
type Algebra   f a = f a -> a 
cata :: Functor f => (Algebra f a) -> (Mu f -> a )
cata g = g . fmap (cata g) . out  

-- Evaluation of an algebra
class Functor f => Eval f a where
    evalAlgebra :: Algebra f a
-- Evaluation function
eval :: (Eval f a) =>  Mu f -> a
eval = cata evalAlgebra

-- links between algebra of coproduct
instance (Eval f a, Eval g a) => Eval (f :+: g) a where
    evalAlgebra (Inl x) = evalAlgebra x
    evalAlgebra (Inr y) = evalAlgebra y

-- automatic injection
class (Functor sub, Functor sup) => sub :<: sup where
    inj :: sub a -> sup a

instance (Functor f) => (:<:) f f where
    inj          = id
instance (Functor f, Functor g) => (:<:) f (f :+: g) where
    inj          = Inl
instance (Functor h, (:<:) f g) => (:<:) f (h :+: g) where
    inj          = Inr . inj

inject ::  ((:<:) sub  f) => sub (Mu f) -> Mu f
inject = In . inj

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

data LProp r = LProp String
instance Functor LProp where
    fmap _ (LProp x) =  LProp x
instance Eval LProp ((String -> Bool) -> Bool) where
    evalAlgebra (LProp x) f = f x
lprop :: (LProp :<: f) => String -> Mu f 
lprop = \s -> inject (LProp s)

data LAnd r = LAnd r r
instance Functor LAnd where
    fmap f (LAnd x y) = LAnd (f x) (f y)
instance Eval LAnd ((String -> Bool) -> Bool) where
    evalAlgebra (LAnd x y) f = (x f) && (y f)
land :: (LAnd :<: f) => Mu f -> Mu f -> Mu f 
land = \x y -> inject (LAnd x y)

data LNot r = LNot r
instance Functor LNot where
    fmap f (LNot x) = LNot (f x)
instance Eval LNot ((String -> Bool) -> Bool) where
    evalAlgebra (LNot x) f = not (x f)
lnot :: (LNot :<: f) => Mu f -> Mu f
lnot = \x -> inject (LNot x)

type ConjLogicF = LProp :+: LNot :+: LAnd
type ConjLogic = Mu ConjLogicF

aConjLogic :: ConjLogic
aConjLogic = (lprop "X") `land` ((lprop "Y") `land` (lnot (lprop "Z")))

aInterpret :: String -> Bool
aInterpret "X"  = True
aInterpret "Y"  = True
aInterpret "Z"  = True
aInterpret  _   = False

anEval :: Bool
anEval = eval aConjLogic aInterpret

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

data LProp' p r = LProp' p
instance Functor (LProp' p) where
    fmap _ (LProp' x) =  LProp' x
instance Eval (LProp' p) ((p -> Bool) -> Bool) where
    evalAlgebra (LProp' x) f = f x
lprop' :: ((LProp' p) :<: (f p)) => p -> Mu (f p)
lprop' = \x -> inject (LProp' x)

data LAnd' p r = LAnd' r r
instance Functor (LAnd' p) where
    fmap f (LAnd' x y) = LAnd' (f x) (f y)
instance Eval (LAnd' p) ((p -> Bool) -> Bool) where
    evalAlgebra (LAnd' x y) f = (x f) && (y f)

-- the error lies there !?
--land' :: ((LAnd' p) :<: (f p)) =>  Mu (f p) ->  Mu (f p) ->  Mu (f p)
--land' = \x y -> inject (LAnd' x y)

type ConjLogicF' p = (LProp' p) :+: (LAnd' p)
type ConjLogic' p = Mu (ConjLogicF' p)