From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 2 Feb 2004 16:38:21 +0000 (+0000)
Subject: - big hack: keep on unifying/refining when SortExpectedMetaFound
X-Git-Tag: V_0_2_3~110
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2f4e2076f4b53f0c3e277bff67268cb80bfae967;p=helm.git

- big hack: keep on unifying/refining when SortExpectedMetaFound
  exception is encountered
---

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 704eecb46..59ccc9ae9 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -33,7 +33,8 @@ let debug_print = prerr_endline
 let type_of_aux' metasenv subst context term =
   try
     CicMetaSubst.type_of_aux' metasenv subst context term
-  with CicMetaSubst.MetaSubstFailure msg ->
+  with
+  | CicMetaSubst.MetaSubstFailure msg ->
     raise (AssertFailure
       ((sprintf
         "Type checking error: %s in context\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
@@ -66,7 +67,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
                 (* First possibility:  restriction    *)
                 (* Second possibility: unification    *)
                 (* Third possibility:  convertibility *)
-                R.are_convertible metasenv subst context t1' t2'
+                R.are_convertible subst context t1' t2'
          ) true ln lm
        in
         if ok then
@@ -79,18 +80,31 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
        fo_unif_subst subst context metasenv t2 t1
    | (C.Meta (n,l), t)   
    | (t, C.Meta (n,l)) ->
-       let subst',metasenv' =
+       let subst'',metasenv' =
         try
          let oldt = (List.assoc n subst) in
          let lifted_oldt = S.lift_meta l oldt in
           fo_unif_subst subst context metasenv lifted_oldt t
         with Not_found ->
-         let t',metasenv' = CicMetaSubst.delift n subst context metasenv l t in
-          (n, t')::subst, metasenv'
+         let t',metasenv',subst' =
+           CicMetaSubst.delift n subst context metasenv l t
+         in
+          (n, t')::subst', metasenv'
        in
         let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv' in
-        let tyt = type_of_aux' metasenv' subst' context t in
-         fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
+        (try
+          let tyt =
+            type_of_aux' metasenv' subst'' context t
+          in
+           fo_unif_subst subst'' context metasenv' (S.lift_meta l meta_type) tyt
+        with CicTypeChecker.SortExpectedMetaFound _ ->
+          (* TODO huge hack!!!!
+           * we keep on unifying/refining in the hope that the problem will be
+           * eventually solved. In the meantime we're breaking a big invariant:
+           * the terms that we are unifying are no longer well typed in the
+           * current context (in the worst case we could even diverge)
+           *)
+          (subst'', metasenv'))
    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
       if UriManager.eq uri1 uri2 then
@@ -164,14 +178,14 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
    | (C.MutConstruct _, _) | (_, C.MutConstruct _)
    | (C.Fix _, _) | (_, C.Fix _) 
    | (C.CoFix _, _) | (_, C.CoFix _) -> 
-       if R.are_convertible metasenv subst context t1 t2 then
+       if R.are_convertible subst context t1 t2 then
         subst, metasenv
        else
         raise (UnificationFailure (sprintf
           "Can't unify %s with %s because they are not convertible"
           (CicPp.ppterm t1) (CicPp.ppterm t2)))
    | (_,_) ->
-       if R.are_convertible metasenv subst context t1 t2 then
+       if R.are_convertible subst context t1 t2 then
         subst, metasenv
        else
         raise (UnificationFailure (sprintf
@@ -200,10 +214,7 @@ debug_print ("@@@: " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst1)) ^
 (* a new substitution which is already unwinded and ready to be applied and  *)
 (* a new metasenv in which some hypothesis in the contexts of the            *)
 (* metavariables may have been restricted.                                   *)
-let fo_unif metasenv context t1 t2 =
- let subst_to_unwind,metasenv' = fo_unif_subst [] context metasenv t1 t2 in
-  CicMetaSubst.unwind_subst metasenv' subst_to_unwind
-;;
+let fo_unif metasenv context t1 t2 = fo_unif_subst [] context metasenv t1 t2 ;;
 
 let fo_unif_subst subst context metasenv t1 t2 =
   let enrich_msg msg =
@@ -217,7 +228,7 @@ let fo_unif_subst subst context metasenv t1 t2 =
         CicPp.ppterm (type_of_aux' metasenv subst context t2)
       with _ -> "MALFORMED")
       (CicMetaSubst.ppcontext subst context)
-      (CicMetaSubst.ppmetasenv subst metasenv) msg
+      (CicMetaSubst.ppmetasenv metasenv subst) msg
   in
   try
     fo_unif_subst subst context metasenv t1 t2