User Tools

Site Tools


imp-interpreter

Differences

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

Link to this comparison view

imp-interpreter [2015/10/08 15:20] (current)
Line 1: Line 1:
 +====== Interpreter of an imperative language ======
 +
 +Let us consider the imperative programming language IMP, 
 +featuring assignment, arrays, sequence, conditionals,​ and while loops.
 +
 +To write an interpreter for [[http://​unicaml.sc.unica.it/​lib/​exe/​fetch.php?​media=:​imp-interpreter.pdf|IMP]],​ we have to go through the following definitions:​
 +  * **environment**:​ semantic domain and functions ''​emptyenv'',​ ''​bind'',​ ''​applyenv''​
 +  * **store**: semantic domain and functions ''​emptystore'',​ ''​applystore'',​ ''​update''​
 +  * **expressions**:​ syntax, semantic domain of their evaluation, and operational semantics ''​sem_exp''​
 +  * **declarations**:​ syntax, operational semantics ''​sem_dec''​
 +  * **commands**:​ syntax, operational semantics ''​sem_com''​
 +  * **programs**:​ syntax, operational semantics ''​sem_prog''​
 +
 +\\
 +
 +
 +===== Environment =====
 +
 +The environment is a mapping from identifiers ''​ide''​ to denoted values ''​dval''​.
 +
 +<code ocaml>
 +type ide = string;;
 +type loc = int;;
 +</​code>​
 +
 +The type ''​dval''​ represent the semantic domain of environments:​
 +<code ocaml>
 +type dval =
 +    Unbound
 +  | DConst of int
 +  | DVar of loc
 +  | DArray of loc
 +;;
 +</​code>​
 +
 +The type ''​env''​ is then defined as follows:
 +<code ocaml>
 +type env = Env of (ide -> dval)
 +</​code>​
 +
 +<code ocaml>
 +exception UnboundIde of ide;;
 +exception TypeMismatch of string;;
 +</​code>​
 +
 +The specification of ''​env''​ requires the following functions: ​
 +  * ''​emptyenv''​ evaluates to the empty environment (i.e. mapping all identifiers to ''​Unbound''​)
 +  * ''​bind r x d''​ evaluates to an environment extending ''​r''​ with a new binding for ''​x''​ to ''​d''​
 +  * ''​applyenv r x''​ evaluates to the value bound to ''​x'',​ if any. It raises an exception if  no binding for ''​x''​ is present in ''​r''​.
 +
 +<code ocaml>
 +# let emptyenv = fun () -> Env (fun x -> Unbound);;
 +val emptyenv : unit -> env
 +</​code>​
 +
 +<code ocaml>
 +# let bind (Env rho) x d = Env (fun y -> if y=x then d else rho y);;
 +val bind : env -> ide -> dval -> env
 +</​code>​
 +
 +<code ocaml>
 +# let applyenv (Env rho) x = match rho x with
 +    Unbound -> raise (UnboundIde x)
 +  | _ as d -> d
 +;;
 +
 +val applyenv : env -> ide -> dval
 +</​code>​
 +
 +\\
 +
 +===== Store =====
 +
 +The store is modelled as a pair. 
 +The first element of the pair is a mapping from locations ''​loc''​ to memorized values ''​mval''​. ​
 +The second element of the pair is an integer that records the size of the store.
 +
 +<code ocaml>
 +type mval = int;;
 +
 +type store = Store of (loc -> mval) * int;;
 +</​code>​
 +
 +The specification of ''​store''​ requires the following functions: ​
 +  * ''​emptystore ()''​ evaluates to the "​empty"​ store (which mapps all locations to the integer 0). The size of the store is 2<​sup>​16</​sup>​ (in hexadecimal,​ ''​0x10000''​)
 +  * ''​update s l m''​ evaluates to an store where the value ''​m''​ is memorized at location ''​l''​
 +  * ''​applystore s l''​ evaluates to the value memorized at location ''​l''​. It raises an ''​AddressOutOfBounds''​ exception if ''​l''​ if a negative number, or exceeds the size of the store.
 +
 +<code ocaml>
 +# let emptystore = fun () -> Store ((fun x -> 0), 0x10000);;
 +val emptystore : unit -> store = <fun>
 +</​code>​
 +
 +<code ocaml>
 +exception AddressOutOfBounds of loc;;
 +</​code>​
 +
 +<code ocaml>
 +# let applystore (Store (sigma,​dim)) l = 
 +    if 0 <= l && l < dim then sigma l
 +    else raise (AddressOutOfBounds l)
 +;;
 +
 +val applystore : store -> loc -> mval = <fun>
 +</​code>​
 +
 +
 +<code ocaml>
 +# let update (Store (sigma,​dim)) l m = 
 +    if 0 <= l && l < dim then Store ((fun l' -> if l'=l then m else sigma l'), dim)
 +    else raise (AddressOutOfBounds l)
 +
 +val update : store -> loc -> mval -> store = <fun>
 +</​code>​
 +
 +\\
 +
 +
 +===== Expressions =====
 +
 +Expressions have the following abstract syntax:
 +<code ocaml>
 +type exp =
 +    N of int
 +  | Val of ide
 +  | ArrayVal of ide * exp
 +  | Add of exp * exp
 +  | Sub of exp * exp
 +  | Mul of exp * exp
 +  | Eq of exp * exp
 +  | Lt of exp * exp
 +  | Not of exp
 +  | And of exp * exp
 +  | Or of exp * exp
 +;;
 +</​code>​
 +
 +The evaluation of an expression ''​e''​ in an environment ''​rho''​ and a store ''​sigma''​ is defined by the function ''​sem_exp'',​ by induction on the structure of ''​e''​. ​
 +An exception is raised when trying to access variables or arrays with the wrong construct. ​
 +
 +<code ocaml>
 +exception TypeMismatch of string
 +
 +let rec sem_exp e (r, s) = match e with
 +  N n -> n
 +| Val x ->  ​
 +    (match applyenv r x with
 +      DVar l -> applystore s l
 +    | DConst c -> c
 +    | DArray l -> raise (TypeMismatch (
 +        "You have tried to access array" ^ x ^ " as a variable"​))
 +    | _ -> raise (UnboundIde x)
 +    )
 +| ArrayVal (x,e') ->  ​
 +    (match applyenv r x with
 +      DArray l -> applystore s (l + sem_exp e' (r,s))
 +    | DVar l -> raise (TypeMismatch (
 +        "You have tried to access variable " ^ x ^ " as an array"​))
 +    | DConst c -> raise (TypeMismatch (
 +        "You have tried to access constant " ^ x ^ " as an array"​))
 +    | Unbound -> raise (UnboundIde x)
 +    )
 +| Add (e1,e2) -> sem_exp e1 (r,s) + sem_exp e2 (r,s)
 +| Sub (e1,e2) -> sem_exp e1 (r,s) - sem_exp e2 (r,s)
 +| Mul (e1,e2) -> sem_exp e1 (r,s) * sem_exp e2 (r,s)
 +| Eq (e1,e2) -> if sem_exp e1 (r,s) = sem_exp e2 (r,s) then 1 else 0
 +| Lt (e1,e2) -> if sem_exp e1 (r,s) < sem_exp e2 (r,s) then 1 else 0
 +| Not e' -> if sem_exp e' (r,s) = 0 then 1 else 0
 +| And (e1,e2) -> if sem_exp e1 (r,s) = 0 || sem_exp e2 (r,s) = 0 then 0 else 1
 +| Or (e1,e2) -> if sem_exp e1 (r,s) = 0 && sem_exp e2 (r,s) = 0 then 0 else 1
 +;;
 +
 +val sem_exp : exp -> env * store -> mval = <fun>
 +</​code>​
 +
 +\\
 +
 +
 +===== Declarations =====
 +
 +Declarations comprise the empty one, the declaration of a constant, ​
 +the declaration of a variable, the declaration of an array, ​
 +and the sequence of two declarations.
 +<code ocaml>
 +type dec =
 +    Empty
 +  | Const of ide * int
 +  | Var of ide
 +  | Array of ide * int
 +  | Dseq of dec * dec
 +;;
 +</​code>​
 +
 +The semantics of a declaration ''​d'' ​
 +in an environment ''​rho''​ and a starting location ''​l'' ​
 +is defined by the function ''​sem_dec'',​ with the following signature.
 +<code ocaml>
 +val sem_dec : dec -> env * loc -> env * loc
 +</​code>​
 +
 +<code ocaml>
 +let rec sem_dec d (r,l) = match d with
 +  Empty -> (r,l)
 +| Const(x,v) -> (bind r x (DConst v), l)
 +| Var x -> (bind r x (DVar l), l+1)
 +| Array (x,v) -> (bind r x (DArray l), l+v)
 +| Dseq(d1,d2) -> sem_dec d2 (sem_dec d1 (r,l))
 +;;
 +</​code>​
 +
 +<note important>​
 +Note that declarations do not affect the store, so we have defined ''​sem_dec''​ as a function ''​dec -> env * loc -> env * loc''​. ​
 +Updating the store is needed when you can declare and initialize a variable at the same time (try it as an exercise).
 +</​note>​
 +
 +\\
 +
 +
 +===== Commands =====
 +
 +A command is either a skip, an assignment to a variable or an array, a sequence of commands, ​
 +an if-then-else,​ or a while loop.
 +<code ocaml>
 +type com =
 +    Skip
 +  | AssignVar of ide * exp
 +  | AssignArray of ide * exp * exp
 +  | Cseq of com * com
 +  | If of exp * com * com
 +  | While of exp * com
 +;;
 +</​code>​
 +
 +The semantics of a command ''​c''​ in an environment ''​r''​ and a store ''​s''​ is defined by the function ''​sem_com''​
 +(note that commands do not modify the environment):​
 +<code ocaml>
 +val sem_com : com -> env * store -> store
 +</​code>​
 +
 +<code ocaml>
 +let rec sem_com c (rho,sigma) = match c with
 +    Skip -> sigma
 +  | AssignVar(x,​e) -> (match applyenv rho x with
 +      DVar l -> update sigma l (sem_exp e (rho,​sigma))
 +    | _ -> raise (TypeMismatch ("You have tried to assign to non-variable"​ ^ x)))
 +  | AssignArray(x,​e,​e'​) -> (match applyenv rho x with
 +      DArray l -> update sigma (l + sem_exp e (rho,​sigma)) (sem_exp e' (rho,​sigma))
 +    | _ -> raise (TypeMismatch ("You have tried to assign to non-array"​ ^ x)))
 +  | Cseq(c1,c2) -> 
 +      sem_com c2 (rho,​sem_com c1 (rho,​sigma))
 +  | If(e,c1,c2) -> 
 +      if sem_exp e (rho,sigma) = 0 
 +      then sem_com c2 (rho,​sigma) ​
 +      else sem_com c1 (rho,sigma)
 +  | While(e,​c'​) -> 
 +      if sem_exp e (rho,sigma) = 0 
 +      then sigma 
 +      else sem_com c (rho,​sem_com c' (rho,​sigma))
 +;;
 +</​code>​
 +
 +\\
 +
 +
 +===== Programs =====
 +
 +A program is a pair (declaration,​ command). Its semantics starts from the empty environment and empty store, ​
 +then applies the semantics of the declaration and of the comment.
 +<code ocaml>
 +type prog = Program of dec * com;;
 +</​code>​
 +
 +<code ocaml>
 +let sem_prog (Program (d,c)) =
 +  let (rho,l) = sem_dec d (emptyenv(),​0)
 +  in sem_com c (rho,​emptystore())
 +;;
 +</​code>​
 +
 +The signature of ''​sem_prog''​ is as follows:
 +<code ocaml>
 +val sem_prog : prog -> store = <fun>
 +</​code>​
 +
 +
 +We now introduce some auxiliary functions to debug programs:
 +<code ocaml>
 +let rec range a b = 
 +  if a>b then []
 +  else a::(range (a+1) b);;
 +
 +let rec ide = function
 +    Empty -> []
 +  | Const (x,v) -> [x]
 +  | Var x -> [x]
 +  | Array (x,v) -> [x]
 +  | Dseq (d1,d2) -> (ide d1) @ (ide d2)
 +;;
 +
 +let dump (Program (d,c)) = 
 +  let (r,l) = sem_dec d (emptyenv(),​0)
 +  in let s' = sem_com c (r,​emptystore())
 +  in (List.map (fun x -> (x,applyenv r x)) (ide d), 
 +      List.map (applystore s') (range 0 (l-1)))
 +;;
 +</​code>​
 +
 +\\
 +
 +
 +===== Examples =====
 +
 +Let us write an IMP program to compute the factorial function:
 +<code ocaml>
 +let fact x = Program(
 +  Dseq(Const ("​n",​ x),Dseq(Var "​i",​Var "​f"​)),​
 +  Cseq(Cseq(AssignVar ("​i",​ N 1),​AssignVar ("​f",​ N 1)),
 +    ​While(Or(Lt (Val "​i",​ Val "​n"​),​Eq (Val "​i",​ Val "​n"​)),​
 + Cseq(AssignVar ("​f",​ Mul (Val "​f",​Val "​i"​)), ​
 +   AssignVar ("​i",​ Add (Val "​i",​N 1))))))
 +;;
 +</​code>​
 +
 +<code ocaml>
 +# dump (fact 5);;
 +([("​n",​ DConst 5); ("​i",​ DVar 0); ("​f",​ DVar 1)], [6; 120])
 +</​code>​
 +
 +\\
 +
 +
 +===== Exercises ===== 
 +
 +[[ex-imp-interpreter|LIP assignment #6]]
 +
 +\\
 +
  
imp-interpreter.txt ยท Last modified: 2015/10/08 15:20 (external edit)