From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 7 Jun 2018 08:18:42 +0000 (+0200)
Subject: Replaced eat with andrea's finish
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4d85faf22614fae57d4b0c45a5699258a9274272;p=fireball-separation.git

Replaced eat with andrea's finish
(fixes examples failing for measure)
---

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 27d0119..4e93965 100644
--- 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
 ;;
 
+let finish p =
+ let compute_max_arity =
+   let rec aux n = function
+   | A(_,t1,t2) -> max (aux (n+1) t1) (aux 0 t2)
+   | L(_,t) -> max n (aux 0 t)
+   | V _ -> n
+ in aux 0 in
+print_cmd "FINISH" "";
+ let div_hd, div_nargs = get_inert p.div in
+ let j = div_nargs - 1 in
+ let arity = compute_max_arity p.conv in
+ let n = 1 + arity + max
+  (compute_max_lambdas_at div_hd j p.div)
+  (compute_max_lambdas_at div_hd j p.conv) in
+ let p = step j n p in
+ let div_hd, div_nargs = get_inert p.div in
+ let rec aux m = function
+  A(_,t1,t2) -> if is_var t2 then
+   (let delta_var, _ = get_inert t2 in
+     if delta_var <> div_hd && get_subterm_with_head_and_args delta_var 1 p.conv = None
+      then m, delta_var
+      else aux (m-1) t1) else aux (m-1) t1
+  | _ -> assert false in
+ let m, delta_var = aux div_nargs p.div in
+ let p = subst_in_problem (delta_var, delta) p in
+ let p = subst_in_problem (div_hd, mk_lams delta (m-1)) p in
+ sanity p
+;;
+
 let rec auto p =
  let hd_var, n_args = get_inert p.div in
  match get_subterm_with_head_and_args hd_var n_args p.conv with
  | None ->
+   (try problem_fail (finish p) "Auto.2 did not complete the problem"
+   with Done sigma -> sigma)
+   (*
    (try
     let phase = p.phase in
      let p = eat p in
@@ -302,6 +334,7 @@ let rec auto p =
       then problem_fail p "Auto.2 did not complete the problem"
       else auto p
     with Done sigma -> sigma)
+    *)
  | Some t ->
   let j = find_eta_difference p t n_args in
   let k = 1 + max