datatype Prop = Atom of string
| /\  of Prop * Prop
| \/  of Prop * Prop
| ==>  of Prop * Prop
| ~   of Prop;

infix 3 \/;
infix 4 /\;
infix 5 ==>;
infix 6 <=>;

val A = Atom "a";
val B = Atom "b";
val C = Atom "c";
val D = Atom "d";

fun pp (Atom x) = x
| pp ( x /\ y) = pp x ^ "/\\" ^ pp y;
(* Finish This *)


fun rmImp (x ==> y) = ~(rmImp x) \/ (rmImp y)
| rmImp (~x) = ~(rmImp x)
| rmImp (x /\ y) = (rmImp x) /\ (rmImp y)
| rmImp (x \/ y) = (rmImp x) \/ (rmImp y)
| rmImp x = x;

fun pushNeg (~(~x)) = pushNeg x
| pushNeg (~(x /\ y)) = pushNeg (~x) \/ pushNeg (~y)
| pushNeg (~(x \/ y)) = pushNeg (~x) /\ pushNeg (~y)
| pushNeg (x /\ y) = (pushNeg x) /\ (pushNeg y)
| pushNeg (x \/ y) = (pushNeg x) \/ (pushNeg y)
| pushNeg x = x;

fun distr (x \/ (y /\ z)) = (distr(x \/ y) /\ distr(x \/ z))
| distr x = x;
fun distl ((y /\ z) \/ x) = (distl(y \/ x) /\ distl(z \/ x))
| distl x = x;

fun dist x = distr(distl x);

fun cnf (x /\ y) = (cnf x) /\ (cnf y)
|   cnf (x \/ y) = dist ((cnf x) \/ (cnf y))
|   cnf x = x;

fun cnf_test x = cnf (pushNeg (rmImp x));