X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=7e9cd70b206dcde2d7fe22ab6fb4044b775c7ca5;hb=30704126796b07213d6da3ca25156d82e761d554;hp=0299df7a76edd12ff5bfda7ba9ab1aff28207e2e;hpb=7bf119d0c9d56ca0cb75c448beebf57bba7c8c6e;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 0299df7a7..7e9cd70b2 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -11,168 +11,26 @@
 
 (* $Id: nCicReduction.ml 8250 2008-03-25 17:56:20Z tassi $ *)
 
+(* web interface stuff *)
+
+let logger = 
+  ref (function (`Start_type_checking _|`Type_checking_completed _) -> ())
+;;
+
+let set_logger f = logger := f;;
+
 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;;
 
-and does_not_occur ?(subst=[]) context n nn te =
- let module C = Cic in
-   match te with
-      C.Rel m when m > n && m <= nn -> false
-    | C.Rel m ->
-       (try
-         (match List.nth context (m-1) with
-             Some (_,C.Def (bo,_)) ->
-              does_not_occur ~subst context n nn (CicSubstitution.lift m bo)
-           | _ -> true)
-        with
-         Failure _ -> assert false)
-    | C.Sort _
-    | C.Implicit _ -> true
-    | C.Meta (_,l) ->
-       List.fold_right
-        (fun x i ->
-          match x with
-             None -> i
-           | Some x -> i && does_not_occur ~subst context n nn x) l true &&
-       (try
-         let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
-          does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term)
-        with
-         CicUtil.Subst_not_found _ -> true)
-    | C.Cast (te,ty) ->
-       does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty
-    | C.Prod (name,so,dest) ->
-       does_not_occur ~subst context n nn so &&
-        does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1)
-         (nn + 1) dest
-    | C.Lambda (name,so,dest) ->
-       does_not_occur ~subst context n nn so &&
-        does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
-         dest
-    | C.LetIn (name,so,ty,dest) ->
-       does_not_occur ~subst context n nn so &&
-        does_not_occur ~subst context n nn ty &&
-         does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context)
-          (n + 1) (nn + 1) dest
-    | C.Appl l ->
-       List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
-    | C.Var (_,exp_named_subst)
-    | C.Const (_,exp_named_subst)
-    | C.MutInd (_,_,exp_named_subst)
-    | C.MutConstruct (_,_,_,exp_named_subst) ->
-       List.fold_right (fun (_,x) i -> i && does_not_occur ~subst context n nn x)
-        exp_named_subst true
-    | C.MutCase (_,_,out,te,pl) ->
-       does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te &&
-        List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) pl true
-    | C.Fix (_,fl) ->
-       let len = List.length fl in
-        let n_plus_len = n + len in
-        let nn_plus_len = nn + 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
-        in
-         List.fold_right
-          (fun (_,_,ty,bo) i ->
-            i && does_not_occur ~subst context n nn ty &&
-            does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo
-          ) fl true
-    | C.CoFix (_,fl) ->
-       let len = List.length fl in
-        let n_plus_len = n + len in
-        let nn_plus_len = nn + 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
-        in
-         List.fold_right
-          (fun (_,ty,bo) i ->
-            i && does_not_occur ~subst context n nn ty &&
-            does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo
-          ) fl true
-
 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla  *)
@@ -407,18 +265,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 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);
@@ -445,488 +303,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
-              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.                            *)
@@ -1149,67 +525,6 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
              args coInductiveTypeURI
          ) fl true
 
-and type_of_branch ~subst context argsno need_dummy outtype term constype =
- let module C = Cic in
- let module R = CicReduction in
-  match R.whd ~subst context constype with
-     C.MutInd (_,_,_) ->
-      if need_dummy then
-       outtype
-      else
-       C.Appl [outtype ; term]
-   | C.Appl (C.MutInd (_,_,_)::tl) ->
-      let (_,arguments) = split tl argsno
-      in
-       if need_dummy && arguments = [] then
-        outtype
-       else
-        C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
-   | C.Prod (name,so,de) ->
-      let term' =
-       match CicSubstitution.lift 1 term with
-          C.Appl l -> C.Appl (l@[C.Rel 1])
-        | t -> C.Appl [t ; C.Rel 1]
-      in
-       C.Prod (name,so,type_of_branch ~subst
-        ((Some (name,(C.Decl so)))::context) argsno need_dummy
-        (CicSubstitution.lift 1 outtype) term' de)
-   | _ -> raise (AssertFailure (lazy "20"))
-
- and returns_a_coinductive ~subst context ty =
-  let module C = Cic in
-   match CicReduction.whd ~subst context ty with
-      C.MutInd (uri,i,_) ->
-       (*CSC: definire una funzioncina per questo codice sempre replicato *)
-        let obj,_ =
-          try
-            CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
-          with Not_found -> assert false
-        in
-        (match obj with
-           C.InductiveDefinition (itl,_,_,_) ->
-            let (_,is_inductive,_,_) = List.nth itl i in
-             if is_inductive then None else (Some uri)
-         | _ ->
-            raise (TypeCheckerFailure
-              (lazy ("Unknown mutual inductive definition:" ^
-              UriManager.string_of_uri uri)))
-        )
-    | C.Appl ((C.MutInd (uri,i,_))::_) ->
-       (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-         match o with
-           C.InductiveDefinition (itl,_,_,_) ->
-            let (_,is_inductive,_,_) = List.nth itl i in
-             if is_inductive then None else (Some uri)
-         | _ ->
-            raise (TypeCheckerFailure
-              (lazy ("Unknown mutual inductive definition:" ^
-              UriManager.string_of_uri uri)))
-        )
-    | C.Prod (n,so,de) ->
-       returns_a_coinductive ~subst ((Some (n,C.Decl so))::context) de
-    | _ -> None
-
  in
   type_of_aux ~logger context t ugraph
 
@@ -1251,6 +566,24 @@ let rec split_prods ~subst context n te =
    | (_, _) -> raise (AssertFailure (lazy "split_prods"))
 ;;
 
+let debruijn ?(cb=fun _ _ -> ()) uri number_of_types = 
+ let rec aux k t =
+  let res =
+   match t with
+    | C.Meta (i,(s,C.Ctx l)) ->
+       let l1 = NCicUtils.sharing_map (aux (k-s)) l in
+       if l1 == l then t else C.Meta (i,(s,C.Ctx l1))
+    | C.Meta _ -> t
+    | C.Const (Ref.Ref (_,uri1,(Ref.Fix (no,_) | Ref.CoFix no))) 
+    | C.Const (Ref.Ref (_,uri1,Ref.Ind no)) when NUri.eq uri uri1 ->
+       C.Rel (k + number_of_types - no)
+    | t -> NCicUtils.map (fun _ k -> k+1) k aux t
+  in
+   cb t res; res
+ in
+  aux 0
+;;
+
 let sort_of_prod ~subst context (name,s) (t1, t2) =
    let t1 = R.whd ~subst context t1 in
    let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in
@@ -1275,6 +608,11 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty =
   | (arg, ty_arg)::tl ->
       (match R.whd ~subst context ty_he with 
       | C.Prod (n,s,t) ->
+(*
+          prerr_endline (NCicPp.ppterm ~context s ^ " - Vs - " ^ NCicPp.ppterm
+          ~context ty_arg);
+          prerr_endline (NCicPp.ppterm ~context (S.subst ~avoid_beta_redexes:true arg t));
+*)
           if R.are_convertible ~subst ~metasenv context ty_arg s then
             aux (S.subst ~avoid_beta_redexes:true arg t) tl
           else
@@ -1291,8 +629,52 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty =
     aux ty_he args_with_ty
 ;;
 
+let fix_lefts_in_constrs ~subst uri 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 uri 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 = 
+  let rec aux (context,n,nn as k) _ = function
+    | C.Rel m when m > n && m <= nn -> raise DoesOccur
+    | C.Rel m ->
+        (try (match List.nth context (m-1) with
+          | _,C.Def (bo,_) -> aux k () (S.lift m bo)
+          | _ -> ())
+         with Failure _ -> assert false)
+    | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
+    | C.Meta (mno,(s,l)) ->
+         (try
+           let _,_,term,_ = U.lookup_subst mno subst in
+           aux (context,n+s,nn+s) () (S.subst_meta (0,l) term)
+          with CicUtil.Subst_not_found _ -> match l with
+          | C.Irl len -> if not (n >= s+len || s > nn) then raise DoesOccur
+          | C.Ctx lc -> List.iter (aux (context,n+s,nn+s) ()) lc)
+    | t -> U.fold (fun e (ctx,n,nn) -> (e::ctx,n+1,nn+1)) k aux () t
+  in
+   try aux (context,n,nn) () t; true
+   with DoesOccur -> false
+;;
+
+exception NotGuarded of string Lazy.t;;
+
 let rec typeof ~subst ~metasenv context term =
-  let rec typeof_aux context = function
+  let rec typeof_aux context = 
+    fun t -> (*prerr_endline (NCicPp.ppterm ~context t); *)
+    match t with
     | C.Rel n ->
        (try
          match List.nth context (n - 1) with
@@ -1305,10 +687,10 @@ let rec typeof ~subst ~metasenv context term =
     | C.Meta (n,l) as t -> 
        let canonical_context,ty =
         try
-         let _,c,_,ty = NCicUtils.lookup_subst n subst in c,ty
-        with NCicUtils.Subst_not_found _ -> try
-         let _,_,c,ty = NCicUtils.lookup_meta n metasenv in c,ty
-        with NCicUtils.Meta_not_found _ ->
+         let _,c,_,ty = U.lookup_subst n subst in c,ty
+        with U.Subst_not_found _ -> try
+         let _,_,c,ty = U.lookup_meta n metasenv in c,ty
+        with U.Meta_not_found _ ->
          raise (AssertFailure (lazy (Printf.sprintf
           "%s not found" (NCicPp.ppterm t))))
        in
@@ -1345,9 +727,16 @@ let rec typeof ~subst ~metasenv context term =
     | C.Appl (he::(_::_ as args)) ->
        let ty_he = typeof_aux context he in
        let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in
+(*
+       prerr_endline ("HEAD: " ^ NCicPp.ppterm ~context ty_he);
+       prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
+       ~context) (List.map snd args_with_ty)));
+       prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
+       ~context) (List.map fst args_with_ty)));
+*)
        eat_prods ~subst ~metasenv context ty_he args_with_ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
-   | C.Match (Ref.Ref (dummy_depth,uri,Ref.Ind tyno) as r,outtype,term,pl) ->
+   | C.Match (Ref.Ref (_,_,Ref.Ind tyno) as r,outtype,term,pl) ->
       let outsort = typeof_aux context outtype in
       let leftno = E.get_indty_leftno r in
       let parameters, arguments =
@@ -1390,35 +779,54 @@ let rec typeof ~subst ~metasenv context term =
       in
       if List.length pl <> constructorsno then
        raise (TypeCheckerFailure (lazy ("Wrong number of cases in a match")));
-      let j,branches_ok =
+      let j,branches_ok,p_ty, exp_p_ty =
         List.fold_left
-          (fun (j,b) p ->
+          (fun (j,b,old_p_ty,old_exp_p_ty) p ->
             if b then
               let cons = 
-                let cons = Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)) in
+                let cons = Ref.mk_constructor j r in
                 if parameters = [] then C.Const cons
                 else C.Appl (C.Const cons::parameters)
               in
               let ty_p = typeof_aux context p in
               let ty_cons = typeof_aux context cons in
               let ty_branch = 
-                type_of_branch ~subst context leftno outtype cons ty_cons in
-              j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch 
+                type_of_branch ~subst context leftno outtype cons ty_cons 0 
+              in
+              j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch,
+              ty_p, ty_branch
             else
-              j,false
-          ) (1,true) pl
-         in
-          if not branches_ok then
-           raise
-            (TypeCheckerFailure 
-              (lazy (Printf.sprintf "Branch for constructor %s has wrong type"
-              (NCicPp.ppterm (C.Const 
-                (Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)))))))); 
-          let res = outtype::arguments@[term] in
-          R.head_beta_reduce (C.Appl res)
+              j,false,old_p_ty,old_exp_p_ty
+          ) (1,true,C.Sort C.Prop,C.Sort C.Prop) pl
+      in
+      if not branches_ok then
+        raise
+         (TypeCheckerFailure 
+          (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^
+          "has type %s\nnot convertible with %s") (NCicPp.ppterm (C.Const 
+          (Ref.mk_constructor j r)))
+          (NCicPp.ppterm ~context (List.nth pl (j-1)))
+          (NCicPp.ppterm ~context p_ty) (NCicPp.ppterm ~context exp_p_ty)))); 
+      let res = outtype::arguments@[term] in
+      R.head_beta_reduce (C.Appl res)
     | C.Match _ -> assert false
 
-  and type_of_branch ~subst context leftno outty cons tycons = assert false
+  and type_of_branch ~subst context leftno outty cons tycons liftno = 
+    match R.whd ~subst context tycons with
+    | C.Const (Ref.Ref (_,_,Ref.Ind _)) -> C.Appl [S.lift liftno outty ; cons]
+    | C.Appl (C.Const (Ref.Ref (_,_,Ref.Ind _))::tl) ->
+        let _,arguments = HExtlib.split_nth leftno tl in
+        C.Appl (S.lift liftno outty::arguments@[cons])
+    | C.Prod (name,so,de) ->
+        let cons =
+         match S.lift 1 cons with
+         | C.Appl l -> C.Appl (l@[C.Rel 1])
+         | t -> C.Appl [t ; C.Rel 1]
+        in
+         C.Prod (name,so,
+           type_of_branch ~subst ((name,(C.Decl so))::context) 
+            leftno outty cons de (liftno+1))
+    | _ -> raise (AssertFailure (lazy "type_of_branch"))
 
   (* check_metasenv_consistency checks that the "canonical" context of a
      metavariable is consitent - up to relocation via the relocation list l -
@@ -1473,7 +881,7 @@ let rec typeof ~subst ~metasenv context term =
                           S.subst_meta l (S.lift i ty)))::(lift_metas (i+1) tl)
          in
           lift_metas 1 canonical_context in
-       let l = NCicUtils.expand_local_context lc_kind in
+       let l = U.expand_local_context lc_kind in
        try
         List.iter2 
         (fun t ct -> 
@@ -1505,10 +913,10 @@ let rec typeof ~subst ~metasenv context term =
               let type_t = typeof_aux context t in
               if not (R.are_convertible ~subst ~metasenv context type_t ct) then
                 raise (TypeCheckerFailure 
-                  (lazy (Printf.sprintf 
-                   ("Not well typed metavariable local context: "^^
-                    "expected a term of type %s, found %s of type %s") 
-                    (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t))))
+                 (lazy (Printf.sprintf 
+                  ("Not well typed metavariable local context: "^^
+                  "expected a term of type %s, found %s of type %s") 
+                  (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t))))
         ) l lifted_canonical_context 
        with
         Invalid_argument _ ->
@@ -1563,190 +971,267 @@ let rec typeof ~subst ~metasenv context term =
  in 
    typeof_aux context term
 
-and type_of_constant ref = assert false (* USARE typecheck_obj0 *)
-(* ALIAS typecheck *)
+and check_mutual_inductive_defs _ = ()
+
+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 as t when List.mem_assoc m recfuns -> 
+      raise (NotGuarded (lazy (NCicPp.ppterm ~context t ^ " passed around")))
+  | 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) as t when List.mem_assoc m recfuns ->
+     let rec_no = List.assoc m recfuns in
+     if not (List.length tl > rec_no) then 
+       raise (NotGuarded (lazy 
+         (NCicPp.ppterm ~context ~subst t ^ 
+         " is a partial application of a fix")))
+     else
+       let rec_arg = List.nth tl rec_no in
+       if not (is_really_smaller ~subst k rec_arg) then 
+         raise (NotGuarded (lazy 
+           (NCicPp.ppterm ~context ~subst rec_arg ^ " not smaller")));
+       List.iter (aux k) tl
+  | C.Match (Ref.Ref (_,uri,_) as 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 c_ctx,len,cl = fix_lefts_in_constrs ~subst uri 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 (_,_,bruijnedc) ->
+             let rl = recursive_args ~subst c_ctx 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
+  with NotGuarded s -> raise (TypeCheckerFailure s)
+
 (*
-  let cobj,ugraph1 =
-   match CicEnvironment.is_type_checked ~trust:true ugraph uri with
-       CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
-     | CicEnvironment.UncheckedObj uobj ->
-         logger#log (`Start_type_checking uri) ;
-         let ugraph1_dust =
-          typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in
-           try 
-             CicEnvironment.set_type_checking_info uri ;
-             logger#log (`Type_checking_completed uri) ;
-             (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
-                  CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
-                | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
-             )
-           with
-            (*
-              this is raised if set_type_checking_info is called on an object
-              that has no associated universe file. If we are in univ_maker 
-              phase this is OK since univ_maker will properly commit the 
-              object.
-            *)
-               Invalid_argument s ->
-                 (*debug_print (lazy s);*)
-                 uobj,ugraph1_dust
-  in
-CASO COSTRUTTORE
-    match cobj with
-        C.InductiveDefinition (dl,_,_,_) ->
-          let (_,_,arity,_) = List.nth dl i in
-            arity,ugraph1
-      | _ ->
-          raise (TypeCheckerFailure
-           (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri)))
-CASO TIPO INDUTTIVO
-    match cobj with
-        C.InductiveDefinition (dl,_,_,_) ->
-          let (_,_,_,cl) = List.nth dl i in
-          let (_,ty) = List.nth cl (j-1) in
-            ty,ugraph1
-      | _ ->
-          raise (TypeCheckerFailure
-           (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri)))
+ | 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 typecheck_obj0 = function
- obj -> assert false
-(*
-   | C.Constant (_,Some te,ty,_,_) ->
-      let _,ugraph = type_of ~logger ty ugraph in
-      let ty_te,ugraph = type_of ~logger te ugraph in
-      let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
-       if not b then
-         raise (TypeCheckerFailure
-          (lazy
-            ("the type of the body is not the one expected:\n" ^
-             CicPp.ppterm ty_te ^ "\nvs\n" ^
-             CicPp.ppterm ty)))
-       else
-        ugraph
-   | C.Constant (_,None,ty,_,_) ->
-      (* only to check that ty is well-typed *)
-      let _,ugraph = type_of ~logger ty ugraph in
-       ugraph
-   | C.CurrentProof (_,conjs,te,ty,_,_) ->
-      let _,ugraph =
-       List.fold_left
-        (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
-          let _,ugraph = 
-           type_of_aux' ~logger metasenv context ty ugraph 
-          in
-           metasenv @ [conj],ugraph
-        ) ([],ugraph) conjs
-      in
-       let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
-       let type_of_te,ugraph = 
-        type_of_aux' ~logger conjs [] te ugraph
-       in
-       let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
-        if not b then
-          raise (TypeCheckerFailure (lazy (sprintf
-           "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s"
-           (CicPp.ppterm type_of_te) (CicPp.ppterm ty))))
-        else
-         ugraph
-   | (C.InductiveDefinition _ as obj) ->
-      check_mutual_inductive_defs ~logger uri obj ugraph
-   | C.Fix (i,fl) ->
-      let types,kl,ugraph1,len =
+and guarded_by_constructors ~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"))
+
+and is_really_smaller ~subst (context, recfuns, x, safes as k) te =
+ match R.whd ~subst context te with
+ | C.Rel m when List.mem m safes -> true
+ | C.Rel _ -> false
+ | C.LetIn _ -> raise (AssertFailure (lazy "letin after whd"))
+ | C.Sort _ | C.Implicit _ | C.Prod _ | C.Lambda _ 
+ | C.Const (Ref.Ref (_,_,(Ref.Decl | Ref.Def | Ref.Ind _ | Ref.CoFix _))) ->
+    raise (AssertFailure (lazy "not a constructor"))
+ | C.Appl ([]|[_]) -> raise (AssertFailure (lazy "empty/unary appl"))
+ | C.Appl (he::_) ->
+    (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
+    (*CSC: solo perche' non abbiamo trovato controesempi            *)
+    (*TASSI: da capire soprattutto se he è un altro fix che non ha ridotto...*)
+    is_really_smaller ~subst k he
+ | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false
+ | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert 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,kl,ugraph,len) (n,k,ty,_) ->
-            let _,ugraph1 = type_of_aux ~logger context ty ugraph in
+          (fun (types,len) (n,_,ty,_) ->
              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
-              k::kl,ugraph1,len+1)
-          ) ([],[],ugraph,0) fl
-      in
-      let ugraph2 = 
+              len+1)
+          ) ([],0) fl
+       and safes' = List.map (fun x -> x + len) safes in
+        List.fold_right
+         (fun (_,_,ty,bo) i ->
+           i &&
+            is_really_smaller ~subst (tys@context) n_plus_len nn_plus_len kl
+             x_plus_len safes' bo
+         ) fl true*)
+ | C.Meta _ -> 
+     true (* XXX if this check is repeated when the user completes the
+             definition *)
+ | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) ->
+    (match term with
+    | C.Rel m | C.Appl (C.Rel m :: _ ) when List.mem m safes || m = x ->
+        let isinductive, paramsno, tl, _, i = E.get_checked_indtys ref in
+        if not isinductive then
+          List.for_all (is_really_smaller ~subst k) pl
+        else
+          let c_ctx,len,cl = fix_lefts_in_constrs ~subst uri paramsno tl i in
+          List.for_all2
+           (fun p (_,_,debruijnedte) -> 
+             let rl' = recursive_args ~subst c_ctx 0 len debruijnedte in
+             let e, k = get_new_safes ~subst k p rl' in
+             is_really_smaller ~subst k e)
+           pl cl
+    | _ -> List.for_all (is_really_smaller ~subst k) pl)
+
+and returns_a_coinductive ~subst context ty =
+  match R.whd ~subst context ty with
+  | C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref) 
+  | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref)::_) ->
+     let isinductive, _, _, _, _ = E.get_checked_indtys ref in
+     if isinductive then None else (Some uri)
+  | C.Prod (n,so,de) ->
+     returns_a_coinductive ~subst ((n,C.Decl so)::context) de
+  | _ -> None
+
+and type_of_constant ((Ref.Ref (_,uri,_)) as ref) = 
+  let cobj =
+    match E.get_obj uri with
+    | true, cobj -> cobj
+    | false, uobj ->
+       !logger (`Start_type_checking uri);
+       check_obj_well_typed uobj;
+       E.add_obj uobj;
+       !logger (`Type_checking_completed uri);
+       if not (fst (E.get_obj uri)) then
+         raise (AssertFailure (lazy "environment error"));
+       uobj
+  in
+  match cobj, ref with
+  | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Ind i)  ->
+      let _,_,arity,_ = List.nth tl i in arity
+  | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Con (i,j))  ->
+      let _,_,_,cl = List.nth tl i in 
+      let _,_,arity = List.nth cl (j-1) in 
+      arity
+  | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,_,(Ref.Fix (i,_)|Ref.CoFix i)) ->
+      let _,_,_,arity,_ = List.nth fl i in
+      arity
+  | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,_,(Ref.Def |Ref.Decl)) -> ty
+  | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference"))
+
+and check_obj_well_typed (uri,height,metasenv,subst,kind) =
+ (* CSC: here we should typecheck the metasenv and the subst *)
+ assert (metasenv = [] && subst = []);
+ match kind with
+   | C.Constant (_,_,Some te,ty,_) ->
+      prerr_endline ("TY: " ^ NCicPp.ppterm ty);
+      prerr_endline ("BO: " ^ NCicPp.ppterm te);
+      let _ = typeof ~subst ~metasenv [] ty in
+      let ty_te = typeof ~subst ~metasenv [] te in
+      prerr_endline "XXXX";
+      if not (R.are_convertible ~subst ~metasenv [] ty_te ty) then
+       raise (TypeCheckerFailure (lazy (Printf.sprintf
+        "the type of the body is not the one expected:\n%s\nvs\n%s"
+        (NCicPp.ppterm ty_te) (NCicPp.ppterm ty))))
+   | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty)
+   | C.Inductive _ as obj -> check_mutual_inductive_defs obj
+   | C.Fixpoint (inductive,fl,_) ->
+      let types,kl,len =
         List.fold_left
-          (fun ugraph (name,x,ty,bo) ->
-             let ty_bo,ugraph1 = 
-               type_of_aux ~logger (types@context) bo ugraph 
-             in
-             let b,ugraph2 = 
-               R.are_convertible ~subst ~metasenv (types@context) 
-                 ty_bo (CicSubstitution.lift len ty) ugraph1 in
-               if b then
-                 begin
-                   let (m, eaten, context') =
-                     eat_lambdas ~subst (types @ context) (x + 1) bo
-                   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
-                       raise
-                         (TypeCheckerFailure 
-                           (lazy ("Fix: not guarded by destructors")))
-                     else
-                       ugraph2
-                 end
-               else
-                 raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies")))
-          ) ugraph1 fl in
-        (*CSC: controlli mancanti solo su D{f,k,x,M} *)
-      let (_,_,ty,_) = List.nth fl i in
-        ty,ugraph2
-   | C.CoFix (i,fl) ->
-       let types,ugraph1,len =
-         List.fold_left
-           (fun (l,ugraph,len) (n,ty,_) -> 
-              let _,ugraph1 = 
-                type_of_aux ~logger context ty ugraph in 
-                (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l,
-                 ugraph1,len+1)
-           ) ([],ugraph,0) fl
-       in
-       let ugraph2 = 
-         List.fold_left
-           (fun ugraph (_,ty,bo) ->
-              let ty_bo,ugraph1 = 
-                type_of_aux ~logger (types @ context) bo ugraph 
-              in
-              let b,ugraph2 = 
-                R.are_convertible ~subst ~metasenv (types @ context) ty_bo
-                  (CicSubstitution.lift len ty) ugraph1 
-              in
-                if b then
-                  begin
-                    (* let's control that the returned type is coinductive *)
-                    match returns_a_coinductive ~subst context ty with
-                        None ->
-                          raise
-                          (TypeCheckerFailure
-                            (lazy "CoFix: does not return a coinductive type"))
-                      | Some uri ->
-                          (*
-                            let's control the guarded by constructors 
-                            conditions C{f,M}
-                          *)
-                          if not (guarded_by_constructors ~subst
-                              (types @ context) 0 len false bo [] uri) then
-                            raise
-                              (TypeCheckerFailure 
-                                (lazy "CoFix: not guarded by constructors"))
-                          else
-                          ugraph2
-                  end
-                else
-                  raise
-                    (TypeCheckerFailure (lazy "CoFix: ill-typed bodies"))
-           ) ugraph1 fl 
-       in
-       let (_,ty,_) = List.nth fl i in
-         ty,ugraph2
+         (fun (types,kl,len) (_,name,k,ty,_) ->
+           let _ = typeof ~subst ~metasenv [] ty in
+            ((name,(C.Decl (S.lift len ty)))::types, k::kl,len+1)
+         ) ([],[],0) fl
+      in
+        List.iter (fun (_,name,x,ty,bo) ->
+         let bo = debruijn uri len bo in
+         let ty_bo = typeof ~subst ~metasenv types bo in
+         if not (R.are_convertible ~subst ~metasenv types ty_bo (S.lift len ty))
+         then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies")))
+         else
+          if inductive then begin
+            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 ~subst context (enum_from (x+1) kl) m;
+          end else
+           match returns_a_coinductive ~subst [] ty with
+            | None ->
+                raise (TypeCheckerFailure
+                  (lazy "CoFix: does not return a coinductive type"))
+            | Some uri ->
+                (* guarded by constructors conditions C{f,M} *)
+                if not (guarded_by_constructors ~subst
+                    types 0 len false bo [] uri)
+                then
+                  raise (TypeCheckerFailure
+                   (lazy "CoFix: not guarded by constructors"))
+          ) fl
 
-*)
+let typecheck_obj = check_obj_well_typed;;
 
-let typecheck_obj (*uri*) obj = assert false (*
- let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
- let ugraph, univlist, obj = CicUnivUtils.clean_and_fill uri obj ugraph in
-  CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist)
-*)
-;;
+(* EOF *)