From e8fb6062a3c126dc242ee7bc44a696d73ca8ed76 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 2 Oct 2008 16:49:11 +0000
Subject: [PATCH] error...

---
 helm/software/components/ng_refiner/check.ml  | 13 ++++++++-
 .../components/ng_refiner/nCicUnification.ml  | 29 ++++++++++++++-----
 2 files changed, 34 insertions(+), 8 deletions(-)

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 4adff1569..1d3408d6b 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -210,9 +210,20 @@ let _ =
             NCicMetaSubst.saturate ~delta:max_int [] ctx ty 0
           in
           let ctx, ty = intros ty in
+          let ity =
+            match ity with
+            | NCic.Appl [eq;t;a;b] ->
+               NCic.Appl [eq;t;NCicReduction.whd ~delta:0 ctx a;b]
+            | t -> t
+          in
+                prerr_endline 
+                 (Printf.sprintf "%s == %s"
+                 (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity)
+                 (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx sty));
           let metasenv, subst = 
             try 
-              NCicUnification.unify menv [] ctx ity sty
+                    prerr_endline ("INIZIO: " ^ NUri.string_of_uri u);
+              NCicUnification.unify menv [] ctx ity sty 
             with
             | NCicUnification.Uncertain msg 
             | NCicUnification.UnificationFailure msg 
diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index cf8f48053..11f90736a 100644
--- 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
@@ -344,9 +350,9 @@ and unify test_eq_only metasenv subst context t1 t2 =
      | 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 _ :: _) -> max_int, true
+(*      | NCic.Rel _ -> 1, WRONG *)
      | _ when is_whd -> 0, false
-     | _ -> 0, false (* !!! with max_int we diverge, with 0 we may do too much
-     reduction *)
+     | _ -> max_int, false
     in
     let small_delta_step is_whd (_,_,t1,_ as m1) (_,_,t2,_ as m2) = 
       let h1, flex1 = height_of is_whd t1 in 
@@ -358,6 +364,10 @@ and unify test_eq_only metasenv subst context t1 t2 =
     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
@@ -367,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 true t1 t2)
+                unif_machines metasenv subst 
+                  (small_delta_step true t1 t2)
               with UnificationFailure _ | Uncertain _ when not b ->
                 metasenv, subst
           in
@@ -386,9 +397,13 @@ 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 -> 
-- 
2.39.2