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 d9bc38917910db68afe1c226d3ae153e85a4e4b4..28603258c04539410f98afb02d2ac301f97c793c 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -38,7 +38,7 @@ let eta_subterm u =
  in aux 0\r
 ;;\r
 \r
-(* does NOT lift t *)\r
+(* does NOT lift the argument *)\r
 let mk_lams = fold_nat (fun x _ -> L x) ;;\r
 \r
 let string_of_t =\r
@@ -217,7 +217,7 @@ let find_eta_difference p t n_args =
  let rec aux t u k = match t, u with\r
  | V _, V _ -> assert false (* div subterm of conv *)\r
  | A(t1,t2), A(u1,u2) ->\r
-    if not (eta_eq t2 u2) then (print_endline((string_of_t t2) ^ " <> " ^ (string_of_t u2)); k)\r
+    if not (eta_eq t2 u2) then ((*print_endline((string_of_t t2) ^ " <> " ^ (string_of_t u2));*) k)\r
     else aux t1 u1 (k-1)\r
  | _, _ -> assert false\r
  in aux p.div t n_args\r
@@ -295,23 +295,6 @@ let parse strs =
   (List.map (aux 0) tms, free)\r
 ;;\r
 \r
-let problem_of div conv =\r
- print_hline ();\r
- let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in\r
- let varno = List.length var_names in\r
- let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in\r
- (* initial sanity check *)\r
- sanity p\r
-;;\r
-\r
-let exec div conv cmds =\r
- let p = problem_of div conv in\r
- try\r
-  problem_fail (List.fold_left (|>) p cmds) "Problem not completed"\r
- with\r
- | Done _ -> ()\r
-;;\r
-\r
 let rec auto p =\r
  let hd_var, n_args = get_inert p.div in\r
  match get_subterm_with_head_and_args hd_var n_args p.conv with\r
@@ -332,7 +315,30 @@ let rec auto p =
   auto p\r
 ;;\r
 \r
-let interactive div conv cmds =\r
+let problem_of div convs =\r
+ let rec conv_join = function\r
+  | [] -> "@"\r
+  | x::xs -> conv_join xs ^ " ("^ x ^")" in\r
+ print_hline ();\r
+ let conv = conv_join convs in\r
+ let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in\r
+ let varno = List.length var_names in\r
+ let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in\r
+ (* initial sanity check *)\r
+ sanity p\r
+;;\r
+\r
+let solve p =\r
+ if eta_subterm p.div p.conv\r
+  then print_endline "!!! div is subterm of conv. Problem was not run !!!"\r
+  else check p (auto p)\r
+;;\r
+\r
+let run x y = solve (problem_of x y);;\r
+\r
+(* Example usage of interactive: *)\r
+\r
+(* let interactive div conv cmds =\r
  let p = problem_of div conv in\r
  try (\r
  let p = List.fold_left (|>) p cmds in\r
@@ -354,40 +360,19 @@ let interactive div conv cmds =
   | Done _ -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds)\r
  in f p []\r
  ) with Done _ -> ()\r
-;;\r
-\r
-let rec conv_join = function\r
- | [] -> "@"\r
- | x::xs -> conv_join xs ^ " ("^ x ^")"\r
-;;\r
-\r
-let auto' a b =\r
- let p = problem_of a (conv_join b) in\r
- let sigma = auto p in\r
- check p sigma\r
-;;\r
-\r
-(* Example usage of exec, interactive:\r
+;; *)\r
 \r
-exec\r
- "x x"\r
- (conv_join["x y"; "y y"; "y x"])\r
- [ step 0 1; eat ]\r
-;;\r
-\r
-interactive "x y"\r
+(* interactive "x y"\r
  "@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat]\r
-;;\r
+;; *)\r
 \r
-*)\r
+run "x x" ["x y"; "y y"; "y x"] ;;\r
+run "x y" ["x (_. x)"; "y z"; "y x"] ;;\r
+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)"] ;;\r
 \r
-auto' "x x" ["x y"; "y y"; "y x"] ;;\r
-auto' "x y" ["x (_. x)"; "y z"; "y x"] ;;\r
-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)"] ;;\r
+run "x (y. x y y)" ["x (y. x y x)"] ;;\r
 \r
-auto' "x (y. x y y)" ["x (y. x y x)"] ;;\r
-\r
-auto' "x a a a a" [\r
+run "x a a a a" [\r
  "x b a a a";\r
  "x a b a a";\r
  "x a a b a";\r
@@ -395,18 +380,10 @@ auto' "x a a a a" [
 ] ;;\r
 \r
 (* Controesempio ad usare un conto dei lambda che non considere le permutazioni *)\r
-auto' "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [\r
+run "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [\r
  "x a a a a (_. a) b b b";\r
  "x a a a a (_. _. _. _. x. y. x y)";\r
 ] ;;\r
 \r
-\r
 print_hline();\r
-print_endline "ALL DONE. "\r
-\r
-let solve div convs =\r
- let p = problem_of div (conv_join convs) in\r
- if eta_subterm p.div p.conv\r
-  then print_endline "!!! div is subterm of conv. Problem was not run !!!"\r
-  else check p (auto p)\r
-;;\r
+print_endline ">>> EXAMPLES IN simple.ml FINISHED <<<"\r

diff --git a/ocaml/simple.mli b/ocaml/simple.mli
index d914117dd2e2089688ee7c6b2656b86981a902f2..216e3810bb241679aa43734ceb38bade28b3fd7b 100644 (file)
--- a/ocaml/simple.mli
+++ b/ocaml/simple.mli
@@ -1 +1,4 @@
-val solve : string -> string list -> unit\r
+(* type problem\r
+val problem_of : string -> string list -> problem\r
+val solve : problem -> unit *)\r
+val run : string -> string list -> unit\r

diff --git a/ocaml/simple_test.ml b/ocaml/simple_test.ml
index 9618113794f6c7ad9c25982ee67924b947c755a4..b766a5298085b053094f5766c04806998a6c4923 100644 (file)
--- 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 ----"