Updated simple with current parser

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

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index efa5c25d88fd47912ed7b5d656074a1c9bc685f9..991779e7ac995f5f980a174b43c292689cac1ce6 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -287,19 +287,10 @@ 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
+\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
@@ -320,13 +311,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 +337,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 +368,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