X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=d34c829199e506cf1925c46402104b9e43295a20;hb=ff2f125b1c37e7c1406ebca16de7b651802ebc91;hp=c67dc5343f622b0ce215c28c0ed5fa4dee3e99d8;hpb=49236887a0dce59bae7df0a672955ffb89f756ff;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index c67dc5343..d34c82919 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -75,7 +75,7 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k+1) t)
+    | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k+1) t)
     | C.Appl l -> C.Appl (List.map (aux k) l)
     | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' = 
@@ -252,14 +252,14 @@ and does_not_occur ?(subst=[]) context n nn te =
          Failure _ -> assert false)
     | C.Sort _
     | C.Implicit _ -> true
-    | C.Meta (_,l) ->
+    | C.Meta (mno,l) ->
        List.fold_right
         (fun x i ->
           match x with
              None -> i
            | Some x -> i && does_not_occur ~subst context n nn x) l true &&
        (try
-         let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
+         let (canonical_context,term,ty) = CicUtil.lookup_subst mno subst in
           does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term)
         with
          CicUtil.Subst_not_found _ -> true)
@@ -273,10 +273,11 @@ and does_not_occur ?(subst=[]) context n nn te =
        does_not_occur ~subst context n nn so &&
         does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
          dest
-    | C.LetIn (name,so,dest) ->
+    | C.LetIn (name,so,ty,dest) ->
        does_not_occur ~subst context n nn so &&
-        does_not_occur ~subst ((Some (name,(C.Def (so,None))))::context)
-         (n + 1) (nn + 1) dest
+        does_not_occur ~subst context n nn ty &&
+         does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context)
+          (n + 1) (nn + 1) dest
     | C.Appl l ->
        List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
     | C.Var (_,exp_named_subst)
@@ -292,8 +293,12 @@ and does_not_occur ?(subst=[]) context n nn te =
        let len = List.length fl in
         let n_plus_len = n + len in
         let nn_plus_len = nn + len in
-        let tys =
-         List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+        let tys,_ =
+         List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
         in
          List.fold_right
           (fun (_,_,ty,bo) i ->
@@ -304,8 +309,12 @@ and does_not_occur ?(subst=[]) context n nn te =
        let len = List.length fl in
         let n_plus_len = n + len in
         let nn_plus_len = nn + len in
-        let tys =
-         List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+        let tys,_ =
+         List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
         in
          List.fold_right
           (fun (_,ty,bo) i ->
@@ -377,7 +386,10 @@ and weakly_positive context n nn uri te =
     | t -> t
   in
   match CicReduction.whd context te with
+(*
      C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
+*)
+     C.Appl ((C.MutInd (uri',_,_))::tl) when UriManager.eq uri' uri -> true
    | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
    | C.Prod (C.Anonymous,source,dest) ->
       strictly_positive context n nn
@@ -389,13 +401,13 @@ and weakly_positive context n nn uri te =
        (* dummy abstraction, so we behave as in the anonimous case *)
        strictly_positive context n nn
         (subst_inductive_type_with_dummy_mutind source) &&
-        weakly_positive ((Some (name,(C.Decl source)))::context)
+         weakly_positive ((Some (name,(C.Decl source)))::context)
          (n + 1) (nn + 1) uri dest
    | C.Prod (name,source,dest) ->
-      does_not_occur context n nn
-       (subst_inductive_type_with_dummy_mutind source)&&
-       weakly_positive ((Some (name,(C.Decl source)))::context)
-        (n + 1) (nn + 1) uri dest
+       does_not_occur context n nn
+	 (subst_inductive_type_with_dummy_mutind source)&&
+	 weakly_positive ((Some (name,(C.Decl source)))::context)
+         (n + 1) (nn + 1) uri dest
    | _ ->
      raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
 
@@ -415,7 +427,8 @@ and strictly_positive context n nn te =
  let module C = Cic in
  let module U = UriManager in
   match CicReduction.whd context te with
-     C.Rel _ -> true
+   | t when does_not_occur context n nn t -> true
+   | C.Rel _ -> true
    | C.Cast (te,ty) ->
       (*CSC: bisogna controllare ty????*)
       strictly_positive context n nn te
@@ -427,37 +440,39 @@ and strictly_positive context n nn te =
    | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) -> 
       let (ok,paramsno,ity,cl,name) =
 	let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-       match o with
-           C.InductiveDefinition (tl,_,paramsno,_) ->
-            let (name,_,ity,cl) = List.nth tl i in
-             (List.length tl = 1, paramsno, ity, cl, name)
-         | _ ->
-           raise (TypeCheckerFailure
-            (lazy ("Unknown inductive type:" ^ U.string_of_uri uri)))
-      in
-       let (params,arguments) = split tl paramsno in
-       let lifted_params = List.map (CicSubstitution.lift 1) params in
-       let cl' =
+	  match o with
+              C.InductiveDefinition (tl,_,paramsno,_) ->
+		let (name,_,ity,cl) = List.nth tl i in
+                (List.length tl = 1, paramsno, ity, cl, name) 
+                (* (true, paramsno, ity, cl, name) *)
+            | _ ->
+		raise 
+		  (TypeCheckerFailure
+		     (lazy ("Unknown inductive type:" ^ U.string_of_uri uri)))
+      in 
+      let (params,arguments) = split tl paramsno in
+      let lifted_params = List.map (CicSubstitution.lift 1) params in
+      let cl' =
         List.map
-         (fun (_,te) ->
-           instantiate_parameters lifted_params
-            (CicSubstitution.subst_vars exp_named_subst te)
-         ) cl
-       in
+          (fun (_,te) ->
+             instantiate_parameters lifted_params
+               (CicSubstitution.subst_vars exp_named_subst te)
+          ) cl
+      in
         ok &&
-         List.fold_right
+          List.fold_right
           (fun x i -> i && does_not_occur context n nn x)
           arguments true &&
          (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
-         List.fold_right
+          List.fold_right
           (fun x i ->
-            i &&
-             weakly_positive
-              ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
-              x
+             i &&
+               weakly_positive
+               ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
+               x
           ) cl' true
-   | t -> does_not_occur context n nn t
-
+   | t -> false
+       
 (* the inductive type indexes are s.t. n < x <= nn *)
 and are_all_occurrences_positive context uri indparamsno i n nn te =
  let module C = Cic in
@@ -494,7 +509,8 @@ and are_all_occurrences_positive context uri indparamsno i n nn te =
          (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
           UriManager.string_of_uri uri)))
    | C.Prod (C.Anonymous,source,dest) ->
-      strictly_positive context n nn source &&
+       let b = strictly_positive context n nn source in
+       b &&
        are_all_occurrences_positive
         ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
         (i+1) (n + 1) (nn + 1) dest
@@ -553,9 +569,12 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
 		  (are_all_occurrences_positive tys uri indparamsno i 0 len
                      debrujinedte)
               then
+                begin
+                prerr_endline (UriManager.string_of_uri uri);
+                prerr_endline (string_of_int (List.length tys));
 		raise
 		  (TypeCheckerFailure
-                    (lazy ("Non positive occurence in " ^ U.string_of_uri uri)))
+                    (lazy ("Non positive occurence in " ^ U.string_of_uri uri)))                end 
               else
 		ugraph'
             ) ugraph cl in
@@ -747,9 +766,10 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
       check_is_really_smaller_arg ~subst context n nn kl x safes so &&
        check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context)
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
-   | C.LetIn (name,so,ta) ->
+   | C.LetIn (name,so,ty,ta) ->
       check_is_really_smaller_arg ~subst context n nn kl x safes so &&
-       check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,None))))::context)
+       check_is_really_smaller_arg ~subst context n nn kl x safes ty &&
+        check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,ty))))::context)
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.Appl (he::_) ->
       (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
@@ -762,7 +782,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match term with
           C.Rel m when List.mem m safes || m = x ->
-           let (tys,len,isinductive,paramsno,cl) =
+           let (lefts_and_tys,len,isinductive,paramsno,cl) =
 	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
                C.InductiveDefinition (tl,_,paramsno,_) ->
@@ -774,9 +794,14 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, snd (split_prods ~subst tys paramsno ty))) cl
+                      (id, snd (split_prods ~subst tys paramsno ty))) cl in
+                  let lefts =
+                   match tl with
+                      [] -> assert false
+                    | (_,_,ty,_)::_ ->
+                       fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys,List.length tl,isinductive,paramsno,cl')
+                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -799,7 +824,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                (fun (p,(_,c)) i ->
                  let rl' =
                   let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args tys 0 len debrujinedte
+                   recursive_args lefts_and_tys 0 len debrujinedte
                  in
                   let (e,safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
@@ -808,7 +833,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
                ) pl_and_cl true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
-           let (tys,len,isinductive,paramsno,cl) =
+           let (lefts_and_tys,len,isinductive,paramsno,cl) =
             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
                C.InductiveDefinition (tl,_,paramsno,_) ->
@@ -820,9 +845,14 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, snd (split_prods ~subst tys paramsno ty))) cl
+                      (id, snd (split_prods ~subst tys paramsno ty))) cl in
+                  let lefts =
+                   match tl with
+                      [] -> assert false
+                    | (_,_,ty,_)::_ ->
+                       fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys,List.length tl,isinductive,paramsno,cl')
+                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -847,7 +877,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                (fun (p,(_,c)) i ->
                  let rl' =
                   let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args tys 0 len debrujinedte
+                   recursive_args lefts_and_tys 0 len debrujinedte
                  in
                   let (e, safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
@@ -866,7 +896,12 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
-       and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,_,ty,bo) i ->
@@ -879,7 +914,12 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
-       and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,ty,bo) i ->
@@ -894,10 +934,10 @@ and guarded_by_destructors ~subst context n nn kl x safes =
   function
      C.Rel m when m > n && m <= nn -> false
    | C.Rel m ->
-      (match List.nth context (n-1) with
+      (match List.nth context (m-1) with
           Some (_,C.Decl _) -> true
         | Some (_,C.Def (bo,_)) ->
-           guarded_by_destructors ~subst context m nn kl x safes
+           guarded_by_destructors ~subst context n nn kl x safes
             (CicSubstitution.lift m bo)
         | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
       )
@@ -915,10 +955,11 @@ and guarded_by_destructors ~subst context n nn kl x safes =
       guarded_by_destructors ~subst context n nn kl x safes so &&
        guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context)
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
-   | C.LetIn (name,so,ta) ->
+   | C.LetIn (name,so,ty,ta) ->
       guarded_by_destructors ~subst context n nn kl x safes so &&
-       guarded_by_destructors ~subst ((Some (name,(C.Def (so,None))))::context)
-        (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
+       guarded_by_destructors ~subst context n nn kl x safes ty &&
+        guarded_by_destructors ~subst ((Some (name,(C.Def (so,ty))))::context)
+         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       let k = List.nth kl (m - n - 1) in
        if not (List.length tl > k) then false
@@ -942,7 +983,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match CicReduction.whd ~subst context term with
           C.Rel m when List.mem m safes || m = x ->
-           let (tys,len,isinductive,paramsno,cl) =
+           let (lefts_and_tys,len,isinductive,paramsno,cl) =
 	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
                C.InductiveDefinition (tl,_,paramsno,_) ->
@@ -958,9 +999,14 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                       let debrujinedty = debrujin_constructor uri len ty in
                        (id, snd (split_prods ~subst tys paramsno ty),
                         snd (split_prods ~subst tys paramsno debrujinedty)
-                       )) cl
+                       )) cl in
+                   let lefts =
+                    match tl with
+                       [] -> assert false
+                     | (_,_,ty,_)::_ ->
+                        fst (split_prods ~subst [] paramsno ty)
                    in
-                    (tys,len,isinductive,paramsno,cl')
+                    (lefts@tys,len,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -986,7 +1032,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
               (*CSC: manca ??? il controllo sul tipo di term? *)
               List.fold_right
                (fun (p,(_,c,brujinedc)) i ->
-                 let rl' = recursive_args tys 0 len brujinedc in
+                 let rl' = recursive_args lefts_and_tys 0 len brujinedc in
                   let (e,safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
                   in
@@ -994,7 +1040,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                    guarded_by_destructors ~subst context' n' nn' kl x' safes' e
                ) pl_and_cl true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
-           let (tys,len,isinductive,paramsno,cl) =
+           let (lefts_and_tys,len,isinductive,paramsno,cl) =
 	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
                C.InductiveDefinition (tl,_,paramsno,_) ->
@@ -1006,9 +1052,14 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, snd (split_prods ~subst tys paramsno ty))) cl
+                      (id, snd (split_prods ~subst tys paramsno ty))) cl in
+                  let lefts =
+                   match tl with
+                      [] -> assert false
+                    | (_,_,ty,_)::_ ->
+                       fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys,List.length tl,isinductive,paramsno,cl')
+                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -1040,7 +1091,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                (fun (p,(_,c)) i ->
                  let rl' =
                   let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args tys 0 len debrujinedte
+                   recursive_args lefts_and_tys 0 len debrujinedte
                  in
                   let (e, safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
@@ -1061,7 +1112,12 @@ and guarded_by_destructors ~subst context n nn kl x safes =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
-       and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,_,ty,bo) i ->
@@ -1074,7 +1130,12 @@ and guarded_by_destructors ~subst context n nn kl x safes =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
-       and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,ty,bo) i ->
@@ -1227,7 +1288,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
         let n_plus_len = n + len
         and nn_plus_len = nn + len
         (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
-        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
+        and tys,_ =
+          List.fold_left
+            (fun (types,len) (n,ty,_) ->
+               (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                len+1)
+	    ) ([],0) fl
+        in
          List.fold_right
           (fun (_,ty,bo) i ->
             i && does_not_occur ~subst context n nn ty &&
@@ -1268,7 +1335,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
-       and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
+       in
         List.fold_right
          (fun (_,_,ty,bo) i ->
            i && does_not_occur ~subst context n nn ty &&
@@ -1279,7 +1352,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
-       and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
+       in
         List.fold_right
          (fun (_,ty,bo) i ->
            i && does_not_occur ~subst context n nn ty &&
@@ -1295,11 +1374,12 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
   let arity1 = CicReduction.whd ~subst context arity1 in
   let rec check_allowed_sort_elimination_aux ugraph context arity2 need_dummy =
    match arity1, CicReduction.whd ~subst context arity2 with
-     (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
+     (C.Prod (name,so1,de1), C.Prod (_,so2,de2)) ->
        let b,ugraph1 =
         CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in
        if b then
-	 check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
+	 check_allowed_sort_elimination ~subst ~metasenv ~logger 
+           ((Some (name,C.Decl so1))::context) uri i
           need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
           ugraph1
        else
@@ -1415,11 +1495,9 @@ and check_metasenv_consistency ~logger ~subst metasenv context
          [] -> []
        | (Some (n,C.Decl t))::tl ->
            (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
-       | (Some (n,C.Def (t,None)))::tl ->
-           (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
        | None::tl -> None::(aux (i+1) tl)
-       | (Some (n,C.Def (t,Some ty)))::tl ->
-           (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl)
+       | (Some (n,C.Def (t,ty)))::tl ->
+           (Some (n,C.Def ((S.subst_meta l (S.lift i t)),S.subst_meta l (S.lift i ty))))::(aux (i+1) tl)
     in
      aux 1 canonical_context
    in
@@ -1428,8 +1506,25 @@ and check_metasenv_consistency ~logger ~subst metasenv context
        match (t,ct) with
        | _,None -> ugraph
        | Some t,Some (_,C.Def (ct,_)) ->
+          (*CSC: the following optimization is to avoid a possibly expensive
+                 reduction that can be easily avoided and that is quite
+                 frequent. However, this is better handled using levels to
+                 control reduction *)
+          let optimized_t =
+           match t with
+              Cic.Rel n ->
+               (try
+                 match List.nth context (n - 1) with
+                    Some (_,C.Def (te,_)) -> S.lift n te
+                  | _ -> t
+                with
+                 Failure _ -> t)
+            | _ -> t
+          in
+(*if t <> optimized_t && optimized_t = ct then prerr_endline "!!!!!!!!!!!!!!!"
+else if t <> optimized_t then prerr_endline ("@@ " ^ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm optimized_t ^ " <==> " ^ CicPp.ppterm ct);*)
 	   let b,ugraph1 = 
-	     R.are_convertible ~subst ~metasenv context t ct ugraph 
+	     R.are_convertible ~subst ~metasenv context optimized_t ct ugraph 
 	   in
 	   if not b then
 	     raise 
@@ -1474,10 +1569,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
        (try
          match List.nth context (n - 1) with
             Some (_,C.Decl t) -> S.lift n t,ugraph
-          | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph
-          | Some (_,C.Def (bo,None)) ->
-             debug_print (lazy "##### CASO DA INVESTIGARE E CAPIRE") ;
-              type_of_aux ~logger context (S.lift n bo) ugraph
+          | Some (_,C.Def (_,ty)) -> S.lift n ty,ugraph
           | None -> raise 
 	      (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
         with
@@ -1513,11 +1605,13 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
       (* TASSI: CONSTRAINTS *)
     | C.Sort (C.Type t) -> 
        let t' = CicUniv.fresh() in
-       let ugraph1 = CicUniv.add_gt t' t ugraph in
-         (C.Sort (C.Type t')),ugraph1
-      (* TASSI: CONSTRAINTS *)
+       (try
+         let ugraph1 = CicUniv.add_gt t' t ugraph in
+           (C.Sort (C.Type t')),ugraph1
+        with
+         CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
     | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
-    | C.Implicit _ -> raise (AssertFailure (lazy "21"))
+    | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
     | C.Cast (te,ty) as t ->
        let _,ugraph1 = type_of_aux ~logger context ty ugraph in
        let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
@@ -1550,9 +1644,20 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 	 type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1 
        in
 	 (C.Prod (n,s,type2)),ugraph2
-   | C.LetIn (n,s,t) ->
+   | C.LetIn (n,s,ty,t) ->
       (* only to check if s is well-typed *)
-      let ty,ugraph1 = type_of_aux ~logger context s ugraph in
+      let ty',ugraph1 = type_of_aux ~logger context s ugraph in
+      let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in
+      let b,ugraph1 =
+       R.are_convertible ~subst ~metasenv context ty ty' ugraph1
+      in 
+       if not b then
+        raise 
+         (TypeCheckerFailure 
+           (lazy (sprintf
+             "The type of %s is %s but it is expected to be %s" 
+               (CicPp.ppterm s) (CicPp.ppterm ty') (CicPp.ppterm ty))))
+       else
        (* The type of a LetIn is a LetIn. Extremely slow since the computed
           LetIn is later reduced and maybe also re-checked.
        (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
@@ -1567,16 +1672,16 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
           Moreover the inferred type is closer to the expected one. *)
        let ty1,ugraph2 = 
 	 type_of_aux ~logger 
-	   ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1 
+	   ((Some (n,(C.Def (s,ty))))::context) t ugraph1 
        in
-       (CicSubstitution.subst s ty1),ugraph2
+       (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2
    | C.Appl (he::tl) when List.length tl > 0 ->
        let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
        let tlbody_and_type,ugraph2 = 
 	 List.fold_right (
 	   fun x (l,ugraph) -> 
 	     let ty,ugraph1 = type_of_aux ~logger context x ugraph in
-	     let _,ugraph1 = type_of_aux ~logger  context ty ugraph1 in
+	     (*let _,ugraph1 = type_of_aux ~logger  context ty ugraph1 in*)
 	       ((x,ty)::l,ugraph1)) 
 	   tl ([],ugraph1) 
        in
@@ -1736,21 +1841,28 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
       in
 	if not b then
         raise
-          (TypeCheckerFailure (lazy ("Case analasys: sort elimination not allowed")));
+          (TypeCheckerFailure (lazy ("Case analysis: sort elimination not allowed")));
         (* let's check if the type of branches are right *)
-      let parsno =
+      let parsno,constructorsno =
         let obj,_ =
           try
             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
           with Not_found -> assert false
         in
         match obj with
-            C.InductiveDefinition (_,_,parsno,_) -> parsno
+            C.InductiveDefinition (il,_,parsno,_) ->
+             let _,_,_,cl =
+              try List.nth il i with Failure _ -> assert false
+             in
+              parsno, List.length cl
           | _ ->
               raise (TypeCheckerFailure
                 (lazy ("Unknown mutual inductive definition:" ^
                   UriManager.string_of_uri uri)))
-	in
+      in
+      if List.length pl <> constructorsno then
+       raise (TypeCheckerFailure
+        (lazy ("Wrong number of cases in case analysis"))) ;
       let (_,branches_ok,ugraph5) =
         List.fold_left
           (fun (j,b,ugraph) p ->
@@ -1802,16 +1914,14 @@ end;
           in
            outtype,ugraph5
    | C.Fix (i,fl) ->
-      let types_times_kl,ugraph1 =
-	(* WAS: list rev list map *)
+      let types,kl,ugraph1,len =
         List.fold_left
-          (fun (l,ugraph) (n,k,ty,_) ->
+          (fun (types,kl,ugraph,len) (n,k,ty,_) ->
             let _,ugraph1 = type_of_aux ~logger context ty ugraph in
-            ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1)
-	  ) ([],ugraph) fl
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              k::kl,ugraph1,len+1)
+	  ) ([],[],ugraph,0) fl
       in
-      let (types,kl) = List.split types_times_kl in
-      let len = List.length types in
       let ugraph2 = 
 	List.fold_left
           (fun ugraph (name,x,ty,bo) ->
@@ -1845,15 +1955,15 @@ end;
       let (_,_,ty,_) = List.nth fl i in
 	ty,ugraph2
    | C.CoFix (i,fl) ->
-       let types,ugraph1 =
+       let types,ugraph1,len =
 	 List.fold_left
-	   (fun (l,ugraph) (n,ty,_) -> 
+	   (fun (l,ugraph,len) (n,ty,_) -> 
               let _,ugraph1 = 
 		type_of_aux ~logger context ty ugraph in 
-		(Some (C.Name n,(C.Decl ty))::l,ugraph1)
-	   ) ([],ugraph) fl
+		(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l,
+                 ugraph1,len+1)
+	   ) ([],ugraph,0) fl
        in
-       let len = List.length types in
        let ugraph2 = 
 	 List.fold_left
            (fun ugraph (_,ty,bo) ->
@@ -1893,7 +2003,7 @@ end;
        let (_,ty,_) = List.nth fl i in
 	 ty,ugraph2
 
- and check_exp_named_subst ~logger ~subst context ugraph =
+ and check_exp_named_subst ~logger ~subst context =
    let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
      match l with
 	 [] -> ugraph
@@ -1919,7 +2029,7 @@ end;
 		 raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution"))
                end
    in
-     check_exp_named_subst_aux ~logger [] ugraph 
+     check_exp_named_subst_aux ~logger []
        
  and sort_of_prod ~subst context (name,s) (t1, t2) ugraph =
   let module C = Cic in
@@ -1933,9 +2043,12 @@ end;
     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
       (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
        let t' = CicUniv.fresh() in
-       let ugraph1 = CicUniv.add_ge t' t1 ugraph in
-       let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
-       C.Sort (C.Type t'),ugraph2
+        (try
+         let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+         let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+          C.Sort (C.Type t'),ugraph2
+        with
+         CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
     | (C.Sort _,C.Sort (C.Type t1)) -> 
         (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
         C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)
@@ -1956,6 +2069,8 @@ end;
 	 (match (CicReduction.whd ~subst context hetype) with 
               Cic.Prod (n,s,t) ->
 		let b,ugraph1 = 
+(*if (match hety,s with Cic.Sort _,Cic.Sort _ -> false | _,_ -> true) && hety <> s then(
+prerr_endline ("AAA22: " ^ CicPp.ppterm hete ^ ": " ^ CicPp.ppterm hety ^ " <==> " ^ CicPp.ppterm s); let res = CicReduction.are_convertible ~subst ~metasenv context hety s ugraph in prerr_endline "#"; res) else*)
 		  CicReduction.are_convertible 
 		    ~subst ~metasenv context hety s ugraph 
 		in	
@@ -1963,7 +2078,8 @@ end;
 		    begin
 		      CicReduction.fdebug := -1 ;
 		      eat_prods ~subst context 
-			(CicSubstitution.subst hete t) tl ugraph1
+			(CicSubstitution.subst ~avoid_beta_redexes:true hete t)
+                         tl ugraph1
 			(*TASSI: not sure *)
 		    end
 		  else
@@ -2088,6 +2204,9 @@ let typecheck_obj0 ~logger uri ugraph =
       let _,ugraph = type_of ~logger ty ugraph in
        ugraph
    | C.CurrentProof (_,conjs,te,ty,_,_) ->
+      (* this block is broken since the metasenv should 
+       * be topologically sorted before typing metas *)
+      ignore(assert false);
       let _,ugraph =
        List.fold_left
         (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
@@ -2189,3 +2308,6 @@ let check_allowed_sort_elimination uri i s1 s2 =
   ~logger:(new CicLogger.logger) [] uri i true
   (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2)
   CicUniv.empty_ugraph)
+;;
+
+Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;