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");