propLogic.idr

%default total

data Prop = Var String 
          | Not Prop 
          | And Prop Prop 
          | Or Prop Prop 
          | Impl Prop Prop
          | Equiv Prop Prop

data Lit = Stmt String | Neg String

implementation Eq Lit where
  (Stmt x) == (Stmt y) = x == y
  (Neg x) == (Neg y) = x == y
  _ == _ = False

-- V OR
Clause : Type
Clause = List Lit

-- ^ AND
CNF : Type
CNF = List Clause

--------------------
---- constrains ----
--------------------

data ConjForm = LitC String
              | NotC ConjForm
              | AndC ConjForm ConjForm
              | OrC ConjForm ConjForm

toConjForm : Prop -> ConjForm
toConjForm (Var x) = LitC x
toConjForm (Not x) = NotC (toConjForm x)
toConjForm (And x y) = AndC (toConjForm x) (toConjForm y)
toConjForm (Or x y) = OrC (toConjForm x) (toConjForm y)
toConjForm (Impl x y) = OrC (NotC (toConjForm x)) (toConjForm y)
toConjForm (Equiv x y) with (((toConjForm x),(toConjForm y)))
  toConjForm (Equiv x y) | (a, b) = AndC (OrC (NotC a) b) (OrC (NotC b) a)

pureClause : String -> Clause
pureClause x = pure (Stmt x)

pureCNF : String -> CNF
pureCNF x = pure (pureClause x)

------------------------
---- Negation rules ----
------------------------

notLit : Lit -> Lit
notLit (Stmt x) = Neg x
notLit (Neg x) = Stmt x

-- apply demorgan law ¬(a v b) -> ((¬a) Λ (¬b))
notClause : Clause -> CNF
notClause = map (pure . notLit)

-- apply demorgan law ¬(a Λ b) -> (¬a v ¬b)
notCNF : CNF -> CNF
notCNF ls = concat $ map (notClause) ls

---------------------------
---- Conjunction rules ----
---------------------------
andCNF : CNF -> CNF -> CNF
andCNF x y = x ++ y

---------------------------
---- Disjunction rules ----
---------------------------
orClause : Clause -> Clause -> Clause
orClause x y = x ++ y

-- apply the distributive law recursively
orCNF : CNF -> CNF -> CNF
orCNF [] y = y
orCNF x [] = x
orCNF x (y :: ys) = andCNF (map (orClause y) x) (orCNF x ys)

toCNF : ConjForm -> CNF
toCNF (LitC x) = pureCNF x
toCNF (NotC x) = notCNF (toCNF x)
toCNF (AndC x y) = andCNF (toCNF x) (toCNF y)
toCNF (OrC x y) = orCNF (toCNF x) (toCNF y)

propToCNF : Prop -> CNF
propToCNF = toCNF . toConjForm

kprintLit : Lit -> String
printLit (Stmt x) = x
printLit (Neg x) = "-" ++ x

prettyPrintClause : Clause -> String
prettyPrintClause x = "(" ++ (unwords $ intersperse " V " (map printLit x)) ++ ")"

prettyPrintCNF : CNF -> String
prettyPrintCNF x = unwords $ intersperse " ^ " (map prettyPrintClause x)

printCNF : CNF -> String
printCNF = prettyPrintCNF . nub