not so nice patch to small_delta_step

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 0f92a18a3ff6d45d46e79cfc0765b4536c5e4a79..22c0881aa26c66160610e37fe0f1b4abce6b82c3 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -66,6 +66,7 @@ let mk_cprop n =
 
 
 let _ =
+  Sys.catch_break true;
   let do_old_logging = ref true in
   HelmLogger.register_log_callback
    (fun ?append_NL html_msg ->

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 99286591d9c2f01c0b67f5f362bccf6f4ebec482..a1a325fa541dd9c33a9ea7eb61b90f02363bc1fb 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -373,9 +373,8 @@ and unify test_eq_only metasenv subst context t1 t2 =
      | NCic.Const (Ref.Ref (_,Ref.Def h)) 
      | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h))) 
      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_) 
-     | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h, false
-     | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> 0, true
-     | _ -> 0, false
+     | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
+     | _ -> 0
     in
     let put_in_whd m1 m2 =
       NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
@@ -383,21 +382,27 @@ and unify test_eq_only metasenv subst context t1 t2 =
       false (* not in normal form *)
     in
     let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) = 
-      let h1, flex1 = height_of t1 in 
-      let h2, flex2 = height_of t2 in
+      let h1 = height_of t1 in 
+      let h2 = height_of t2 in
       let delta = 
-        if flex1 then max 0 (h2 - 1) else
-        if flex2 then max 0 (h1 - 1) else
+        if flexible [t1] then max 0 (h2 - 1) else
+        if flexible [t2] then max 0 (h1 - 1) else
         if h1 = h2 then max 0 (h1 -1) else min h1 h2 
       in
       pp ("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
-      (* if we have as heads two Fix of height n>0, they may or may not
-       * reduce, depending on their rec argument... we thus check if
-       * something changed or not. This relies on the reduction machine
-       * preserving the original machine if it performs no action *)
+      if (m1' == m1 && m2' == m2 && delta > 0) then
+         (* if we have as heads a Fix of height n>m>0 and another term of height
+          * m, we set delta = m. The Fix may or may not reduce, depending on its
+          * rec argument. if no reduction was performed we decrease delta to m-1
+          * to reduce the other term *)
+         let delta = delta - 1 in
+         pp ("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
     in
     let rec unif_machines metasenv subst = 
       function