(*
A Quick and Dirty (especially in terms of presentation) Solution 
to Homework 1
*)

(* just wanted to show a non-string solution *)
datatype exp = trues 
           | falses
           | name of int  
           | neg of exp
           | conj of exp * exp 
           | disj of exp * exp 
           | impl of exp * exp
           | eq of   exp * exp;


fun names trues = [] 
  | names falses = []
  | names (name i) = [i]
  | names (neg e) = names e
  | names (conj(e1,e2)) = (names e1) @ (names e2) 
  | names (disj(e1,e2)) = (names e1) @ (names e2) 
  | names (impl(e1,e2)) = (names e1) @ (names e2) 
  | names (eq(e1,e2)) = (names e1) @ (names e2) ;

fun member e [] = false
  | member e (x::l) = if x=e then true else member e l;

fun removedups [] = [] |
    removedups (x::l) = if (member x l) then (removedups l) 
                           else x::(removedups l);

fun lookup [] i = (name i) |
    lookup ((j,v)::l) i = if i=j then v else lookup l i;

fun peval trues _ = trues |
    peval falses _ = falses |
    peval (name i) s = lookup s i |
    peval (neg trues) s = falses |
    peval (neg falses) s = trues |
    peval (neg e) s = (neg (peval e s)) |
    peval (conj(falses, _)) s = falses |
    peval (conj(_ , falses)) s = falses |
    peval (conj(trues, e)) s = peval e s |
    peval (conj(e,trues)) s = peval e s |
    peval (conj(e1,e2)) s = conj((peval e1 s),peval e2 s) |
    peval (disj(falses,falses)) s = falses |
    peval (disj(trues,_)) s = trues |
    peval (disj(_,trues)) s = trues |
    peval (disj(e1,e2)) s = disj(peval e1 s,peval e2 s) |
    peval (impl(trues,falses)) s = falses |
    peval (impl(falses,_)) s = trues |
    peval (impl(_,trues)) s = trues |
    peval (impl(e1,e2)) s = impl(peval e1 s,peval e2 s) |
    peval (eq(falses,falses)) s = trues |
    peval (eq(trues,trues)) s = trues |
    peval (eq(trues,falses)) s = falses |
    peval (eq(falses,trues)) s = falses |
    peval (eq(e1,e2)) s = eq(peval e1 s,peval e2 s);

fun coerce falses = false |
    coerce trues = true |
    coerce e = coerce (peval e []);

fun runcheck e [] s = coerce (peval e s) |
    runcheck e (x::l) s = (runcheck (peval e ((x,trues)::s)) 
                                    l 
                                    ((x,trues)::s)) 
                             andalso
                          (runcheck (peval e ((x,falses)::s))
                                    l
                                    ((x,falses)::s));

fun tautp exp = runcheck exp (removedups (names exp)) [];


(* some meager test cases *)
val yes1 = disj(name 1,(neg (name 1)));

val no1 = disj(name 1,name 2);

val yes2 = disj(impl(name 1,name 1),conj(name 2,impl(name 2,neg (name 1))));