diff options
Diffstat (limited to 'code/krivine.ml')
| -rw-r--r-- | code/krivine.ml | 37 |
1 files changed, 25 insertions, 12 deletions
diff --git a/code/krivine.ml b/code/krivine.ml index dfbdd4a..0c34d3f 100644 --- a/code/krivine.ml +++ b/code/krivine.ml @@ -65,7 +65,7 @@ module Lambda = struct let none = symbol "None" let some = symbol "Some" - (* Peano arithmetic *) + (* Peano arithmetic helpers *) let z = symbol "z" let s = symbol "s" @@ -75,11 +75,19 @@ module Lambda = struct let peano_of_int ?(base=Constr (z, [])) n = peano_add n base (* Examples *) + + (* (λx.((λy.y) x)) *) let 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 x = symbol "x" in + let y = symbol "y" in let z = symbol "z" in - App (Abs (x, Var x), App (Abs (y, Var y), Abs (z, Var z))) + 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 @@ -124,7 +132,7 @@ module Lambda = struct ((z, []), peano_of_int 0)]))), peano_of_int 3) - (* fix(λf.λg.λc. case c of (s(x) → g (f g x)) (z → z)) (λy.s(s(y))) s(s(s(z))) *) + (* 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 f = symbol "f" in let g = symbol "g" in @@ -134,7 +142,7 @@ module Lambda = struct App (App (Fix (f, Abs (g, Abs (c, Case (Var c, [((s, [x]), App (Var g, (App (App (Var f, Var g), Var x)))); ((z, []), peano_of_int 0)])))), - Abs (y, peano_add 2 (Var y))), + Abs (y, peano_add 3 (Var y))), peano_of_int 3) end @@ -152,12 +160,17 @@ module DBILambda = struct let dbi dbis x = (find_idx_exn x dbis, x) - let show_dbi_symbol (n, x) = show_symbol x + let output_dbi = false + let show_dbi_symbol (n, x) = + if output_dbi then string_of_int n else show_symbol x + let show_dbi_param x = + if output_dbi then "" else show_symbol x + let rec show m = match m with | Var x -> show_dbi_symbol x | App (m1, m2) -> "(" ^ show m1 ^ " " ^ show m2 ^ ")" - | Abs (x, m) -> "(λ" ^ show_symbol x ^ "." ^ show m ^ ")" + | Abs (x, m) -> "(λ" ^ show_dbi_param x ^ "." ^ show m ^ ")" | If (m1, m2, m3) -> "if " ^ show m1 ^ " then " ^ show m2 ^ " else " ^ show m3 @@ -198,7 +211,7 @@ module KM = struct type st_elm = Clos of DBILambda.t * stack | IfCont of DBILambda.t * DBILambda.t - | CaseCont of (symbol constr * t) list * stack + | CaseCont of (symbol DBILambda.constr * DBILambda.t) list * stack | FixClos of symbol * DBILambda.t * stack and stack = st_elm list @@ -230,21 +243,21 @@ module KM = struct Constr (x, List.map (fun m -> reduce (m, s, e)) ms) (* Fixpoints *) | (Fix (x, m), s, e) -> reduce (m, s, FixClos (x, m, e) :: e) - (* Termination *) + (* Termination checks *) | (m, [], []) -> m | (_, _, _) -> m in reduce (m, [], []) end -let do_compile_and_red m = +let dbi_and_red m = let dbi_m = DBILambda.of_lambda m in print_endline ("# Lambda term:\n " ^ DBILambda.show dbi_m); let red_m = KM.reduce dbi_m in print_endline ("# Reduced term:\n " ^ DBILambda.show red_m); - print_endline "--------------------------------------------------------------\n" + print_endline "----------------------------------------------------------\n" let () = let open Lambda in - List.iter do_compile_and_red [m1; plus; nested_if; constr_test; - case_some; case_triple; fix_dup; fix_scale] + List.iter dbi_and_red [m1; m2; plus; nested_if; constr_test; + case_some; case_triple; fix_dup; fix_scale] |