From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 3 Apr 2008 16:16:59 +0000 (+0000)
Subject: guarded_by_destructor ported, many auxiliary functions still to be done
X-Git-Tag: make_still_working~5464
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=670911cb7c47a0deaf69b11bbaec4946b3f8e6c6;p=helm.git

guarded_by_destructor ported, many auxiliary functions still to be done
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index fd7e756ce..4679de20a 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -14,79 +14,13 @@
 exception TypeCheckerFailure of string Lazy.t
 exception AssertFailure of string Lazy.t
 
+let shift_k e (c,rf,x,safes) =
+  e::c,List.map (fun (k,v) -> k+1,v) rf,x+1,List.map ((+)1) safes
+;;
+
 (* $Id: cicTypeChecker.ml 8213 2008-03-13 18:48:26Z sacerdot $ *)
 
 (*
-let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
- let rec aux k t =
-  let module C = Cic in
-  let res =
-   match t with
-      C.Rel n as t when n <= k -> t
-    | C.Rel _ ->
-        raise (TypeCheckerFailure (lazy "unbound variable found in constructor type"))
-    | C.Var (uri,exp_named_subst) ->
-       let exp_named_subst' = 
-        List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
-       in
-        C.Var (uri,exp_named_subst')
-    | C.Meta (i,l) ->
-       let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in
-        C.Meta (i,l')
-    | C.Sort _
-    | C.Implicit _ as t -> t
-    | 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,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' = 
-        List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
-       in
-        C.Const (uri,exp_named_subst')
-    | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' ->
-       if exp_named_subst != [] then
-        raise (TypeCheckerFailure
-          (lazy ("non-empty explicit named substitution is applied to "^
-           "a mutual inductive type which is being defined"))) ;
-       C.Rel (k + number_of_types - tyno) ;
-    | C.MutInd (uri',tyno,exp_named_subst) ->
-       let exp_named_subst' = 
-        List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
-       in
-        C.MutInd (uri',tyno,exp_named_subst')
-    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
-       let exp_named_subst' = 
-        List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
-       in
-        C.MutConstruct (uri,tyno,consno,exp_named_subst')
-    | C.MutCase (sp,i,outty,t,pl) ->
-       C.MutCase (sp, i, aux k outty, aux k t,
-        List.map (aux k) pl)
-    | C.Fix (i, fl) ->
-       let len = List.length fl in
-       let liftedfl =
-        List.map
-         (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo))
-          fl
-       in
-        C.Fix (i, liftedfl)
-    | C.CoFix (i, fl) ->
-       let len = List.length fl in
-       let liftedfl =
-        List.map
-         (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo))
-          fl
-       in
-        C.CoFix (i, liftedfl)
-  in
-   cb t res;
-   res
- in
-  aux 0
-;;
-
 exception CicEnvironmentError;;
 
 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
@@ -323,18 +257,18 @@ 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 debruijnedte = debruijn_constructor uri len te in
               let augmented_term =
                 List.fold_right
                   (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
-                  itl debrujinedte
+                  itl debruijnedte
               in
               let _,ugraph' = type_of ~logger augmented_term ugraph in
               (* let's check also the positivity conditions *)
               if
                 not
                   (are_all_occurrences_positive tys uri indparamsno i 0 len
-                     debrujinedte)
+                     debruijnedte)
               then
                 begin
                 prerr_endline (UriManager.string_of_uri uri);
@@ -361,490 +295,6 @@ and check_mutual_inductive_defs uri obj ugraph =
                 lazy ("Unknown mutual inductive definition:" ^
                  UriManager.string_of_uri uri)))
 
-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 *)
-
-and get_new_safes ~subst context p c 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)  *)
-      raise
-       (AssertFailure (lazy
-         (Printf.sprintf "Get New Safes: c=%s ; p=%s"
-           (CicPp.ppterm c) (CicPp.ppterm p))))
-
-and split_prods ~subst context n te =
- let module C = Cic in
- let module R = CicReduction in
-  match (n, R.whd ~subst context te) with
-     (0, _) -> context,te
-   | (n, C.Prod (name,so,ta)) when n > 0 ->
-       split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
-   | (_, _) -> raise (AssertFailure (lazy "8"))
-
-and eat_lambdas ~subst context n te =
- let module C = Cic in
- let module R = CicReduction in
-  match (n, R.whd ~subst context te) with
-     (0, _) -> (te, 0, context)
-   | (n, C.Lambda (name,so,ta)) when n > 0 ->
-      let (te, k, context') =
-       eat_lambdas ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
-      in
-       (te, k + 1, context')
-   | (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                             *)
- let module C = Cic in
- let module U = UriManager in
- 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.Const _
-   | C.MutInd _ -> raise (AssertFailure (lazy "12"))
-   | C.MutConstruct _ -> false
-   | 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
-              (*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.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
-        | _ ->
-          List.fold_right
-           (fun p i ->
-             i && check_is_really_smaller_arg ~subst context n nn kl x safes p
-           ) pl true
-      )
-   | C.Fix (_, 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
-   | 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
-
-and guarded_by_destructors ~subst context n nn kl x safes =
- let module C = Cic in
- let module U = UriManager in
-  function
-     C.Rel m when m > n && m <= nn -> false
-   | C.Rel m ->
-      (match List.nth context (n-1) with
-          Some (_,C.Decl _) -> true
-        | Some (_,C.Def (bo,_)) ->
-           guarded_by_destructors ~subst context m nn kl x safes
-            (CicSubstitution.lift m bo)
-        | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
-      )
-   | C.Meta _
-   | 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
-   | 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)
-        (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)
-        (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)
-         (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
-   | 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
-   | 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)))
-           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)))
-           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 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 ~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
-      )
-   | C.Fix (_, 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 && 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
-   | 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 &&
-            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
-
 (* the boolean h means already protected *)
 (* args is the list of arguments the type of the constructor that may be *)
 (* found in head position must be applied to.                            *)
@@ -1129,45 +579,117 @@ and type_of_branch ~subst context argsno need_dummy outtype term constype =
     | _ -> None
 
  in
-  type_of_aux ~logger context t ugraph
-
-;;
-
-(** wrappers which instantiate fresh loggers *)
-
-(* check_allowed_sort_elimination uri i s1 s2
-   This function is used outside the kernel to determine in advance whether
-   a MutCase will be allowed or not.
-   [uri,i] is the type of the term to match
-   [s1] is the sort of the term to eliminate (i.e. the head of the arity
-        of the inductive type [uri,i])
-   [s2] is the sort of the goal (i.e. the head of the type of the outtype
-        of the MutCase) *)
-let check_allowed_sort_elimination uri i s1 s2 =
- fst (check_allowed_sort_elimination ~subst:[] ~metasenv:[]
-  ~logger:(new CicLogger.logger) [] uri i true
-  (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2)
-  CicUniv.empty_ugraph)
+  type_of_aux ~logger context t ugraph
+
+;;
+
+(** wrappers which instantiate fresh loggers *)
+
+(* check_allowed_sort_elimination uri i s1 s2
+   This function is used outside the kernel to determine in advance whether
+   a MutCase will be allowed or not.
+   [uri,i] is the type of the term to match
+   [s1] is the sort of the term to eliminate (i.e. the head of the arity
+        of the inductive type [uri,i])
+   [s2] is the sort of the goal (i.e. the head of the type of the outtype
+        of the MutCase) *)
+let check_allowed_sort_elimination uri i s1 s2 =
+ fst (check_allowed_sort_elimination ~subst:[] ~metasenv:[]
+  ~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);;
+
+*)
+
+module C = NCic 
+module R = NCicReduction
+module Ref = NReference
+module S = NCicSubstitution 
+module U = NCicUtils
+module E = NCicEnvironment
+
+let rec split_prods ~subst context n te =
+  match (n, R.whd ~subst context te) with
+   | (0, _) -> context,te
+   | (n, C.Prod (name,so,ta)) when n > 0 ->
+       split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta
+   | (_, _) -> raise (AssertFailure (lazy "split_prods"))
+;;
+
+let debruijn_constructor ?(cb=fun _ _ -> ()) uri number_of_types t = assert false
+(*
+ let rec aux k t =
+  let module C = Cic in
+  let res =
+   match t with
+      C.Rel n as t when n <= k -> t
+    | C.Rel _ ->
+        raise (TypeCheckerFailure (lazy "unbound variable found in constructor type"))
+    | C.Var (uri,exp_named_subst) ->
+       let exp_named_subst' = 
+        List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
+       in
+        C.Var (uri,exp_named_subst')
+    | C.Meta (i,l) ->
+       let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in
+        C.Meta (i,l')
+    | C.Sort _
+    | C.Implicit _ as t -> t
+    | 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,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' = 
+        List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
+       in
+        C.Const (uri,exp_named_subst')
+    | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' ->
+       if exp_named_subst != [] then
+        raise (TypeCheckerFailure
+          (lazy ("non-empty explicit named substitution is applied to "^
+           "a mutual inductive type which is being defined"))) ;
+       C.Rel (k + number_of_types - tyno) ;
+    | C.MutInd (uri',tyno,exp_named_subst) ->
+       let exp_named_subst' = 
+        List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
+       in
+        C.MutInd (uri',tyno,exp_named_subst')
+    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+       let exp_named_subst' = 
+        List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
+       in
+        C.MutConstruct (uri,tyno,consno,exp_named_subst')
+    | C.MutCase (sp,i,outty,t,pl) ->
+       C.MutCase (sp, i, aux k outty, aux k t,
+        List.map (aux k) pl)
+    | C.Fix (i, fl) ->
+       let len = List.length fl in
+       let liftedfl =
+        List.map
+         (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo))
+          fl
+       in
+        C.Fix (i, liftedfl)
+    | C.CoFix (i, fl) ->
+       let len = List.length fl in
+       let liftedfl =
+        List.map
+         (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo))
+          fl
+       in
+        C.CoFix (i, liftedfl)
+  in
+   cb t res;
+   res
+ in
+  aux 0*)
 ;;
 
-Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;
-
-*)
-
-module C = NCic 
-module R = NCicReduction
-module Ref = NReference
-module S = NCicSubstitution 
-module U = NCicUtils
-module E = NCicEnvironment
-
-let rec split_prods ~subst context n te =
-  match (n, R.whd ~subst context te) with
-   | (0, _) -> context,te
-   | (n, C.Prod (name,so,ta)) when n > 0 ->
-       split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta
-   | (_, _) -> raise (AssertFailure (lazy "split_prods"))
-;;
 
 let sort_of_prod ~subst context (name,s) (t1, t2) =
    let t1 = R.whd ~subst context t1 in
@@ -1209,6 +731,22 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty =
     aux ty_he args_with_ty
 ;;
 
+let fix_lefts_in_constrs ~subst paramsno tyl i =
+  let len = List.length tyl in
+  let _,_,arity,cl = List.nth tyl i in
+  let tys = List.map (fun (_,n,ty,_) -> n,C.Decl ty) tyl in
+  let cl' =
+   List.map
+    (fun (_,id,ty) ->
+      let debruijnedty = debruijn_constructor ref len ty in
+      id, snd (split_prods ~subst tys paramsno ty),
+       snd (split_prods ~subst tys paramsno debruijnedty))
+    cl 
+  in
+  let lefts = fst (split_prods ~subst [] paramsno arity) in
+  tys@lefts, len, cl'
+;;
+
 exception DoesOccur;;
 
 let does_not_occur ~subst context n nn t = 
@@ -1233,6 +771,8 @@ let does_not_occur ~subst context n nn t =
    with DoesOccur -> false
 ;;
 
+exception NotGuarded;;
+
 let rec typeof ~subst ~metasenv context term =
   let rec typeof_aux context = function
     | C.Rel n ->
@@ -1506,9 +1046,312 @@ let rec typeof ~subst ~metasenv context term =
    typeof_aux context term
 
 and check_mutual_inductive_defs _ = assert false
-and eat_lambdas ~subst _ _ _ = assert false
+
+and eat_lambdas ~subst context n te =
+  match (n, R.whd ~subst context te) with
+  | (0, _) -> (te, context)
+  | (n, C.Lambda (name,so,ta)) when n > 0 ->
+      eat_lambdas ~subst ((name,(C.Decl so))::context) (n - 1) ta
+   | (n, te) ->
+      raise (AssertFailure 
+        (lazy (Printf.sprintf "9 (%d, %s)" n (NCicPp.ppterm te))))
+
+and guarded_by_destructors ~subst context recfuns t = 
+ let recursor f k t = NCicUtils.fold shift_k k (fun k () -> f k) () t in
+ let rec aux (context, recfuns, x, safes as k) = function
+  | C.Rel m when List.mem_assoc m recfuns -> raise NotGuarded 
+  | C.Rel m ->
+     (match List.nth context (m-1) with 
+     | _,C.Decl _ -> ()
+     | _,C.Def (bo,_) -> aux (context, recfuns, x, safes) (S.lift m bo))
+  | C.Meta _ -> ()
+  | C.Appl ((C.Rel m)::tl) when List.mem_assoc m recfuns ->
+     let rec_no = List.assoc m recfuns in
+     if not (List.length tl > rec_no) then raise NotGuarded
+     else
+       let rec_arg = List.nth tl rec_no in
+       aux k rec_arg;
+       List.iter (aux k) tl
+  | C.Match (ref,outtype,term,pl) as t ->
+     (match R.whd ~subst context term with
+     | C.Rel m | C.Appl (C.Rel m :: _ ) as t when List.mem m safes || m = x ->
+        let isinductive, paramsno, tl, _, i = E.get_checked_indtys ref in
+        if not isinductive then recursor aux k t
+        else
+         let lefts_and_tys,len,cl = fix_lefts_in_constrs ~subst paramsno tl i in
+         let args = match t with C.Appl (_::tl) -> tl | _ -> [] in
+         aux k outtype; 
+         List.iter (aux k) args; 
+         List.iter2
+           (fun p (_,c,bruijnedc) ->
+             let rl = recursive_args ~subst lefts_and_tys 0 len bruijnedc in
+             let p, k = get_new_safes ~subst k p rl in
+             aux k p) 
+           pl cl
+     | _ -> recursor aux k t)
+  | t -> recursor aux k t
+ in
+  try aux (context, recfuns, 1, []) t;true
+  with NotGuarded -> false
+
+(*
+ | C.Fix (_, 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 && 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
+ | 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 &&
+          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
+*)
+
 and guarded_by_constructors ~subst _ _ _ _ _ _ _ = assert false
-and guarded_by_destructors ~subst _ _ _ _ _ _ _ = assert false
+
+and recursive_args ~subst context n nn te =
+  match R.whd context te with
+  | C.Rel _ -> []
+  | C.Prod (name,so,de) ->
+     (not (does_not_occur ~subst context n nn so)) ::
+      (recursive_args ~subst ((name,(C.Decl so))::context) (n+1) (nn + 1) de)
+  | _ -> raise (AssertFailure (lazy ("recursive_args")))
+
+and get_new_safes ~subst (context, recfuns, x, safes as k) p rl =
+  match R.whd ~subst context p, rl with
+  | C.Lambda (name,so,ta), b::tl ->
+      let safes = (if b then [0] else []) @ safes in
+      get_new_safes ~subst 
+        (shift_k (name,(C.Decl so)) (context, recfuns, x, safes)) ta tl
+  | C.Meta _ as e, _ | e, [] -> e, k
+  | _ -> raise (AssertFailure (lazy "Ill formed pattern"))
+
+and split_prods ~subst context n te =
+  match n, R.whd ~subst context te with
+  | 0, _ -> context,te
+  | n, C.Prod (name,so,ta) when n > 0 ->
+       split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta
+  | _ -> raise (AssertFailure (lazy "split_prods"))
+
+(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) 
+and check_is_really_smaller_arg ~subst context n nn kl x safes te =
+assert false        (*
+ (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
+ (*CSC: cfr guarded_by_destructors                             *)
+ let module C = Cic in
+ let module U = UriManager in
+ 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.Const _
+   | C.MutInd _ -> raise (AssertFailure (lazy "12"))
+   | C.MutConstruct _ -> false
+   | 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
+              (*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 debruijnedte = debruijn_constructor uri len c in
+                   recursive_args lefts_and_tys 0 len debruijnedte
+                 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 debruijnedte = debruijn_constructor uri len c in
+                   recursive_args lefts_and_tys 0 len debruijnedte
+                 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
+        | _ ->
+          List.fold_right
+           (fun p i ->
+             i && check_is_really_smaller_arg ~subst context n nn kl x safes p
+           ) pl true
+      )
+   | C.Fix (_, 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
+   | 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
+         *)
+
 and returns_a_coinductive ~subst _ _ = assert false
 
 and type_of_constant ref = assert false (* USARE typecheck_obj0 *)
@@ -1576,9 +1419,9 @@ and typecheck_obj0 (uri,height,metasenv,subst,kind) =
    | C.Fixpoint (inductive,fl,_) ->
       let types,kl,len =
         List.fold_left
-         (fun (types,kl,len) (_,n,k,ty,_) ->
+         (fun (types,kl,len) (_,name,k,ty,_) ->
            let _ = typeof ~subst ~metasenv [] ty in
-            ((n,(C.Decl (S.lift len ty)))::types, k::kl,len+1)
+            ((name,(C.Decl (S.lift len ty)))::types, k::kl,len+1)
          ) ([],[],0) fl
       in
         List.iter (fun (_,name,x,ty,bo) ->
@@ -1587,13 +1430,13 @@ and typecheck_obj0 (uri,height,metasenv,subst,kind) =
          then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies")))
          else
           if inductive then begin
-            let m, eaten, context =
-              eat_lambdas ~subst types (x + 1) bo
+            let m, context = eat_lambdas ~subst types (x + 1) bo in
+            (* guarded by destructors conditions D{f,k,x,M} *)
+            let rec enum_from k = 
+              function [] -> [] | v::tl -> (k,v)::enum_from (k+1) tl 
             in
-             (* 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 
+                      ~subst context (enum_from (x+1) kl) m) then
               raise(TypeCheckerFailure(lazy("Fix: not guarded by destructors")))
           end else
            match returns_a_coinductive ~subst [] ty with