(* evaluation2.ml: evaluation-based interpreter *)
type literal = Num of int | Bool of bool (* intersection of values and Constant terms *)
type primFunction = Succ | Pred | IsZero | Leq (* | Leq_partially_applied of int *)
(* these have to be declared later, inside the Env modules ...
type value = LiteralV of literal | Closure of lambdaTerm * env
type bound_value = value (* for now, "x" is bound to the same type of thing that Var "x" expresses, but in later stages that won't always be true *)
*)
type constant = LiteralC of literal | FunctC of primFunction
type identifier = string
type lambdaTerm = Constant of constant | Var of identifier | Abstract of identifier * lambdaTerm | App of lambdaTerm * lambdaTerm | IfThenElse of lambdaTerm * lambdaTerm * lambdaTerm | Let of identifier * lambdaTerm * lambdaTerm
module type Env = sig
type env
type value = LiteralV of literal | Closure of lambdaTerm * env
type bound_value = value
val empty: env
val push: identifier -> bound_value -> env -> env
val lookup: identifier -> env -> bound_value option
end
module Env1: Env = struct
type env = (identifier * bound_value) list
and value = LiteralV of literal | Closure of lambdaTerm * env
and bound_value = value
let empty = []
let push ident value env = (ident,value)::env
let rec lookup ident' env = match env with
| [] -> None
| (ident,value)::_ when ident = ident' -> Some value
| _::env' -> lookup ident' env'
end
module Env2: Env = struct
type env = identifier -> bound_value option
and value = LiteralV of literal | Closure of lambdaTerm * env
and bound_value = value
let empty = fun _ -> None
let push ident value env = fun ident' -> if ident = ident' then Some value else env ident'
let lookup ident' env = env ident'
end
open Env1
exception Stuck of lambdaTerm
let rec eval (term:lambdaTerm) (r:env) : value =
match term with
| IfThenElse(test, yes, no) -> (match eval test r with
| LiteralV(Bool true) -> eval yes r
| LiteralV(Bool false) -> eval no r
| LiteralV lit -> raise (Stuck (IfThenElse(Constant(LiteralC lit),yes,no)))
| Closure(term, _) -> raise (Stuck (IfThenElse(term,yes,no))))
| Let(bound_ident, arg, body) -> (match eval arg r with
| value -> eval body (push bound_ident value r))
| App(head, arg) -> (match eval head r with
| LiteralV lit -> raise (Stuck (App(Constant(LiteralC lit), arg)))
| Closure (Abstract(bound_ident, body), saved_r) -> let argval = eval arg r in eval body (push bound_ident argval saved_r)
| Closure (Constant (FunctC Leq), saved_r) -> failwith "not yet implemented"
| Closure (Constant (FunctC (_ as prim)), saved_r) ->
(match (prim, eval arg r) with
| (Succ, LiteralV(Num n)) -> LiteralV(Num (n+1))
| (Pred, LiteralV(Num n)) -> LiteralV(Num (if n = 0 then 0 else n-1))
| (IsZero, LiteralV(Num n)) -> LiteralV(Bool (n=0))
| (_, LiteralV lit) -> raise (Stuck (App(Constant(FunctC prim), Constant(LiteralC lit))))
| (_, Closure(term, _)) -> raise (Stuck (App(Constant(FunctC prim), term))))
| Closure (term, _) -> raise (Stuck (App(term, arg))))
| Var ident -> (match lookup ident r with
| Some v -> v
| None -> raise (Stuck term)) (* free variables are stuck *)
| Constant (LiteralC lit) -> LiteralV lit
| Constant (FunctC _) -> Closure(term, empty) (* primFunctions evaluate as Closures with empty environments *)
| Abstract (_,_) -> Closure(term, r) (* Abstracts evaluate as Closures with the current environment; a more efficient implementation would save only that part of the environment that binds variables that are free in the Abstract *)
let rec check_numbers (term:lambdaTerm) : unit =
match term with
| Constant(LiteralC(Num n)) when n < 0 -> failwith ("Bad Number: " ^ string_of_int n)
| Constant _ -> ()
| Var _ -> ()
| Abstract(_, body) -> check_numbers body
| App(head, arg) -> let () = check_numbers head
in check_numbers arg
| Let(_, arg, body) -> let () = check_numbers arg
in check_numbers body
| IfThenElse(test, yes, no) -> let () = check_numbers test
in let () = check_numbers yes
in check_numbers no
let evaluate (term:lambdaTerm) : value =
(* scan to verify that term doesn't have any Const(Num (negative)) *)
let () = check_numbers term
(* evaluate starting with empty env *)
in eval term empty