X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FdoubleTypeInference.ml;h=71422ced12d6190d09b2829d2f80d1fcffaef6c5;hb=4f171cba0be2e0543cf49b221ee22b553305488a;hp=50a81c56a50596181c5755b4889c8d7a53a45a70;hpb=cedc0cfe0ea81f94ac8b88b71d8f855a33329593;p=helm.git

diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml
index 50a81c56a..71422ced1 100644
--- a/helm/gTopLevel/doubleTypeInference.ml
+++ b/helm/gTopLevel/doubleTypeInference.ml
@@ -31,7 +31,204 @@ exception WrongUriToMutualInductiveDefinitions of string;;
 exception ListTooShort;;
 exception RelToHiddenHypothesis;;
 
-type types = {synthesized : Cic.term ; expected : Cic.term};;
+type types = {synthesized : Cic.term ; expected : Cic.term option};;
+
+(* does_not_occur n te                              *)
+(* returns [true] if [Rel n] does not occur in [te] *)
+let rec does_not_occur n =
+ let module C = Cic in
+  function
+     C.Rel m when m = n -> false
+   | C.Rel _
+   | C.Meta _
+   | C.Sort _
+   | C.Implicit -> true 
+   | C.Cast (te,ty) ->
+      does_not_occur n te && does_not_occur n ty
+   | C.Prod (name,so,dest) ->
+      does_not_occur n so &&
+       does_not_occur (n + 1) dest
+   | C.Lambda (name,so,dest) ->
+      does_not_occur n so &&
+       does_not_occur (n + 1) dest
+   | C.LetIn (name,so,dest) ->
+      does_not_occur n so &&
+       does_not_occur (n + 1) dest
+   | C.Appl l ->
+      List.fold_right (fun x i -> i && does_not_occur n x) l true
+   | C.Var (_,exp_named_subst)
+   | C.Const (_,exp_named_subst)
+   | C.MutInd (_,_,exp_named_subst)
+   | C.MutConstruct (_,_,_,exp_named_subst) ->
+      List.fold_right (fun (_,x) i -> i && does_not_occur n x)
+       exp_named_subst true
+   | C.MutCase (_,_,out,te,pl) ->
+      does_not_occur n out && does_not_occur n te &&
+       List.fold_right (fun x i -> i && does_not_occur n x) pl true
+   | C.Fix (_,fl) ->
+      let len = List.length fl in
+       let n_plus_len = n + len in
+       let tys =
+        List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+       in
+        List.fold_right
+         (fun (_,_,ty,bo) i ->
+           i && does_not_occur n ty &&
+           does_not_occur n_plus_len bo
+         ) fl true
+   | C.CoFix (_,fl) ->
+      let len = List.length fl in
+       let n_plus_len = n + len in
+       let tys =
+        List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+       in
+        List.fold_right
+         (fun (_,ty,bo) i ->
+           i && does_not_occur n ty &&
+           does_not_occur n_plus_len bo
+         ) fl true
+;;
+
+(*CSC: potrebbe creare applicazioni di applicazioni *)
+(*CSC: ora non e' piu' head, ma completa!!! *)
+let rec head_beta_reduce =
+ let module S = CicSubstitution in
+ let module C = Cic in
+  function
+      C.Rel _ as t -> t
+    | C.Var (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+       in
+        C.Var (uri,exp_named_subst)
+    | C.Meta (n,l) ->
+       C.Meta (n,
+        List.map
+         (function None -> None | Some t -> Some (head_beta_reduce t)) l
+       )
+    | C.Sort _ as t -> t
+    | C.Implicit -> assert false
+    | C.Cast (te,ty) ->
+       C.Cast (head_beta_reduce te, head_beta_reduce ty)
+    | C.Prod (n,s,t) ->
+       C.Prod (n, head_beta_reduce s, head_beta_reduce t)
+    | C.Lambda (n,s,t) ->
+       C.Lambda (n, head_beta_reduce s, head_beta_reduce t)
+    | C.LetIn (n,s,t) ->
+       C.LetIn (n, head_beta_reduce s, head_beta_reduce t)
+    | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
+       let he' = S.subst he t in
+        if tl = [] then
+         head_beta_reduce he'
+        else
+         head_beta_reduce (C.Appl (he'::tl))
+    | C.Appl l ->
+       C.Appl (List.map head_beta_reduce l)
+    | C.Const (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+       in
+        C.Const (uri,exp_named_subst')
+    | C.MutInd (uri,i,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+       in
+        C.MutInd (uri,i,exp_named_subst')
+    | C.MutConstruct (uri,i,j,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+       in
+        C.MutConstruct (uri,i,j,exp_named_subst')
+    | C.MutCase (sp,i,outt,t,pl) ->
+       C.MutCase (sp,i,head_beta_reduce outt,head_beta_reduce t,
+        List.map head_beta_reduce pl)
+    | C.Fix (i,fl) ->
+       let fl' =
+        List.map
+         (function (name,i,ty,bo) ->
+           name,i,head_beta_reduce ty,head_beta_reduce bo
+         ) fl
+       in
+        C.Fix (i,fl')
+    | C.CoFix (i,fl) ->
+       let fl' =
+        List.map
+         (function (name,ty,bo) ->
+           name,head_beta_reduce ty,head_beta_reduce bo
+         ) fl
+       in
+        C.CoFix (i,fl')
+;;
+
+(* syntactic_equality up to cookingsno for uris *)
+(* (which is often syntactically irrilevant),   *)
+(* distinction between fake dependent products  *)
+(* and non-dependent products, alfa-conversion  *)
+(*CSC: must alfa-conversion be considered or not? *)
+let syntactic_equality t t' =
+ let module C = Cic in
+ let rec syntactic_equality t t' =
+  if t = t' then true
+  else
+   match t, t' with
+      C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') ->
+       UriManager.eq uri uri' &&
+        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
+    | C.Cast (te,ty), C.Cast (te',ty') ->
+       syntactic_equality te te' &&
+        syntactic_equality ty ty'
+    | C.Prod (_,s,t), C.Prod (_,s',t') ->
+       syntactic_equality s s' &&
+        syntactic_equality t t'
+    | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
+       syntactic_equality s s' &&
+        syntactic_equality t t'
+    | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
+       syntactic_equality s s' &&
+        syntactic_equality t t'
+    | C.Appl l, C.Appl l' ->
+       List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
+    | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') ->
+       UriManager.eq uri uri' &&
+        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
+    | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') ->
+       UriManager.eq uri uri' && i = i' &&
+        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
+    | C.MutConstruct (uri,i,j,exp_named_subst),
+      C.MutConstruct (uri',i',j',exp_named_subst') ->
+       UriManager.eq uri uri' && i = i' && j = j' &&
+        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
+    | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
+       UriManager.eq sp sp' && i = i' &&
+        syntactic_equality outt outt' &&
+         syntactic_equality t t' &&
+          List.fold_left2
+           (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
+    | C.Fix (i,fl), C.Fix (i',fl') ->
+       i = i' &&
+        List.fold_left2
+         (fun b (_,i,ty,bo) (_,i',ty',bo') ->
+           b && i = i' &&
+            syntactic_equality ty ty' &&
+             syntactic_equality bo bo') true fl fl'
+    | C.CoFix (i,fl), C.CoFix (i',fl') ->
+       i = i' &&
+        List.fold_left2
+         (fun b (_,ty,bo) (_,ty',bo') ->
+           b &&
+            syntactic_equality ty ty' &&
+             syntactic_equality bo bo') true fl fl'
+    | _, _ -> false (* we already know that t != t' *)
+ and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 =
+  List.fold_left2
+   (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true
+   exp_named_subst1 exp_named_subst2
+ in
+  try
+   syntactic_equality t t'
+  with
+   _ -> false
+;;
 
 let rec split l n =
  match (l,n) with
@@ -40,20 +237,19 @@ let rec split l n =
   | (_,_) -> raise ListTooShort
 ;;
 
-let cooked_type_of_constant uri cookingsno =
+let type_of_constant uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri cookingsno with
+   match CicEnvironment.is_type_checked uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked constant")
   in
    match cobj with
-      C.Definition (_,_,ty,_) -> ty
-    | C.Axiom (_,ty,_) -> ty
-    | C.CurrentProof (_,_,_,ty) -> ty
+      C.Constant (_,_,ty,_) -> ty
+    | C.CurrentProof (_,_,_,ty,_) -> ty
     | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
 ;;
 
@@ -61,20 +257,19 @@ let type_of_variable uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
-  (* 0 because a variable is never cooked => no partial cooking at one level *)
-  match CicEnvironment.is_type_checked uri 0 with
-     CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty
+  match CicEnvironment.is_type_checked uri with
+     CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
    | CicEnvironment.UncheckedObj (C.Variable _) ->
       raise (NotWellTyped "Reference to an unchecked variable")
    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 ;;
 
-let cooked_type_of_mutual_inductive_defs uri cookingsno i =
+let type_of_mutual_inductive_defs uri i =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri cookingsno with
+   match CicEnvironment.is_type_checked uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked inductive type")
@@ -86,12 +281,12 @@ let cooked_type_of_mutual_inductive_defs uri cookingsno i =
     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 ;;
 
-let cooked_type_of_mutual_inductive_constr uri cookingsno i j =
+let type_of_mutual_inductive_constr uri i j =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri cookingsno with
+   match CicEnvironment.is_type_checked uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked constructor")
@@ -99,7 +294,7 @@ let cooked_type_of_mutual_inductive_constr uri cookingsno i j =
    match cobj with
       C.InductiveDefinition (dl,_,_) ->
        let (_,_,_,cl) = List.nth dl i in
-        let (_,ty,_) = List.nth cl (j-1) in
+        let (_,ty) = List.nth cl (j-1) in
          ty
     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 ;;
@@ -114,12 +309,12 @@ module CicHash =
 ;;
 
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
-let rec type_of_aux' subterms_to_types metasenv context t =
+let rec type_of_aux' subterms_to_types metasenv context t expectedty =
  (* Coscoy's double type-inference algorithm             *)
  (* It computes the inner-types of every subterm of [t], *)
  (* even when they are not needed to compute the types   *)
  (* of other terms.                                      *)
- let rec type_of_aux context t =
+ let rec type_of_aux context t expectedty =
   let module C = Cic in
   let module R = CicReduction in
   let module S = CicSubstitution in
@@ -130,113 +325,216 @@ let rec type_of_aux' subterms_to_types metasenv context t =
         (try
           match List.nth context (n - 1) with
              Some (_,C.Decl t) -> S.lift n t
-           | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo)
+           | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo) expectedty
 	   | None -> raise RelToHiddenHypothesis
          with
           _ -> raise (NotWellTyped "Not a close term")
         )
-     | C.Var uri -> type_of_variable uri
+     | C.Var (uri,exp_named_subst) ->
+        visit_exp_named_subst context uri exp_named_subst ;
+        CicSubstitution.subst_vars exp_named_subst (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)) 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) ->
         (* Let's visit all the subterms that will not be visited later *)
-        let _ = type_of_aux context te in
-        let _ = type_of_aux context ty in
+        let _ = type_of_aux context te (Some (head_beta_reduce ty)) in
+        let _ = type_of_aux context ty None in
          (* Checks suppressed *)
          ty
      | C.Prod (name,s,t) ->
-        let sort1 = type_of_aux context s
-        and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
+        let sort1 = type_of_aux context s None
+        and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in
          sort_of_prod context (name,s) (sort1,sort2)
      | C.Lambda (n,s,t) ->
         (* Let's visit all the subterms that will not be visited later *)
-        let _ = type_of_aux context s in
-         let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
-          (* Checks suppressed *)
-          C.Prod (n,s,type2)
+        let _ = type_of_aux context s None in
+         let expected_target_type =
+          match expectedty with
+             None -> None
+           | Some expectedty' ->
+              let ty =
+               match R.whd context expectedty' with
+                  C.Prod (_,_,expected_target_type) ->
+                   head_beta_reduce expected_target_type
+                | _ -> assert false
+              in
+               Some ty
+         in
+          let type2 =
+           type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
+          in
+           (* Checks suppressed *)
+           C.Prod (n,s,type2)
      | C.LetIn (n,s,t) ->
+(*CSC: What are the right expected types for the source and *)
+(*CSC: target of a LetIn? None used.                        *)
         (* Let's visit all the subterms that will not be visited later *)
-        let _ = type_of_aux context s in
-         (* Checks suppressed *)
-         C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)
+        let _ = type_of_aux context s None in
+         let t_typ =
+          (* Checks suppressed *)
+          type_of_aux ((Some (n,(C.Def s)))::context) t None
+         in
+          if does_not_occur 1 t_typ then
+           (* since [Rel 1] does not occur in typ, substituting any term *)
+           (* in place of [Rel 1] is equivalent to delifting once        *)
+           CicSubstitution.subst C.Implicit t_typ
+          else
+           C.LetIn (n,s,t_typ)
      | C.Appl (he::tl) when List.length tl > 0 ->
-        let hetype = type_of_aux context he
-        and tlbody_and_type =
-         List.map (fun x -> (x, type_of_aux context x)) 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
-     | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
-     | C.Const (uri,cookingsno) ->
-        cooked_type_of_constant uri cookingsno
-     | C.Abst _ -> raise (Impossible 22)
-     | C.MutInd (uri,cookingsno,i) ->
-        cooked_type_of_mutual_inductive_defs uri cookingsno i
-     | C.MutConstruct (uri,cookingsno,i,j) ->
-        let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j in
-         cty
-     | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
-        (* Let's visit all the subterms that will not be visited later *)
-        let _ = List.map (type_of_aux context) pl in
-         let outsort = type_of_aux context outtype in
-         let (need_dummy, k) =
-          let rec guess_args context t =
-           match CicReduction.whd context t with
-              C.Sort _ -> (true, 0)
-            | C.Prod (name, s, t) ->
-               let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
-                if n = 0 then
-                 (* last prod before sort *)
-                 match CicReduction.whd context s with
-                    (*CSC vedi nota delirante su cookingsno in cicReduction.ml *)
-                    C.MutInd (uri',_,i') when U.eq uri' uri && i' = i ->
-                     (false, 1)
-                  | C.Appl ((C.MutInd (uri',_,i')) :: _)
-                     when U.eq uri' uri && i' = i -> (false, 1)
-                  | _ -> (true, 1)
-                else
-                 (b, n + 1)
-            | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
+         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
-           (*CSC whd non serve dopo type_of_aux ? *)
-           let (b, k) = guess_args context outsort in
-            if not b then (b, k - 1) else (b, k)
+           aux (expected_hetype, tl)
+         in
+          eat_prods context hetype tlbody_and_type
+     | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
+     | C.Const (uri,exp_named_subst) ->
+        visit_exp_named_subst context uri exp_named_subst ;
+        CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
+     | C.MutInd (uri,i,exp_named_subst) ->
+        visit_exp_named_subst context uri exp_named_subst ;
+        CicSubstitution.subst_vars exp_named_subst
+         (type_of_mutual_inductive_defs uri i)
+     | C.MutConstruct (uri,i,j,exp_named_subst) ->
+        visit_exp_named_subst context uri exp_named_subst ;
+        CicSubstitution.subst_vars exp_named_subst
+         (type_of_mutual_inductive_constr uri i j)
+     | C.MutCase (uri,i,outtype,term,pl) ->
+        let outsort = type_of_aux context outtype None in
+        let (need_dummy, k) =
+         let rec guess_args context t =
+          match CicReduction.whd context t with
+             C.Sort _ -> (true, 0)
+           | C.Prod (name, s, t) ->
+              let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
+               if n = 0 then
+                (* last prod before sort *)
+                match CicReduction.whd context s with
+                   C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
+                    (false, 1)
+                 | C.Appl ((C.MutInd (uri',i',_)) :: _)
+                    when U.eq uri' uri && i' = i -> (false, 1)
+                 | _ -> (true, 1)
+               else
+                (b, n + 1)
+           | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
          in
-         let (_, arguments) =
-           match R.whd context (type_of_aux context term) with
-              (*CSC manca il caso dei CAST *)
-              C.MutInd (uri',_,i') ->
-               (* Checks suppressed *)
-               [],[]
-            | C.Appl (C.MutInd (uri',_,i') :: tl) ->
-               split tl (List.length tl - k)
-            | _ ->
-              raise (NotWellTyped "MutCase: the term is not an inductive one")
+          let (b, k) = guess_args context outsort in
+           if not b then (b, k - 1) else (b, k)
+        in
+        let (parameters, arguments,exp_named_subst) =
+         let type_of_term =
+          CicTypeChecker.type_of_aux' metasenv context term
          in
-          (* Checks suppressed *)
-          if not need_dummy then
-           C.Appl ((outtype::arguments)@[term])
-          else if arguments = [] then
-           outtype
-          else
-           C.Appl (outtype::arguments)
+          match
+           R.whd context (type_of_aux context term
+            (Some (head_beta_reduce type_of_term)))
+          with
+             (*CSC manca il caso dei CAST *)
+             C.MutInd (uri',i',exp_named_subst) ->
+              (* Checks suppressed *)
+              [],[],exp_named_subst
+           | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) ->
+             let params,args =
+              split tl (List.length tl - k)
+             in params,args,exp_named_subst
+           | _ ->
+             raise (NotWellTyped "MutCase: the term is not an inductive one")
+        in
+         (* Checks suppressed *)
+         (* Let's visit all the subterms that will not be visited later *)
+         let (cl,parsno) =
+          match CicEnvironment.get_cooked_obj uri with
+             C.InductiveDefinition (tl,_,parsno) ->
+              let (_,_,_,cl) = List.nth tl i in (cl,parsno)
+           | _ ->
+             raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+         in
+          let _ =
+           List.fold_left
+            (fun j (p,(_,c)) ->
+              let cons =
+               if parameters = [] then
+                (C.MutConstruct (uri,i,j,exp_named_subst))
+               else
+                (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
+              in
+               let expectedtype =
+                type_of_branch context parsno need_dummy outtype cons
+                  (CicTypeChecker.type_of_aux' metasenv context cons)
+               in
+                ignore (type_of_aux context p
+                 (Some (head_beta_reduce expectedtype))) ;
+                j+1
+            ) 1 (List.combine pl cl)
+          in
+           if not need_dummy then
+            C.Appl ((outtype::arguments)@[term])
+           else if arguments = [] then
+            outtype
+           else
+            C.Appl (outtype::arguments)
      | C.Fix (i,fl) ->
         (* Let's visit all the subterms that will not be visited later *)
         let context' =
          List.rev
           (List.map
             (fun (n,_,ty,_) ->
-              let _ = type_of_aux context ty in
+              let _ = type_of_aux context ty None in
                (Some (C.Name n,(C.Decl ty)))
             ) fl
           ) @
@@ -244,7 +542,12 @@ let rec type_of_aux' subterms_to_types metasenv context t =
         in
          let _ =
           List.iter
-           (fun (_,_,_,bo) -> ignore (type_of_aux context' bo))
+           (fun (_,_,ty,bo) ->
+             let expectedty =
+              head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
+             in
+              ignore (type_of_aux context' bo (Some expectedty))
+           ) fl
          in
           (* Checks suppressed *)
           let (_,_,ty,_) = List.nth fl i in
@@ -255,7 +558,7 @@ let rec type_of_aux' subterms_to_types metasenv context t =
          List.rev
           (List.map
             (fun (n,ty,_) ->
-              let _ = type_of_aux context ty in
+              let _ = type_of_aux context ty None in
                (Some (C.Name n,(C.Decl ty)))
             ) fl
           ) @
@@ -263,20 +566,61 @@ let rec type_of_aux' subterms_to_types metasenv context t =
         in
          let _ =
           List.iter
-           (fun (_,_,bo) -> ignore (type_of_aux context' bo))
+           (fun (_,ty,bo) ->
+             let expectedty =
+              head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
+             in
+              ignore (type_of_aux context' bo (Some expectedty))
+           ) fl
          in
           (* Checks suppressed *)
           let (_,ty,_) = List.nth fl i in
            ty
    in
-    (*CSC: Is whd the right thing to do? Or should full beta *)
-    (*CSC: reduction be more appropriate?                    *)
-(*CSC: Nota: whd fa troppo (esempio: fa anche iota) e full beta sembra molto *)
-(*CSC: costosa quando fatta ogni passo. Fare solo un passo? *)
-    let synthesized' = CicReduction.whd context synthesized in
-     CicHash.add subterms_to_types t
-      {synthesized = synthesized' ; expected = Cic.Implicit} ;
-     synthesized'
+    let synthesized' = head_beta_reduce synthesized in
+     let types,res =
+      match expectedty with
+         None ->
+          (* No expected type *)
+          {synthesized = synthesized' ; expected = None}, synthesized
+       | Some ty when syntactic_equality synthesized' ty ->
+          (* The expected type is synthactically equal to *)
+          (* the synthesized type. Let's forget it.       *)
+          {synthesized = synthesized' ; expected = None}, synthesized
+       | Some expectedty' ->
+          {synthesized = synthesized' ; expected = Some expectedty'},
+          expectedty'
+     in
+      CicHash.add subterms_to_types t types ;
+      res
+
+ and visit_exp_named_subst context uri exp_named_subst =
+  let uris_and_types =
+   match CicEnvironment.get_cooked_obj uri with
+      Cic.Constant (_,_,_,params)
+    | Cic.CurrentProof (_,_,_,_,params)
+    | Cic.Variable (_,_,_,params)
+    | Cic.InductiveDefinition (_,params,_) ->
+       List.map
+        (function uri ->
+          match CicEnvironment.get_cooked_obj uri with
+             Cic.Variable (_,None,ty,_) -> uri,ty
+           | _ -> assert false (* the theorem is well-typed *)
+        ) params
+  in
+   let rec check uris_and_types subst =
+    match uris_and_types,subst with
+       _,[] -> []
+     | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
+        ignore (type_of_aux context t (Some ty)) ;
+        let tytl' =
+         List.map
+          (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl
+        in
+         check tytl' substtl
+     | _,_ -> assert false (* the theorem is well-typed *)
+   in
+    check uris_and_types exp_named_subst
 
  and sort_of_prod context (name,s) (t1, t2) =
   let module C = Cic in
@@ -305,12 +649,39 @@ let rec type_of_aux' subterms_to_types metasenv context t =
       | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
     )
 
+and type_of_branch context argsno need_dummy outtype term constype =
+ let module C = Cic in
+ let module R = CicReduction in
+  match R.whd context constype with
+     C.MutInd (_,_,_) ->
+      if need_dummy then
+       outtype
+      else
+       C.Appl [outtype ; term]
+   | C.Appl (C.MutInd (_,_,_)::tl) ->
+      let (_,arguments) = split tl argsno
+      in
+       if need_dummy && arguments = [] then
+        outtype
+       else
+        C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
+   | C.Prod (name,so,de) ->
+      let term' =
+       match CicSubstitution.lift 1 term with
+          C.Appl l -> C.Appl (l@[C.Rel 1])
+        | t -> C.Appl [t ; C.Rel 1]
+      in
+       C.Prod (C.Anonymous,so,type_of_branch
+        ((Some (name,(C.Decl so)))::context) argsno need_dummy
+        (CicSubstitution.lift 1 outtype) term' de)
+  | _ -> raise (Impossible 20)
+
  in
-  type_of_aux context t
+  type_of_aux context t expectedty
 ;;
 
-let double_type_of metasenv context t =
+let double_type_of metasenv context t expectedty =
  let subterms_to_types = CicHash.create 503 in
-  ignore (type_of_aux' subterms_to_types metasenv context t) ;
+  ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;
   subterms_to_types
 ;;