From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 2 Feb 2007 18:15:59 +0000 (+0000)
Subject: Serious bug fixed: the types of a real mutual fix definition were not lifted
X-Git-Tag: 0.4.95@7852~630
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0ffad67d97b1495a4444e2cf2dbd82f882ed15e9;p=helm.git

Serious bug fixed: the types of a real mutual fix definition were not lifted
as required. Moreover, an unification exception used to escape the refiner.
Now it does no more, but the error is not localized (being about the branch
of a MutCase that has no precise localization).
---

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 6d26a868b..120fed3eb 100644
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -509,7 +509,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               in
                 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
         | C.Lambda (n,s,t) ->
-
             let s',sort1,subst',metasenv',ugraph1 = 
               type_of_aux subst metasenv context s ugraph in
             let s',sort1,subst',metasenv',ugraph1 =
@@ -721,8 +720,21 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                     type_of_aux subst metasenv context constructor ugraph1 
                   in
                   let outtypeinstance,subst,metasenv,ugraph3 =
-                    check_branch 0 context metasenv subst no_left_params 
-                      actual_type constructor' expected_type ugraph2 
+                   try
+                    check_branch 0 context metasenv subst
+                     no_left_params actual_type constructor' expected_type
+                     ugraph2 
+                   with
+                    exn ->
+                     enrich localization_tbl constructor'
+                      ~f:(fun _ ->
+                        lazy ("The term " ^
+                         CicMetaSubst.ppterm_in_context metasenv subst p'
+                          context ^ " has type " ^
+                         CicMetaSubst.ppterm_in_context metasenv subst actual_type
+                          context ^ " but is here used with type " ^
+                         CicMetaSubst.ppterm_in_context metasenv subst expected_type
+                          context)) exn
                   in
                     (p'::pl,j-1,
                      outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
@@ -919,17 +931,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                    (C.Appl(outtype::right_args@[term]))),
                  subst,metasenv,ugraph6)
         | C.Fix (i,fl) ->
-            let fl_ty',subst,metasenv,types,ugraph1 =
+            let fl_ty',subst,metasenv,types,ugraph1,len =
               List.fold_left
-                (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
+                (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
                    let ty',_,subst',metasenv',ugraph1 = 
                       type_of_aux subst metasenv context ty ugraph 
                    in
                      fl @ [ty'],subst',metasenv', 
-                       Some (C.Name n,(C.Decl ty')) :: types, ugraph
-                ) ([],subst,metasenv,[],ugraph) fl
+                       Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
+                        :: types, ugraph, len+1
+                ) ([],subst,metasenv,[],ugraph,0) fl
             in
-            let len = List.length types in
             let context' = types@context in
             let fl_bo',subst,metasenv,ugraph2 =
               List.fold_left
@@ -972,17 +984,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
             in
               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
         | C.CoFix (i,fl) ->
-            let fl_ty',subst,metasenv,types,ugraph1 =
+            let fl_ty',subst,metasenv,types,ugraph1,len =
               List.fold_left
-                (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
+                (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
                    let ty',_,subst',metasenv',ugraph1 = 
                      type_of_aux subst metasenv context ty ugraph 
                    in
                      fl @ [ty'],subst',metasenv', 
-                       Some (C.Name n,(C.Decl ty')) :: types, ugraph1
-                ) ([],subst,metasenv,[],ugraph) fl
+                      Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
+                        types, ugraph1, len+1
+                ) ([],subst,metasenv,[],ugraph,0) fl
             in
-            let len = List.length types in
             let context' = types@context in
             let fl_bo',subst,metasenv,ugraph2 =
               List.fold_left