compdata-0.4: examples/Examples/MultiParam/FOL.hs
{-# LANGUAGE TemplateHaskell, TypeOperators, FlexibleInstances,
FlexibleContexts, UndecidableInstances, GADTs, KindSignatures,
OverlappingInstances, TypeSynonymInstances #-}
--------------------------------------------------------------------------------
-- |
-- Module : Examples.MultiParam.FOL
-- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved
-- License : BSD3
-- Maintainer : Tom Hvitved <hvitved@diku.dk>
-- Stability : experimental
-- Portability : non-portable (GHC Extensions)
--
-- First-Order Logic à la Carte
--
-- This example illustrates how to implement First-Order Logic à la Carte
-- (Knowles, The Monad.Reader Issue 11, '08) using Generalised Parametric
-- Compositional Data Types.
--
-- Rather than having a fixed domain @Term@ for binders, a la Knowles, our
-- encoding uses a mutually recursive data structure for terms and formulae.
-- This enables variables to be introduced only when they are actually needed
-- in the term language, i.e. in stage 5.
--
--------------------------------------------------------------------------------
module Examples.MultiParam.FOL where
import Data.Comp.MultiParam hiding (Const)
import Data.Comp.MultiParam.Show ()
import Data.Comp.MultiParam.Derive
import Data.Comp.MultiParam.FreshM (genVar)
import Data.List (intersperse)
import Data.Maybe
import Control.Monad.State
import Control.Monad.Reader
-- Phantom types indicating whether a (recursive) term is a formula or a term
data TFormula
data TTerm
-- Terms
data Const :: (* -> *) -> (* -> *) -> * -> * where
Const :: String -> [e TTerm] -> Const a e TTerm
data Var :: (* -> *) -> (* -> *) -> * -> * where
Var :: String -> Var a e TTerm
-- Formulae
data TT :: (* -> *) -> (* -> *) -> * -> * where
TT :: TT a e TFormula
data FF :: (* -> *) -> (* -> *) -> * -> * where
FF :: FF a e TFormula
data Atom :: (* -> *) -> (* -> *) -> * -> * where
Atom :: String -> [e TTerm] -> Atom a e TFormula
data NAtom :: (* -> *) -> (* -> *) -> * -> * where
NAtom :: String -> [e TTerm] -> NAtom a e TFormula
data Not :: (* -> *) -> (* -> *) -> * -> * where
Not :: e TFormula -> Not a e TFormula
data Or :: (* -> *) -> (* -> *) -> * -> * where
Or :: e TFormula -> e TFormula -> Or a e TFormula
data And :: (* -> *) -> (* -> *) -> * -> * where
And :: e TFormula -> e TFormula -> And a e TFormula
data Impl :: (* -> *) -> (* -> *) -> * -> * where
Impl :: e TFormula -> e TFormula -> Impl a e TFormula
data Exists :: (* -> *) -> (* -> *) -> * -> * where
Exists :: (a TTerm -> e TFormula) -> Exists a e TFormula
data Forall :: (* -> *) -> (* -> *) -> * -> * where
Forall :: (a TTerm -> e TFormula) -> Forall a e TFormula
-- Derive boilerplate code using Template Haskell
$(derive [makeHDifunctor, smartConstructors]
[''Const, ''Var, ''TT, ''FF, ''Atom, ''NAtom,
''Not, ''Or, ''And, ''Impl, ''Exists, ''Forall])
--------------------------------------------------------------------------------
-- Pretty printing of terms and formulae
--------------------------------------------------------------------------------
instance ShowHD Const where
showHD (Const f t) = do
ts <- mapM pshow t
return $ f ++ "(" ++ concat (intersperse ", " ts) ++ ")"
instance ShowHD Var where
showHD (Var x) = return x
instance ShowHD TT where
showHD TT = return "true"
instance ShowHD FF where
showHD FF = return "false"
instance ShowHD Atom where
showHD (Atom p t) = do
ts <- mapM pshow t
return $ p ++ "(" ++ concat (intersperse ", " ts) ++ ")"
instance ShowHD NAtom where
showHD (NAtom p t) = do
ts <- mapM pshow t
return $ "not " ++ p ++ "(" ++ concat (intersperse ", " ts) ++ ")"
instance ShowHD Not where
showHD (Not f) = liftM (\x -> "not (" ++ x ++ ")") (pshow f)
instance ShowHD Or where
showHD (Or f1 f2) =
liftM2 (\x y -> "(" ++ x ++ ") or (" ++ y ++ ")") (pshow f1) (pshow f2)
instance ShowHD And where
showHD (And f1 f2) =
liftM2 (\x y -> "(" ++ x ++ ") and (" ++ y ++ ")") (pshow f1) (pshow f2)
instance ShowHD Impl where
showHD (Impl f1 f2) =
liftM2 (\x y -> "(" ++ x ++ ") -> (" ++ y ++ ")") (pshow f1) (pshow f2)
instance ShowHD Exists where
showHD (Exists f) = do x <- genVar
x' <- pshow x
b <- pshow $ f x
return $ "exists " ++ x' ++ ". " ++ b
instance ShowHD Forall where
showHD (Forall f) = do x <- genVar
x' <- pshow x
b <- pshow $ f x
return $ "forall " ++ x' ++ ". " ++ b
--------------------------------------------------------------------------------
-- Stage 0
--------------------------------------------------------------------------------
type Input = Const :+: TT :+: FF :+: Atom :+: Not :+: Or :+: And :+:
Impl :+: Exists :+: Forall
foodFact :: Term Input TFormula
foodFact =
(iExists $ \p -> iAtom "Person" [Place p] `iAnd`
(iForall $ \f -> iAtom "Food" [Place f] `iImpl`
iAtom "Eats" [Place p,Place f])) `iImpl`
iNot (iExists $ \f -> iAtom "Food" [Place f] `iAnd`
iNot (iExists $ \p -> iAtom "Person" [Place p] `iAnd`
iAtom "Eats" [Place p,Place f]))
--------------------------------------------------------------------------------
-- Stage 1
--------------------------------------------------------------------------------
type Stage1 = Const :+: TT :+: FF :+: Atom :+: Not :+: Or :+: And :+:
Exists :+: Forall
class ElimImp f where
elimImpHom :: Hom f Stage1
$(derive [liftSum] [''ElimImp])
instance (f :<: Stage1) => ElimImp f where
elimImpHom = simpCxt . inj
instance ElimImp Impl where
elimImpHom (Impl f1 f2) = iNot (Hole f1) `iOr` (Hole f2)
elimImp :: Term Input :-> Term Stage1
elimImp = appHom elimImpHom
foodFact1 :: Term Stage1 TFormula
foodFact1 = elimImp foodFact
--------------------------------------------------------------------------------
-- Stage 2
--------------------------------------------------------------------------------
type Stage2 = Const :+: TT :+: FF :+: Atom :+: NAtom :+: Or :+: And :+:
Exists :+: Forall
class Dualize f where
dualizeHom :: Hom f Stage2
$(derive [liftSum] [''Dualize])
instance Dualize Const where
dualizeHom (Const f t) = iConst f $ map Hole t
instance Dualize TT where
dualizeHom TT = iFF
instance Dualize FF where
dualizeHom FF = iTT
instance Dualize Atom where
dualizeHom (Atom p t) = iNAtom p $ map Hole t
instance Dualize NAtom where
dualizeHom (NAtom p t) = iAtom p $ map Hole t
instance Dualize Or where
dualizeHom (Or f1 f2) = Hole f1 `iAnd` Hole f2
instance Dualize And where
dualizeHom (And f1 f2) = Hole f1 `iOr` Hole f2
instance Dualize Exists where
dualizeHom (Exists f) = iForall (Hole . f)
instance Dualize Forall where
dualizeHom (Forall f) = iExists (Hole . f)
dualize :: Term Stage2 :-> Term Stage2
dualize = appHom dualizeHom
class PushNot f where
pushNotAlg :: Alg f (Term Stage2)
$(derive [liftSum] [''PushNot])
instance PushNot Const where
pushNotAlg (Const f t) = iConst f t
instance PushNot TT where
pushNotAlg TT = iTT
instance PushNot FF where
pushNotAlg FF = iFF
instance PushNot Atom where
pushNotAlg (Atom p t) = iAtom p t
instance PushNot Not where
pushNotAlg (Not f) = dualize f
instance PushNot Or where
pushNotAlg (Or f1 f2) = f1 `iOr` f2
instance PushNot And where
pushNotAlg (And f1 f2) = f1 `iAnd` f2
instance PushNot Exists where
pushNotAlg (Exists f) = iExists (f . Place)
instance PushNot Forall where
pushNotAlg (Forall f) = iForall (f . Place)
pushNotInwards :: Term Stage1 :-> Term Stage2
pushNotInwards = cata pushNotAlg
foodFact2 :: Term Stage2 TFormula
foodFact2 = pushNotInwards foodFact1
--------------------------------------------------------------------------------
-- Stage 4
--------------------------------------------------------------------------------
type Stage4 = Const :+: TT :+: FF :+: Atom :+: NAtom :+: Or :+: And :+: Forall
type Unique = Int
data UniqueSupply = UniqueSupply Unique UniqueSupply UniqueSupply
initialUniqueSupply :: UniqueSupply
initialUniqueSupply = genSupply 1
where genSupply n = UniqueSupply n (genSupply (2 * n))
(genSupply (2 * n + 1))
splitUniqueSupply :: UniqueSupply -> (UniqueSupply, UniqueSupply)
splitUniqueSupply (UniqueSupply _ l r) = (l,r)
getUnique :: UniqueSupply -> (Unique, UniqueSupply)
getUnique (UniqueSupply n l _) = (n,l)
type Supply = State UniqueSupply
type S = ReaderT [Term Stage4 TTerm] Supply
evalS :: S a -> [Term Stage4 TTerm] -> UniqueSupply -> a
evalS m env s = evalState (runReaderT m env) s
fresh :: S Int
fresh = do supply <- get
let (uniq,rest) = getUnique supply
put rest
return uniq
freshes :: S UniqueSupply
freshes = do supply <- get
let (l,r) = splitUniqueSupply supply
put r
return l
class Skolem f where
skolemAlg :: AlgM' S f (Term Stage4)
$(derive [liftSum] [''Skolem])
instance Skolem Const where
skolemAlg (Const f t) = liftM (iConst f) $ mapM getCompose t
instance Skolem TT where
skolemAlg TT = return iTT
instance Skolem FF where
skolemAlg FF = return iFF
instance Skolem Atom where
skolemAlg (Atom p t) = liftM (iAtom p) $ mapM getCompose t
instance Skolem NAtom where
skolemAlg (NAtom p t) = liftM (iNAtom p) $ mapM getCompose t
instance Skolem Or where
skolemAlg (Or f1 f2) = liftM2 iOr (getCompose f1) (getCompose f2)
instance Skolem And where
skolemAlg (And f1 f2) = liftM2 iAnd (getCompose f1) (getCompose f2)
instance Skolem Forall where
skolemAlg (Forall f) = do
supply <- freshes
xs <- ask
return $ iForall $ \x -> evalS (getCompose $ f (Place x))
(Place x : xs)
supply
instance Skolem Exists where
skolemAlg (Exists f) = do uniq <- fresh
xs <- ask
getCompose $ f (iConst ("Skol" ++ show uniq) xs)
skolemize :: Term Stage2 :-> Term Stage4
skolemize f = evalState (runReaderT (cataM' skolemAlg f) []) initialUniqueSupply
foodFact4 :: Term Stage4 TFormula
foodFact4 = skolemize foodFact2
--------------------------------------------------------------------------------
-- Stage 5
--------------------------------------------------------------------------------
type Stage5 = Const :+: Var :+: TT :+: FF :+: Atom :+: NAtom :+: Or :+: And
class Prenex f where
prenexAlg :: AlgM' S f (Term Stage5)
$(derive [liftSum] [''Prenex])
instance Prenex Const where
prenexAlg (Const f t) = liftM (iConst f) $ mapM getCompose t
instance Prenex TT where
prenexAlg TT = return iTT
instance Prenex FF where
prenexAlg FF = return iFF
instance Prenex Atom where
prenexAlg (Atom p t) = liftM (iAtom p) $ mapM getCompose t
instance Prenex NAtom where
prenexAlg (NAtom p t) = liftM (iNAtom p) $ mapM getCompose t
instance Prenex Or where
prenexAlg (Or f1 f2) = liftM2 iOr (getCompose f1) (getCompose f2)
instance Prenex And where
prenexAlg (And f1 f2) = liftM2 iAnd (getCompose f1) (getCompose f2)
instance Prenex Forall where
prenexAlg (Forall f) = do uniq <- fresh
getCompose $ f (iVar ("x" ++ show uniq))
prenex :: Term Stage4 :-> Term Stage5
prenex f = evalState (runReaderT (cataM' prenexAlg f) []) initialUniqueSupply
foodFact5 :: Term Stage5 TFormula
foodFact5 = prenex foodFact4
--------------------------------------------------------------------------------
-- Stage 6
--------------------------------------------------------------------------------
type Literal = Term (Const :+: Var :+: Atom :+: NAtom)
newtype Clause i = Clause {unClause :: [Literal i]} -- implicit disjunction
newtype CNF i = CNF {unCNF :: [Clause i]} -- implicit conjunction
instance Show (Clause i) where
show c = concat $ intersperse " or " $ map show $ unClause c
instance Show (CNF i) where
show c = concat $ intersperse "\n" $ map show $ unCNF c
class ToCNF f where
cnfAlg :: Alg f CNF
$(derive [liftSum] [''ToCNF])
instance ToCNF Const where
cnfAlg (Const f t) = CNF [Clause [iConst f (map (head . unClause . head . unCNF) t)]]
instance ToCNF Var where
cnfAlg (Var x) = CNF [Clause [iVar x]]
instance ToCNF TT where
cnfAlg TT = CNF []
instance ToCNF FF where
cnfAlg FF = CNF [Clause []]
instance ToCNF Atom where
cnfAlg (Atom p t) = CNF [Clause [iAtom p (map (head . unClause . head . unCNF) t)]]
instance ToCNF NAtom where
cnfAlg (NAtom p t) = CNF [Clause [iNAtom p (map (head . unClause . head . unCNF) t)]]
instance ToCNF And where
cnfAlg (And f1 f2) = CNF $ unCNF f1 ++ unCNF f2
instance ToCNF Or where
cnfAlg (Or f1 f2) = CNF [Clause (x ++ y) | Clause x <- unCNF f1, Clause y <- unCNF f2]
cnf :: Term Stage5 :-> CNF
cnf = cata cnfAlg
foodFact6 :: CNF TFormula
foodFact6 = cnf foodFact5
--------------------------------------------------------------------------------
-- Stage 7
--------------------------------------------------------------------------------
type T = Const :+: Var :+: Atom :+: NAtom
newtype IClause i = IClause ([Term T i], -- implicit conjunction
[Term T i]) -- implicit disjunction
newtype INF i = INF [IClause i] -- implicit conjunction
instance Show (IClause i) where
show (IClause (cs,ds)) =
let cs' = concat $ intersperse " and " $ map show cs
ds' = concat $ intersperse " or " $ map show ds
in "(" ++ cs' ++ ") -> (" ++ ds' ++ ")"
instance Show (INF i) where
show (INF fs) = concat $ intersperse "\n" $ map show fs
inf :: CNF TFormula -> INF TFormula
inf (CNF f) = INF $ map (toImpl . unClause) f
where toImpl :: [Literal TFormula] -> IClause TFormula
toImpl disj = IClause ([iAtom p t | NAtom p t <- mapMaybe proj1 disj],
[inject t | t <- mapMaybe proj2 disj])
proj1 :: NatM Maybe (Term T) (NAtom Any (Term T))
proj1 = project
proj2 :: NatM Maybe (Term T) (Atom Any (Term T))
proj2 = project
foodFact7 :: INF TFormula
foodFact7 = inf foodFact6