<![CDATA[
fun curry f x y = f(x,y);
val $ = curry;
(* -------------------------------------------- *)
(* denotational semantics definitions: in SML *)
(* = d.ml *)
(* -------------------------------------------- *)
(* -------------------------------------------- *)
(* Skeleton for Lab # 2; *)
(* fill in all missing sections. *)
(* -------------------------------------------- *)
(* -------------------------------------------- *)
(* Template for Continuations *)
(* -------------------------------------------- *)
(* -------------------------------------------- *)
(* ---------- Abstract Syntax ----------------- *)
(* terminal nodes of the syntax *)
type Numeral = int;
type Ident = string;
(* parsed phrases of the abstract syntax *)
datatype
Command =
skip
| assign of Ident * Expression
| letin of Declaration * Command
| cmdcmd of Command * Command
| ifthen of Expression * Command * Command
| whiledo of Expression * Command
and
Expression =
num of Numeral
| False
| True
| id of Ident
| sumof of Expression * Expression
| subof of Expression * Expression
| prodof of Expression * Expression
| less of Expression * Expression
| notexp of Expression
and
Declaration =
constdef of Ident * Expression
| vardef of Ident * TypeDef
and
TypeDef =
Bool | Int
;
(* -------------------------------------------- *)
(* ---------- Semantic Domains ---------------- *)
type Integer = int;
type Boolean = bool;
type Location= int;
datatype Value = integer of int
| truth_value of bool;
type Storable = Value;
datatype Bindable = value of Value | variable of Location;
datatype Denotable = unbound | bound of Bindable ;
exception fail;
(* -------------------------------------------- *)
(* ---------- Semantic Functions -------------- *)
(* These declarations are automatically inferred
* from the defining equations below...
type Environ = Ident -> Denotable;
type Store = Location -> (Storable + undef + unused);
*)
(* -------------------------------------------- *)
(* ---------- Auxiliary Semantic Functions ---- *)
fun sum (x, y) = x + y:int;
fun diff (x, y) = x - y:int;
fun prod (x, y) = x * y:int;
fun lessthan (x, y) = x < (y:int);
(* ---------- Storage ---------- *)
datatype Sval = stored of Storable | undef | unused;
(* --bot--- --top--- ----data--------- *)
datatype Store = store of Location * Location * (Location -> Sval);
val sto_init = fn loc:Location => unused;
val sto_null = store( 1, 0, sto_init);
fun update (store(bot,top,data), loc, v) =
let fun new adr = if adr=loc
then stored v else (data adr);
in store( bot, top, new)
end;
(* fetch from store, and convert into Storable (=Value) *)
fun fetch (store(bot,top,data), loc:Location) =
let fun stored_value(stored stble) = stble
| stored_value(unused) = raise fail
| stored_value(undef) = raise fail
in stored_value( data loc)
end;
(* create a new "undefined" location in a store *)
fun allocate ( store(bot,top,data) ) =
let val newtop = top+1
fun new adr = if adr=newtop
then undef else (data adr);
in (store( bot, newtop, new), newtop)
end;
(* ---------- Envirionment ---------- *)
type Environ = Ident -> Denotable;
val env_null = fn i:Ident => unbound;
fun bind (name, vl) = fn idn => if idn=(name:Ident)
then bound(vl) else unbound;
fun find (env:Environ, idn) =
let fun getbv(bound bdbl) = bdbl
| getbv(unbound) = raise fail
in getbv( env idn)
end;
fun overlay (env', env:Environ) =
fn idn => let val val' = env' idn
in if val'<>unbound then val'
else env idn
end;
(* ---------- Continuations --------- *)
(* Answers *)
type Ans = Storable list;
(* Command continuations *)
type Cc = Store -> Ans;
(* Expression continuations *)
type Ec = Storable -> Cc;
(* Declaration continuations *)
type Dc = Environ -> Cc;
(* Dumps only position 1, change to dump all used store *)
fun final_continuation (s:Store) : Ans =
map ($ fetch s) [1];
(* ---------- Etc.... ---------- *)
(* coerce a Bindable into a Value.. *)
fun coerc (sto, value v) = v
| coerc (sto, variable loc) = fetch(sto,loc);
(* ---------- Initialize system ---------- *)
(* -------------------------------------------- *)
(* ---------- Semantic Equations -------------- *)
(* from integer to Value *)
fun valuation ( n ) = integer(n)
and
execute ( assign(name,exp) ) (u: Environ) (c:Cc) : Cc =
let val variable loc = find(u,name) (*variable 1*)
fun new_ec (ev: Storable) (s:Store) : Ans =
let
val new_store = update( s, loc, ev)
in
c new_store
end
in
Reval exp u new_ec
end
| execute ( letin(def,com) ) (u: Environ) (c:Cc) : Cc =
let fun new_dc (u1: Environ) : Cc =
execute com (overlay (u1, u)) c
in
elaborate def u new_dc
end
| execute ( cmdcmd(com1,com2) ) (u: Environ) (c:Cc) : Cc =
execute com1 u (execute com2 u c)
| execute ( ifthen(e,c1,c2) ) env sto =
...
| execute ( whiledo(e,c) ) en st =
...
and
(* simple, just build a Value *)
evaluate ( num(n) ) (u:Environ) (k:Ec) :Cc = k( integer n )
| evaluate ( True ) env sto =
...
| evaluate ( False ) env sto =
...
| evaluate ( id(n) ) env sto =
...
(* get values, and compute result *)
| evaluate ( sumof (e1,e2) ) (u:Environ) (k:Ec) :Cc =
let fun exp1_ec ((integer i1): Storable) : Cc =
let fun exp2_ec ((integer i2): Storable) : Cc =
k( integer(i1 + i2) )
in
Reval e2 u exp2_ec
end
in
Reval e1 u exp1_ec
end
| evaluate ( subof (e1,e2) ) env sto =
...
| evaluate ( prodof(e1,e2) ) env sto =
...
| evaluate ( less(e1,e2) ) env sto =
...
and
elaborate ( constdef(name,e) ) env sto =
...
|
elaborate ( vardef(name,tdef) ) (u: Environ) (c:Dc) : Cc =
let fun new_cc (s:Store) : Ans =
let
val (new_store, loc) = allocate s
val new_env = bind(name, variable loc)
in
c new_env new_store
end
in
new_cc
end
and
deref (k: Ec) (ev: Storable) (s: Store) : Ans =
k ev s
and
Reval (exp: Expression) (u: Environ) (k: Ec) : Cc =
evaluate exp u (deref k)
;
(* ============================================ *)
(* ---------- Test it..! ---------------------- *)
val pgm1 =
letin (
vardef ("y", Int),
assign("y", num(3))
);
execute pgm1 env_null final_continuation sto_null;
val pgm2 =
letin (
vardef ("y", Int),
cmdcmd (
assign("y", num(3)),
assign("y", sumof(num(3),num(1)))
)
);
execute pgm2 env_null final_continuation sto_null;
]]>