imp-types

This page is a draft

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`

The environment is a mapping from identifiers `ide`

to denoted values `dval`

.
The store is a mapping from locations `loc`

to memorized values `mval`

.

type ide = Ide of string and loc = Loc of int;;

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`

.

type dval = DVar of loc | DConst of eval | Unbound and mval = Mem of eval | Uninitialized and eval = Bool of bool | Int of int ;;

Then, `env`

and `store`

are defined as follows:

type env = Env of (ide -> dval) and store = Store of (loc -> mval);;

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`

.

exception UnboundIde val emptyenv : unit -> env val bind : env -> ide -> dval -> env val applyenv : env -> ide -> dval

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.

exception UninitializedLoc val emptystore : unit -> store val newloc : unit -> loc val update : store -> loc -> mval -> store val applystore : store -> loc -> eval

The function `newloc`

is specified as follows, using *side effects*:

# let count = ref(-1);; val count : int ref = {contents = -1} # let newloc = fun () -> count := !count +1; Loc (!count);; val newloc : unit -> loc = <fun>

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

Expressions have the following abstract syntax:

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

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.

exception TypeMismatch val sem_exp : exp -> env * store -> eval

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

Declarations comprise the empty one, the declaration of a constant, the declaration of a variable, and the sequence of two declarations.

type dec = Empty | Const of ide * exp | Var of ide | Dseq of dec * dec ;;

The semantics of a declaration `d`

in an environment `e`

and a store `s`

is defined by the function `sem_dec`

.

val sem_dec : dec -> env * store -> env * store

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

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

type com = Skip | Assign of ide * exp | Cseq of com * com | If of exp * com * com | While of exp * com ;;

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

exception AssignNonVar val sem_com : com -> env * store -> store

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

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.

type prog = Program of dec * com;; let sem_prog (Program (d,c)) = sem_com c (sem_dec d (emptyenv(),emptystore())) ;;

First we need some auxiliary functions to “debug” a program:

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

Then, we write and test an IMP program to compute the factorial function:

# 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)]

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