Add some tests

src/cui.ml

@@ -1,4 +1,4 @@
-open Reduction
+open Evaluation
 open Syntax
 
 exception Error of string

src/dune

@@ -2,11 +2,8 @@
  (name lambda))
 
 (ocamllex
-  (modules lexer)
-)
+ (modules lexer))
 
 (menhir
-  (modules parser)
-  (flags -la 2)
-)
-
+ (modules parser)
+ (flags -la 2))

src/reduction.ml → src/evaluation.ml

@@ -19,14 +19,19 @@ let rec substitute x t exp = match exp with
 let rec beta = function
     Application (Abstraction (x, t1), exp2) ->
       let t2 = beta exp2 in
-      let e = substitute x t2 t1 in
-      beta e
+      substitute x t2 t1
   | Application (exp1, exp2) ->
       let t = beta exp1 in
       Application (t, exp2)
   | e -> e
 
+(* 
+  TODO:
+    - consider better way to detect stop condition
+    - detect infinite reduction
+    - set timeout
+*)
 let rec eval t =
   let b = beta t in
   if (string_of_exp b) = (string_of_exp t)
-  then [] else b :: (eval b)
+  then [t] else t :: (eval b)

src/lexer.mll

@@ -2,6 +2,7 @@ rule main = parse
 | (* ignore spacing and newline characters *)
   [' ' '\009' '\012']+     { main lexbuf }
 | "\\" { Parser.BACKSLASH }
+| "λ" { Parser.LAMBDA }
 | "(" { Parser.LPAREN }
 | ")" { Parser.RPAREN }
 | "." { Parser.DOT }

src/parser.mly

@@ -2,7 +2,7 @@
 open Syntax
 %}
 
-%token BACKSLASH LPAREN RPAREN DOT 
+%token BACKSLASH LAMBDA LPAREN RPAREN DOT 
 %token <Syntax.id> ID
 %token EOL
 
@@ -20,6 +20,7 @@ let expr :=
 // associativity: right
 let abstraction :=
     BACKSLASH; id = ID; DOT; ~ = abstraction; { Abstraction (id, abstraction) }
+  | LAMBDA; id = ID; DOT; ~ = abstraction; { Abstraction (id, abstraction) } 
   | ~ = application; <>
 
 // associativity: left

test/dune

@@ -1,2 +1,3 @@
 (test
- (name lambda))
+ (name lambda_test)
+ (libraries ounit2 lambda))

test/lambda_test.ml

@@ -0,0 +1,40 @@
+open OUnit2
+open Lambda
+
+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 (parse s) in
+  let len = List.length e in
+  if len > 0 then List.nth e (len - 1) else err ("Failed to evaluate")
+
+type testcase = {input: string; expected: Syntax.exp}
+
+let tests = [
+  { input = "x"; expected = Var "x" };
+  { input = "λx.x"; expected = Abstraction ("x", Var "x") };
+  { input = "λx.x y"; expected = Abstraction ("x", Application (Var "x", Var "y")) };
+  { input = "λx.x y"; expected = Abstraction ("x", Application (Var "x", Var "y")) };
+  { input = "(λx.x) x"; expected = Var "x" };
+  { input = "(λl. λm. λn. l m n) (λt. λf. t) v w"; expected = Var "v" };
+  { 
+    input = "(λx. x x) (λx. x x)"; 
+    expected = Application (
+      Abstraction ("x", Application (Var "x", Var "x")), 
+      Abstraction ("x", Application (Var "x", Var "x"))) 
+  };
+]
+
+let suite = "test suite for lambda" >:::
+  List.map (fun tt ->
+    let i = Syntax.string_of_exp (eval(tt.input ^ "\n")) in
+    let e = Syntax.string_of_exp tt.expected in
+    tt.input >:: (fun _ -> assert_equal
+    ~printer: (fun x -> x)
+    i e)
+    ) tests
+
+let _ = run_test_tt_main suite