Operational interpreter of a functional language
Syntax
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 *)