update ski_evaluators
[lambda.git] / code / reduction_with_environments.ml
1 (* evaluation1.ml: evaluation-based interpreter *)
2
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 *)
5
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 *)
8
9 type constant = LiteralC of literal | FunctC of primFunction
10 type identifier = string
11
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
13
14 module type Env = sig
15   type env
16   val empty: env
17   val push: identifier -> bound_value -> env -> env
18   val lookup: identifier -> env -> bound_value option
19 end
20
21 module Env1: Env = struct
22   type env = (identifier * bound_value) list
23   let empty = []
24   let push ident value env = (ident,value)::env
25   let rec lookup ident' env = match env with
26     | [] -> None
27     | (ident,value)::_ when ident = ident' -> Some value
28     | _::env' -> lookup ident' env'
29 end
30
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'
36 end
37
38 open Env1
39
40 exception Stuck of lambdaTerm
41
42 let rec eval (term:lambdaTerm) (r:env) : value =
43   match term with
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
56                               | Some v -> v
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"
61
62 let rec check_numbers (term:lambdaTerm) : unit =
63   match term with
64     | Constant(LiteralC(Num n)) when n < 0 -> failwith ("Bad Number: " ^ string_of_int n)
65     | Constant _ -> ()
66     | Var _ -> ()
67     | Abstract(_, body) -> check_numbers body
68     | App(head, arg) -> let () = check_numbers head
69                         in check_numbers arg
70     | Let(_, arg, body) -> let () = check_numbers arg
71                            in check_numbers body
72     | IfThenElse(test, yes, no) -> let () = check_numbers test
73                            in let () = check_numbers yes
74                            in check_numbers no
75
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 *)
80   in eval term empty
81
82