From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 19 Jun 2002 10:43:42 +0000 (+0000)
Subject: Coscoy double inner types now available also for Meta arguments.
X-Git-Tag: V_0_3_0_debian_8~31
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cef3f6e2e971c3a6fb313b1c9541501f9be8f421;p=helm.git

Coscoy double inner types now available also for Meta arguments.
---

diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml
index f58c554fb..b06619c4d 100644
--- a/helm/gTopLevel/doubleTypeInference.ml
+++ b/helm/gTopLevel/doubleTypeInference.ml
@@ -256,18 +256,46 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
      | C.Var uri -> type_of_variable uri
      | C.Meta (n,l) -> 
         (* Let's visit all the subterms that will not be visited later *)
-        let _ =
-         List.iter
-          (function
-              None -> ()
-            | Some t -> ignore (type_of_aux context t None)
-          ) l
+        let (_,canonical_context,_) =
+         List.find (function (m,_,_) -> n = m) metasenv
         in
-         let (_,canonical_context,ty) =
-          List.find (function (m,_,_) -> n = m) metasenv
+         let lifted_canonical_context =
+          let rec aux i =
+           function
+              [] -> []
+            | (Some (n,C.Decl t))::tl ->
+               (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+            | (Some (n,C.Def t))::tl ->
+               (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+            | None::tl -> None::(aux (i+1) tl)
+          in
+           aux 1 canonical_context
          in
-          (* Checks suppressed *)
-          CicSubstitution.lift_meta l ty
+          let _ =
+           List.iter2
+            (fun t ct ->
+              match t,ct with
+                 _,None -> ()
+               | Some t,Some (_,C.Def ct) ->
+                  let expected_type =
+                   R.whd context
+                    (CicTypeChecker.type_of_aux' metasenv context ct)
+                  in
+                   (* Maybe I am a bit too paranoid, because   *)
+                   (* if the term is well-typed than t and ct  *)
+                   (* are convertible. Nevertheless, I compute *)
+                   (* the expected type.                       *)
+                   ignore (type_of_aux context t (Some expected_type))
+               | Some t,Some (_,C.Decl ct) ->
+                  ignore (type_of_aux context t (Some ct))
+               | _,_ -> assert false (* the term is not well typed!!! *)
+            ) l lifted_canonical_context
+          in
+           let (_,canonical_context,ty) =
+            List.find (function (m,_,_) -> n = m) metasenv
+           in
+            (* Checks suppressed *)
+            CicSubstitution.lift_meta l ty
      | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
      | C.Implicit -> raise (Impossible 21)
      | C.Cast (te,ty) ->