1. datatype logicexpr = Var of string
  2.                      | Neg of logicexpr
  3.                      | And of logicexpr * logicexpr
  4.                      | Or of logicexpr * logicexpr;
  5. datatype logiccontext = CNeg | CAnd | COr;
  6. datatype logiclex = LVar of string | LLeft | LRight | LNeg | LAnd | LOr;
  7.  
  8. fun distributeLeft(X, And(e,f)) = And(distributeLeft(X,e),distributeLeft(X,f))
  9. | distributeLeft(X, Y) = Or(X, Y);
  10.  
  11. fun distributeOr(And(e,f), Y) = And(distributeOr(e,Y),distributeOr(f,Y))
  12. | distributeOr(X, Y) = distributeLeft(X, Y);
  13.  
  14. fun makeCNF(Var x) = Var x
  15. | makeCNF(Neg(Var x)) = Neg(Var x)
  16. | makeCNF(Neg(Neg e)) = makeCNF e
  17. | makeCNF(Neg(And(e,f))) = makeCNF(Or(Neg e, Neg f))
  18. | makeCNF(Neg(Or(e,f))) = makeCNF(And(Neg e, Neg f))
  19. | makeCNF(And(e,f)) = And(makeCNF e, makeCNF f)
  20. | makeCNF(Or(e,f)) = distributeOr(makeCNF e, makeCNF f);
  21.  
  22. fun displayLogic(E) = let
  23.    fun dispLogic(Var x,_) = x
  24.    | dispLogic(Neg(X),_) = "!" ^ dispLogic(X,CNeg)
  25.    | dispLogic(And(X,Y),CNeg) = "(" ^ dispLogic(X,CAnd) ^ "&" ^ dispLogic(Y,CAnd) ^ ")"
  26.    | dispLogic(And(X,Y),_) = dispLogic(X,CAnd) ^ "&" ^ dispLogic(Y,CAnd)
  27.    | dispLogic(Or(X,Y),COr) = dispLogic(X,COr) ^ "|" ^ dispLogic(Y,COr)
  28.    | dispLogic(Or(X,Y),_) = "(" ^ dispLogic(X,COr) ^ "|" ^ dispLogic(Y,COr) ^ ")";
  29. in
  30.    dispLogic(E,COr)
  31. end;
  32.  
  33. fun parseLogic(s) = let
  34.    fun collect a [] = (LVar (implode a),[])
  35.    | collect a (c::r) = if Char.isAlpha c then collect (a@[c]) r else (LVar (implode a),c::r);
  36.    fun lex [] = []
  37.    | lex (#"("::r) = LLeft :: lex r
  38.    | lex (#")"::r) = LRight :: lex r
  39.    | lex (#"!"::r) = LNeg :: lex r
  40.    | lex (#"&"::r) = LAnd :: lex r
  41.    | lex (#"|"::r) = LOr :: lex r
  42.    | lex (c::r) = if Char.isAlpha c then let val (v,s) = collect [] (c::r); in v :: lex s end  
  43.       else lex r;
  44.    fun parseExpr e = let val (l,u) = parseAnd e; in
  45.       if u = [] then (l,[])
  46.       else if hd u = LOr then let val (r,v) = parseExpr(tl u); in (Or(l,r),v) end
  47.       else (l,u)
  48.    end
  49.    and parseAnd e = let val (l,u) = parseNot e; in
  50.       if u = [] then (l,[])
  51.       else if hd u = LAnd then let val (r,v) = parseAnd (tl u); in (And(l,r),v) end
  52.       else (l,u)
  53.    end
  54.    and parseNot (LNeg::t) = let val (r,u) = parseNot t; in (Neg(r),u) end
  55.    | parseNot s = parseTerm s
  56.    and parseTerm (LVar(x)::t) = (Var(x),t)
  57.    | parseTerm (LLeft::t) = let val (e,LRight::u) = parseExpr t; in (e,u) end;
  58.    val (parse,leftover) = parseExpr(lex(explode s));
  59. in parse end;
  60.  
  61. fun printCNF expr = print(displayLogic(makeCNF(parseLogic(expr))) ^ "\n");