From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 7 Jun 2018 16:08:10 +0000 (+0200)
Subject: Using andrea's finish instead of eat. All tests succeed.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2a95284a8f26d27ae7e1e13224d87d9774e11b06;p=fireball-separation.git

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 b2e8234..c86796e 100644
--- 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
 ;;
 
+let finish p =
+ (* one-step version of eat *)
+ 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)
+   | _ -> n
+ in aux 0 in
+print_cmd "FINISH" "";
+ (* First, a step on the last argument of the divergent.
+    Because of the sanity check, it will never be a constant term. *)
+ let div_hd, div_nargs = get_inert p.div in
+ let div_hd = match div_hd with V n -> n | _ -> assert false 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
+ (* Now, find first argument of div that is a variable never applied anywhere.
+ It must exist because of some invariant, since we just did a step,
+ and because of the arity of the divergent *)
+ let div_hd, div_nargs = get_inert p.div in
+ let div_hd = match div_hd with V n -> n | _ -> assert false in
+ let rec aux m = function
+ | A(t, V delta_var) ->
+   if delta_var <> div_hd && get_subterms_with_head delta_var p.conv = []
+   then m, delta_var
+   else aux (m-1) t
+ | A(t,_) -> aux (m-1) t
+ | _ -> 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
+ let p = {p with phase=`Two} in
+ sanity p
+;;
+
 let auto p =
  let rec aux p =
  let hd, n_args = get_inert p.div in
@@ -370,11 +408,14 @@ let auto p =
      raise (Fail(-1, "no similar terms"))
    )
   else
+    (*
     (let phase = p.phase in
      let p = eat p in
      if phase = `Two
       then problem_fail p "Auto.2 did not complete the problem"
       else aux p)
+      *)
+    problem_fail (finish p) "Finish did not complete the problem"
   in
   try
    aux p