X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FdoubleTypeInference.ml;h=b06619c4ddf74d98929420761a7d3a61e34119c5;hb=5a369548a2f04fb59b5cbb94526325aae9bf415a;hp=b9a79b64ff74b0ec71eb80e54e8024a224a6984c;hpb=7e60b896247a228beea1b2a547c1f606e1834921;p=helm.git

diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml
index b9a79b64f..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) ->
@@ -308,19 +336,24 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          (* Checks suppressed *)
          C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t None)
      | C.Appl (he::tl) when List.length tl > 0 ->
-        let hetype = type_of_aux context he None in
-        let tlbody_and_type =
-         let rec aux =
-          function
-             _,[] -> []
-           | C.Prod (n,s,t),he::tl ->
-              (he, type_of_aux context he (Some (head_beta_reduce s)))::
-               (aux (R.whd context (S.subst he t), tl))
-           | _ -> assert false
-         in
-          aux (R.whd context hetype, tl)
+        let expected_hetype =
+         (* Inefficient, the head is computed twice. But I know *)
+         (* of no other solution.                               *)
+         R.whd context (CicTypeChecker.type_of_aux' metasenv context he)
         in
-         eat_prods context hetype tlbody_and_type
+         let hetype = type_of_aux context he (Some expected_hetype) in
+         let tlbody_and_type =
+          let rec aux =
+           function
+              _,[] -> []
+            | C.Prod (n,s,t),he::tl ->
+               (he, type_of_aux context he (Some (head_beta_reduce s)))::
+                (aux (R.whd context (S.subst he t), tl))
+            | _ -> assert false
+          in
+           aux (expected_hetype, tl)
+         in
+          eat_prods context hetype tlbody_and_type
      | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
      | C.Const (uri,cookingsno) ->
         cooked_type_of_constant uri cookingsno
@@ -463,8 +496,6 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           (* the synthesized type. Let's forget it.       *)
           {synthesized = synthesized' ; expected = None}, synthesized
        | Some expectedty' ->
-prerr_endline ("t: " ^ CicPp.ppterm t) ; flush stderr ;
-prerr_endline (CicPp.ppterm synthesized' ^ " <-> " ^ CicPp.ppterm expectedty') ; flush stderr ;
           {synthesized = synthesized' ; expected = Some expectedty'},
           expectedty'
      in