datatype logicexpr = Var of string
| Neg of logicexpr
| And of logicexpr * logicexpr
| Or of logicexpr * logicexpr;
datatype logiccontext = CNeg | CAnd | COr;
datatype logiclex = LVar of string | LLeft | LRight | LNeg | LAnd | LOr;
fun distributeLeft(X, And(e,f)) = And(distributeLeft(X,e),distributeLeft(X,f))
| distributeLeft(X, Y) = Or(X, Y);
fun distributeOr(And(e,f), Y) = And(distributeOr(e,Y),distributeOr(f,Y))
| distributeOr(X, Y) = distributeLeft(X, Y);
fun makeCNF(Var x) = Var x
| makeCNF(Neg(Var x)) = Neg(Var x)
| makeCNF(Neg(Neg e)) = makeCNF e
| makeCNF(Neg(And(e,f))) = makeCNF(Or(Neg e, Neg f))
| makeCNF(Neg(Or(e,f))) = makeCNF(And(Neg e, Neg f))
| makeCNF(And(e,f)) = And(makeCNF e, makeCNF f)
| makeCNF(Or(e,f)) = distributeOr(makeCNF e, makeCNF f);
fun displayLogic(E) = let
fun dispLogic(Var x,_) = x
| dispLogic(Neg(X),_) = "!" ^ dispLogic(X,CNeg)
| dispLogic(And(X,Y),CNeg) = "(" ^ dispLogic(X,CAnd) ^ "&" ^ dispLogic(Y,CAnd) ^ ")"
| dispLogic(And(X,Y),_) = dispLogic(X,CAnd) ^ "&" ^ dispLogic(Y,CAnd)
| dispLogic(Or(X,Y),COr) = dispLogic(X,COr) ^ "|" ^ dispLogic(Y,COr)
| dispLogic(Or(X,Y),_) = "(" ^ dispLogic(X,COr) ^ "|" ^ dispLogic(Y,COr) ^ ")";
in
dispLogic(E,COr)
end;
fun parseLogic(s) = let
fun collect a [] = (LVar (implode a),[])
| collect a (c::r) = if Char.isAlpha c then collect (a@[c]) r else (LVar (implode a),c::r);
fun lex [] = []
| lex (#"("::r) = LLeft :: lex r
| lex (#")"::r) = LRight :: lex r
| lex (#"!"::r) = LNeg :: lex r
| lex (#"&"::r) = LAnd :: lex r
| lex (#"|"::r) = LOr :: lex r
| lex (c::r) = if Char.isAlpha c then let val (v,s) = collect [] (c::r); in v :: lex s end
else lex r;
fun parseExpr e = let val (l,u) = parseAnd e; in
if u = [] then (l,[])
else if hd u = LOr then let val (r,v) = parseExpr(tl u); in (Or(l,r),v) end
else (l,u)
end
and parseAnd e = let val (l,u) = parseNot e; in
if u = [] then (l,[])
else if hd u = LAnd then let val (r,v) = parseAnd (tl u); in (And(l,r),v) end
else (l,u)
end
and parseNot (LNeg::t) = let val (r,u) = parseNot t; in (Neg(r),u) end
| parseNot s = parseTerm s
and parseTerm (LVar(x)::t) = (Var(x),t)
| parseTerm (LLeft::t) = let val (e,LRight::u) = parseExpr t; in (e,u) end;
val (parse,leftover) = parseExpr(lex(explode s));
in parse end;
fun printCNF expr = print(displayLogic(makeCNF(parseLogic(expr))) ^ "\n");