Fixed a performance problem with unif_machines and small_delta_step.

Previously, small_delta_step would occasionally return two machines in
normal form, with a false "are_normal" flag: this in turn caused
unif_machines to perform more steps than necessary. Now the flag returned
by small_delta_step is true iff it could not perform any reduction step;
therefore unif_machines won't try a recursive call on the new machines
(which are equal to the old ones).

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index a12ef1164dd8fbc0bf54eb03fb1c4db1860ceacf..bfa8fff4758db1c620b7e5cc0fd40832f113a1b0 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -408,8 +408,8 @@ and unify test_eq_only metasenv subst context t1 t2 =
          pp (lazy("DELTA STEP TO: " ^ string_of_int delta));
          let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in
          let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in
-         m1', m2', (m1 == m1' && m2 == m2') || delta = 0
-      else m1', m2', delta = 0
+         m1', m2', (m1 == m1' && m2 == m2') (* || delta = 0 *)
+      else m1', m2', (m1 == m1' && m2 == m2') (* delta = 0 *)
     in
     let rec unif_machines metasenv subst = 
       function
@@ -448,7 +448,9 @@ and unify test_eq_only metasenv subst context t1 t2 =
           in
         try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
         with UnificationFailure _ | Uncertain _ when not are_normal ->
-          unif_machines metasenv subst (small_delta_step m1 m2)
+         let m1,m2,normal as small = small_delta_step m1 m2 in
+           if not normal then unif_machines metasenv subst small
+           else raise (UnificationFailure (lazy "TEST x"))
 (*      (*D*)  in outside(); rc with exn -> outside (); raise exn *)
      in
      try fo_unif test_eq_only metasenv subst t1 t2