From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 13 Aug 2009 16:50:31 +0000 (+0000)
Subject: fix_sorts (cfr. previous commit) used to break too many things.
X-Git-Tag: make_still_working~3548
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d44567ba4b1a658974ee353e67c05d114c264f7f;p=helm.git

fix_sorts (cfr. previous commit) used to break too many things.
This commit is a more conservative extension...
---

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 325cd3e5f..b71413984 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -109,7 +109,9 @@ let fix_sorts swap exc t =
     | NCic.Sort (NCic.Type u) as orig ->
         if swap then
          match NCicEnvironment.sup u with
-         | None -> prerr_endline "no sup for" ; raise exc
+         | None ->
+            prerr_endline ("no sup for " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] orig) ;
+            raise exc
          | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
         else
          NCic.Sort (NCic.Type (
@@ -217,7 +219,6 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
               prerr_endline (Lazy.force msg);
               pp msg; assert false
        in
-       let ty_t = fix_sorts swap exc_to_be ty_t in 
        let lty = NCicSubstitution.subst_meta lc ty in
        match ty_t with
        | NCic.Implicit _ -> 
@@ -229,7 +230,12 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
            NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
             ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); 
           let metasenv,subst = 
-            unify test_eq_only metasenv subst context lty ty_t in
+           try
+            unify test_eq_only metasenv subst context lty ty_t
+           with NCicEnvironment.BadConstraint _ as exc ->
+            let ty_t = fix_sorts swap exc_to_be ty_t in 
+             try unify test_eq_only metasenv subst context lty ty_t
+             with _ -> raise exc in
           metasenv, subst, t
   in
          pp (lazy(string_of_int n ^ " := 111 = "^
@@ -666,3 +672,5 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
 let unify rdb ?(test_eq_only=false) = 
   indent := "";      
   unify rdb test_eq_only;;
+
+let fix_sorts = fix_sorts false (UnificationFailure (lazy "no sup"));;
diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli
index 47a59d4f2..891c0738e 100644
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -29,6 +29,9 @@ val unify :
   NCic.term -> NCic.term ->
    NCic.metasenv * NCic.substitution
 
+(* this should be moved elsewhere *)
+val fix_sorts: NCic.term -> NCic.term
+
 (* 
 exception UnificationFailure of string Lazy.t;;
 exception Uncertain of string Lazy.t;;