From 62d2aea15e05a7366e0bbdc71574ad50cda28ff5 Mon Sep 17 00:00:00 2001 From: acondolu Date: Thu, 31 May 2018 15:32:01 +0200 Subject: [PATCH] Clean up, improve comments, move functions `run' is the new entrypoint in simple.ml --- ocaml/simple.ml | 95 +++++++++++++++++--------------------------- ocaml/simple.mli | 5 ++- ocaml/simple_test.ml | 2 +- 3 files changed, 41 insertions(+), 61 deletions(-) diff --git a/ocaml/simple.ml b/ocaml/simple.ml index d9bc389..2860325 100644 --- a/ocaml/simple.ml +++ b/ocaml/simple.ml @@ -38,7 +38,7 @@ let eta_subterm u = in aux 0 ;; -(* does NOT lift t *) +(* does NOT lift the argument *) let mk_lams = fold_nat (fun x _ -> L x) ;; let string_of_t = @@ -217,7 +217,7 @@ let find_eta_difference p t n_args = let rec aux t u k = match t, u with | V _, V _ -> assert false (* div subterm of conv *) | A(t1,t2), A(u1,u2) -> - if not (eta_eq t2 u2) then (print_endline((string_of_t t2) ^ " <> " ^ (string_of_t u2)); k) + if not (eta_eq t2 u2) then ((*print_endline((string_of_t t2) ^ " <> " ^ (string_of_t u2));*) k) else aux t1 u1 (k-1) | _, _ -> assert false in aux p.div t n_args @@ -295,23 +295,6 @@ let parse strs = (List.map (aux 0) tms, free) ;; -let problem_of div conv = - print_hline (); - let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in - let varno = List.length var_names in - let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in - (* initial sanity check *) - sanity p -;; - -let exec div conv cmds = - let p = problem_of div conv in - try - problem_fail (List.fold_left (|>) p cmds) "Problem not completed" - with - | Done _ -> () -;; - let rec auto p = let hd_var, n_args = get_inert p.div in match get_subterm_with_head_and_args hd_var n_args p.conv with @@ -332,7 +315,30 @@ let rec auto p = auto p ;; -let interactive div conv cmds = +let problem_of div convs = + let rec conv_join = function + | [] -> "@" + | x::xs -> conv_join xs ^ " ("^ x ^")" in + print_hline (); + let conv = conv_join convs in + let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in + let varno = List.length var_names in + let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in + (* initial sanity check *) + sanity p +;; + +let solve p = + if eta_subterm p.div p.conv + then print_endline "!!! div is subterm of conv. Problem was not run !!!" + else check p (auto p) +;; + +let run x y = solve (problem_of x y);; + +(* Example usage of interactive: *) + +(* let interactive div conv cmds = let p = problem_of div conv in try ( let p = List.fold_left (|>) p cmds in @@ -354,40 +360,19 @@ let interactive div conv cmds = | Done _ -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds) in f p [] ) with Done _ -> () -;; - -let rec conv_join = function - | [] -> "@" - | x::xs -> conv_join xs ^ " ("^ x ^")" -;; - -let auto' a b = - let p = problem_of a (conv_join b) in - let sigma = auto p in - check p sigma -;; - -(* Example usage of exec, interactive: +;; *) -exec - "x x" - (conv_join["x y"; "y y"; "y x"]) - [ step 0 1; eat ] -;; - -interactive "x y" +(* interactive "x y" "@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat] -;; +;; *) -*) +run "x x" ["x y"; "y y"; "y x"] ;; +run "x y" ["x (_. x)"; "y z"; "y x"] ;; +run "a (x. x b) (x. x c)" ["a (x. b b) @"; "a @ c"; "a (x. x x) a"; "a (a a a) (a c c)"] ;; -auto' "x x" ["x y"; "y y"; "y x"] ;; -auto' "x y" ["x (_. x)"; "y z"; "y x"] ;; -auto' "a (x. x b) (x. x c)" ["a (x. b b) @"; "a @ c"; "a (x. x x) a"; "a (a a a) (a c c)"] ;; +run "x (y. x y y)" ["x (y. x y x)"] ;; -auto' "x (y. x y y)" ["x (y. x y x)"] ;; - -auto' "x a a a a" [ +run "x a a a a" [ "x b a a a"; "x a b a a"; "x a a b a"; @@ -395,18 +380,10 @@ auto' "x a a a a" [ ] ;; (* Controesempio ad usare un conto dei lambda che non considere le permutazioni *) -auto' "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [ +run "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [ "x a a a a (_. a) b b b"; "x a a a a (_. _. _. _. x. y. x y)"; ] ;; - print_hline(); -print_endline "ALL DONE. " - -let solve div convs = - let p = problem_of div (conv_join convs) in - if eta_subterm p.div p.conv - then print_endline "!!! div is subterm of conv. Problem was not run !!!" - else check p (auto p) -;; +print_endline ">>> EXAMPLES IN simple.ml FINISHED <<<" diff --git a/ocaml/simple.mli b/ocaml/simple.mli index d914117..216e381 100644 --- a/ocaml/simple.mli +++ b/ocaml/simple.mli @@ -1 +1,4 @@ -val solve : string -> string list -> unit +(* type problem +val problem_of : string -> string list -> problem +val solve : problem -> unit *) +val run : string -> string list -> unit diff --git a/ocaml/simple_test.ml b/ocaml/simple_test.ml index 9618113..b766a52 100644 --- a/ocaml/simple_test.ml +++ b/ocaml/simple_test.ml @@ -43,7 +43,7 @@ let main = repeat (fun _ -> let div, convs = gen complex vars in - Simple.solve div convs + Simple.run div convs ) num ; prerr_endline "\n---- ALL TESTS COMPLETED ----" -- 2.39.2