From 5cecab147f53f77dcf70a0f1845772d41cff1597 Mon Sep 17 00:00:00 2001 From: acondolu Date: Mon, 28 May 2018 15:14:34 +0200 Subject: [PATCH] Machine implements strong reduction The machine is very inefficient (uses unwind under lambdas) --- ocaml/pure.ml | 68 ++++++++++++++++++++++++++++++++++----------------- ocaml/util.ml | 1 + 2 files changed, 46 insertions(+), 23 deletions(-) diff --git a/ocaml/pure.ml b/ocaml/pure.ml index 29288aa..f1cac84 100644 --- a/ocaml/pure.ml +++ b/ocaml/pure.ml @@ -21,7 +21,7 @@ let rec print ?(l=[]) = let lift m = let rec aux l = function - | V n -> V (if n < l then n else n+m) + | V n -> V (if n >= l then n+m else n) | A (t1,t2) -> A (aux l t1, aux l t2) | L t -> L (aux (l+1) t) | B -> B @@ -29,21 +29,22 @@ let lift m = aux 0 (* Reference implementation. - Reduction machine used below + Reduction machine used below *) let subst delift_by_one what with_what = let rec aux l = function | A(t1,t2) -> A(aux l t1, aux l t2) | V n -> - if n = what + l then + if (if what < 0 then n = what else n = what + l) then lift l with_what else V (if delift_by_one && n >= l then n-1 else n) | L t -> L (aux (l+1) t) + | B -> B in aux 0 -let rec whd = +(* let rec whd = function | A(t1, t2) -> let t2 = whd t2 in @@ -82,25 +83,46 @@ let unwind ?(tbl = Hashtbl.create 317) m = in unwind m -let mwhd m = - let rec aux = - function - | (e,A(t1,t2),s) -> - let t2' = aux (e,t2,[]) in - let (_,t,_) = t2' in - if t = B - then t2' - else aux (e,t1,t2'::s) - | (e,L t,x::s) -> aux (x::e,t,s) - | (e,V n,s) as m -> - (try - let e,t,s' = List.nth e n in - aux (e,t,s'@s) - with Failure _ -> m) - | (e, B, _) -> (e, B, []) - | (_,L _,[]) as m -> m - in - unwind (aux m) + +(* let rec print_machine (e,t,s) = + "[" ^ String.concat "," (List.map print_machine e) ^ + "|" ^ print t ^ "|" ^ + String.concat "," (List.map print_machine s) ^ "]" +;; *) + + let mwhd m = + let rec aux g = + function + (* mmm -> print_endline (print_machine mmm); match mmm with *) + | (e,A(t1,t2),s) -> + let t2' = aux g (e,t2,[]) in + let (_,t,_) = t2' in + if t = B + then t2' + else aux g (e,t1,t2'::s) + | (e,L t,x::s) -> aux g (x::e,t,s) + | (e,V n,s) as m -> + (try + let e,t,s' = List.nth e n in + aux g (e,t,s'@s) + with Invalid_argument "List.nth" | Failure _ -> m + ) + | (e, B, _) -> (e, B, []) + | (e, L t, []) -> + let t = subst true 0 (V g) t in + (* print_endline ("." ^ string_of_int g ^ " " ^ print_machine ((e,t,[]))); *) + let m' = aux (g-1) (e, t, []) in + let t' = unwind m' in + (* print_endline ("=" ^ print t'); + print_endline ("==" ^ print (lift 1 t')); *) + let t' = subst false g (V 0) (lift 1 t') in + (* print_endline ("===" ^ print t'); *) + [], (if t' = B then t' else L t'), [] + + in + unwind (aux ~-2 m) +;; + let omega should_explode = if should_explode then let f t = A(t,t) in f (L (f (V 0))) diff --git a/ocaml/util.ml b/ocaml/util.ml index a87b96f..05b9526 100644 --- a/ocaml/util.ml +++ b/ocaml/util.ml @@ -113,6 +113,7 @@ let var_of_string s = let print_name l n = if n = -1 then "*" + else if n < 0 then "c" ^ string_of_int n else if n >= List.length l then "x" ^ string_of_int (List.length l - n - 1) else List.nth l n end -- 2.39.2