X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;f=code%2Freduction_with_closures.ml;fp=code%2Freduction_with_closures.ml;h=dc3d8fa284b186fe60eab63bf62e4b0073d212f8;hb=ff5b3f5a76fb744b332bc5d0fb3ef5632ce02879;hp=0000000000000000000000000000000000000000;hpb=73f8e125d9910c93213d357c2779cc743fa22e8b;p=lambda.git

diff --git a/code/reduction_with_closures.ml b/code/reduction_with_closures.ml
new file mode 100644
index 00000000..dc3d8fa2
--- /dev/null
+++ b/code/reduction_with_closures.ml
@@ -0,0 +1,96 @@
+(* 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) -> eval body (push bound_ident arg saved_r) (* FIX ME *)
+                           | 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