User Tools

Site Tools


imp-types

This page is a draft

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.

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

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, commands and programs

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

Examples

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)