(* We represent variables as strings containing a name *)
type variable = string;
 
(* equality on variable names *)
fun eqVar (v0:variable) (v1:variable) = (v0 = v1);
 
(* Formulas are either... *)
datatype formula = 
	 True                          (* boolean True *)
       | False                         (* boolean False *)
       | Var of variable               (* a simple variable *)
       | Not of formula                (* a negation of a single formula *)
       | And of (formula list)         (* a conjunction of several formulas *)
       | Or of (formula list)          (* a disjunction of several formulas *)
       | Implies of formula * formula; (* an implication between one formula
                                        * and another *)
 
fun getValue ((variable, value)::taila) b = 
   if variable = b then value
   else getValue (taila) b
   | getValue (_) b = raise valueNotFound b;
getValue : (variable * 'a) list -> variable -> 'a;
 
fun evaluate a (Var part) = getValue a part
   | evaluate a (Not part) = not (evaluate a part)
   | evaluate a (Or part) = (evaluate a (hd part)) orelse (evaluate a (tl part))
   | evaluate a (And part) = (evaluate a (hd part)) andalso (evaluate a (tl part))
   | evaluate a (Implies part) = not(evaluate a (hd part)) orelse (evaluate a (tl part));