Hello once again. Now I have another problem which I cannot
understand.
Below I paste a short fragment form:
http://www.csse.monash.edu.au/~lloyd/tildeFP/SML/1997
(* "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
WHERE:
Dec = vardec of Ide | (* declarations *)
declist of Dec*Dec |
procdec of Ide*Cmd |
decErr of string;
I don't understand call of function D.
D (vardec x) rho (l, s, a)
or
D (declist (d1,d2)) rho s
D has argument x:string and return tuplet (rho, s) but what about this
rho and (l,s,a) in front.
I will be verry happy if someone translate it for me.
Regards JP
|
