User Tools

Site Tools


imp-types

Differences

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

Link to this comparison view

imp-types [2015/10/08 15:20] (current)
Line 1: Line 1:
 +<note warning>​This page is a draft</​note>​
  
 +====== A typed imperative language ======
 +
 +Let us consider an imperative programming language IMP with assignment, sequence, and while loops.
 +
 +To write an interpreter for IMP, we have to go through the following definitions:​
 +  * **environment**:​ semantic domain and functions ''​emptyenv'',​ ''​bind'',​ ''​applyenv''​
 +  * **store**: semantic domain and functions ''​emptystore'',​ ''​newloc'',​ ''​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,​ store and semantic domains =====
 +
 +The environment is a mapping from identifiers ''​ide''​ to denoted values ''​dval''​.
 +The store is a mapping from locations ''​loc''​ to memorized values ''​mval''​.
 +
 +<code ocaml>
 +type ide = Ide of string
 +and  loc = Loc of int;;
 +</​code>​
 +
 +The semantic domains are defined as follows. Note that the definition is recursive (''​type''​ declarations are always considered as such), because both denoted and memorized values refer to ''​eval''​.
 +
 +<code ocaml>
 +type dval =
 +    DVar of loc
 +  | DConst of eval
 +  | Unbound
 +
 +and mval =
 +    Mem of eval
 +  | Uninitialized
 +
 +and eval =
 +    Bool of bool
 +  | Int of int
 +;;
 +</​code>​
 +
 +Then, ''​env''​ and ''​store''​ are defined as follows:
 +<code ocaml>
 +type env = Env of (ide -> dval)
 +and  store = Store of (loc -> mval);;
 +</​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>
 +exception UnboundIde
 +val emptyenv : unit -> env
 +val bind : env -> ide -> dval -> env
 +val applyenv : env -> ide -> dval
 +</​code>​
 +
 +The specification of ''​store''​ requires the following functions: ​
 +  * ''​emptystore''​ evaluates to the empty store (i.e. mapping all locations to ''​Uninitialized''​)
 +  * ''​newloc''​ returns a free location
 +  * ''​update s l e''​ evaluates to an store where the value ''​e''​ is memorized at location ''​l''​
 +  * ''​applystore s l''​ evaluates to the value memorized at location ''​l'',​ if any. It raises an exception if ''​l''​ is not initialized.
 +
 +<code ocaml>
 +exception UninitializedLoc
 +val emptystore : unit -> store
 +val newloc : unit -> loc
 +val update : store -> loc -> mval -> store
 +val applystore : store -> loc -> eval
 +</​code>​
 +
 +The function ''​newloc''​ is specified as follows, using //side effects//:
 +<code ocaml>
 +# let count = ref(-1);;
 +val count : int ref = {contents = -1}
 +
 +# let newloc = fun () -> count := !count +1; Loc (!count);;
 +val newloc : unit -> loc = <fun>
 +</​code>​
 +
 +<code ocaml>
 +let emptyenv = fun () -> Env (fun x -> Unbound);;
 +
 +let bind (Env r) x d = Env (fun y -> if y=x then d else r y);;
 +
 +let applyenv (Env r) x = match r x with
 +  Unbound -> raise UnboundIde
 +| _ as d -> d
 +;;
 +
 +let emptystore = fun () -> (count := -1); Store (fun x -> Uninitialized);;​
 +
 +let applystore (Store s) l = match s l with
 +  Uninitialized -> raise UninitializedLoc
 +| Mem m -> m
 +;;
 +
 +let update (Store s) l m = Store (fun l' -> if l'=l then m else s l');;
 +</​code>​
 +
 +
 +===== Expressions =====
 +
 +Expressions have the following abstract syntax:
 +<code ocaml>
 +type exp =
 +    N of int
 +  | Val of ide
 +  | Add of exp * exp
 +  | Sub of exp * exp
 +  | Mul of exp * exp
 +  | Div of exp * exp
 +  | True
 +  | False
 +  | Eq of exp * exp
 +  | Leq of exp * exp
 +  | Not of exp
 +  | And of exp * exp
 +  | Or of exp * exp
 +;;
 +</​code>​
 +
 +The evaluation of an expression ''​e''​ in an environment ''​r''​ and a store ''​s''​ is defined by the function ''​sem_exp'',​ by induction on the structure of ''​e''​. An exception is raised when trying to mix operands of the wrong type, 
 +e.g. adding an Int to a Bool.
 +
 +<code ocaml>
 +exception TypeMismatch
 +val sem_exp : exp -> env * store -> eval
 +</​code>​
 +
 +<code ocaml>
 +let rec intval e (r,s) = match (sem_exp e (r,s)) with 
 +  Int n -> n
 +| _ -> raise TypeMismatch
 +
 +and boolval e (r,s) = match sem_exp e (r,s) with 
 +  Bool b -> b
 +| _ -> raise TypeMismatch
 +
 +and sem_exp e (r, s) = match e with
 +  N n -> Int n
 +| Val x ->  (match applyenv r x with
 +    DVar l -> applystore s l
 +  | DConst c -> c
 +  | _ -> raise UnboundIde)
 +| Add (e1,e2) ->  Int (intval e1 (r,s) + intval e2 (r,s))
 +| Sub (e1,e2) ->  Int (intval e1 (r,s) - intval e2 (r,s))
 +| Mul (e1,e2) ->  Int (intval e1 (r,s) * intval e2 (r,s))
 +| Div (e1,e2) ->  Int (intval e1 (r,s) / intval e2 (r,s))
 +| True -> Bool true
 +| False -> Bool false
 +| Eq (e1,e2) -> Bool (intval e1 (r,s) = intval e2 (r,s))
 +| Leq (e1,e2) -> Bool (intval e1 (r,s) <= intval e2 (r,s))
 +| Not e' -> Bool (not (boolval e' (r,s)))
 +| And (e1,e2) -> Bool (boolval e1 (r,s) && boolval e2 (r,​s)) ​
 +| Or (e1,e2) -> Bool (boolval e1 (r,s) || boolval e2 (r,​s)) ​
 +;;
 +</​code>​
 +
 +
 +
 +===== Declarations,​ commands and programs =====
 +
 +Declarations comprise the empty one, the declaration of a constant, the declaration of a variable, and the sequence of two declarations.
 +<code ocaml>
 +type dec =
 +    Empty
 +  | Const of ide * exp
 +  | Var of ide
 +  | Dseq of dec * dec
 +;;
 +</​code>​
 +
 +The semantics of a declaration ''​d''​ in an environment ''​e''​ and a store ''​s''​ is defined by the function ''​sem_dec''​.
 +<code ocaml>
 +val sem_dec : dec -> env * store -> env * store
 +</​code>​
 +
 +<code ocaml>
 +let rec sem_dec d (r,s) = match d with
 +  Empty -> (r,s)
 +| Const(x,e) -> (bind r x (DConst (sem_exp e (r,s))),s)
 +| Var x -> let l = newloc() in (bind r x (DVar l), s)
 +| Dseq(d1,d2) -> sem_dec d2 (sem_dec d1 (r,s))
 +;;
 +</​code>​
 +
 +<note important>​
 +In this case, declarations do not affect the store, so we could have defined ''​sem_dec''​ as a function ''​dec -> env * store -> env''​. ​
 +Updating the store is needed when you can declare and initialize a variable at the same time (try it as an exercise).
 +</​note>​
 +
 +A command is either a skip, or an assignment to a variable, or a sequence of commands, or an if-then-else,​ or a while loop.
 +<code ocaml>
 +type com =
 +    Skip
 +  | Assign of ide * exp
 +  | Cseq of com * com
 +  | If of exp * com * com
 +  | While of exp * com
 +;;
 +</​code>​
 +
 +The semantics of a command ''​c''​ in an environment ''​e''​ and a store ''​s''​ is defined by the function ''​sem_com''​
 +(note that commands do not extend the environment):​
 +<code ocaml>
 +exception AssignNonVar
 +val sem_com : com -> env * store -> store
 +</​code>​
 +
 +<code ocaml>
 +let rec sem_com c (r,s) = match c with
 +    Skip -> s
 +  | Assign(x,e) -> (match applyenv r x with
 +      DVar l -> update s l (Mem (sem_exp e (r,s)))
 +    | _ -> raise AssignNonVar)
 +  | Cseq(c1,c2) -> sem_com c2 (r,sem_com c1 (r,s))
 +  | If(b,c1,c2) -> if boolval b (r,s) then sem_com c1 (r,s) else sem_com c2 (r,s)
 +  | While(b,​c'​) -> if boolval b (r,s) then sem_com c (r,sem_com c' (r,s)) else s
 +;;
 +</​code>​
 +
 +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;;
 +
 +let sem_prog (Program (d,c)) =
 +    sem_com c (sem_dec d (emptyenv(),​emptystore()))
 +;;
 +</​code>​
 +
 +===== Examples =====
 +
 +First we need some auxiliary functions to "​debug"​ a program:
 +<code ocaml>
 +let debug_prog (Program (d,c)) = 
 +  let (r,s) = sem_dec d (emptyenv(),​emptystore())
 +  in let s' = sem_com c (r,s)
 +  in (r,s')
 +;;
 +
 +let rec map f l = match l with
 +  [] -> []
 +| x::xl -> (f x) :: (map f xl)
 +;;
 +
 +let inspect xl (r,s) = 
 +  let inspect_id x (r,s) = (match applyenv r (Ide x) with 
 + DVar l ->  (x,​applystore s l)
 +  | _ -> raise UninitializedLoc)
 +  in map (fun l -> inspect_id l (r,s)) xl
 +;;
 +</​code>​
 +
 +Then, we write and test an IMP program to compute the factorial function:
 +<code ocaml>
 +# let fact x = Program(
 +  Dseq(Const (Ide "​n",​ N x),Dseq(Var (Ide "​i"​),​Var (Ide "​f"​))),​
 +  Cseq(Cseq(Assign (Ide "​i",​ N 1),Assign (Ide "​f",​ N 1)),
 +    ​While(Leq (Val (Ide "​i"​),​ Val (Ide "​n"​)),​
 + Cseq(Assign (Ide "​f",​ Mul (Val (Ide "​f"​),​Val (Ide "​i"​))), ​
 +   Assign (Ide "​i",​ Add (Val (Ide "​i"​),​N 1))))))
 +;;
 +
 +# inspect ["​i";"​f"​] (debug_prog (fact 5));;
 +- : (string * eval) list = [("​i",​ Int 6); ("​f",​ Int 120)]
 +</​code>​
imp-types.txt ยท Last modified: 2015/10/08 15:20 (external edit)