X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=9336cb84ab3c6e8af65624525867ee6f1b9035fc;hb=6ebe894ff0fee5d99bad615ce053128292657dee;hp=ad00c0eeb614bfc2ce958c9818386041a9fc084d;hpb=04d8e2282a3536a9b822a8dbfcbdb4e3a949f04d;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index ad00c0eeb..9336cb84a 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -54,7 +54,7 @@ let rec split l n =
       raise (TypeCheckerFailure (lazy "Parameters number < left parameters number"))
 ;;
 
-let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
+let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri number_of_types context =
  let rec aux k t =
   let module C = Cic in
   let res =
@@ -83,7 +83,7 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
        in
         C.Const (uri,exp_named_subst')
     | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' ->
-       if exp_named_subst != [] then
+       if check_exp_named_subst && exp_named_subst != [] then
         raise (TypeCheckerFailure
           (lazy ("non-empty explicit named substitution is applied to "^
            "a mutual inductive type which is being defined"))) ;
@@ -121,7 +121,7 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
    cb t res;
    res
  in
-  aux 0
+  aux (List.length context)
 ;;
 
 exception CicEnvironmentError;;
@@ -347,6 +347,10 @@ and weakly_positive context n nn uri te =
     | C.Lambda (name,so,ta) ->
        C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
         subst_inductive_type_with_dummy_mutind ta)
+    | C.LetIn (name,so,ty,ta) ->
+       C.LetIn (name, subst_inductive_type_with_dummy_mutind so,
+        subst_inductive_type_with_dummy_mutind ty,
+        subst_inductive_type_with_dummy_mutind ta)
     | C.Appl tl ->
        C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
     | C.MutCase (uri,i,outtype,term,pl) ->
@@ -369,6 +373,13 @@ and weakly_positive context n nn uri te =
          exp_named_subst
        in
         C.Const (uri,exp_named_subst')
+    | C.Var (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map
+         (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
+         exp_named_subst
+       in
+        C.Var (uri,exp_named_subst')
     | C.MutInd (uri,typeno,exp_named_subst) ->
        let exp_named_subst' =
         List.map
@@ -391,13 +402,8 @@ and weakly_positive context n nn uri te =
 *)
      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
-       (subst_inductive_type_with_dummy_mutind source) &&
-       weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
-        (n + 1) (nn + 1) uri dest
    | C.Prod (name,source,dest) when
-      does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
+      does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
        (* dummy abstraction, so we behave as in the anonimous case *)
        strictly_positive context n nn
         (subst_inductive_type_with_dummy_mutind source) &&
@@ -437,7 +443,9 @@ and strictly_positive context n nn te =
        strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
-   | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) -> 
+   | C.Appl ((C.MutInd (uri,i,exp_named_subst))::_) 
+   | (C.MutInd (uri,i,exp_named_subst)) as t -> 
+      let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
       let (ok,paramsno,ity,cl,name) =
 	let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 	  match o with
@@ -463,7 +471,6 @@ and strictly_positive context n nn te =
           List.fold_right
           (fun x i -> i && does_not_occur context n nn x)
           arguments true &&
-         (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
           List.fold_right
           (fun x i ->
              i &&
@@ -508,14 +515,8 @@ and are_all_occurrences_positive context uri indparamsno i n nn te =
         raise (TypeCheckerFailure
          (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
           UriManager.string_of_uri uri)))
-   | C.Prod (C.Anonymous,source,dest) ->
-       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
    | C.Prod (name,source,dest) when
-      does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
+      does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
       (* dummy abstraction, so we behave as in the anonimous case *)
       strictly_positive context n nn source &&
        are_all_occurrences_positive
@@ -556,7 +557,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
 	let ugraph'' = 
           List.fold_left
             (fun ugraph (name,te) -> 
-              let debrujinedte = debrujin_constructor uri len te in
+              let debrujinedte = debrujin_constructor uri len [] te in
               let augmented_term =
 		List.fold_right
 		  (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
@@ -665,58 +666,45 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph =
 
 and recursive_args context n nn te =
  let module C = Cic in
-  match CicReduction.whd context te with
-     C.Rel _ -> []
-   | C.Var _
-   | C.Meta _
-   | C.Sort _
-   | C.Implicit _
-   | C.Cast _ (*CSC ??? *) ->
-      raise (AssertFailure (lazy "3")) (* due to type-checking *)
-   | C.Prod (name,so,de) ->
-      (not (does_not_occur context n nn so)) ::
-       (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
-   | C.Lambda _
-   | C.LetIn _ ->
-      raise (AssertFailure (lazy "4")) (* due to type-checking *)
-   | C.Appl _ -> []
-   | C.Const _ -> raise (AssertFailure (lazy "5"))
-   | C.MutInd _
-   | C.MutConstruct _
-   | C.MutCase _
-   | C.Fix _
-   | C.CoFix _ -> raise (AssertFailure (lazy "6")) (* due to type-checking *)
+ match CicReduction.whd context te with
+    C.Rel _ 
+  | C.MutInd _ -> []
+  | C.Var _
+  | C.Meta _
+  | C.Sort _
+  | C.Implicit _
+  | C.Cast _ (*CSC ??? *) ->
+     raise (AssertFailure (lazy "3")) (* due to type-checking *)
+  | C.Prod (name,so,de) ->
+     (not (does_not_occur context n nn so)) ::
+      (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
+  | C.Lambda _
+  | C.LetIn _ ->
+     raise (AssertFailure (lazy "4")) (* due to type-checking *)
+  | C.Appl _ -> []
+  | C.Const _ -> raise (AssertFailure (lazy "5"))
+  | C.MutConstruct _
+  | C.MutCase _
+  | C.Fix _
+  | C.CoFix _ -> raise (AssertFailure (lazy "6")) (* due to type-checking *)
 
-and get_new_safes ~subst context p c rl safes n nn x =
+and get_new_safes ~subst context p rl safes n nn x =
  let module C = Cic in
  let module U = UriManager in
  let module R = CicReduction in
-  match (R.whd ~subst context c, R.whd ~subst context p, rl) with
-     (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
-       (* we are sure that the two sources are convertible because we *)
-       (* have just checked this. So let's go along ...               *)
-       let safes' =
-        List.map (fun x -> x + 1) safes
-       in
-        let safes'' =
-         if b then 1::safes' else safes'
-        in
-         get_new_safes ~subst ((Some (name,(C.Decl so)))::context)
-          ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
-   | (C.Prod _, (C.MutConstruct _ as e), _)
-   | (C.Prod _, (C.Rel _ as e), _)
-   | (C.MutInd _, e, [])
-   | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
-   | (c,p,l) ->
-      (* CSC: If the next exception is raised, it just means that   *)
-      (* CSC: the proof-assistant allows to use very strange things *)
-      (* CSC: as a branch of a case whose type is a Prod. In        *)
-      (* CSC: particular, this means that a new (C.Prod, x,_) case  *)
-      (* CSC: must be considered in this match. (e.g. x = MutCase)  *)
+  match R.whd ~subst context p, rl with
+   | C.Lambda (name,so,ta), b::tl ->
+       let safes = List.map (fun x -> x + 1) safes in
+       let safes = if b then 1::safes else safes in
+       get_new_safes ~subst ((Some (name,(C.Decl so)))::context)
+          ta tl safes (n+1) (nn+1) (x+1)
+   | C.MutConstruct _ as e, _
+   | (C.Rel _ as e), _
+   | e, [] -> (e,safes,n,nn,x,context)
+   | p,_::_ ->
       raise
        (AssertFailure (lazy
-         (Printf.sprintf "Get New Safes: c=%s ; p=%s"
-           (CicPp.ppterm c) (CicPp.ppterm p))))
+         (Printf.sprintf "Get New Safes: p=%s" (CicPp.ppterm p))))
 
 and split_prods ~subst context n te =
  let module C = Cic in
@@ -740,156 +728,87 @@ and eat_lambdas ~subst context n te =
    | (n, te) ->
        raise (AssertFailure (lazy (sprintf "9 (%d, %s)" n (CicPp.ppterm te))))
 
-(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) 
-and check_is_really_smaller_arg ~subst context n nn kl x safes te =
- (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
- (*CSC: cfr guarded_by_destructors                             *)
+and specialize_inductive_type ~logger ~subst ~metasenv context t = 
+  let ty,_= type_of_aux' ~logger ~subst metasenv context t CicUniv.oblivion_ugraph in
+  match CicReduction.whd ~subst context ty with
+  | Cic.MutInd (uri,_,exp) 
+  | Cic.Appl (Cic.MutInd (uri,_,exp) :: _) as ty ->
+      let args = match ty with Cic.Appl (_::tl) -> tl | _ -> [] in
+      let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
+      (match o with
+      | Cic.InductiveDefinition (tl,_,paramsno,_) ->
+          let left_args,_ = HExtlib.split_nth paramsno args in
+          List.map (fun (name, isind, arity, cl) ->
+            let arity = CicSubstitution.subst_vars exp arity in
+            let arity = instantiate_parameters left_args arity in
+            let cl =
+              List.map
+               (fun (id,ty) -> 
+                 let ty = CicSubstitution.subst_vars exp ty in
+                 id, instantiate_parameters left_args ty) 
+               cl 
+            in
+            name, isind, arity, cl)
+          tl
+      | _ -> assert false)
+  | _ -> assert false
+
+and check_is_really_smaller_arg 
+  ~logger ~metasenv ~subst rec_uri rec_uri_len context n nn kl x safes te 
+=
  let module C = Cic in
  let module U = UriManager in
+ (*CSC: we could perform beta-iota(-zeta?) immediately, and
+   delta only on-demand when it fails without *)
  match CicReduction.whd ~subst context te with
      C.Rel m when List.mem m safes -> true
-   | C.Rel _ -> false
-   | C.Var _
-   | C.Meta _
-   | C.Sort _
-   | C.Implicit _
-   | C.Cast _
-(*   | C.Cast (te,ty) ->
-      check_is_really_smaller_arg ~subst n nn kl x safes te &&
-       check_is_really_smaller_arg ~subst n nn kl x safes ty*)
-(*   | C.Prod (_,so,ta) ->
-      check_is_really_smaller_arg ~subst n nn kl x safes so &&
-       check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1)
-        (List.map (fun x -> x + 1) safes) ta*)
-   | C.Prod _ -> raise (AssertFailure (lazy "10"))
-   | C.Lambda (name,so,ta) ->
-      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,ty,ta) ->
-      check_is_really_smaller_arg ~subst context n nn kl x safes so &&
-       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 *)
-      (*CSC: solo perche' non abbiamo trovato controesempi            *)
-      check_is_really_smaller_arg ~subst context n nn kl x safes he
-   | C.Appl [] -> raise (AssertFailure (lazy "11"))
+   | C.Rel _ 
+   | C.MutConstruct _
    | C.Const _
-   | C.MutInd _ -> raise (AssertFailure (lazy "12"))
-   | C.MutConstruct _ -> false
+   | C.Var _ -> false
+   | C.Appl (he::_) ->
+        check_is_really_smaller_arg rec_uri rec_uri_len 
+          ~logger ~metasenv ~subst context n nn kl x safes he
+   | C.Lambda (name,ty,ta) ->
+      check_is_really_smaller_arg rec_uri rec_uri_len 
+        ~logger ~metasenv ~subst (Some (name,Cic.Decl ty)::context)
+        (n+1) (nn+1) kl (x+1) (List.map (fun n -> n+1) safes) ta
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match term with
-          C.Rel m when List.mem m safes || m = x ->
-           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,_) ->
-                let tys =
-                 List.map
-                  (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
-                in
-                 let (_,isinductive,_,cl) = List.nth tl i in
-                  let cl' =
-                   List.map
-                    (fun (id,ty) ->
-                      (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@lefts,List.length tl,isinductive,paramsno,cl')
-             | _ ->
-                raise (TypeCheckerFailure
-                  (lazy ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri)))
-           in
-            if not isinductive then
-              List.fold_right
-               (fun p i ->
-                 i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
-               pl true
-            else
-             let pl_and_cl =
-              try
-               List.combine pl cl
-              with
-               Invalid_argument _ ->
-                raise (TypeCheckerFailure (lazy "not enough patterns"))
-             in
-              List.fold_right
-               (fun (p,(_,c)) i ->
-                 let rl' =
-                  let debrujinedte = debrujin_constructor uri len c in
-                   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
-                  in
-                   i &&
-                   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 (lefts_and_tys,len,isinductive,paramsno,cl) =
-            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-            match o with
-               C.InductiveDefinition (tl,_,paramsno,_) ->
-                let (_,isinductive,_,cl) = List.nth tl i in
-                 let tys =
-                  List.map (fun (n,_,ty,_) ->
-                   Some(Cic.Name n,(Cic.Decl ty))) tl
-                 in
-                  let cl' =
-                   List.map
-                    (fun (id,ty) ->
-                      (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@lefts,List.length tl,isinductive,paramsno,cl')
-             | _ ->
-                raise (TypeCheckerFailure
-                  (lazy ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri)))
-           in
-            if not isinductive then
-              List.fold_right
-               (fun p i ->
-                 i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
-               pl true
-            else
-             let pl_and_cl =
-              try
-               List.combine pl cl
-              with
-               Invalid_argument _ ->
-                raise (TypeCheckerFailure (lazy "not enough patterns"))
-             in
-              (*CSC: supponiamo come prima che nessun controllo sia necessario*)
-              (*CSC: sugli argomenti di una applicazione                      *)
-              List.fold_right
-               (fun (p,(_,c)) i ->
-                 let rl' =
-                  let debrujinedte = debrujin_constructor uri len c in
-                   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
-                  in
-                   i &&
-                   check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
-               ) pl_and_cl true
+      | C.Rel m | C.Appl ((C.Rel m)::_) when List.mem m safes || m = x ->
+         let tys = 
+           specialize_inductive_type ~logger ~subst ~metasenv context term 
+         in
+         let tys_ctx = 
+           List.map (fun (name,_,ty,_) -> Some (Cic.Name name, Cic.Decl ty)) tys
+         in
+         let _,isinductive,_,cl = List.nth tys i in
+         if not isinductive then
+           List.for_all
+            (check_is_really_smaller_arg rec_uri rec_uri_len 
+              ~logger ~metasenv ~subst context n nn kl x safes)
+            pl
+         else
+           List.for_all2
+            (fun p (_,c) ->
+              let rec_params =
+               let c = 
+                 debrujin_constructor ~check_exp_named_subst:false
+                  rec_uri rec_uri_len context c in
+               let len_ctx = List.length context in
+               recursive_args (context@tys_ctx) len_ctx (len_ctx+rec_uri_len) c
+              in
+              let (e, safes',n',nn',x',context') =
+                get_new_safes ~subst context p rec_params safes n nn x
+              in
+               check_is_really_smaller_arg rec_uri rec_uri_len 
+                ~logger ~metasenv ~subst context' n' nn' kl x' safes' e
+            ) pl cl
         | _ ->
-          List.fold_right
-           (fun p i ->
-             i && check_is_really_smaller_arg ~subst context n nn kl x safes p
-           ) pl true
+          List.for_all
+           (check_is_really_smaller_arg 
+             rec_uri rec_uri_len ~logger ~metasenv ~subst 
+             context n nn kl x safes) pl
       )
    | C.Fix (_, fl) ->
       let len = List.length fl in
@@ -903,41 +822,28 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
               len+1)
 	  ) ([],0) fl
        and safes' = List.map (fun x -> x + len) safes in
-        List.fold_right
-         (fun (_,_,ty,bo) i ->
-           i &&
-            check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
+        List.for_all
+         (fun (_,_,_,bo) ->
+            check_is_really_smaller_arg 
+              rec_uri rec_uri_len ~logger ~metasenv ~subst 
+                (tys@context) n_plus_len nn_plus_len kl
              x_plus_len safes' bo
-         ) fl true
-   | C.CoFix (_, fl) ->
-      let len = List.length fl in
-       let n_plus_len = n + len
-       and nn_plus_len = nn + len
-       and x_plus_len = x + len
-       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 ->
-           i &&
-            check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
-             x_plus_len safes' bo
-         ) fl true
+         ) fl
+   | t ->
+      raise (AssertFailure (lazy ("An inhabitant of an inductive type in normal form cannot have this shape: " ^ CicPp.ppterm t)))
 
-and guarded_by_destructors ~subst context n nn kl x safes =
+and guarded_by_destructors 
+  ~logger ~metasenv ~subst rec_uri rec_uri_len context n nn kl x safes t 
+=
  let module C = Cic in
  let module U = UriManager in
-  function
+  match CicReduction.whd ~subst context t with
      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 rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes
             (CicSubstitution.lift m bo)
         | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
       )
@@ -945,186 +851,123 @@ and guarded_by_destructors ~subst context n nn kl x safes =
    | C.Sort _
    | C.Implicit _ -> true
    | C.Cast (te,ty) ->
-      guarded_by_destructors ~subst context n nn kl x safes te &&
-       guarded_by_destructors ~subst context n nn kl x safes ty
+      guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes te &&
+       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes ty
    | C.Prod (name,so,ta) ->
-      guarded_by_destructors ~subst context n nn kl x safes so &&
-       guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context)
+      guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes so &&
+       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst ((Some (name,(C.Decl so)))::context)
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.Lambda (name,so,ta) ->
-      guarded_by_destructors ~subst context n nn kl x safes so &&
-       guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context)
+      guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes so &&
+       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~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,ty,ta) ->
-      guarded_by_destructors ~subst context n nn kl x safes so &&
-       guarded_by_destructors ~subst context n nn kl x safes ty &&
-        guarded_by_destructors ~subst ((Some (name,(C.Def (so,ty))))::context)
+      guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes so &&
+       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes ty &&
+        guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~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
        else
-        List.fold_right
-         (fun param i ->
-           i && guarded_by_destructors ~subst context n nn kl x safes param
-         ) tl true &&
-         check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k)
-   | C.Appl tl ->
-      List.fold_right
-       (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
-       tl true
+        List.for_all
+         (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes) tl &&
+        check_is_really_smaller_arg 
+          rec_uri rec_uri_len 
+          ~logger ~metasenv ~subst context n nn kl x safes (List.nth tl k)
    | C.Var (_,exp_named_subst)
    | C.Const (_,exp_named_subst)
    | C.MutInd (_,_,exp_named_subst)
    | C.MutConstruct (_,_,_,exp_named_subst) ->
-      List.fold_right
-       (fun (_,t) i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
-       exp_named_subst true
+      List.for_all
+       (fun (_,t) -> guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t)
+       exp_named_subst 
    | 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 (lefts_and_tys,len,isinductive,paramsno,cl) =
-	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-            match o with
-               C.InductiveDefinition (tl,_,paramsno,_) ->
-                let len = List.length tl in
-                 let (_,isinductive,_,cl) = List.nth tl i in
-                  let tys =
-                   List.map (fun (n,_,ty,_) ->
-                    Some(Cic.Name n,(Cic.Decl ty))) tl
-                  in
-                   let cl' =
-                    List.map
-                     (fun (id,ty) ->
-                      let debrujinedty = debrujin_constructor uri len ty in
-                       (id, snd (split_prods ~subst tys paramsno ty),
-                        snd (split_prods ~subst tys paramsno debrujinedty)
-                       )) cl in
-                   let lefts =
-                    match tl with
-                       [] -> assert false
-                     | (_,_,ty,_)::_ ->
-                        fst (split_prods ~subst [] paramsno ty)
-                   in
-                    (tys@lefts,len,isinductive,paramsno,cl')
-             | _ ->
-                raise (TypeCheckerFailure
-                  (lazy ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri)))
+        | C.Rel m 
+        | C.Appl ((C.Rel m)::_) as t when List.mem m safes || m = x ->
+           let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
+           List.for_all
+             (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes)
+             tl &&
+           let tys = 
+             specialize_inductive_type ~logger ~subst ~metasenv context t
            in
-            if not isinductive then
-             guarded_by_destructors ~subst context n nn kl x safes outtype &&
-              guarded_by_destructors ~subst context n nn kl x safes term &&
-              (*CSC: manca ??? il controllo sul tipo di term? *)
-              List.fold_right
-               (fun p i ->
-                 i && guarded_by_destructors ~subst context n nn kl x safes p)
-               pl true
-            else
-             let pl_and_cl =
-              try
-               List.combine pl cl
-              with
-               Invalid_argument _ ->
-                raise (TypeCheckerFailure (lazy "not enough patterns"))
-             in
-             guarded_by_destructors ~subst context n nn kl x safes outtype &&
-              (*CSC: manca ??? il controllo sul tipo di term? *)
-              List.fold_right
-               (fun (p,(_,c,brujinedc)) i ->
-                 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
-                   i &&
-                   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 (lefts_and_tys,len,isinductive,paramsno,cl) =
-	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-            match o with
-               C.InductiveDefinition (tl,_,paramsno,_) ->
-                let (_,isinductive,_,cl) = List.nth tl i in
-                 let tys =
-                  List.map
-                   (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
-                 in
-                  let cl' =
-                   List.map
-                    (fun (id,ty) ->
-                      (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@lefts,List.length tl,isinductive,paramsno,cl')
-             | _ ->
-                raise (TypeCheckerFailure
-                  (lazy ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri)))
+           let tys_ctx = 
+             List.map 
+               (fun (name,_,ty,_) -> Some (Cic.Name name, Cic.Decl ty)) tys
            in
+           let _,isinductive,_,cl = List.nth tys i in
             if not isinductive then
-             guarded_by_destructors ~subst context n nn kl x safes outtype &&
-              guarded_by_destructors ~subst context n nn kl x safes term &&
-              (*CSC: manca ??? il controllo sul tipo di term? *)
-              List.fold_right
-               (fun p i ->
-                 i && guarded_by_destructors ~subst context n nn kl x safes p)
-               pl true
+             guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes outtype &&
+              guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes term &&
+              List.for_all
+               (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes)
+               pl
             else
-             let pl_and_cl =
-              try
-               List.combine pl cl
-              with
-               Invalid_argument _ ->
-                raise (TypeCheckerFailure (lazy "not enough patterns"))
-             in
-             guarded_by_destructors ~subst context n nn kl x safes outtype &&
-              (*CSC: manca ??? il controllo sul tipo di term? *)
-              List.fold_right
-               (fun t i ->
-                 i && guarded_by_destructors ~subst context n nn kl x safes t)
-               tl true &&
-              List.fold_right
-               (fun (p,(_,c)) i ->
-                 let rl' =
-                  let debrujinedte = debrujin_constructor uri len c in
-                   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
-                  in
-                   i &&
-                   guarded_by_destructors ~subst context' n' nn' kl x' safes' e
-               ) pl_and_cl true
+             guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes outtype &&
+             List.for_all2
+              (fun p (_,c) ->
+               let rec_params =
+                let c = 
+                 debrujin_constructor ~check_exp_named_subst:false 
+                  rec_uri rec_uri_len context c in
+                let len_ctx = List.length context in
+                recursive_args (context@tys_ctx) len_ctx (len_ctx+rec_uri_len) c
+               in
+               let (e, safes',n',nn',x',context') =
+                get_new_safes ~subst context p rec_params safes n nn x
+               in
+                guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context' n' nn' kl x' safes' e
+               ) pl cl
         | _ ->
-          guarded_by_destructors ~subst context n nn kl x safes outtype &&
-           guarded_by_destructors ~subst context n nn kl x safes term &&
+          guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes outtype &&
+           guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes term &&
            (*CSC: manca ??? il controllo sul tipo di term? *)
            List.fold_right
-            (fun p i -> i && guarded_by_destructors ~subst context n nn kl x safes p)
+            (fun p i -> i && guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes p)
             pl true
       )
-   | C.Fix (_, fl) ->
+   | C.Appl (C.Fix (fixno, fl)::_) | C.Fix (fixno,fl) as t->
+      let l = match t with C.Appl (_::tl) -> tl | _ -> [] in
       let len = List.length fl in
-       let n_plus_len = n + len
-       and nn_plus_len = nn + len
-       and x_plus_len = x + len
-       and tys,_ =
+      let n_plus_len = n + len in
+      let nn_plus_len = nn + len in
+      let x_plus_len = x + len in
+      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
-       and safes' = List.map (fun x -> x + len) safes in
-        List.fold_right
-         (fun (_,_,ty,bo) i ->
-           i && guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
-            guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl
-             x_plus_len safes' bo
-         ) fl true
+	  ) ([],0) fl in
+       let safes' = List.map (fun x -> x + len) safes in
+        List.for_all
+         (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes) l &&
+        snd (List.fold_left
+         (fun (fixno',i) (_,recno,ty,bo) ->
+           fixno'+1,
+           i &&
+           guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x_plus_len safes' ty &&
+           if
+            fixno' = fixno &&
+            List.length l > recno &&
+            (*case where the recursive argument is already really_smaller *)
+            check_is_really_smaller_arg 
+              rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes
+              (List.nth l recno)
+           then
+            let bo_without_lambdas,_,context =
+             eat_lambdas ~subst (tys@context) (recno+1) bo
+            in
+             (* we assume the formal argument to be safe *)
+             guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context (n_plus_len+recno+1)
+              (nn_plus_len+recno+1) kl (x_plus_len+recno+1)
+              (1::List.map (fun x -> x+recno+1) safes')
+              bo_without_lambdas
+           else
+            guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst (tys@context) n_plus_len nn_plus_len
+             kl x_plus_len safes' bo
+         ) (0,true) fl)
    | C.CoFix (_, fl) ->
       let len = List.length fl in
        let n_plus_len = n + len
@@ -1140,10 +983,14 @@ and guarded_by_destructors ~subst context n nn kl x safes =
         List.fold_right
          (fun (_,ty,bo) i ->
            i &&
-            guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
-            guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl
+            guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x_plus_len safes' ty &&
+            guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst (tys@context) n_plus_len nn_plus_len kl
              x_plus_len safes' bo
          ) fl true
+   | C.Appl tl ->
+      List.fold_right
+       (fun t i -> i && guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t)
+       tl true
 
 (* the boolean h means already protected *)
 (* args is the list of arguments the type of the constructor that may be *)
@@ -1647,6 +1494,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
    | 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 _,ugraph1 = type_of_aux ~logger context ty ugraph1 in
       let b,ugraph1 =
        R.are_convertible ~subst ~metasenv context ty ty' ugraph1
       in 
@@ -1935,15 +1783,36 @@ end;
 		   let (m, eaten, context') =
 		     eat_lambdas ~subst (types @ context) (x + 1) bo
 		   in
+                   let rec_uri, rec_uri_len =
+                    let he =
+                     match List.hd context' with
+                        Some (_,Cic.Decl he) -> he
+                      | _ -> assert false
+                    in
+                     match CicReduction.whd ~subst (List.tl context') he with
+                     | Cic.MutInd (uri,_,_)
+                     | Cic.Appl (Cic.MutInd (uri,_,_)::_) ->
+                         uri,
+                           (match
+                            CicEnvironment.get_obj
+                             CicUniv.oblivion_ugraph uri
+                           with
+                           | Cic.InductiveDefinition (tl,_,_,_), _ ->
+                               List.length tl
+                           | _ -> assert false)
+                     | _ -> assert false
+                   in 
 		     (*
 		       let's control the guarded by 
 		       destructors conditions D{f,k,x,M}
 		     *)
-		     if not (guarded_by_destructors ~subst context' eaten 
-			       (len + eaten) kl 1 [] m) then
+		     if not (guarded_by_destructors ~logger ~metasenv ~subst 
+                       rec_uri rec_uri_len context' eaten (len + eaten) kl 
+                       1 [] m) 
+                     then
 		       raise
 			 (TypeCheckerFailure 
-			   (lazy ("Fix: not guarded by destructors")))
+			   (lazy ("Fix: not guarded by destructors:"^CicPp.ppterm t)))
 		     else
 		       ugraph2
 		 end
@@ -2002,7 +1871,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
@@ -2028,7 +1897,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
@@ -2309,4 +2178,18 @@ let check_allowed_sort_elimination uri i s1 s2 =
   CicUniv.empty_ugraph)
 ;;
 
-Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;
+Deannotate.type_of_aux' :=
+ fun context t ->
+  ignore (
+  List.fold_right
+   (fun el context ->
+      (match el with
+          None -> ()
+        | Some (_,Cic.Decl ty) ->
+           ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph)
+        | Some (_,Cic.Def (bo,ty)) ->
+           ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph);
+           ignore (type_of_aux' [] context bo CicUniv.oblivion_ugraph));
+      el::context
+   ) context []);
+  fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;