datatype Aexp = num of int |
		loc of string |
		sum of Aexp * Aexp |
   		diff of Aexp * Aexp |
		prod of Aexp * Aexp;

datatype Bexp = trueb |
		falseb |
		eq of Aexp * Aexp |
		leq of Aexp * Aexp |
		neg of Bexp |
		conj of Bexp * Bexp |
		disj of Bexp * Bexp;

datatype Cexp = skip |
		assign of string * Aexp |
		seq of Cexp * Cexp |
		ifthen of Bexp * Cexp * Cexp |
		whiledo of Bexp * Cexp;

val dummy = []:(string*int) list;
val state = ref dummy;

fun aeq (num n) (num m) = m=n |
    aeq (loc s) (loc t) = s=t |
    aeq (sum (a1,a2)) (sum (a3,a4)) = (aeq a1 a3) andalso (aeq a2 a4) |
    aeq (diff (a1,a2)) (diff (a3,a4)) = (aeq a1 a3) andalso (aeq a2 a4) |
    aeq (prod (a1,a2)) (prod (a3,a4)) = (aeq a1 a3) andalso (aeq a2 a4) |
    aeq _ _ = false;

fun beq trueb trueb = true |
    beq falseb falseb = true |
    beq (eq (a1,a2)) (eq (a3,a4)) = (aeq a1 a3) andalso (seq a2 a4) |
    beq (leq (a1,a2)) (leq (a3,a4)) = (aeq a1 a3) andalso (seq a2 a4) |
    beq (neg b1) (neg b2) = (beq b1 b2) |
    beq (conj (b1,b2)) (conj (b3,b4)) = (beq b1 b3) andalso (beq b2 b4) |
    beq (disj (b1,b2)) (disj (b3,b4)) = (beq b1 b3) andalso (beq b2 b4) |
    beq _ _ = false;

fun ceq skip skip = true |
    ceq (assign (s1,a1)) (assign (s2,a2)) = (s1=s2) andalso (aeq a1 a2) |
    ceq (ifthen (b1,c1,c2)) (ifthen (b2,c3,c4)) = (beq b1 b2) andalso
			(ceq c1 c3) andalso (ceq c2 c4) |
    ceq (whiledo (b1,c1)) (whiledo (b2,c2)) = (beq b1 b2) andalso (ceq c1 c2) |
    ceq _ _ = false;

fun lookup [] spot = raise Match |
    lookup ((l,n)::b) spot = if spot=l then n else lookup b spot;

fun aeval (num n) = n |
    aeval (loc s) = lookup (!state) s |
    aeval (sum (a1,a2)) = (aeval a1) + (aeval a2) |
    aeval (diff (a1,a2)) = (aeval a1) - (aeval a2) |
    aeval (prod (a1,a2)) = (aeval a1) * (aeval a2);

fun beval trueb = true |
    beval falseb = false |
    beval (eq (a1,a2)) = (aeval a1) = (aeval a2) |
    beval (leq (a1,a2)) = (aeval a1) <= (aeval a2) |
    beval (neg b1) = not (beval b1) |
    beval (conj (b1,b2)) = (beval b1) andalso (beval b2) |
    beval (disj (b1,b2)) = (beval b1) orelse (beval b2);

fun update [] spot value = [(spot,value)] |
    update ((l,n)::b) spot value = if l=spot then (l,value)::b
					else (l,n)::(update b spot value);

fun ceval skip = state := !state |
    ceval (assign (s1,a1)) = state := update (!state) s1 (aeval a1) |
    ceval (seq (c1,c2)) = (ceval c1; ceval c2);
    ceval (ifthen (b1,c1,c2)) = if (beval b1) then (ceval c1) else (ceval c2) |
    ceval (whiledo (b1,c1)) = if (beval b1)
			then (ceval c1;ceval (whiledo (b1,c1)))
			else state := !state;