22/07/15

2 files changed, 49 insertions, 117 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]
diff --git a/code/zam.ml b/code/zam.ml
index 07fb85e..bd39ad4 100644
--- a/code/zam.ml
+++ b/code/zam.ml
@@ -1,3 +1,13 @@
+(*********************************************)
+(* (Extended) Krivine Machine implementation *)
+(*                                           *)
+(* Guillermo Ramos Gutiérrez (2015)          *)
+(*********************************************)
+
+
+(*********)
+(* Utils *)
+(*********)
 let print_with f x = print_endline (f x)
 let concat_with sep f xs = String.concat sep (List.map f xs)
 let split n xs =
@@ -15,16 +25,20 @@ let fold_left1 f = function
   | [] -> raise (Invalid_argument "empty string")
   | (x::xs) -> List.fold_left f x xs
 
-let dbg_lev = 5
+let dbg_lev = 1
 let debug lev spaces s =
   if dbg_lev >= lev
   then print_endline (" -- " ^ String.concat "" (repeat spaces "  ") ^ s)
 
+
 (* Compile, decompile and reduce errors *)
 exception CpErr of string
 exception DcErr of string
 exception RdErr of string
 
+(************************************)
+(*  Calculus of Constructions terms *)
+(************************************)
 module CCLambda = struct
     type symbol = string * int
     let symbol : string -> symbol =
@@ -67,66 +81,42 @@ module CCLambda = struct
       let x = symbol s in
       Abs (x, Var x)
 
-    let rec appN n f m = if n = 0 then m else appN (n-1) f (App (f, m))
     let apps = fold_left1 (fun m n -> App (m, n))
 
-    let church_of_int n =
-      let f = symbol "f" in
-      let x = symbol "x" in
-      Abs (f, Abs (x, appN n (Var f) (Var x)))
-
     let none = symbol "None"
     let some = symbol "Some"
     let cons = symbol "Cons"
     let nil  = symbol "Nil"
 
-    (* Peano arithmetic *)
+    (* Peano arithmetic helpers *)
     let z = symbol "z"
     let s = symbol "s"
 
     let rec peano_add n x =
       if n == 0 then x else peano_add (n-1) (Constr (s, [x]))
 
-    let peano_of_int n = peano_add n (Constr (z, []))
+    let peano_of_int ?(base=Constr (z, [])) n = peano_add n base
 
     (* Examples *)
 
-    (* (λx.λy. (x y)) (λxx.xx) *)
-    let partial =
-      let x = symbol "x" in
+    (* (λx.x) (λy. ((λz.z) y) (λt.t) *)
+    let ex_m1 =
       let y = symbol "y" in
-      App (Abs (x, Abs (y, App (Var x, Var y))),
-           identity "xx")
-
-    (* (λm.λn.λf.λx. (m f)((n f) x) *)
-    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 _3plus1 =
-      App (App (plus, church_of_int 3), church_of_int 1)
+      App (identity "x",
+           Abs (y, App (App (identity "z",
+                             Var y),
+                        identity "t")))
 
     (* (λf.λx. f (f x)) (λy.y) (λz.z) *)
-    let twiceId =
+    let ex_id_id =
       let f = symbol "f" in
       let x = symbol "x" in
       App (App (Abs (f, Abs (x, App (Var f, App (Var f, Var x)))),
                 identity "y"),
            identity "z")
 
-    (* (λc. case c of (Some(x) → x) (None → c)) Some(s(z))) *)
-    let 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 (Cons(x, xs) → x) (Nil → Nil)) Cons(λx.x, Nil) *)
-    let case_head =
+    let ex_case_head =
       let c = symbol "c" in
       let x = symbol "x" in
       let xs = symbol "xs" in
@@ -135,7 +125,7 @@ module CCLambda = struct
            Constr (cons, [identity "m"; Constr (nil, [])]))
 
     (* fix_0(λf.λc. case c of (s(x) → s(s(f x))) (z → z)) s(s(s(z))) *)
-    let fix_dup =
+    let ex_fixpt_dup =
       let f = symbol "f" in
       let c = symbol "c" in
       let x = symbol "x" in
@@ -143,45 +133,6 @@ module CCLambda = struct
                  [((s, [x]), peano_add 2 (App (Var f, Var x)));
                   ((z, []), peano_of_int 0)])),
            peano_of_int 3)
-
-    (* fix_1(λf.λg.λc. case c of (s(x) → g(f x)) (z → z)) (λy.s(s(y))) s(s(s(z))) *)
-    let fix_scale =
-      let f = symbol "f" in
-      let g = symbol "g" in
-      let c = symbol "c" in
-      let x = symbol "x" in
-      let y = symbol "y" in
-      App (App (Fix (f, [g], c, Case (Var c,
-                 [((s, [x]), App (Var g, (App (Var f, Var x))));
-                  ((z, []), peano_of_int 0)])),
-                Abs (y, peano_add 2 (Var y))),
-           peano_of_int 1)
-
-    (* (λx.x) (λy. ((λz.z) y) (λt.t) *)
-    let acc_app =
-      let y = symbol "y" in
-      App (identity "x",
-           Abs (y, App (App (identity "z",
-                             Var y),
-                        identity "t")))
-
-    (* (λc. case c of (Cons(x, xs) → x) (Nil → Nil)) *)
-    let acc_case =
-      let c = symbol "c" in
-      let x = symbol "x" in
-      let xs = symbol "xs" in
-      Abs (c, Case (Var c, [((cons, [x;xs]), Var c);
-                            ((nil, []), Constr (nil, []))]))
-
-    (* fix_0(λf.λn. case c of (s(x) → s(s(f x))) (z → z)) *)
-    let acc_fix =
-      let f = symbol "f" in
-      let c = symbol "c" in
-      let x = symbol "x" in
-      Fix (f, [], c, Case (Var c,
-            [((s, [x]), peano_add 2 (App (Var f, Var x)));
-             ((z, []), peano_of_int 0)]))
-
 end
 
 module WeakRed : sig
@@ -234,10 +185,9 @@ end = struct
         st_n : int;
     }
 
-    let show_dbi = function
-      | (x, i) ->
-         string_of_int i ^
-           if dbg_lev > 2 then " (" ^ show_symbol x ^ ")" else ""
+    let show_dbi (x, i) =
+      string_of_int i ^
+        if dbg_lev > 2 then " (" ^ show_symbol x ^ ")" else ""
     let rec show_instr = function
       | ACCESS dbi -> "ACCESS(" ^ show_dbi dbi ^ ")"
       | CLOSURE is -> "CLOSURE(" ^ show_instrs is ^ ")"
@@ -494,7 +444,6 @@ module StrongRed = struct
          let f' = unique f in
          let c' = unique c in
          let accs = List.map (fun x -> Acc (Var x)) (f' :: xs' @ [c']) in
-         (* debug 2 10 (concat_with " # " show accs); *)
          let m' = reduce (apps (m :: accs)) in
          Fix (f', xs', c', m')
       | _ -> readback (WeakRed.reduce m)
@@ -507,7 +456,6 @@ module StrongRed = struct
       | Acc k -> readback_acc k
       | App (Fix (f, xs, c, m), p) ->
          App (reduce (Fix (f, xs, c, m)), readback p)
-      (* | Fix (f, xs, c, m) -> *)
       | _ -> raise (RdErr "Readback of invalid value")
     and readback_acc m =
       debug 2 2 ("R'( " ^ show m ^ " )");
@@ -525,22 +473,22 @@ module StrongRed = struct
       | _ -> raise (RdErr "Readback of invalid accumulator")
 end
 
-let test_weakred m =
+let weakred m =
   print_endline "WEAK REDUCTION TEST";
-  print_endline ("Target expression: '" ^ CCLambda.show m ^ "'...");
-
-  print_string "Compiling... ";
+  print_endline ("Lambda term:\n    " ^ CCLambda.show m);
   let compiled = WeakRed.compile m in
-
-  print_endline "Reducing...";
   let reduced = WeakRed.am_reduce compiled in
-  print_endline ("Final value: " ^ CCLambda.show (WeakRed.extract reduced))
+  print_endline ("Reduced term:\n    " ^ CCLambda.show (WeakRed.extract reduced));
+  print_endline "----------------------------------------------------------\n"
 
-let test_strongred m =
+let strongred m =
   print_endline "STRONG REDUCTION TEST";
-  print_endline ("Target expression: '" ^ CCLambda.show m ^ "'...");
-  print_endline ("Final value: " ^ CCLambda.show (StrongRed.reduce m))
+  print_endline ("Lambda term:\n    " ^ CCLambda.show m);
+  print_endline ("Reduced term:\n    " ^ CCLambda.show (StrongRed.reduce m));
+  print_endline "----------------------------------------------------------\n"
 
 let () =
-  let m = CCLambda.fix_scale in
-  test_strongred m
+  let open CCLambda in
+  let examples = [ex_m1; ex_id_id; ex_case_head; ex_fixpt_dup] in
+  List.iter weakred examples;
+  List.iter strongred examples