(* "Direct" denotational semantics of simple imperative features *)
(* see "A Practical Introduction to Denotational Semantics"      *)
(*     Cambridge University Press                                *)
(* LA, Dept Comp Sci, Monash, 1988 and CSSE, Monash, .au, 2005   *)
                                                         (* 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;                                          (* Environments *)

(* =======================================LA==csse==monash==.au==1988-2005== *)
                                                      (* 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;     (* the empty store / memory *)
val state0 = (1, store0, []);       (* (counter, store, output) *)

fun rho0   x = raise undecName;     (* the empty environment *)

(* =======================================LA==csse==monash==.au==1988-2005== *)
                                                       (* 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          (* if *)
                                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       (* while *)
                                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       (* write *)
                        in  (l2,s2,(append a2 [v]))
                        end |
    C (block (d,c)) rho s = let val (rho',s') = D d rho s   (* begin ... end *)
                            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 divide v1 v2  = eint(v1 div 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) |
    B ge v1 v2 = eint(if v1 >= v2 then 1 else 0) |
    B lt v1 v2 = eint(if v1 >= v2 then 0 else 1) |
    B gt v1 v2 = eint(if v1 >  v2 then 1 else 0) |
    B le v1 v2 = eint(if v1 >  v2 then 0 else 1) |
    
    B conj v1 v2 = eint(if v1=1 andalso v2=1 then 1 else 0) |
    B disj v1 v2 = eint(if v1=1 orelse  v2=1 then 1 else 0) ;

(* L. Allison, Computer Science, Monash University, Australia 3168 *)
(* http://www.csse.monash.edu.au/~lloyd/tildeFP/    about 1988     *)
(* parse added April 2005                                          *)
(* ========================================================================= *)
                                                                     (* e.g. *)
(*
   C( parse(lexical(explode
    "begin var x; x:=7; while x <> 0 do write x; x := x-1 od end")) )
    rho0 state0;
*)