1 (* evaluation1.ml: evaluation-based interpreter *)
3 type literal = Num of int | Bool of bool (* intersection of values and Constant terms *)
4 type primFunction = Succ | Pred | IsZero | Leq (* | Leq_partially_applied of int *)
6 type value = LiteralV of literal (* | Closure ... *)
7 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 *)
9 type constant = LiteralC of literal | FunctC of primFunction
10 type identifier = string
12 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
17 val push: identifier -> bound_value -> env -> env
18 val lookup: identifier -> env -> bound_value option
21 module Env1: Env = struct
22 type env = (identifier * bound_value) list
24 let push ident value env = (ident,value)::env
25 let rec lookup ident' env = match env with
27 | (ident,value)::_ when ident = ident' -> Some value
28 | _::env' -> lookup ident' env'
31 module Env2: Env = struct
32 type env = identifier -> bound_value option
33 let empty = fun _ -> None
34 let push ident value env = fun ident' -> if ident = ident' then Some value else env ident'
35 let lookup ident' env = env ident'
40 exception Stuck of lambdaTerm
42 let rec eval (term:lambdaTerm) (r:env) : value =
44 | IfThenElse(test, yes, no) -> (match eval test r with
45 | LiteralV(Bool true) -> eval yes r
46 | LiteralV(Bool false) -> eval no r
47 | LiteralV lit -> raise (Stuck (IfThenElse(Constant(LiteralC lit),yes,no))))
48 | Let(bound_var, arg, body) -> (match eval arg r with
49 | value -> eval body (push bound_var value r))
50 | App(head, arg) -> let headval = eval head r
51 in let argval = eval arg r
52 in (match (headval, argval) with
53 | (LiteralV lit, _) -> raise (Stuck (App(Constant(LiteralC lit), arg)))
54 | (_,_) -> failwith "not yet implemented")
55 | Var ident -> (match lookup ident r with
57 | None -> raise (Stuck term)) (* free variables are stuck *)
58 | Constant (LiteralC lit) -> LiteralV lit
59 | Constant (FunctC _) -> failwith "not yet implemented"
60 | Abstract (_,_) -> failwith "not yet implemented"
62 let rec check_numbers (term:lambdaTerm) : unit =
64 | Constant(LiteralC(Num n)) when n < 0 -> failwith ("Bad Number: " ^ string_of_int n)
67 | Abstract(_, body) -> check_numbers body
68 | App(head, arg) -> let () = check_numbers head
70 | Let(_, arg, body) -> let () = check_numbers arg
72 | IfThenElse(test, yes, no) -> let () = check_numbers test
73 in let () = check_numbers yes
76 let evaluate (term:lambdaTerm) : value =
77 (* scan to verify that term doesn't have any Const(Num (negative)) *)
78 let () = check_numbers term
79 (* evaluate starting with empty env *)