summaryrefslogtreecommitdiff
path: root/code
diff options
context:
space:
mode:
Diffstat (limited to 'code')
-rw-r--r--code/krivine.ml32
-rw-r--r--code/zam.ml134
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
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-22 18:26:31 +0000