Simplified divergent problem

[fireball-separation.git] / ocaml / simple.ml

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index efa5c25d88fd47912ed7b5d656074a1c9bc685f9..8e4f61946e453827b4024dccca02d6ce8ac2f19b 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -287,18 +287,6 @@ print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")")
  let p = subst_in_problem subst p in\r
  sanity p\r
 ;;\r
-;;\r
-\r
-let parse strs =\r
-  let rec aux level = function\r
-  | Parser_andrea.Lam t -> L (aux (level + 1) t)\r
-  | Parser_andrea.App (t1, t2) ->\r
-   if level = 0 then mk_app (aux level t1) (aux level t2)\r
-    else A(aux level t1, aux level t2)\r
-  | Parser_andrea.Var v -> V v in\r
-  let (tms, free) = Parser_andrea.parse_many strs in\r
-  (List.map (aux 0) tms, free)\r
-;;\r
 \r
 let rec auto p =\r
  let hd_var, n_args = get_inert p.div in\r
@@ -320,13 +308,20 @@ let rec auto p =
   auto p\r
 ;;\r
 \r
-let problem_of div convs =\r
- let rec conv_join = function\r
-  | [] -> "@"\r
-  | x::xs -> conv_join xs ^ " ("^ x ^")" in\r
+let problem_of (label, div, convs, ps, var_names) =\r
  print_hline ();\r
- let conv = conv_join convs in\r
- let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in\r
+ let rec aux = function\r
+ | `Lam(_, t) -> L (aux t)\r
+ | `I ((v,_), args) -> Listx.fold_left (fun x y -> mk_app x (aux y)) (V v) args\r
+ | `Var(v,_) -> V v\r
+ | `N _ | `Match _ -> assert false in\r
+ assert (List.length ps = 0);\r
+ let convs = List.rev convs in\r
+ let conv = List.fold_left (fun x y -> mk_app x (aux (y :> Num.nf))) (V (List.length var_names)) convs in\r
+ let var_names = "@" :: var_names in\r
+ let div = match div with\r
+ | Some div -> aux (div :> Num.nf)\r
+ | None -> assert false 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
@@ -339,7 +334,7 @@ let solve p =
   else check p (auto p)\r
 ;;\r
 \r
-let run x y = solve (problem_of x y);;\r
+Problems.main (solve ++ problem_of);\r
 \r
 (* Example usage of interactive: *)\r
 \r
@@ -370,37 +365,3 @@ let run x y = solve (problem_of x y);;
 (* interactive "x y"\r
  "@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat]\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
-run "x (y. x y y)" ["x (y. x y x)"] ;;\r
-\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
- "x a a a b";\r
-] ;;\r
-\r
-(* Controesempio ad usare un conto dei lambda che non considere le permutazioni *)\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
-(* bug in eat that was erasing terms in convergent that then diverged *)\r
-run "x y z"\r
-[\r
-"x @ @";\r
-"z (y @ (y @))"\r
-] ;;\r
-\r
-(* bug in no_leading_lambdas where x in j-th position *)\r
-run "v0 (v1 v2) (x. y. v0 v3 v4 v2)"\r
-["v5 (v6 (x. v6) v7 v8 (x. v9) (x. v9 (v10 v10))) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y))) (v9 (x. v11) (v4 v8) (x. y. z. v12) (v4 v6 (x. v7 v11) v12) (x. x v8)) (v0 v3 v4 v9 (v7 v11) (v0 v3 v4 v2) v10) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y)) (v9 (x. v11) (v4 v8)))"]\r
-;;\r
-\r
-print_hline();\r
-print_endline ">>> EXAMPLES IN simple.ml FINISHED <<<"\r