User Tools

Site Tools


sem_op_implip

This page is a draft

Operational interpreter of an imperative language

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.


Syntax, environment and store

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:

Exercise Write the interpreter for the language

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);;

Global and local declarations

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")

Exercise Local declarations need some structuring of commands, hence we introduce blocks, which have the following syntax Block of decl * com. Modify the interpreter accordingly.

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

Functions and parameters

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.

Exercise. Modify the above implementation to realize a dynamically scoped language.

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.

Exercise. Modify the above implementation to add recursive procedures in a statically scoped language.

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)