Make the code OCaml-4.06.1-friendly

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

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 7be80c430b9bbac484e4d8f8029f9dbd8073a5ee..8e4f61946e453827b4024dccca02d6ce8ac2f19b 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -117,6 +117,7 @@ let rec no_leading_lambdas hd_var j = function
  | V n -> if n = hd_var then j else 0\r
  | B | C _ -> 0\r
 ;;\r
+\r
 let rec subst level delift sub =\r
  function\r
  | V v -> if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)\r
@@ -246,23 +247,27 @@ let eat p =
 print_cmd "EAT" "";\r
  let var, k = get_inert p.div in\r
  let phase = p.phase in\r
- let p, t =\r
+ let p =\r
   match phase with\r
   | `One ->\r
       let n = 1 + max\r
-       (compute_max_lambdas_at var k p.div)\r
-       (compute_max_lambdas_at var k p.conv) in\r
+       (compute_max_lambdas_at var (k-1) p.div)\r
+       (compute_max_lambdas_at var (k-1) p.conv) in\r
       (* apply fresh vars *)\r
       let p, t = fold_nat (fun (p, t) _ ->\r
         let p, v = freshvar p in\r
         p, A(t, V (v + k))\r
       ) (p, V 0) n in\r
-      let p = {p with phase=`Two} in p, A(t, delta)\r
-  | `Two -> p, delta in\r
- let subst = var, mk_lams t k in\r
- let p = subst_in_problem subst p in\r
- sanity p;\r
- let p = if phase = `One then {p with div = (match p.div with A(t,_) -> t | _ -> assert false)} else p in\r
+      let p = {p with phase=`Two} in\r
+      let t = A(t, delta) in\r
+      let t = fold_nat (fun t m -> A(t, V (k-m))) t (k-1) in\r
+      let subst = var, mk_lams t k in\r
+      let p = subst_in_problem subst p in\r
+      let _, args = get_inert p.div in\r
+      {p with div = inert_cut_at (args-k) p.div}\r
+  | `Two ->\r
+      let subst = var, mk_lams delta k in\r
+      subst_in_problem subst p in\r
  sanity p\r
 ;;\r
 \r
@@ -282,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
@@ -315,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
@@ -334,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
@@ -365,30 +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 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