impl environment

src/cui.ml

@@ -5,14 +5,16 @@ exception Error of string
 
 let err s = raise (Error s)
 
+let initial_env =
+  Environment.extend "id" (Abstraction ("_x", Var "_x")) Environment.empty
+
+
 (* read eval print *)
 let rec rep env =
   print_string "# ";
   flush stdout;
   let exp = Parser.main Lexer.main (Lexing.from_channel stdin) in
-  print_string (string_of_exp exp);
-  print_newline ();
-  let b = eval exp in
+  let b = eval initial_env exp in
   List.iter (fun b ->
   print_string ("β " ^ (string_of_exp b));
   print_newline ()) b;

src/environment.ml

@@ -0,0 +1,19 @@
+type 'a t = (Syntax.id * 'a) list
+
+exception Not_bound
+exception Bound_Several_Times of string
+
+let empty = []
+let extend x v env = (x,v)::env
+
+let lookup x env =
+  try List.assoc x env with Not_found -> raise Not_bound
+
+let rec map f = function
+    [] -> []
+  | (id, v)::rest -> (id, f v) :: map f rest
+
+let rec fold_right f env a =
+  match env with
+    [] -> a
+  | (_, v)::rest -> f v (fold_right f rest a)

src/environment.mli

@@ -0,0 +1,11 @@
+
+type 'a t
+
+exception Not_bound
+exception Bound_Several_Times of string
+
+val empty : 'a t
+val extend : Syntax.id -> 'a -> 'a t -> 'a t
+val lookup : Syntax.id -> 'a t -> 'a
+val map : ('a -> 'b) -> 'a t -> 'b t
+val fold_right : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b

src/evaluation.ml

@@ -16,13 +16,14 @@ let rec substitute x t exp = match exp with
   only outermost redexes are reduced and where a redex is reduced only when its right-hand side has already been reduced to a value
   (λx. t1) t2 -> [x → t2]t1
 *)
-let rec beta = function
+let rec beta env = function
     Application (Abstraction (x, t1), exp2) ->
-      let t2 = beta exp2 in
+      let t2 = beta env exp2 in
       substitute x t2 t1
   | Application (exp1, exp2) ->
-      let t = beta exp1 in
+      let t = beta env exp1 in
       Application (t, exp2)
+  | Var id -> Environment.lookup id env
   | e -> e
 
 (* 
@@ -31,7 +32,7 @@ let rec beta = function
     - detect infinite reduction
     - set timeout
 *)
-let rec eval t =
-  let b = beta t in
+let rec eval env t =
+  let b = beta env t in
   if (string_of_exp b) = (string_of_exp t)
-  then [t] else t :: (eval b)
+  then [t] else t :: (eval env b)

test/lambda_test.ml

@@ -7,7 +7,7 @@ let err s = raise (Error s)
 
 let parse s = Parser.main Lexer.main (Lexing.from_string s)
 let eval s =
-  let e = Evaluation.eval (parse s) in
+  let e = Evaluation.eval Lambda.Environment.empty (parse s) in
   let len = List.length e in
   if len > 0 then List.nth e (len - 1) else err ("Failed to evaluate")