impl full beta reduction

main.ml

@@ -1,3 +1,3 @@
 open Lambda.Cui
 
-let () = rep ()
+let () = repl ()

src/cui.ml

@@ -31,14 +31,23 @@ let initial_env = Environment.from_list [
   ("head", parse "λh. λt. λc. λn. c h (t c n)");
 ]
 
+let usage_msg = "lambda [-v] [-s <strategy>]"
+let opt_verbose = ref false
+let opt_strategy = ref "full"
+let speclist =
+  [("-v", Arg.Set opt_verbose, "Output all reduction steps");
+   ("-s", Arg.Set_string opt_strategy, "Set strategy (full or call_by_value). default strategy is call_by_value")]
+let strategy_of_str s = match s with "full" -> Full | _ -> CallByValue
 
-(* read eval print *)
-let rec rep env =
-  print_string "# ";
-  flush stdout;
-  let exp = Parser.main Lexer.main (Lexing.from_channel stdin) in
-  let b = eval initial_env exp in
-  List.iter (fun b ->
-  print_string ("β " ^ (string_of_exp b));
-  print_newline ()) b;
-  rep env
+
+(* read eval print loop *)
+let repl () =
+  Arg.parse speclist (fun _ -> ()) usage_msg;
+  while true do
+    print_string "# ";
+    flush stdout;
+    let t = Parser.main Lexer.main (Lexing.from_channel stdin) in
+    let b = eval initial_env t { verbose = !opt_verbose; strategy = strategy_of_str !opt_strategy } in
+    print_string ("→ " ^ (string_of_exp b));
+    print_newline ();
+  done

src/evaluation.ml

@@ -4,6 +4,12 @@ exception Error of string
 
 let err s = raise (Error s)
 
+type strategy =
+    Full
+  | CallByValue
+
+type option = {verbose: bool; strategy: strategy}
+
 (* alpha reduction
   substitute id with id ^ "'"
 *)
@@ -41,24 +47,39 @@ let rec substitute x t exp = match exp with
   - E-App2 (t2 → t2': v1 t2 → v1 t2')
   - E-AppAbs ((λx.t12) v2 → [x → v2]t12)
 *)
-let rec beta = function
+let rec call_by_value = function
     (* E-AppAbs *)
     Application (Abstraction (x1, t1), Abstraction (x2, t2)) -> 
       substitute x1 (Abstraction (x2, t2)) t1
     (* E-App2 *)
-  | Application (Abstraction(x, t1), t2) -> Application (Abstraction(x, t1), beta t2)
+  | Application (Abstraction(x, t1), t2) -> Application (Abstraction(x, t1), call_by_value t2)
     (* E-App1 *)
-  | Application (t1, t2) -> Application (beta t1, t2)
+  | Application (t1, t2) -> Application (call_by_value t1, t2)
   | e -> e
 
-(* 
+let full t =
+  let rec full2 = function
+      Application (Abstraction (x, t1), t2) -> substitute x t2 t1
+    | Application (Var x, t) -> Application (Var x, full2 t)
+    | Application (t1, t2) -> Application (full2 t1, t2)
+    | Abstraction (x, t) -> Abstraction (x, full2 t)
+    | t -> t
+  in
+  let b = call_by_value t in
+  if (string_of_exp b) = (string_of_exp t) then full2 b else b
+
+(*
   TODO:
     - consider better way to detect stop condition
     - detect infinite reduction
     - set timeout
 *)
-let rec eval env t =
+let eval env t option =
   let t1 = Environment.fold_right (fun (x, t) exp -> substitute x t exp) env t in
-  let b = beta t1 in
-  if (string_of_exp b) = (string_of_exp t) then [t]
-  else t :: (eval env b)
+  let reduce = (match option.strategy with Full -> full | CallByValue -> call_by_value) in
+  let rec eval1 t2 =
+    let b = reduce t2 in
+    if (string_of_exp b) = (string_of_exp t2) then t2 else
+      (if option.verbose then print_endline ("β " ^ (string_of_exp t2));
+      eval1 b)
+  in eval1 t1

test/lambda_test.ml

@@ -5,11 +5,10 @@ exception Error of string
 
 let err s = raise (Error s)
 
-let parse s = Parser.main Lexer.main (Lexing.from_string s)
-let eval s =
-  let e = Evaluation.eval Lambda.Cui.initial_env (parse s) in
-  let len = List.length e in
-  if len > 0 then List.nth e (len - 1) else err ("Failed to evaluate")
+let eval s = 
+  let t = try Lambda.Cui.parse s with _ -> err ("parse error") in
+  Evaluation.eval Lambda.Cui.initial_env t
+  {verbose=false; strategy=Lambda.Evaluation.CallByValue}
 
 type testcase = {input: string; expected: Syntax.exp}
 
@@ -75,7 +74,7 @@ let tests = [
 
 let suite = "test suite for lambda" >:::
   List.map (fun tt ->
-    let i = Syntax.string_of_exp (eval(tt.input ^ "\n")) in
+    let i = Syntax.string_of_exp (eval(tt.input)) in
     let e = Syntax.string_of_exp tt.expected in
     tt.input >:: (fun _ -> assert_equal
     ~printer: (fun x -> x)