sem_op_implip

This page is a draft

In this part we will develop the operational semantics of a quite simple *imperative* language where the functional
language (without functions) we have seen so far are the expressions to be **assigned** to variables. As we have variables in the language, we have to provide not only an environment but a store as well, and we have now to keep in mind that now we have to
decide which are the *expressible* values, the ones that can be *denoted* and finally those that can be *memorized*.

We start with the syntax of the language (without declarations):

(* Expressions *) type ide = string type exp = | Eint of int | Ebool of bool | Den of ide | Prod of exp * exp | Sum of exp * exp | Diff of exp * exp | Eq of exp * exp | Minus of exp | Iszero of exp | Or of exp * exp | And of exp * exp | Not of exp | Ifthenelse of exp * exp * exp (* new for the imperative fragment *) | Val of ide (* Commands *) type com = | Assign of ide * exp | Cifthenelse of exp * com * com | While of exp * com | Cseq of com * com

We have added to the expressions now the possibility of looking at the value that is associated to a variable.
The new syntactic category (`com`

) is self explaining.

We have then values that can be denoted (in the environment), memorized (in the store) and, like before, given as result. Clearly we must be able to convert a value of a kind to a value of another kind (to convince yourself, simply consider the assignment of the value of an expression to a variable: the evaluation of the expression will give something like the previous eval, and we have to convert it in a value that can be placed in the store…)

(* SEMANTIC DOMAINS *) exception Nonstorable exception Nonexpressible type eval = | Int of int | Bool of bool | Novalue type dval = | Dint of int | Dbool of bool | Unbound | Dloc of loc type mval = | Mint of int | Mbool of bool | Undefined let evaltomval e = match e with | Int n -> Mint n | Bool n -> Mbool n | _ -> raise Nonstorable let mvaltoeval m = match m with | Mint n -> Int n | Mbool n -> Bool n | _ -> Novalue let evaltodval e = match e with | Int n -> Dint n | Bool n -> Dbool n | Novalue -> Unbound let dvaltoeval e = match e with | Dint n -> Int n | Dbool n -> Bool n | Dloc n -> raise Nonexpressible | Unbound -> Novalue

once we have done this we have to implement the store, that will be a function
from `loc`

to memorizable value:

type 't env = string -> 't ;; exception WrongBindlist;; let emptyenv(x) = function y -> x;; let applyenv(x,y) = x y;; let bind((r: 'a env) , (l:string), (e:'a)) = function lu -> if lu = l then e else applyenv(r,lu);; let rec bindlist(r, il, el) = match (il,el) with | ([],[]) -> r | i::il1, e::el1 -> bindlist (bind(r, i, e), il1, el1) | _ -> raise WrongBindlist;; type loc = int;; type 't store = loc -> 't;; let (newloc,initloc) = let count = ref(-1) in (fun () -> count := !count +1; !count), (fun () -> count := -1);; let emptystore(x) = initloc(); function y -> x;; let applystore((x: 't store),(y : loc)) = x y;; let allocate((r: 'a store) , (e:'a)) = let l = newloc() in (l, function lu -> if lu = l then e else applystore(r,lu));; let update((r: 'a store) , (l:loc), (e:'a)) = function lu -> if lu = l then e else applystore(r,lu);;

The store is implemented as the environment as a function, but it *needs* to generate a fresh location when
needed. This is the `newloc`

. Simply use it.

Keeping in mind that the interpreter for the expression has been already defined, we have all the ingredients to solve the exercise:

A **Solution**:

let rec sem (e:exp) (r:dval env) (s: mval store) = match e with | Eint(n) -> Int(n) | Ebool(b) -> Bool(b) | Den(i) -> dvaltoeval(applyenv(r,i)) | Iszero(a) -> iszero((sem a r s) ) | Eq(a,b) -> equ((sem a r s) ,(sem b r s) ) | Prod(a,b) -> mult ( (sem a r s), (sem b r s)) | Sum(a,b) -> plus ( (sem a r s), (sem b r s)) | Diff(a,b) -> diff ( (sem a r s), (sem b r s)) | Minus(a) -> minus( (sem a r s)) | And(a,b) -> et ( (sem a r s), (sem b r s)) | Or(a,b) -> vel ( (sem a r s), (sem b r s)) | Not(a) -> non( (sem a r s)) | Ifthenelse(a,b,c) -> let g = sem a r s in if typecheck("bool",g) then (if g = Bool(true) then sem b r s else sem c r s) else failwith ("nonboolean guard") | Val(i) -> match applyenv(r,i) with | Dloc n -> mvaltoeval(applystore(s, n)) | _ -> failwith("not a variable") and semc (c: com) (r:dval env) (s: mval store) = match c with | Assign(i, e2) -> (match applyenv(r,i) with | Dloc(n) -> update(s, n, evaltomval(sem e2 r s)) | _ -> failwith ("wrong location in assignment")) | Cifthenelse(e, cl1, cl2) -> let g = sem e r s in if typecheck("bool",g) then (if g = Bool(true) then semc cl1 r s else semc cl2 r s) else failwith ("nonboolean guard") | While(e, cl) -> let g = sem e r s in if typecheck("bool",g) then (if g = Bool(true) then semc (While(e, cl)) r (semc cl r s) else s) else failwith ("nonboolean guard") | Cseq(c1,c2) -> semc c2 r (semc c1 r s);;

We add to the language **declarations**. Global ones are those which are at the beginning of a *program* (we will introduce a notion of program), whereas local declarations
are those local to each block.

We start adding the syntax of declarations (which goes together with the one of expressions and commands):

type ide = string;; type exp = | Eint of int | Ebool of bool | Den of ide | Prod of exp * exp | Sum of exp * exp | Diff of exp * exp | Eq of exp * exp | Minus of exp | Iszero of exp | Or of exp * exp | And of exp * exp | Not of exp | Ifthenelse of exp * exp * exp (* new for the imperative fragment *) | Val of ide and decl = | Dconst of ide * exp | Dvar of ide * exp | Dseq of decl * decl (* Commands *) and com = | Assign of ide * exp | Cifthenelse of exp * com * com | While of exp * com | Cseq of com * com

We can declare *constants* or *variables* and we assume that to each variable an initial value has to
be assigned. Clearly the use within the commands or expression should be consistent with the declaration
(i.e., you cannot assign a value to a constant!).

A declaration returns a possibly modified environment and a possibly modified store. In particular the declaration
of a constant modifies only the environment, whereas the declaration of a variable should first *allocate* a new
location and then associate the identifier to this location and the evaluation of the expression (properly converted) to
the location in the memory.

We can now declare a type program as follows:

type prog = Prog of decl * com

and complete the interpreter by stating what has to be done for declarations (that goes together with `sem`

and `semc`

):

... and semd (d:decl) (r:dval env) (s: mval store) = match d with | Dconst(i,e) -> (bind(r,i,evaltodval(sem e r s)),s) | Dvar(i,e) -> let (l,s1) = allocate(s,evaltomval(sem e r s)) in (bind(r, i, Dloc l), s1) | Dseq(d1,d2) -> let (r1,s1) = (semd d1 r s) in semd d2 r1 s1

and for programs (assuming that variables and identifier appearing in the program are declared):

let semprog (p:prog) = match p with | Prog(d,c) -> let (r1,s1) = (semd d (emptyenv Unbound) (emptystore Undefined)) in semc c r1 s1 | _ -> failwith("not a program")

`Block of decl * com`

. Modify the interpreter accordingly.
and semc .... | Block(d,c) -> let (r1,s1) = semd d r s in semc r1 s1

As we did for the functional language, we add functions and, as we may pass variables as arguments,
we want to implement also the way parameters can be passed to functions. We assume that functions must be
*declared* hence they are denotable. Furthermore we assume that functions modify the state and do not return
any value. Thus we have also to introduce a new command corresponding to function call.

We implement two modality of parameter passing: by *value* and by *reference*. We assume that an actual parameter
must be an expression, hence to pass a variable by reference, we assume that its *denotation* is passed (hence `Den “x”`

).

We omit the implementation of the environment and store, that do not change:

type ide = string type mode = Value | Reference type param = mode * ide (* Expressions *) type exp = | Eint of int | Ebool of bool | Den of ide | Prod of exp * exp | Sum of exp * exp | Diff of exp * exp | Eq of exp * exp | Minus of exp | Iszero of exp | Or of exp * exp | And of exp * exp | Not of exp | Ifthenelse of exp * exp * exp | Val of ide (* Declarations *) and decl = | Dconst of ide * exp | Dvar of ide * exp | Dseq of decl * decl | Declproc of ide * param list * com (* Commands *) and com = | Assign of ide * exp | Cifthenelse of exp * com * com | While of exp * com | Cseq of com * com | Block of decl * com | Call of ide * exp list

We added a type (`mode`

) for the two modalities, parameters are in a list, and we added
a *declaration* for procedures (`Declproc of ide * param list * com`

, as well as a way to call them (`Call of ide * exp list`

).

Clearly procedures must be denotable, hence the denotable values changes:

type dval = | Dint of int | Dbool of bool | Unbound | Dloc of loc | Dproc of proc and proc = param list * com * dval env

The other domains, as well as the converting mappings, do not change.

We are now ready to modify the `semd`

and `semc`

functions in such a way
non recursive procedures can be taken into account. As we did for the functional language, we add
a number of auxiliary functions:

and semd (d:decl) (r:dval env) (s: mval store) = match d with ... | Declproc(i,pl,c) -> (bind(r,i,makeproc(pl,c,r)),s) and makeproc ((pl:param list),(c:com),(r:dval env)) = Dproc(pl,c,r)

The `makeproc`

gives back the proper element of the denotable value.

We can now implement the `semc`

(as before, we give only the **new** parts)

and semc (c: com) (r:dval env) (s: mval store) = match c with ... | Call(i,el) -> applyproc(applyenv(r,i),el,r,s) and applyproc ((p:dval),(el:exp list),(r:dval env),(s:mval store)) = match p with | Dproc(pl,c,r2) -> let (r1,s1) = bindacttoform(pl,el,r,r2, s) in semc c r1 s1 | _ -> failwith("not a procedure") and bindacttoform ((pl:param list),(el:exp list),(r:dval env),(racc:dval env),(s:mval store)) = match (pl,el) with | ([],[]) -> (racc,s) | ((Value,i)::pl1,e::el1) -> let (l,s1) = allocate(s,evaltomval(sem e r s)) in bindacttoform(pl1,el1,r,bind(racc, i, Dloc l),s1) | ((Reference,i)::pl1,(e:exp)::el1) -> (match e with Den(j) -> (match applyenv(r,j) with | Dloc(l) -> bindacttoform(pl1,el1,r,bind(racc, i, Dloc(l)),s) | _ -> failwith("this parameter is a constant")) | _ -> failwith("this parameter is not a variable")) | _ -> failwith("parameter list mismatch")

The `applyproc`

should first calculate the proper environment and store for the body of the procedure,
which are those built from the environment at declaration time and store at run time. The new
env and store are calculated by the bindacttoform (bind actual to formal), which inspect the mode of the
parameter passing, and it accordingly behaves. It should be noticed that we have always to pass the
environment at call time without modifying it.

Here a small example:

# let dich = Dseq(Declproc("foo",[(Value,"y");(Reference,"x")],Assign("x",Sum(Val "y",Val "x"))),Dvar("y",Eint 7));; val dich : decl = Dseq (Declproc ("foo", [(Value, "y"); (Reference, "x")], Assign ("x", Sum (Val "y", Val "x"))), Dvar ("y", Eint 7)) # let comm = Call("foo",[Eint 1;Den("y")]);; val comm : com = Call ("foo", [Eint 1; Den "y"]) # let (r,s) = (semd dich (emptyenv Unbound) (emptystore Undefined)) in sem (Val("y")) r (semc comm r s);; - : eval = Int 8

The procedure `foo`

receives two parameter (`“x”`

and `“y”`

) and assign to `“x”`

its value plus the one of `“y”`

.
To a variable with the same name (`“y”`

, but it is a different variable) a value is associated. The
procedure is called passing an expression and a variable, and we inspect then the value of the variable passed by reference.

A variation in the call is

# let comm = Call("foo",[Val "y";Den("y")]);; val comm : com = Call ("foo", [Val "y"; Den "y"]) # let (r,s) = (semd dich (emptyenv Unbound) (emptystore Undefined)) in sem (Val("y")) r (semc comm r s);; - : eval = Int 14

Observe that in this implementation the scope is static and no recursion is allowed.

A solution: as we did the functional language we have to modify the denotable value stating that now procedures should use the environment that is used during the call. Hence now we have the following

type dval = ... and proc = param list * com

Then we simply modify the function `applyproc`

as follows:

and applyproc ((p:dval),(el:exp list),(r:dval env),(s:mval store)) = match p with | Dproc(pl,c) -> let (r1,s1) = bindacttoform(pl,el,r,r, s) in semc c r1 s1 | _ -> failwith("not a procedure")

Notice that now the `bindacttoform`

uses the environment that is passed as argument to
the `applyproc`

.

In this case we add a *declaration* and we add a `makeprocric`

following the same pattern we saw in the case of the functional language:

... and decl = | Dconst of ide * exp | Dvar of ide * exp | Dseq of decl * decl | Declproc of ide * param list * com | Declprocric of ide * param list * com ... and semd (d:decl) (r:dval env) (s: mval store) = match d with ... | Declprocric(i,pl,c) -> (bind(r,i,makeprocric(pl,c,r,i)),s) ... and makeprocric ((pl:param list),(c:com),(r:dval env),(i:ide)) = let calculateenv (rr: dval env) = (bind(rr,i,(makeproc(pl,c,rr)))) in let rec rfix = function x -> calculateenv rfix x in Dproc(pl,c,rfix)

sem_op_implip.txt · Last modified: 2015/10/08 15:20 (external edit)