sem_op_imp_proc

This page is a draft

We add functions to the language IMP defined here.

- A function is composed by a local declaration, a command, and an expression that represents the value to be returned to the caller.
- Declarations have a static scope.
- A single parameter can be passed to a function, either in a call-by-value or in a call-by-name fashion.
- Functions do
*not*modify the value of global variables. - In this version of the semantics, I do not require that functions can be passed as parameters, or returned by other functions.

The syntax of declarations is extended as follows:

type dec = ... | Fun of ide * ide * mode * dec * com * exp

The first item is the function identifier.
The second item is the parameter identifier, and `mode`

is the parameter passing style.
The last three items are the local declaration, the command, and the expression for the return value.

type mode = Value | Name

For instance, this is a fuction (named `succ`

) to compute the successor of the integer parameter `x`

:

Fun(Ide "succ", Ide "x", Value, Empty, Skip, Add(Val(Ide "x"), N 1));;

The syntax of expressions is extended as follows:

type exp = ... | Apply of ide * exp

For instance, this expression applies the function `succ`

to the integer 3:

Apply(Ide "succ", N 3);;

The syntax of commands is unchanged, as well as that of programs.

The semantic domain of denotable values is extended with two constructors.
`DFun`

is for denoting a function, while `DName`

is for denoting a *closure*
used to evaluate a parameter passed by name (more details below).
To implement static scoping, the value denoted by a function includes the environment where the function is defined (last item in `DFun`

).

type dval = ... | DFun of ide * mode * dec * com * exp * env | DName of exp * env

To save time and focus on the core aspects of this lecture, you can copy&paste this code.
It contains the basic definitions of the syntactic and semantic domains, and the specification of environment and memory.

The operational semantics of expressions and declarations is extended to deal with the
expression `Apply(f,e)`

and the declaration `Fun(f,x,m,d,c,e)`

.
Moreover, the case `Val(x)`

has to be revised to deal with closures (see below).

- The semantics of a function declaration
`Fun(f,x,m,d,c,e)`

in the environment`r`

extends`r`

with a binding for`f`

. The denoted value associated to`f`

is a closure`DFun(x,m,d,c,e,r)`

. The value of the parameter passing style`m`

is immaterial. - The semantics of the expression
`Apply(f,a)`

depends on the parameter passing style`m`

.- if
`m = Value`

, then the semantics of`a`

is computed in the current environment, and its value is bound to the formal parameter`x`

in the static environment. Then, the local declaration`d`

, the command`c`

and the expression`e`

are evaluated in sequence, starting from the extended static environment. - if
`m = Name`

, then`a`

is not yet evaluated. Instead, the formal parameter`x`

is bound to the closure`DName(a,r)`

, where`r`

is static environment. Then, evaluation proceeds as in the previous case.

In both cases, to allow for recursive functions we have to bind the function identifier `f`

to its closure `DFun(x,m,d,c,e,r)`

before evaluating the command `c`

.

- The semantics of the expression
`Val(x)`

has to consider the case when`x`

is bound to a closure`DName(a,r)`

. This requires evaluating`a`

in the enviroment`r`

.

The semantics of commands is unchanged.

exception TypeMismatch;; exception AssignNonVariable of ide;; 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 | DName (e',r') -> sem_exp e' (r',s) | _ -> raise (UnboundIde x)) | 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)) | Apply (f,a) -> (match applyenv r f with DFun (x,m,d,c,e',r') -> let r1 = bind r' f (DFun(x,m,d,c,e',r')) in let r2 = (match m with Value -> bind r1 x (DConst (sem_exp a (r,s))) | Name -> bind r1 x (DName (a,r1))) in let (r3,s3) = sem_dec d (r2,s) in let s4 = sem_com c (r3,s3) in sem_exp e' (r3,s4)) and 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) | Fun(f,x,m,d',c,e) -> (bind r f (DFun(x,m,d',c,e,r)), s) | Dseq(d1,d2) -> sem_dec d2 (sem_dec d1 (r,s)) and 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 (AssignNonVariable x)) | 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 and sem_prog (Program (d,c)) = sem_com c (sem_dec d (emptyenv(),emptystore())) ;;

To facilitate copy&paste, I have reversed the use of the symbol

`#`

.
From now on, it will always be used to represent output of the ocaml environment, instead that user input.
First, an example to show recursion:

let factfun = Fun(Ide "fact", Ide "x", Value, Var (Ide "res"), If(Leq (Val (Ide "x"), N 0), Assign (Ide "res", N 1), Assign (Ide "res", Mul(Val (Ide "x"), Apply(Ide "fact", Sub(Val (Ide "x"),N 1))))), Val (Ide "res"));; let fact x = Program(Dseq(factfun, Var (Ide "f")), Assign(Ide "f", Apply (Ide "fact", N x)));; inspect ["f"] (debug_prog (fact 5));; # - : (string * eval) list = [("f", Int 120)]

The following example shows that the application of a function does not modify global variables.
If not, the final value of the variable `z`

would have been `2`

instead of `1`

.

let f0 = Fun(Ide "f0", Ide "x", Value, Empty, Assign(Ide "z", N 2), N 10);; let sideeffect = Program(Dseq(Var (Ide "z"), Dseq(f0, Var (Ide "res"))), Cseq(Assign(Ide "z", N 1), Assign(Ide "res", Apply(Ide "f0", N 11))));; inspect ["z"] (debug_prog sideeffect);; # - : (string * eval) list = [("z", Int 1)]

The following example illustrates static scoping. If we had implemented *dynamic* scoping, the result would have been 12 instead of 11.

let f1 = Fun(Ide "f1", Ide "x", Value, Empty, Skip, Add(Val(Ide "x"),Val(Ide "z")));; let f2 = Fun(Ide "f2", Ide "y", Value, Const (Ide "z", N 2), Skip, Apply(Ide "f1", Val(Ide "y")));; let scoping = Program(Dseq(Const (Ide "z", N 1),Dseq(f1,Dseq(f2,Var (Ide "res")))), Assign(Ide "res", Apply(Ide "f2", N 10)));; inspect ["res"] (debug_prog scoping);; # - : (string * eval) list = [("res", Int 11)]

let f m k = Fun(Ide "f", Ide "x", m, Var (Ide "res"), Cseq(Assign(Ide "res", N k), If(Leq(Val (Ide "res"), N 9), Skip, Assign(Ide "res", Val (Ide "x")))), Val (Ide "res"));; let fmismatch = Fun(Ide "fmismatch", Ide "z", Value, Empty, Skip, Add(True, N 1));; let pmismatch m k = Program( Dseq(fmismatch, Dseq(f m k, Var (Ide "res"))), Assign(Ide "res", Apply (Ide "f", Apply(Ide "fmismatch", N 1))));; inspect ["res"] (debug_prog (pmismatch Value 5));; # Exception: TypeMismatch. inspect ["res"] (debug_prog (pmismatch Value 10));; # Exception: TypeMismatch. inspect ["res"] (debug_prog (pmismatch Name 5));; # - : (string * eval) list = [("res", Int 5)] inspect ["res"] (debug_prog (pmismatch Name 10));; # Exception: TypeMismatch.

let bot = Fun(Ide "bot", Ide "y", Value, Empty, While(True,Skip), N 51);; let pbot m k = Program(Dseq(bot, Dseq(f m k, Var (Ide "res"))), Assign(Ide "res", Apply (Ide "f", Apply(Ide "bot", N 1))));; inspect ["res"] (debug_prog (pbot Name 5));; # (* non-termination *)

The type-checking algorithm defined here is refined to deal with functions. Roughly, one has to check that the type of the parameter and the type of the returned value are used consistently in a program.

The types are extended as follows:

type etype = ... | TFunction of (etype * etype)

The typed declarations are extended with functions.
Respect to the syntax of `dec`

seen above, we have added the type for the parameter and the type for the return value.

type tdec = ... | TFun of ide * ide * mode * etype * tdec * com * exp * etype

The functions `idetypes`

, `typecheck_exp`

and `typecheck_tdec`

have to be extended to deal with functions.

Here are some examples.

let tfactfun = TFun(Ide "fact", Ide "x", Value, TInt, TVar (Ide "res", TInt), If(Leq (Val (Ide "x"), N 0), Assign (Ide "res", N 1), Assign (Ide "res", Mul(Val (Ide "x"), Apply(Ide "fact", Sub(Val (Ide "x"),N 1))))), Val (Ide "res"), TInt);; let tfact x = TProgram(TDseq(tfactfun, TVar (Ide "f", TInt)), Assign(Ide "f", Apply (Ide "fact", N x)));; typecheck_prog (tfact 5);; # - : bool = true

The program `wrong1`

below is not well-typed, because it applies the function `fact`

to a boolean value.

let wrong1 = TProgram(TDseq(tfactfun, TVar (Ide "f", TInt)), Assign(Ide "f", Apply (Ide "fact", True)));; typecheck_prog wrong1;; # - : bool = false

The program `wrong2`

below is not well-typed, because it assigns an integer value (the result of invoking the `fact`

function) to a variable `f`

declared as boolean.

let wrong2 = TProgram(TDseq(tfactfun, TVar (Ide "f", TBool)), Assign(Ide "f", Apply (Ide "fact", N 5)));; typecheck_prog wrong2;; # - : bool = false

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