hofl_op_eager

Operational interpreter of a functional language

Syntax

```type ide = Ide of string;;

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
| If of exp * exp * exp
| Let of ide * exp * exp
| Letrec of ide * exp * exp
| Fun of ide * exp
| Apply of exp * exp
;;```

Semantic domains and environment

```type eval =
Bool of bool
| Int of int
| EFun of ide * exp * env
| Unbound

and env = Env of (ide -> eval);;

exception UnboundIde of ide;;

let emptyenv = Env (fun x -> Unbound)
and bind (Env r) x d = Env (fun y -> if y=x then d else r y)
and applyenv (Env r) x = match r x with
Unbound -> raise (UnboundIde x)
| _ as d -> d
;;```

Operational semantics

```let rec intval e r = match (sem e r) with
Int n -> n
| _ -> raise TypeMismatch

and boolval e r = match sem e r with
Bool b -> b
| _ -> raise TypeMismatch

and sem e r = match e with
N n -> Int n
| Val x ->  applyenv r x
| Add (e1,e2) ->  Int (intval e1 r + intval e2 r)
| Sub (e1,e2) ->  Int (intval e1 r - intval e2 r)
| Mul (e1,e2) ->  Int (intval e1 r * intval e2 r)
| Div (e1,e2) ->  Int (intval e1 r / intval e2 r)
| True -> Bool true
| False -> Bool false
| Eq (e1,e2) -> Bool (intval e1 r = intval e2 r)
| Leq (e1,e2) -> Bool (intval e1 r <= intval e2 r)
| Not e' -> Bool (not (boolval e' r))
| And (e1,e2) -> Bool (boolval e1 r && boolval e2 r)
| Or (e1,e2) -> Bool (boolval e1 r || boolval e2 r)
| If(e0,e1,e2) -> if boolval e0 r then sem e1 r else sem e2 r
| Let (x,e1,e2) -> sem e2 (bind r x (sem e1 r))
| Letrec (x,e1,e2) -> let rec r' = Env(fun y -> applyenv (bind r' x (sem e1 r')) y) in sem e2 r'
| Fun (x,e') -> EFun (x,e',r)
| Apply (e1,e2) -> match sem e1 r with
EFun (x,e',r') -> sem e' (bind r' x (sem e2 r))
| _ -> raise TypeMismatch
;;```
`val sem : exp -> env -> eval = <fun>`

Examples

```let e0 = Let(Ide "succ",Fun(Ide "x", Add(Val(Ide "x"), N 1)),Apply(Val(Ide "succ"),N 8));;
sem e0 emptyenv;;

# - : eval = Int 9```
```let e1 = Letrec(Ide "fact",
Fun(Ide "x",
If(Eq(Val(Ide "x"),N 0),
N 1,
Mul(Val(Ide "x"),
Apply(Val(Ide "fact"),Sub(Val(Ide "x"), N 1))))),
Apply(Val(Ide "fact"),N 5));;

sem e1 emptyenv;;

# - : eval = Int 120```
```let bot = Letrec(Ide "f", Fun(Ide "x", Apply(Val(Ide "f"),Val(Ide "x"))),
Apply(Val(Ide "f"), N 1));;

sem bot emptyenv;;

# (* non-terminating computation *)```