22/07/15

1 files changed, 8 insertions, 24 deletions

diff --git a/code/krivine.ml b/code/krivine.ml
index 0c34d3f..6e0eeb3 100644
--- a/code/krivine.ml
+++ b/code/krivine.ml
@@ -77,43 +77,27 @@ module Lambda = struct
     (* Examples *)
 
     (* (λx.((λy.y) x)) *)
-    let m1 =
+    let ex_m1 =
       let x = symbol "x" in
       let y = symbol "y" in
       Abs (x, App (Abs (y, Var y), Var x))
 
     (* (((λx.(λy.(y x))) (λz.z)) (λy.y)) *)
-    let m2 =
+    let ex_m2 =
       let x = symbol "x" in
       let y = symbol "y" in
       let z = symbol "z" in
       App (App (Abs (x, Abs (y, App (Var y, Var x))), Abs (z, Var z)), Abs (y, Var y))
 
-    let plus =
-      let m = symbol "m" in
-      let n = symbol "n" in
-      let f = symbol "f" in
-      let x = symbol "x" in
-      Abs (m, Abs (n, Abs (f, Abs (x, App (App (Var m, Var f),
-                                           App (App (Var n, Var f), Var x))))))
-
-    let nested_if =
-      If (True, If (False, False, True), False)
-
-    (* s((λx.x) z) *)
-    let constr_test =
-      let x = symbol "x" in
-      peano_of_int ~base:(App (Abs (x, Var x), Constr (z, []))) 1
-
     (* (λc. case c of (Some(x) → x) (None → c)) Some(s(z))) *)
-    let case_some =
+    let ex_case_some =
       let c = symbol "c" in
       let x = symbol "x" in
       App (Abs (c, Case (Var c, [((some, [x]), Var x); ((none, []), Var c)])),
            Constr (some, [peano_of_int 1]))
 
     (* (λc. case c of (Triple(x,y,z) → y)) Triple(1,2,3)) *)
-    let case_triple =
+    let ex_case_tuple =
       let c = symbol "c" in
       let x = symbol "x" in
       let y = symbol "y" in
@@ -123,7 +107,7 @@ module Lambda = struct
            Constr (triple, List.map peano_of_int [1;2;3]))
 
     (* fix(λf.λc. case c of (s(x) → s(s(f x))) (z → z)) s(s(s(z))) *)
-    let fix_dup =
+    let ex_fixpt_mul2 =
       let f = symbol "f" in
       let c = symbol "c" in
       let x = symbol "x" in
@@ -133,7 +117,7 @@ module Lambda = struct
            peano_of_int 3)
 
     (* fix(λf.λg.λc. case c of (s(x) → g (f g x)) (z → z)) (λy.s(s(s(y)))) s(s(s(z))) *)
-    let fix_scale =
+    let ex_fix_scale =
       let f = symbol "f" in
       let g = symbol "g" in
       let c = symbol "c" in
@@ -259,5 +243,5 @@ let dbi_and_red m =
 
 let () =
   let open Lambda in
-  List.iter dbi_and_red [m1; m2; plus; nested_if; constr_test;
-                         case_some; case_triple; fix_dup; fix_scale]
+  List.iter dbi_and_red [ex_m1; ex_m2; ex_case_some;
+                         ex_case_tuple; ex_fixpt_mul2; ex_fix_scale]