From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 31 May 2018 13:32:01 +0000 (+0200)
Subject: Clean up, improve comments, move functions
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=62d2aea15e05a7366e0bbdc71574ad50cda28ff5;p=fireball-separation.git

Clean up, improve comments, move functions

`run' is the new entrypoint in simple.ml
---

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 ----"