X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=883bc329600be45d2decfbefc498860fe837d4f7;hb=5acff80c93b3e3df4a52ff8cb9596de46f7bd924;hp=68bbe416a698d80473851d3891761e665147480d;hpb=998a7855d00bcb55525a82138a3bfb4183d99014;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 68bbe416a..883bc3296 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;;
@@ -557,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))
@@ -666,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
@@ -741,7 +728,34 @@ and eat_lambdas ~subst context n te =
    | (n, te) ->
        raise (AssertFailure (lazy (sprintf "9 (%d, %s)" n (CicPp.ppterm te))))
 
-and check_is_really_smaller_arg ~subst context n nn kl x safes te =
+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
@@ -754,60 +768,45 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
    | C.Const _
    | C.Var _ -> false
    | C.Lambda (name,ty,ta) ->
-      check_is_really_smaller_arg ~subst (Some (name,Cic.Decl ty)::context)
-       (n+1) (nn+1) kl (x+1) (List.map (fun n -> n+1) safes) 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 | C.Appl ((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 (_,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
-                   (lefts@tys,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
-              List.for_all2
-               (fun p (_,c) ->
-                 let rl' =
-                  let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args lefts_and_tys paramsno 
-                     (len+paramsno) debrujinedte
-                 in
-                  let (e, safes',n',nn',x',context') =
-                   get_new_safes ~subst context p c rl' safes n nn x
-                  in
-                  check_is_really_smaller_arg 
-                    ~subst context' n' nn' kl x' safes' e
-               ) pl cl
+      | 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
@@ -821,16 +820,19 @@ 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 (_,_,_,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
+         ) 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 t =
+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
   match CicReduction.whd ~subst context t with
@@ -839,7 +841,7 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
       (match List.nth context (m-1) with
           Some (_,C.Decl _) -> true
         | Some (_,C.Def (bo,_)) ->
-           guarded_by_destructors ~subst context n 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"))
       )
@@ -847,36 +849,36 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
    | 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)
+        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.for_all
-       (fun (_,t) -> guarded_by_destructors ~subst context n nn kl x safes t)
+       (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
@@ -884,59 +886,44 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
         | 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 ~subst context n nn kl x safes)
+             (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes)
              tl &&
-           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
-                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
-             | _ ->
-                raise (TypeCheckerFailure
-                  (lazy ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri)))
+           let tys = 
+             specialize_inductive_type ~logger ~subst ~metasenv context t
+           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
-             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 &&
               List.for_all
-               (guarded_by_destructors ~subst context n nn kl x safes)
+               (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes)
                pl
             else
-             guarded_by_destructors ~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 outtype &&
              List.for_all2
-               (fun p (_,c) ->
-                 let rl' =
-                  let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args lefts_and_tys paramsno 
-                     (len+paramsno) debrujinedte
-                 in
-                  let (e, safes',n',nn',x',context') =
-                   get_new_safes ~subst context p c rl' safes n nn x
-                  in
-                   guarded_by_destructors ~subst context' n' nn' kl x' safes' e
+              (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.Appl (C.Fix (fixno, fl)::_) | C.Fix (fixno,fl) as t->
@@ -953,29 +940,30 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
 	  ) ([],0) fl in
        let safes' = List.map (fun x -> x + len) safes in
         List.for_all
-         (guarded_by_destructors ~subst context n nn kl x safes) l &&
+         (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 ~subst context n nn kl x_plus_len safes' ty &&
+           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 ~subst context n nn kl x safes
-             (List.nth l recno)
+            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 ~subst context (n_plus_len+recno+1)
+             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 ~subst (tys@context) n_plus_len nn_plus_len
+            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) ->
@@ -993,13 +981,13 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
         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 ~subst context n nn kl x safes t)
+       (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 *)
@@ -1793,12 +1781,33 @@ 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:"^CicPp.ppterm t)))