Using andrea's finish instead of eat. All tests succeed.

But again, most generated tests are solved in one step.

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index b2e8234aeb68cd2bfd36cfe7dd44f03cf49a0154..c86796e56c8d2a690787cba48f40a536c08b1232 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -340,6 +340,44 @@ print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (on " ^ string_of_int (k+1) ^
  sanity p\r
 ;;\r
 \r
+let finish p =\r
+ (* one-step version of eat *)\r
+ let compute_max_arity =\r
+   let rec aux n = function\r
+   | A(t1,t2) -> max (aux (n+1) t1) (aux 0 t2)\r
+   | L t -> max n (aux 0 t)\r
+   | _ -> n\r
+ in aux 0 in\r
+print_cmd "FINISH" "";\r
+ (* First, a step on the last argument of the divergent.\r
+    Because of the sanity check, it will never be a constant term. *)\r
+ let div_hd, div_nargs = get_inert p.div in\r
+ let div_hd = match div_hd with V n -> n | _ -> assert false in\r
+ let j = div_nargs - 1 in\r
+ let arity = compute_max_arity p.conv in\r
+ let n = 1 + arity + max\r
+  (compute_max_lambdas_at div_hd j p.div)\r
+  (compute_max_lambdas_at div_hd j p.conv) in\r
+ let p = step j n p in\r
+ (* Now, find first argument of div that is a variable never applied anywhere.\r
+ It must exist because of some invariant, since we just did a step,\r
+ and because of the arity of the divergent *)\r
+ let div_hd, div_nargs = get_inert p.div in\r
+ let div_hd = match div_hd with V n -> n | _ -> assert false in\r
+ let rec aux m = function\r
+ | A(t, V delta_var) ->\r
+   if delta_var <> div_hd && get_subterms_with_head delta_var p.conv = []\r
+   then m, delta_var\r
+   else aux (m-1) t\r
+ | A(t,_) -> aux (m-1) t\r
+ | _ -> assert false in\r
+ let m, delta_var = aux div_nargs p.div in\r
+ let p = subst_in_problem (delta_var, delta) p in\r
+ let p = subst_in_problem (div_hd, mk_lams delta (m-1)) p in\r
+ let p = {p with phase=`Two} in\r
+ sanity p\r
+;;\r
+\r
 let auto p =\r
  let rec aux p =\r
  let hd, n_args = get_inert p.div in\r
@@ -370,11 +408,14 @@ let auto p =
      raise (Fail(-1, "no similar terms"))\r
    )\r
   else\r
+    (*\r
     (let phase = p.phase in\r
      let p = eat p in\r
      if phase = `Two\r
       then problem_fail p "Auto.2 did not complete the problem"\r
       else aux p)\r
+      *)\r
+    problem_fail (finish p) "Finish did not complete the problem"\r
   in\r
   try\r
    aux p\r