NCicReduction.reduce_machine returns a boolean stating if the machine is in normal...

[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index bfa8fff4758db1c620b7e5cc0fd40832f113a1b0..d34e3efcc00abb6a485ecafe1de844b8ea9f902d 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -385,35 +385,26 @@ and unify test_eq_only metasenv subst context t1 t2 =
     in
     let put_in_whd m1 m2 =
       NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
-      NCicReduction.reduce_machine ~delta:max_int ~subst context m2,
-      false (* not in normal form *)
+      NCicReduction.reduce_machine ~delta:max_int ~subst context m2
     in
-    let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) = 
+    let small_delta_step 
+      ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
+    =
+     assert (not (norm1 && norm2));
+     if norm1 then
+      x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
+     else if norm2 then
+      NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
+     else 
       let h1 = height_of t1 in 
       let h2 = height_of t2 in
-      let delta = 
-        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 (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
-      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 (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', (m1 == m1' && m2 == m2') (* delta = 0 *)
+      let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
+      NCicReduction.reduce_machine ~delta ~subst context m1,
+      NCicReduction.reduce_machine ~delta ~subst context m2
     in
     let rec unif_machines metasenv subst = 
       function
-      | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),are_normal) ->
+      | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
 (*     (*D*) inside 'M'; try let rc = *)
 (*
          pp (lazy((if are_normal then "*" else " ") ^ " " ^
@@ -447,10 +438,8 @@ and unify test_eq_only metasenv subst context t1 t2 =
                    (NCicReduction.unwind (k2,e2,t2,List.rev l2))
           in
         try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
-        with UnificationFailure _ | Uncertain _ when not are_normal ->
-         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"))
+        with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
+           unif_machines metasenv subst (small_delta_step m1 m2)
 (*      (*D*)  in outside(); rc with exn -> outside (); raise exn *)
      in
      try fo_unif test_eq_only metasenv subst t1 t2