type Ide = string;

datatype Uopr = uminus | knot;
datatype Bopr = plus | minus | times | eq | ne ;

datatype Exp = binexp   of Exp * Bopr * Exp |
               unexp    of Uopr * Exp |
               varid    of Ide |
               numeral  of int

and      Cmd = assign   of Ide * Exp |
               ifcmd    of Exp * Cmd * Cmd |
               whilecmd of Exp * Cmd |
               cmdlist  of Cmd * Cmd |
               proccall of Ide |
               write    of Exp |
               block    of Dec * Cmd

and      Dec = vardec   of Ide |
               declist  of Dec*Dec |
               procdec  of Ide*Cmd;

(* Semantic Domains ---------------------------------------------------------*)

type Locn = int;
type Sv = int;                                        (* Storable Values *)
type Answer = int list;
type Store = Locn->Sv;
type State = int (* free store ptr *)   * Store * Answer;

datatype Dv = locn of Locn | closure of State->State  (* Denotable Values *)
and      Ev = eloc of Locn | eint of int;             (* Expressible Values *)

type Env = Ide->Dv;

(* Auxiliary Functions ------------------------------------------------------*)

fun append nil b = b |
    append (h::t) b = h::(append t b);

fun update f x v y = if x=y then v else f y;

exception undefLocn
and       undecName;

fun store0 l = raise undefLocn;
val state0 = (1, store0, []);

fun rho0   x = raise undecName;

(* Semantic Equations -------------------------------------------------------*)

(* Declarations *)

fun D (vardec x) rho (l, s, a) = ((update rho x (locn l)), (l+1,s,a))  |
    D (procdec (p,c)) rho s = let fun body s' = C c rho' s'
                                  and rho' x = update rho p (closure body) x
                              in  (rho',s)
                              end |
    D (declist (d1,d2)) rho s = let val (rho2,s2)=D d1 rho s
                                in D d2 rho2 s2
                                end

(* Commands *)

and C (assign (x,e)) rho s =
       let val (eint v, s2)=R e rho s;
           val (eloc lc, (l3,s3,a3))=L (varid x) rho s2
       in (l3, update s3 lc v, a3)
       end  |
    C (cmdlist (c1,c2)) rho s = ((C c2 rho) o (C c1 rho) )s |
    C (proccall p) rho s =  let val closure x = rho p
                            in  x s
                            end |
    C (ifcmd (e,c1,c2)) rho s = let val (eint v,s2)=R e rho s
                                in  C (if v=1 then c1 else c2) rho s2
                                end  |
    C (whilecmd (e,c)) rho s  = let val (eint v,s2)=R e rho s
                                in  if v=1 then
                                         ((C (whilecmd (e,c)) rho)o(C c rho))s2
                                    else s
                                end |
    C (write e) rho s = let val (eint v,(l2,s2,a2))=R e rho s
                        in  (l2,s2,(append a2 [v]))
                        end |
    C (block (d,c)) rho s = let val (rho',s') = D d rho s
                            in  C c rho' s'
                            end

(* Expressions *)

and E (binexp (e1,opr,e2)) rho s = let val (eint v1,s2)=R e1 rho s
                                   in let val (eint v2,s3)=R e2 rho s2
                                      in ((B opr v1 v2),s3)
                                      end
                                   end |
    E (unexp (opr,e)) rho s = let val (eint v,s2)=R e rho s
                              in ((U opr v),s2)
                              end |
    E (varid x) rho s = let val locn(l)=rho x
                        in  (eloc l, s)
                        end |
    E (numeral n) rho s = (eint n,s)

(* Left Values *)

and L e rho s = let val (eloc(l),s2) = E e rho s
                in (eloc(l),s2)
                end

(* Right Values *)

and R e rho s  =
       let val (v, (l2,st2,a2)) = E e rho s
       in case v of
          (eloc l)=> (eint (st2 l), (l2,st2,a2)) |
          _       => (v, (l2,st2,a2))
          end

(* Operators *)

and U uminus v = eint( ~ v ) |
    U knot   v = eint(if v=0 then 1 else 0)

and B plus v1 v2   = eint(v1+v2) |
    B minus v1 v2  = eint(v1-v2) |
    B times v1 v2  = eint(v1-v2) |
    B eq  v1 v2    = eint(if v1=v2 then 1 else 0) |
    B ne  v1 v2    = eint(if v1=v2 then 0 else 1) ;

(*---------------------------------------------------------------------------*)

(* Example *)
let val dec = vardec "n"
    and cmd = assign ("n", (numeral 7))
    and outp  = write (varid "n")
in  C (block (dec,(cmdlist(cmd,outp)))) rho0 state0
end;

(* L. Allison, Australia, http://www.allisons.org/ll/FP/ *)
(* updated for ML97, SML/NJ, March 2005                  *)