X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fsimple.ml;h=8e4f61946e453827b4024dccca02d6ce8ac2f19b;hb=428691717031468f6583a899fe8edbe58163428a;hp=efa5c25d88fd47912ed7b5d656074a1c9bc685f9;hpb=3ba5ecfc8372d4c9f380bad5cdf7387f2bbcea6a;p=fireball-separation.git

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