User Tools

Site Tools


sem_op_implip

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sem_op_implip [2015/10/08 15:20] (current)
Line 1: Line 1:
 +<note warning>​This page is a draft</​note>​
 +
 +
 +====== 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):​
 +
 +<code ocaml>
 +(* 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
 +</​code>​
 +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...)
 +
 +<code ocaml>
 +(* 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 ​
 +</​code>​
 +
 +once we have done this we have to implement the store, that will be a function
 +from ''​loc''​ to memorizable value:
 +
 +<code ocaml>
 +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);; ​   ​
 +</​code>​
 +
 +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:
 +
 +<​note>​ **Exercise** Write the interpreter for the language</​note>​
 +
 +A **Solution**:​
 +
 +<code ocaml>
 +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);;
 +</​code>​
 +
 +===== 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):
 +
 +<code ocaml>
 +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
 +</​code>​
 +
 +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:
 +
 +<code ocaml>
 +type prog = Prog of decl * com
 +</​code>​
 +
 +and complete the interpreter by stating what has to be done for declarations (that goes together with ''​sem''​ and ''​semc''​):​
 +
 +<code ocaml>
 +...
 +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
 +</​code>​
 +
 +and for programs (assuming that variables and identifier appearing in the program are declared):
 +
 +<code ocaml>
 +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"​)
 +</​code>​
 +
 +<​note>​ **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.</​note>​
 +
 +<code ocaml>
 +and semc ....
 +   | Block(d,c) -> let (r1,s1) = semd d r s in semc r1 s1
 +</​code>​
 +
 +===== 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:
 +
 +<code ocaml>
 +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
 +</​code>​
 +
 +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:
 +
 +<code ocaml>
 +type dval =     
 +    | Dint of int 
 +    | Dbool of bool 
 +    | Unbound
 +    | Dloc of loc
 +    | Dproc of proc
 +and proc = param list * com * dval env
 +</​code>​
 +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 [[sem_op_fun|functional language]], we add
 +a number of auxiliary functions:
 +
 +<code ocaml>
 +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)
 +</​code>​
 +
 +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) ​
 +
 +<code ocaml>
 +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"​)
 +</​code>​
 +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:
 +<code ocaml>
 +# 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
 +</​code>​
 +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
 +<code ocaml>
 +# 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
 +</​code> ​
 +Observe that in this implementation the scope is static and no recursion is allowed.
 +
 +<​note>​
 +**Exercise**. Modify the above implementation to realize a dynamically scoped language.
 +</​note>​
 +
 +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 ​
 +<code ocaml>
 +type dval =
 +    ...
 +and proc = param list * com
 +</​code>​
 +Then we simply modify the function ''​applyproc''​ as follows:
 +<code ocaml>
 +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"​)
 +</​code>​
 +
 +Notice that now the ''​bindacttoform''​ uses the environment that is passed as argument to
 +the ''​applyproc''​.
 +
 +<​note>​
 +**Exercise**. Modify the above implementation to add recursive procedures in a statically scoped language.
 +</​note>​
 +
 +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:
 +
 +<code ocaml>
 +...
 +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)
 +</​code>​
 +
  
sem_op_implip.txt ยท Last modified: 2015/10/08 15:20 (external edit)