error...

[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 16178bd3b3e8af51a21591322c6071074a75afca..11f90736a23e01ff088d54779c574c7d8dc679f6 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -129,11 +129,14 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
   in
   let ty_t = 
     try NCicTypeChecker.typeof ~subst ~metasenv context t 
-    with NCicTypeChecker.TypeCheckerFailure _ -> assert false
+    with NCicTypeChecker.TypeCheckerFailure msg -> 
+      prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
+      prerr_endline (Lazy.force msg);
+      assert false
   in
   let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
-  let ty = NCicSubstitution.subst_meta lc ty in
-  let metasenv, subst = unify test_eq_only metasenv subst context ty ty_t in
+  let lty = NCicSubstitution.subst_meta lc ty in
+  let metasenv, subst = unify test_eq_only metasenv subst context lty ty_t in
   let (metasenv, subst), t = 
     NCicMetaSubst.delift metasenv subst context n lc t
   in
@@ -154,6 +157,9 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
 
 and unify test_eq_only metasenv subst context t1 t2 =
    let fo_unif test_eq_only metasenv subst t1 t2 =
+        prerr_endline ("A " ^ 
+          NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ NCicPp.ppterm
+          ~metasenv ~subst ~context t2 );
      if t1 === t2 then
        metasenv, subst
      else
@@ -338,24 +344,30 @@ and unify test_eq_only metasenv subst context t1 t2 =
        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
        | _ -> raise (uncert_exc metasenv subst context t1 t2)
     in
-    let height_of = function
+    let height_of is_whd = function
      | 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
-     | NCic.Meta _ -> max_int
-     | _ -> 0
+     | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h, false
+     | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> max_int, true
+(*      | NCic.Rel _ -> 1, WRONG *)
+     | _ when is_whd -> 0, false
+     | _ -> max_int, false
     in
-    let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) = 
-      let h1 = height_of t1 in 
-      let h2 = height_of t2 in
+    let small_delta_step is_whd (_,_,t1,_ as m1) (_,_,t2,_ as m2) = 
+      let h1, flex1 = height_of is_whd t1 in 
+      let h2, flex2 = height_of is_whd t2 in
       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,
-      delta
+      if is_whd && flex1 && flex2 then 0 else delta
     in
     let rec unif_machines metasenv subst = function
       | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) ->
+        prerr_endline ("M(" ^ string_of_int delta^ "  " ^ 
+          NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^ 
+          " === " ^ NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind
+          m2));
         try
           let relevance = [] (* TO BE UNDERSTOOD 
             match t1 with
@@ -365,7 +377,8 @@ and unify test_eq_only metasenv subst context t1 t2 =
               try
                 let t1 = NCicReduction.from_stack t1 in
                 let t2 = NCicReduction.from_stack t2 in
-                unif_machines metasenv subst (small_delta_step t1 t2)
+                unif_machines metasenv subst 
+                  (small_delta_step true t1 t2)
               with UnificationFailure _ | Uncertain _ when not b ->
                 metasenv, subst
           in
@@ -384,16 +397,19 @@ and unify test_eq_only metasenv subst context t1 t2 =
           in
            check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
         with UnificationFailure _ | Uncertain _ when delta > 0 ->
+(*
           let delta = delta - 1 in 
           let red = NCicReduction.reduce_machine ~delta ~subst context in
-          unif_machines metasenv subst (red m1,red m2,delta)
+*)
+        prerr_endline ("RIPARTO RIDUCENDO"^string_of_int delta);
+          unif_machines metasenv subst (small_delta_step true m1 m2)
+            | exn -> prerr_endline ")"; raise exn
      in
      try fo_unif test_eq_only metasenv subst t1 t2
-     with UnificationFailure msg |Uncertain msg as exn 
-     when not (flexible [t1;t2]) -> 
+     with UnificationFailure msg | Uncertain msg as exn -> 
        try 
          unif_machines metasenv subst 
-          (small_delta_step (0,[],t1,[]) (0,[],t2,[]))
+          (small_delta_step false (0,[],t1,[]) (0,[],t2,[]))
        with 
        | UnificationFailure _ -> raise (UnificationFailure msg)
        | Uncertain _ -> raise exn