- A new interesting elimination principle over inductively generated topologies:

[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 202e68e4c86c3d056a8914451a70b6c4b25aae13..d5cf3892270f3c05c81c9d4decb82e268c0b65cf 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -85,7 +85,8 @@ let fix_sorts swap metasenv subst context meta t =
     | NCic.Sort (NCic.Type u) as orig ->
         if swap then
          match NCicEnvironment.sup u with
-         | None ->  raise (fail_exc metasenv subst context meta t)
+         | None -> prerr_endline "no sup for" ;
+            raise (fail_exc metasenv subst context meta t)
          | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
         else
          NCic.Sort (NCic.Type (
@@ -161,6 +162,8 @@ and beta_expand_many test_equality_only swap metasenv subst context t args =
 
 and instantiate test_eq_only metasenv subst context n lc t swap =
  (*D*)  inside 'I'; try let rc =  
+         pp (lazy(string_of_int n ^ " :=?= "^
+           NCicPp.ppterm ~metasenv ~subst ~context t));
   let unify test_eq_only m s c t1 t2 = 
     if swap then unify test_eq_only m s c t2 t1 
     else unify test_eq_only m s c t1 t2
@@ -169,23 +172,38 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
   let metasenv, subst, t = 
     match ty with 
     | NCic.Implicit (`Typeof _) -> 
-       metasenv,subst,fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t
+       metasenv,subst, t
+         (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *)
     | _ ->
-       pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
+       pp (lazy (
+         "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^
+          NCicPp.ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^
+          NCicPp.ppmetasenv ~subst metasenv));
        let t, ty_t = 
          try t, NCicTypeChecker.typeof ~subst ~metasenv context t 
-         with NCicTypeChecker.TypeCheckerFailure _ -> 
+         with 
+         | NCicTypeChecker.AssertFailure msg -> 
+           (pp (lazy "fine typeof (fallimento)");
            let ft = 
             fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t
            in
-           if ft == t then assert false
+           if ft == t then 
+             (prerr_endline ( ("ILLTYPED: " ^ 
+                NCicPp.ppterm ~metasenv ~subst ~context t
+            ^ "\nBECAUSE:" ^ Lazy.force msg ^ "\nCONTEXT:\n" ^
+            NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^
+            NCicPp.ppmetasenv ~subst metasenv
+            ));
+                     assert false)
            else
             try 
               pp (lazy ("typeof: " ^ 
                 NCicPp.ppterm ~metasenv ~subst ~context ft));
               ft, NCicTypeChecker.typeof ~subst ~metasenv context ft 
-            with NCicTypeChecker.TypeCheckerFailure _ -> 
-              assert false
+            with NCicTypeChecker.AssertFailure _ -> 
+              assert false)
+         | NCicTypeChecker.TypeCheckerFailure msg ->
+              pp msg; assert false
        in
        let lty = NCicSubstitution.subst_meta lc ty in
        pp (lazy("On the types: " ^
@@ -195,11 +213,22 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
        let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
        metasenv, subst, t
   in
+         pp (lazy(string_of_int n ^ " := 111 = "^
+           NCicPp.ppterm ~metasenv ~subst ~context t));
   let (metasenv, subst), t = 
     try NCicMetaSubst.delift metasenv subst context n lc t
-    with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg)
-    |    NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg)
+    with NCicMetaSubst.Uncertain msg -> 
+         pp (lazy ("delift fails: " ^ Lazy.force msg));
+         raise (Uncertain msg)
+    | NCicMetaSubst.MetaSubstFailure msg -> 
+         pp (lazy ("delift fails: " ^ Lazy.force msg));
+         raise (UnificationFailure msg)
   in
+         pp (lazy(string_of_int n ^ " := 222 = "^
+           NCicPp.ppterm ~metasenv ~subst ~context:ctx t
+         ^ "\n" ^ NCicPp.ppmetasenv ~subst metasenv
+         
+         ));
   (* Unifying the types may have already instantiated n. *)
   try
     let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
@@ -266,10 +295,12 @@ and unify test_eq_only metasenv subst context t1 t2 =
                   metasenv, subst, i::to_restrict, i-1)
              l1 l2 (metasenv, subst, [], List.length l1)
            in
-           let metasenv, subst, _ = 
-             NCicMetaSubst.restrict metasenv subst n1 to_restrict
-           in
-             metasenv, subst
+           if to_restrict <> [] then
+             let metasenv, subst, _ = 
+               NCicMetaSubst.restrict metasenv subst n1 to_restrict
+             in
+               metasenv, subst
+           else metasenv, subst
           with 
            | Invalid_argument _ -> assert false
            | NCicMetaSubst.MetaSubstFailure msg ->