From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Wed, 8 Oct 2008 13:22:35 +0000 (+0000)
Subject: Fixed a performance problem with unif_machines and small_delta_step.
X-Git-Tag: make_still_working~4696
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=97c6371d232b0bb8d0842226d5ceabad6f4ff8bb;p=helm.git

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 a12ef1164..bfa8fff47 100644
--- 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