Replaced eat with andrea's finish

(fixes examples failing for measure)

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 27d0119e58c505ba6918f43a02bf3bad879d8015..4e93965e029a606419b3984a2af9e36d4792b5f8 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -291,10 +291,42 @@ print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")")
  sanity p\r
 ;;\r
 \r
+let finish p =\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
+   | V _ -> n\r
+ in aux 0 in\r
+print_cmd "FINISH" "";\r
+ let div_hd, div_nargs = get_inert p.div 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
+ let div_hd, div_nargs = get_inert p.div in\r
+ let rec aux m = function\r
+  A(_,t1,t2) -> if is_var t2 then\r
+   (let delta_var, _ = get_inert t2 in\r
+     if delta_var <> div_hd && get_subterm_with_head_and_args delta_var 1 p.conv = None\r
+      then m, delta_var\r
+      else aux (m-1) t1) else aux (m-1) t1\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
+ sanity p\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
  | None ->\r
+   (try problem_fail (finish p) "Auto.2 did not complete the problem"\r
+   with Done sigma -> sigma)\r
+   (*\r
    (try\r
     let phase = p.phase in\r
      let p = eat p in\r
@@ -302,6 +334,7 @@ let rec auto p =
       then problem_fail p "Auto.2 did not complete the problem"\r
       else auto p\r
     with Done sigma -> sigma)\r
+    *)\r
  | Some t ->\r
   let j = find_eta_difference p t n_args in\r
   let k = 1 + max\r