propToCNF.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

-- V OR
data Clause = Bot | Disj Lit Clause

-- ^ AND
data CNF = Top | Conj Clause CNF

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

pureClause : String -> Clause
pureClause x = Disj (Stmt x) Bot

pureCNF : String -> CNF
pureCNF x = Conj (pureClause x) Top


toConjForm' : (p: 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)

toCNF : ConjForm -> CNF
toCNF (LitC x) = pureCNF x
toCNF (NotC (LitC x)) = Conj (Disj (Neg x) Bot) Top
toCNF (NotC (NotC x)) = toCNF x
toCNF (NotC (AndC x y)) = ?toCNF_rhs_6 -- stuck here
toCNF (NotC (OrC x y)) = ?toCNF_rhs_7
toCNF (AndC x y) = ?toCNF_rhs_3
toCNF (OrC x y) = ?toCNF_rhs_4