(* 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));