X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=6f516b8db6eb010aaac1e3a6d449de901843f333;hb=67dd51c6c9ceb0186490033d77769d49404964ac;hp=e0f6bbaed6646f0a1efd0903b3728b8e9895807b;hpb=79501fecaa51e1afff2ac940706b4490b368dc27;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index e0f6bbaed..6f516b8db 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -22,287 +22,80 @@ 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
+type recf_entry = 
+  | Evil of int (* rno *) 
+  | UnfFix of bool list (* fixed arguments *) 
+  | Safe
 ;;
 
-(* $Id: cicTypeChecker.ml 8213 2008-03-13 18:48:26Z sacerdot $ *)
+let is_dangerous i l = 
+  List.exists (function (j,Evil _) when j=i -> true | _ -> false) l
+;;
 
-(*
-exception CicEnvironmentError;;
+let is_unfolded i l = 
+  List.exists (function (j,UnfFix _) when j=i -> true | _ -> false) l
+;;
 
-(*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  *)
-(*CSC strictly_positive                                                  *)
-(*CSC definizione (giusta???) tratta dalla mail di Hugo ;-)              *)
-and weakly_positive context n nn uri te =
- let module C = Cic in
-(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
-  let dummy_mutind =
-   C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
-  in
-  (*CSC: mettere in cicSubstitution *)
-  let rec subst_inductive_type_with_dummy_mutind =
-   function
-      C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
-       dummy_mutind
-    | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
-       dummy_mutind
-    | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
-    | C.Prod (name,so,ta) ->
-       C.Prod (name, subst_inductive_type_with_dummy_mutind so,
-        subst_inductive_type_with_dummy_mutind ta)
-    | C.Lambda (name,so,ta) ->
-       C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
-        subst_inductive_type_with_dummy_mutind ta)
-    | C.Appl tl ->
-       C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
-    | C.MutCase (uri,i,outtype,term,pl) ->
-       C.MutCase (uri,i,
-        subst_inductive_type_with_dummy_mutind outtype,
-        subst_inductive_type_with_dummy_mutind term,
-        List.map subst_inductive_type_with_dummy_mutind pl)
-    | C.Fix (i,fl) ->
-       C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
-        subst_inductive_type_with_dummy_mutind ty,
-        subst_inductive_type_with_dummy_mutind bo)) fl)
-    | C.CoFix (i,fl) ->
-       C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
-        subst_inductive_type_with_dummy_mutind ty,
-        subst_inductive_type_with_dummy_mutind bo)) fl)
-    | C.Const (uri,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map
-         (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
-         exp_named_subst
-       in
-        C.Const (uri,exp_named_subst')
-    | C.MutInd (uri,typeno,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map
-         (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
-         exp_named_subst
-       in
-        C.MutInd (uri,typeno,exp_named_subst')
-    | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map
-         (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
-         exp_named_subst
-       in
-        C.MutConstruct (uri,typeno,consno,exp_named_subst')
-    | t -> t
-  in
-  match CicReduction.whd context te with
-(*
-     C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
-*)
-     C.Appl ((C.MutInd (uri',_,_))::tl) when UriManager.eq uri' uri -> true
-   | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
-   | C.Prod (C.Anonymous,source,dest) ->
-      strictly_positive context n nn
-       (subst_inductive_type_with_dummy_mutind source) &&
-       weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
-        (n + 1) (nn + 1) uri dest
-   | C.Prod (name,source,dest) when
-      does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
-       (* dummy abstraction, so we behave as in the anonimous case *)
-       strictly_positive context n nn
-        (subst_inductive_type_with_dummy_mutind source) &&
-         weakly_positive ((Some (name,(C.Decl source)))::context)
-         (n + 1) (nn + 1) uri dest
-   | C.Prod (name,source,dest) ->
-       does_not_occur context n nn
-         (subst_inductive_type_with_dummy_mutind source)&&
-         weakly_positive ((Some (name,(C.Decl source)))::context)
-         (n + 1) (nn + 1) uri dest
-   | _ ->
-     raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
+let is_safe i l =
+  List.exists (function (j,Safe) when j=i -> true | _ -> false) l
+;;
 
-(* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
-(* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
-and instantiate_parameters params c =
- let module C = Cic in
-  match (c,params) with
-     (c,[]) -> c
-   | (C.Prod (_,_,ta), he::tl) ->
-       instantiate_parameters tl
-        (CicSubstitution.subst he ta)
-   | (C.Cast (te,_), _) -> instantiate_parameters params te
-   | (t,l) -> raise (AssertFailure (lazy "1"))
+let get_recno i l = 
+  try match List.assoc i l with Evil rno -> rno | _ -> assert false
+  with Not_found -> assert false
+;;
 
-and strictly_positive context n nn te =
- let module C = Cic in
- let module U = UriManager in
-  match CicReduction.whd context te with
-   | t when does_not_occur context n nn t -> true
-   | C.Rel _ -> true
-   | C.Cast (te,ty) ->
-      (*CSC: bisogna controllare ty????*)
-      strictly_positive context n nn te
-   | C.Prod (name,so,ta) ->
-      does_not_occur context n nn so &&
-       strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
-   | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
-      List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
-   | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) -> 
-      let (ok,paramsno,ity,cl,name) =
-        let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-          match o with
-              C.InductiveDefinition (tl,_,paramsno,_) ->
-                let (name,_,ity,cl) = List.nth tl i in
-                (List.length tl = 1, paramsno, ity, cl, name) 
-                (* (true, paramsno, ity, cl, name) *)
-            | _ ->
-                raise 
-                  (TypeCheckerFailure
-                     (lazy ("Unknown inductive type:" ^ U.string_of_uri uri)))
-      in 
-      let (params,arguments) = split tl paramsno in
-      let lifted_params = List.map (CicSubstitution.lift 1) params in
-      let cl' =
-        List.map
-          (fun (_,te) ->
-             instantiate_parameters lifted_params
-               (CicSubstitution.subst_vars exp_named_subst te)
-          ) cl
-      in
-        ok &&
-          List.fold_right
-          (fun x i -> i && does_not_occur context n nn x)
-          arguments true &&
-         (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
-          List.fold_right
-          (fun x i ->
-             i &&
-               weakly_positive
-               ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
-               x
-          ) cl' true
-   | t -> false
-       
-(* the inductive type indexes are s.t. n < x <= nn *)
-and are_all_occurrences_positive context uri indparamsno i n nn te =
- let module C = Cic in
-  match CicReduction.whd context te with
-     C.Appl ((C.Rel m)::tl) when m = i ->
-      (*CSC: riscrivere fermandosi a 0 *)
-      (* let's check if the inductive type is applied at least to *)
-      (* indparamsno parameters                                   *)
-      let last =
-       List.fold_left
-        (fun k x ->
-          if k = 0 then 0
-          else
-           match CicReduction.whd context x with
-              C.Rel m when m = n - (indparamsno - k) -> k - 1
-            | _ ->
-              raise (TypeCheckerFailure
-               (lazy 
-               ("Non-positive occurence in mutual inductive definition(s) [1]" ^
-                UriManager.string_of_uri uri)))
-        ) indparamsno tl
-      in
-       if last = 0 then
-        List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
-       else
-        raise (TypeCheckerFailure
-         (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
-          UriManager.string_of_uri uri)))
-   | C.Rel m when m = i ->
-      if indparamsno = 0 then
-       true
-      else
-        raise (TypeCheckerFailure
-         (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
-          UriManager.string_of_uri uri)))
-   | C.Prod (C.Anonymous,source,dest) ->
-       let b = strictly_positive context n nn source in
-       b &&
-       are_all_occurrences_positive
-        ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
-        (i+1) (n + 1) (nn + 1) dest
-   | C.Prod (name,source,dest) when
-      does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
-      (* dummy abstraction, so we behave as in the anonimous case *)
-      strictly_positive context n nn source &&
-       are_all_occurrences_positive
-        ((Some (name,(C.Decl source)))::context) uri indparamsno
-        (i+1) (n + 1) (nn + 1) dest
-   | C.Prod (name,source,dest) ->
-      does_not_occur context n nn source &&
-       are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
-        uri indparamsno (i+1) (n + 1) (nn + 1) dest
-   | _ ->
-     raise
-      (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^
-        (UriManager.string_of_uri uri))))
+let get_fixed_args i l = 
+  try match List.assoc i l with UnfFix fa -> fa | _ -> assert false
+  with Not_found -> assert false
+;;
 
-(* Main function to checks the correctness of a mutual *)
-(* inductive block definition. This is the function    *)
-(* exported to the proof-engine.                       *)
-and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
- let module U = UriManager in
-  (* let's check if the arity of the inductive types are well *)
-  (* formed                                                   *)
-  let ugrap1 = List.fold_left 
-   (fun ugraph (_,_,x,_) -> let _,ugraph' = 
-      type_of ~logger x ugraph in ugraph') 
-   ugraph itl in
+let shift_k e (c,rf,x) = e::c,List.map (fun (k,v) -> k+1,v) rf,x+1;;
 
-  (* let's check if the types of the inductive constructors  *)
-  (* are well formed.                                        *)
-  (* In order not to use type_of_aux we put the types of the *)
-  (* mutual inductive types at the head of the types of the  *)
-  (* constructors using Prods                                *)
-  let len = List.length itl in
-  let tys =
-    List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
-  let _,ugraph2 =
-    List.fold_right
-      (fun (_,_,_,cl) (i,ugraph) ->
-        let ugraph'' = 
-          List.fold_left
-            (fun ugraph (name,te) -> 
-              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 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
-                     debruijnedte)
-              then
-                begin
-                prerr_endline (UriManager.string_of_uri uri);
-                prerr_endline (string_of_int (List.length tys));
-                raise
-                  (TypeCheckerFailure
-                    (lazy ("Non positive occurence in " ^ U.string_of_uri uri)))                end 
-              else
-                ugraph'
-            ) ugraph cl in
-        (i + 1),ugraph''
-      ) itl (1,ugrap1)
-  in
-  ugraph2
+let string_of_recfuns ~subst ~metasenv ~context l = 
+  let pp = NCicPp.ppterm ~subst ~metasenv ~context in
+  let safe, rest = List.partition (function (_,Safe) -> true | _ -> false) l in
+  let dang, unf = List.partition (function (_,UnfFix _) -> false | _->true)rest in
+  "\n\tsafes: "^String.concat "," (List.map (fun (i,_)->pp (NCic.Rel i)) safe) ^
+  "\n\tfix  : "^String.concat "," 
+   (List.map 
+     (function (i,UnfFix l)-> pp(NCic.Rel i)^"/"^String.concat "," (List.map
+       string_of_bool l)
+     | _ ->assert false) unf) ^
+  "\n\trec  : "^String.concat "," 
+   (List.map 
+     (function (i,Evil rno)->pp(NCic.Rel i)^"/"^string_of_int rno
+     | _ -> assert false) dang)
+;;
+
+let fixed_args bos j n nn =
+ let rec aux k acc = function
+  | NCic.Appl (NCic.Rel i::args) when i-k > n && i-k <= nn ->
+     let rec combine l1 l2 =
+      match l1,l2 with
+         [],[] -> []
+       | he1::tl1, he2::tl2 -> (he1,he2)::combine tl1 tl2
+       | he::tl, [] -> (false,NCic.Rel ~-1)::combine tl [] (* dummy term *)
+       | [],_::_ -> assert false
+     in
+     let lefts, _ = HExtlib.split_nth (min j (List.length args)) args in
+      List.map (fun ((b,x),i) -> b && x = NCic.Rel (k-i)) 
+       (HExtlib.list_mapi (fun x i -> x,i) (combine acc lefts))
+  | t -> NCicUtils.fold (fun _ k -> k+1) k aux acc t    
+ in
+  List.fold_left (aux 0) 
+   (let rec f = function 0 -> [] | n -> true :: f (n-1) in f j) bos
+;;
+
+let rec list_iter_default2 f l1 def l2 = 
+  match l1,l2 with
+    | [], _ -> ()
+    | a::ta, b::tb -> f a b; list_iter_default2 f ta def tb 
+    | a::ta, [] -> f a def; list_iter_default2 f ta def [] 
+;;
 
-(* Main function to checks the correctness of a mutual *)
-(* inductive block definition.                         *)
-and check_mutual_inductive_defs uri obj ugraph =
-  match obj with
-      Cic.InductiveDefinition (itl, params, indparamsno, _) ->
-        typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph 
-    | _ ->
-        raise (TypeCheckerFailure (
-                lazy ("Unknown mutual inductive definition:" ^
-                 UriManager.string_of_uri uri)))
 
+(*
 (* 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.                            *)
@@ -566,7 +359,7 @@ let rec split_prods ~subst context n te =
    | (_, _) -> raise (AssertFailure (lazy "split_prods"))
 ;;
 
-let debruijn ?(cb=fun _ _ -> ()) uri number_of_types = 
+let debruijn ?(cb=fun _ _ -> ()) uri number_of_types context = 
  let rec aux k t =
   let res =
    match t with
@@ -581,10 +374,10 @@ let debruijn ?(cb=fun _ _ -> ()) uri number_of_types =
   in
    cb t res; res
  in
-  aux 0
+  aux (List.length context)
 ;;
 
-let sort_of_prod ~subst context (name,s) (t1, t2) =
+let sort_of_prod ~metasenv ~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
    match t1, t2 with
@@ -599,45 +392,88 @@ let sort_of_prod ~subst context (name,s) (t1, t2) =
    | _ -> 
       raise (TypeCheckerFailure (lazy (Printf.sprintf
         "Prod: expected two sorts, found = %s, %s" 
-         (NCicPp.ppterm t1) (NCicPp.ppterm t2))))
+         (NCicPp.ppterm ~subst ~metasenv ~context t1) 
+         (NCicPp.ppterm ~subst ~metasenv ~context t2))))
 ;;
 
-let eat_prods ~subst ~metasenv context ty_he args_with_ty = 
+let eat_prods ~subst ~metasenv context he ty_he args_with_ty = 
   let rec aux ty_he = function 
   | [] -> ty_he
   | (arg, ty_arg)::tl ->
-      (match R.whd ~subst context ty_he with 
+      match R.whd ~subst context ty_he with 
       | C.Prod (n,s,t) ->
+(*
+          prerr_endline (NCicPp.ppterm ~subst ~metasenv ~context s ^ " - Vs - "
+          ^ NCicPp.ppterm ~subst ~metasenv
+          ~context ty_arg);
+          prerr_endline (NCicPp.ppterm ~subst ~metasenv ~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
             raise 
               (TypeCheckerFailure 
                 (lazy (Printf.sprintf
-                  ("Appl: wrong parameter-type, expected %s, found %s")
-                  (NCicPp.ppterm ty_arg) (NCicPp.ppterm s))))
+                  ("Appl: wrong application of %s: the parameter %s has type"^^
+                   "\n%s\nbut it should have type \n%s\nContext:\n%s\n")
+                  (NCicPp.ppterm ~subst ~metasenv ~context he)
+                  (NCicPp.ppterm ~subst ~metasenv ~context arg)
+                  (NCicPp.ppterm ~subst ~metasenv ~context ty_arg)
+                  (NCicPp.ppterm ~subst ~metasenv ~context s)
+                  (NCicPp.ppcontext ~subst ~metasenv context))))
        | _ ->
           raise 
             (TypeCheckerFailure
-              (lazy "Appl: this is not a function, it cannot be applied")))
+              (lazy (Printf.sprintf
+                "Appl: %s is not a function, it cannot be applied"
+                (NCicPp.ppterm ~subst ~metasenv ~context
+                 (let res = List.length tl in
+                  let eaten = List.length args_with_ty - res in
+                   (NCic.Appl
+                    (he::List.map fst
+                     (fst (HExtlib.split_nth eaten args_with_ty)))))))))
   in
     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 
+(* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
+(* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
+let rec instantiate_parameters params c =
+  match c, params with
+  | c,[] -> c
+  | C.Prod (_,_,ta), he::tl -> instantiate_parameters tl (S.subst he ta)
+  | t,l -> raise (AssertFailure (lazy "1"))
+;;
+
+let specialize_inductive_type ~subst context ty_term =
+  match R.whd ~subst context ty_term with
+  | C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref)  
+  | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref) :: _ ) as ty ->
+      let args = match ty with C.Appl (_::tl) -> tl | _ -> [] in
+      let is_ind, leftno, itl, attrs, i = E.get_checked_indtys ref in
+      let left_args,_ = HExtlib.split_nth leftno args in
+      let itl =
+        List.map (fun (rel, name, arity, cl) ->
+          let arity = instantiate_parameters left_args arity in
+          let cl = 
+            List.map (fun (rel, name, ty) -> 
+              rel, name, instantiate_parameters left_args ty)
+              cl
+          in
+            rel, name, arity, cl)
+          itl
+      in
+        is_ind, leftno, itl, attrs, i
+  | _ -> assert false
+;;
+
+let fix_lefts_in_constrs ~subst r_uri r_len context ty_term =
+  let _,_,itl,_,i = specialize_inductive_type ~subst context ty_term in
+  let _,_,_,cl = List.nth itl i in  
+  let cl =
+    List.map (fun (_,id,ty) -> id, debruijn r_uri r_len context ty) cl 
   in
-  let lefts = fst (split_prods ~subst [] paramsno arity) in
-  tys@lefts, len, cl'
+  List.map (fun (_,name,arity,_) -> name, C.Decl arity) itl, cl
 ;;
 
 exception DoesOccur;;
@@ -664,10 +500,118 @@ let does_not_occur ~subst context n nn t =
    with DoesOccur -> false
 ;;
 
-exception NotGuarded;;
+(*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  *)
+(*CSC strictly_positive                                                  *)
+(*CSC definizione (giusta???) tratta dalla mail di Hugo ;-)              *)
+let rec weakly_positive ~subst context n nn uri te =
+(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
+  let dummy = C.Sort (C.Type ~-1) in
+  (*CSC: mettere in cicSubstitution *)
+  let rec subst_inductive_type_with_dummy _ = function
+    | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy
+    | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl) 
+        when NUri.eq uri' uri -> dummy
+    | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t
+  in
+  match R.whd context te with
+   | C.Const (Ref.Ref (_,uri',Ref.Ind _))
+   | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind _)))::_) 
+      when NUri.eq uri' uri -> true
+   | C.Prod (name,source,dest) when
+      does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
+       (* dummy abstraction, so we behave as in the anonimous case *)
+       strictly_positive ~subst context n nn
+        (subst_inductive_type_with_dummy () source) &&
+       weakly_positive ~subst ((name,C.Decl source)::context)
+        (n + 1) (nn + 1) uri dest
+   | C.Prod (name,source,dest) ->
+       does_not_occur ~subst context n nn
+        (subst_inductive_type_with_dummy () source)&&
+       weakly_positive ~subst ((name,C.Decl source)::context)
+        (n + 1) (nn + 1) uri dest
+   | _ ->
+     raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
+
+and strictly_positive ~subst context n nn te =
+  match R.whd context te with
+   | t when does_not_occur ~subst context n nn t -> true
+   | C.Rel _ -> true
+   | C.Prod (name,so,ta) ->
+      does_not_occur ~subst context n nn so &&
+       strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1) ta
+   | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
+      List.for_all (does_not_occur ~subst context n nn) tl
+   | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind i) as r)::tl) -> 
+      let _,paramsno,tyl,_,i = E.get_checked_indtys r in
+      let _,name,ity,cl = List.nth tyl i in
+      let ok = List.length tyl = 1 in
+      let params, arguments = HExtlib.split_nth paramsno tl in
+      let lifted_params = List.map (S.lift 1) params in
+      let cl =
+        List.map (fun (_,_,te) -> instantiate_parameters lifted_params te) cl 
+      in
+      ok &&
+      List.for_all (does_not_occur ~subst context n nn) arguments &&
+      List.for_all 
+        (weakly_positive ~subst ((name,C.Decl ity)::context) (n+1) (nn+1) uri) cl
+   | _ -> false
+       
+(* the inductive type indexes are s.t. n < x <= nn *)
+and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
+  match R.whd context te with
+  |  C.Appl ((C.Rel m)::tl) as reduct when m = i ->
+      let last =
+       List.fold_left
+        (fun k x ->
+          if k = 0 then 0
+          else
+           match R.whd context x with
+           |  C.Rel m when m = n - (indparamsno - k) -> k - 1
+           | y -> raise (TypeCheckerFailure (lazy 
+              ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^
+              string_of_int indparamsno ^ " fixed) is not homogeneous in "^
+              "appl:\n"^ NCicPp.ppterm ~context ~subst ~metasenv:[] reduct))))
+        indparamsno tl
+      in
+       if last = 0 then
+        List.for_all (does_not_occur ~subst context n nn) tl
+       else
+        raise (TypeCheckerFailure
+         (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
+          NUri.string_of_uri uri)))
+  | C.Rel m when m = i ->
+      if indparamsno = 0 then
+       true
+      else
+        raise (TypeCheckerFailure
+         (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
+          NUri.string_of_uri uri)))
+  | C.Prod (name,source,dest) when
+      does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
+      strictly_positive ~subst context n nn source &&
+       are_all_occurrences_positive ~subst 
+        ((name,C.Decl source)::context) uri indparamsno
+        (i+1) (n + 1) (nn + 1) dest
+   | C.Prod (name,source,dest) ->
+       if not (does_not_occur ~subst context n nn source) then
+         raise (TypeCheckerFailure (lazy ("Non-positive occurrence in "^
+         NCicPp.ppterm ~context ~metasenv:[] ~subst te)));
+       are_all_occurrences_positive ~subst ((name,C.Decl source)::context)
+        uri indparamsno (i+1) (n + 1) (nn + 1) dest
+   | _ ->
+     raise
+      (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^
+        (NUri.string_of_uri uri))))
+;;
+
+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 ~metasenv ~subst ~context t);*)
+    match t with
     | C.Rel n ->
        (try
          match List.nth context (n - 1) with
@@ -678,22 +622,22 @@ let rec typeof ~subst ~metasenv context term =
     | C.Sort s -> C.Sort (C.Type 0)
     | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
     | C.Meta (n,l) as t -> 
-       let canonical_context,ty =
+       let canonical_ctx,ty =
         try
          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))))
+          "%s not found" (NCicPp.ppterm ~subst ~metasenv ~context t))))
        in
-        check_metasenv_consistency t context canonical_context l;
+        check_metasenv_consistency t ~subst ~metasenv context canonical_ctx l;
         S.subst_meta l ty
     | C.Const ref -> type_of_constant ref
     | C.Prod (name,s,t) ->
        let sort1 = typeof_aux context s in
        let sort2 = typeof_aux ((name,(C.Decl s))::context) t in
-       sort_of_prod ~subst context (name,s) (sort1,sort2)
+       sort_of_prod ~metasenv ~subst context (name,s) (sort1,sort2)
     | C.Lambda (n,s,t) ->
        let sort = typeof_aux context s in
        (match R.whd ~subst context sort with
@@ -703,28 +647,42 @@ let rec typeof ~subst ~metasenv context term =
            (TypeCheckerFailure (lazy (Printf.sprintf
              ("Not well-typed lambda-abstraction: " ^^
              "the source %s should be a type; instead it is a term " ^^ 
-             "of type %s") (NCicPp.ppterm s) (NCicPp.ppterm sort)))));
+             "of type %s") (NCicPp.ppterm ~subst ~metasenv ~context s)
+             (NCicPp.ppterm ~subst ~metasenv ~context sort)))));
        let ty = typeof_aux ((n,(C.Decl s))::context) t in
          C.Prod (n,s,ty)
     | C.LetIn (n,ty,t,bo) ->
        let ty_t = typeof_aux context t in
+       let _ = typeof_aux context ty in
        if not (R.are_convertible ~subst ~metasenv context ty ty_t) then
          raise 
           (TypeCheckerFailure 
             (lazy (Printf.sprintf
               "The type of %s is %s but it is expected to be %s" 
-                (NCicPp.ppterm t) (NCicPp.ppterm ty_t) (NCicPp.ppterm ty))))
+                (NCicPp.ppterm ~subst ~metasenv ~context t) 
+                (NCicPp.ppterm ~subst ~metasenv ~context ty_t) 
+                (NCicPp.ppterm ~subst ~metasenv ~context ty))))
        else
          let ty_bo = typeof_aux  ((n,C.Def (t,ty))::context) bo in
          S.subst ~avoid_beta_redexes:true t ty_bo
     | 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
-       eat_prods ~subst ~metasenv context ty_he args_with_ty
+(*
+       prerr_endline ("HEAD: " ^ NCicPp.ppterm ~subst ~metasenv ~context ty_he);
+       prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
+       ~subst ~metasenv ~context) (List.map snd args_with_ty)));
+       prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
+       ~subst ~metasenv ~context) (List.map fst args_with_ty)));
+*)
+       eat_prods ~subst ~metasenv context he 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 inductive,leftno,itl,_,_ = E.get_checked_indtys r in
+      let constructorsno =
+        let _,_,_,cl = List.nth itl tyno in List.length cl
+      in
       let parameters, arguments =
         let ty = R.whd ~subst context (typeof_aux context term) in
         let r',tl =
@@ -735,34 +693,29 @@ let rec typeof ~subst ~metasenv context term =
              raise 
                (TypeCheckerFailure (lazy (Printf.sprintf
                  "Case analysis: analysed term %s is not an inductive one"
-                 (NCicPp.ppterm term)))) in
+                 (NCicPp.ppterm ~subst ~metasenv ~context term)))) in
         if not (Ref.eq r r') then
          raise
           (TypeCheckerFailure (lazy (Printf.sprintf
             ("Case analysys: analysed term type is %s, but is expected " ^^
              "to be (an application of) %s")
-            (NCicPp.ppterm ty) (NCicPp.ppterm (C.Const r')))))
+            (NCicPp.ppterm ~subst ~metasenv ~context ty) 
+            (NCicPp.ppterm ~subst ~metasenv ~context (C.Const r')))))
         else
          try HExtlib.split_nth leftno tl
          with
           Failure _ ->
-           raise (TypeCheckerFailure (lazy (Printf.sprintf
-            "%s is partially applied" (NCicPp.ppterm ty)))) in
+           raise (TypeCheckerFailure (lazy (Printf.sprintf 
+           "%s is partially applied" 
+           (NCicPp.ppterm  ~subst ~metasenv ~context ty)))) in
       (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
       let sort_of_ind_type =
         if parameters = [] then C.Const r
         else C.Appl ((C.Const r)::parameters) in
       let type_of_sort_of_ind_ty = typeof_aux context sort_of_ind_type in
-      if not (check_allowed_sort_elimination ~subst ~metasenv r context
-          sort_of_ind_type type_of_sort_of_ind_ty outsort)
-      then raise (TypeCheckerFailure (lazy ("Sort elimination not allowed")));
+      check_allowed_sort_elimination ~subst ~metasenv r context
+       sort_of_ind_type type_of_sort_of_ind_ty outsort;
       (* let's check if the type of branches are right *)
-      let leftno,constructorsno =
-        let inductive,leftno,itl,_,i = E.get_checked_indtys r in
-        let _,name,ty,cl = List.nth itl i in
-        let cl_len = List.length cl in
-        leftno, cl_len
-      in
       if List.length pl <> constructorsno then
        raise (TypeCheckerFailure (lazy ("Wrong number of cases in a match")));
       let j,branches_ok,p_ty, exp_p_ty =
@@ -770,14 +723,15 @@ let rec typeof ~subst ~metasenv context term =
           (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 0 in
+                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
@@ -787,10 +741,13 @@ let rec typeof ~subst ~metasenv context term =
       if not branches_ok then
         raise
          (TypeCheckerFailure 
-          (lazy (Printf.sprintf "Branch for constructor %s has type %s != %s"
-          (NCicPp.ppterm (C.Const 
-            (Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)))))
-          (NCicPp.ppterm ~context p_ty) (NCicPp.ppterm ~context exp_p_ty)))); 
+          (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^
+          "has type %s\nnot convertible with %s") 
+          (NCicPp.ppterm  ~subst ~metasenv ~context
+            (C.Const (Ref.mk_constructor (j-1) r)))
+          (NCicPp.ppterm ~metasenv ~subst ~context (List.nth pl (j-2)))
+          (NCicPp.ppterm ~metasenv ~subst ~context p_ty) 
+          (NCicPp.ppterm ~metasenv ~subst ~context exp_p_ty)))); 
       let res = outtype::arguments@[term] in
       R.head_beta_reduce (C.Appl res)
     | C.Match _ -> assert false
@@ -815,7 +772,9 @@ let rec typeof ~subst ~metasenv context term =
   (* check_metasenv_consistency checks that the "canonical" context of a
      metavariable is consitent - up to relocation via the relocation list l -
      with the actual context *)
-  and check_metasenv_consistency term context canonical_context l =
+  and check_metasenv_consistency 
+    ~subst ~metasenv term context canonical_context l 
+  =
    match l with
     | shift, NCic.Irl n ->
        let context = snd (HExtlib.split_nth shift context) in
@@ -825,10 +784,11 @@ let rec typeof ~subst ~metasenv context term =
          | _,_,[] ->
             raise (AssertFailure (lazy (Printf.sprintf
              "Local and canonical context %s have different lengths"
-             (NCicPp.ppterm term))))
+             (NCicPp.ppterm ~subst ~context ~metasenv term))))
          | m,[],_::_ ->
             raise (TypeCheckerFailure (lazy (Printf.sprintf
-             "Unbound variable -%d in %s" m (NCicPp.ppterm term))))
+             "Unbound variable -%d in %s" m 
+             (NCicPp.ppterm ~subst ~metasenv ~context term))))
          | m,t::tl,ct::ctl ->
             (match t,ct with
                 (_,C.Decl t1), (_,C.Decl t2)
@@ -840,15 +800,15 @@ let rec typeof ~subst ~metasenv context term =
                         (lazy (Printf.sprintf 
                       ("Not well typed metavariable local context for %s: " ^^ 
                        "%s expected, which is not convertible with %s")
-                      (NCicPp.ppterm term) (NCicPp.ppterm t2) (NCicPp.ppterm t1)
-                      )))
+                      (NCicPp.ppterm ~subst ~metasenv ~context term) 
+                      (NCicPp.ppterm ~subst ~metasenv ~context t2) 
+                      (NCicPp.ppterm ~subst ~metasenv ~context t1))))
               | _,_ ->
                raise 
-                   (TypeCheckerFailure 
-                     (lazy (Printf.sprintf 
+                   (TypeCheckerFailure (lazy (Printf.sprintf 
                     ("Not well typed metavariable local context for %s: " ^^ 
                      "a definition expected, but a declaration found")
-                    (NCicPp.ppterm term)))));
+                    (NCicPp.ppterm ~subst ~metasenv ~context term)))));
             compare (m - 1,tl,ctl)
         in
          compare (n,context,canonical_context)
@@ -892,7 +852,8 @@ let rec typeof ~subst ~metasenv context term =
                    (lazy (Printf.sprintf 
                      ("Not well typed metavariable local context: " ^^ 
                       "expected a term convertible with %s, found %s")
-                     (NCicPp.ppterm ct) (NCicPp.ppterm t))))
+                     (NCicPp.ppterm ~subst ~metasenv ~context ct) 
+                     (NCicPp.ppterm ~subst ~metasenv ~context t))))
           | t, (_,C.Decl ct) ->
               let type_t = typeof_aux context t in
               if not (R.are_convertible ~subst ~metasenv context type_t ct) then
@@ -900,13 +861,15 @@ let rec typeof ~subst ~metasenv context term =
                  (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))))
+                  (NCicPp.ppterm ~subst ~metasenv ~context ct) 
+                  (NCicPp.ppterm ~subst ~metasenv ~context t) 
+                  (NCicPp.ppterm ~subst ~metasenv ~context type_t))))
         ) l lifted_canonical_context 
        with
         Invalid_argument _ ->
           raise (AssertFailure (lazy (Printf.sprintf
            "Local and canonical context %s have different lengths"
-           (NCicPp.ppterm term))))
+           (NCicPp.ppterm ~subst ~metasenv ~context term))))
 
   and is_non_informative context paramsno c =
    let rec aux context c =
@@ -928,82 +891,194 @@ let rec typeof ~subst ~metasenv context term =
     let arity2 = R.whd ~subst context arity2 in
       match arity1,arity2 with
        | C.Prod (name,so1,de1), C.Prod (_,so2,de2) ->
-          R.are_convertible ~subst ~metasenv context so1 so2 &&
-           aux ((name, C.Decl so1)::context)
-            (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2
+          if not (R.are_convertible ~subst ~metasenv context so1 so2) then
+           raise (TypeCheckerFailure (lazy (Printf.sprintf
+            "In outtype: expected %s, found %s"
+            (NCicPp.ppterm ~subst ~metasenv ~context so1)
+            (NCicPp.ppterm ~subst ~metasenv ~context so2)
+            )));
+          aux ((name, C.Decl so1)::context)
+           (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2
        | C.Sort _, C.Prod (name,so,ta) ->
-        (R.are_convertible ~subst ~metasenv context so ind &&
-          match arity1,ta with
-          | (C.Sort (C.CProp | C.Type _), C.Sort _)
-          | (C.Sort C.Prop, C.Sort C.Prop) -> true
-          | (C.Sort C.Prop, C.Sort (C.CProp | C.Type _)) ->
-              let inductive,leftno,itl,_,i = E.get_checked_indtys r in
-              let itl_len = List.length itl in
-              let _,name,ty,cl = List.nth itl i in
-              let cl_len = List.length cl in
-               (* is it a singleton or empty non recursive and non informative
-                  definition? *)
-               cl_len = 0 ||
-                (itl_len = 1 && cl_len = 1 &&
-                 is_non_informative [name,C.Decl ty] leftno
-                  (let _,_,x = List.nth cl 0 in x))
-          | _,_ -> false)
-       | _,_ -> false
+          if not (R.are_convertible ~subst ~metasenv context so ind) then
+           raise (TypeCheckerFailure (lazy (Printf.sprintf
+            "In outtype: expected %s, found %s"
+            (NCicPp.ppterm ~subst ~metasenv ~context ind)
+            (NCicPp.ppterm ~subst ~metasenv ~context so)
+            )));
+          (match arity1,ta with
+            | (C.Sort (C.CProp | C.Type _), C.Sort _)
+            | (C.Sort C.Prop, C.Sort C.Prop) -> ()
+            | (C.Sort C.Prop, C.Sort (C.CProp | C.Type _)) ->
+        (* TODO: we should pass all these parameters since we
+         * have them already *)
+                let inductive,leftno,itl,_,i = E.get_checked_indtys r in
+                let itl_len = List.length itl in
+                let _,name,ty,cl = List.nth itl i in
+                let cl_len = List.length cl in
+                 (* is it a singleton or empty non recursive and non informative
+                    definition? *)
+                 if not
+                  (cl_len = 0 ||
+                   (itl_len = 1 && cl_len = 1 &&
+                    is_non_informative [name,C.Decl ty] leftno
+                     (let _,_,x = List.nth cl 0 in x)))
+                 then
+                  raise (TypeCheckerFailure (lazy
+                   ("Sort elimination not allowed")));
+          | _,_ -> ())
+       | _,_ -> ()
    in
     aux 
 
  in 
    typeof_aux context term
 
-and check_mutual_inductive_defs _ = ()
+and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl = 
+  (* let's check if the arity of the inductive types are well formed *)
+  List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;
+  (* let's check if the types of the inductive constructors are well formed. *)
+  let len = List.length tyl in
+  let tys = List.rev (List.map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl) in
+  ignore
+   (List.fold_right
+    (fun (_,_,_,cl) i ->
+       List.iter
+         (fun (_,name,te) -> 
+           let debruijnedte = debruijn uri len [] te in
+           ignore (typeof ~subst ~metasenv tys debruijnedte);
+           (* let's check also the positivity conditions *)
+           if 
+             not
+               (are_all_occurrences_positive ~subst tys uri leftno i 0 len
+                  debruijnedte) 
+           then
+             raise
+               (TypeCheckerFailure
+                 (lazy ("Non positive occurence in "^NUri.string_of_uri uri))))
+         cl;
+        i + 1)
+    tyl 1)
 
-and eat_lambdas ~subst context n te =
+and eat_lambdas ~subst ~metasenv 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
+      eat_lambdas ~subst ~metasenv ((name,(C.Decl so))::context) (n - 1) ta
    | (n, te) ->
-      raise (AssertFailure 
-        (lazy (Printf.sprintf "9 (%d, %s)" n (NCicPp.ppterm te))))
+      raise (AssertFailure (lazy (Printf.sprintf "eat_lambdas (%d, %s)" n 
+        (NCicPp.ppterm ~subst ~metasenv ~context te))))
+
+and eat_or_subst_lambdas 
+ ~subst ~metasenv app_all_args n te to_be_subst args (context, recfuns, x as k) 
+=
+  match n, R.whd ~subst context te, to_be_subst, args with
+  | (0, _,_,_) when args = [] || not app_all_args -> te, k
+  | (0, _,_,_::_) -> C.Appl (te::args), k
+  | (n, C.Lambda (name,so,ta),true::to_be_subst,arg::args) when n > 0 ->
+      eat_or_subst_lambdas ~subst ~metasenv app_all_args
+       (n - 1) (S.subst arg ta) to_be_subst args k
+  | (n, C.Lambda (name,so,ta),false::to_be_subst,arg::args) when n > 0 ->
+      eat_or_subst_lambdas ~subst ~metasenv app_all_args
+       (n - 1) ta to_be_subst args (shift_k (name,(C.Decl so)) k)
+  | (n, te, _, _) when args = [] || not app_all_args -> te, k
+  | (n, te, _, _::_) -> C.Appl (te::args), k
+  | (_,_,_,[]) -> assert false (* caml thinks is missing *)
 
-and guarded_by_destructors ~subst context recfuns t = 
+and guarded_by_destructors r_uri r_len ~subst ~metasenv 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 
+ let rec aux (context, recfuns, x as k) t = 
+  let t = R.whd ~delta:max_int ~subst context t in
+(*
+   prerr_endline ("GB:\n" ^ 
+     NCicPp.ppcontext ~subst ~metasenv context^
+     NCicPp.ppterm ~metasenv ~subst ~context t^
+       string_of_recfuns ~subst ~metasenv ~context recfuns);
+*)
+  try
+  match t with
+  | C.Rel m as t when is_dangerous m recfuns -> 
+      raise (NotGuarded (lazy 
+        (NCicPp.ppterm ~subst ~metasenv ~context t ^ 
+         " is a partial application of a fix")))
+  | C.Appl ((C.Rel m)::tl) as t when is_dangerous m recfuns ->
+     let rec_no = get_recno m recfuns in
+     if not (List.length tl > rec_no) then 
+       raise (NotGuarded (lazy 
+         (NCicPp.ppterm ~context ~subst ~metasenv t ^ 
+         " is a partial application of a fix")))
+     else
+       let rec_arg = List.nth tl rec_no in
+       if not (is_really_smaller r_uri r_len ~subst ~metasenv k rec_arg) then 
+         raise (NotGuarded (lazy (Printf.sprintf ("Recursive call %s, %s is not"
+          ^^ " smaller.\ncontext:\n%s") (NCicPp.ppterm ~context ~subst ~metasenv
+          t) (NCicPp.ppterm ~context ~subst ~metasenv rec_arg)
+          (NCicPp.ppcontext ~subst ~metasenv context))));
+       List.iter (aux k) tl
+  | C.Appl ((C.Rel m)::tl) when is_unfolded m recfuns ->
+       let fixed_args = get_fixed_args m recfuns in
+       list_iter_default2 (fun x b -> if not b then aux k x) tl false fixed_args
   | 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.Def (bo,_) -> aux k (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
-       if not (is_really_smaller ~subst k rec_arg) then raise
-       NotGuarded;
-       List.iter (aux k) tl
+  | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,_))) as r)::args) ->
+      if List.exists (fun t -> try aux k t;false with NotGuarded _ -> true) args
+      then
+      let fl,_,_ = E.get_checked_fixes r in
+      let ctx_tys, bos = 
+        List.split (List.map (fun (_,name,_,ty,bo) -> (name, C.Decl ty), bo) fl)
+      in
+      let fl_len = List.length fl in
+      let bos = List.map (debruijn uri fl_len context) bos in
+      let j = List.fold_left min max_int (List.map (fun (_,_,i,_,_)->i) fl) in
+      let ctx_len = List.length context in
+        (* we may look for fixed params not only up to j ... *)
+      let fa = fixed_args bos j ctx_len (ctx_len + fl_len) in
+      list_iter_default2 (fun x b -> if not b then aux k x) args false fa; 
+      let context = context@ctx_tys in
+      let ctx_len = List.length context in
+      let extra_recfuns = 
+        HExtlib.list_mapi (fun _ i -> ctx_len - i, UnfFix fa) ctx_tys
+      in
+      let k = context, extra_recfuns@recfuns, x in
+      let bos_and_ks = 
+        HExtlib.list_mapi (fun bo fno ->
+          (* potrebbe anche aggiungere un arg di cui fa push alle safe *)
+          eat_or_subst_lambdas ~subst ~metasenv (fno=i) j bo fa args k) bos
+      in
+       List.iter (fun (bo,k) -> aux k bo) bos_and_ks
   | 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
+     | C.Rel m | C.Appl (C.Rel m :: _ ) as t when is_safe m recfuns || m = x ->
+        (* TODO: add CoInd to references so that this call is useless *)
+        let isinductive, _, _, _, _ = 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 ty = typeof ~subst ~metasenv context term in
+         let itl_ctx,dcl = fix_lefts_in_constrs ~subst r_uri r_len context ty in
          let args = match t with C.Appl (_::tl) -> tl | _ -> [] in
+         let dc_ctx = context @ itl_ctx in
+         let start, stop = List.length context, List.length context + r_len 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
+           (fun p (_,dc) ->
+             let rl = recursive_args ~subst ~metasenv dc_ctx start stop dc in
              let p, k = get_new_safes ~subst k p rl in
              aux k p) 
-           pl cl
+           pl dcl
      | _ -> recursor aux k t)
   | t -> recursor aux k t
+  with
+   NotGuarded _ as exc ->
+    let t' = R.whd ~delta:0 ~subst context t in
+    if t = t' then raise exc
+    else aux k t'
  in
-  try aux (context, recfuns, 1, []) t;true
-  with NotGuarded -> false
+  try aux (context, recfuns, 1) t
+  with NotGuarded s -> raise (TypeCheckerFailure s)
 
 (*
  | C.Fix (_, fl) ->
@@ -1045,22 +1120,25 @@ and guarded_by_destructors ~subst context recfuns t =
        ) fl true
 *)
 
-and guarded_by_constructors ~subst _ _ _ _ _ _ _ = assert false
+and guarded_by_constructors ~subst ~metasenv _ _ _ _ _ _ _ = true
 
-and recursive_args ~subst context n nn te =
+and recursive_args ~subst ~metasenv context n nn te =
   match R.whd context te with
-  | C.Rel _ -> []
+  | C.Rel _ | C.Appl _ | C.Const _ -> []
   | 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")))
+      (recursive_args ~subst ~metasenv 
+        ((name,(C.Decl so))::context) (n+1) (nn + 1) de)
+  | t -> 
+     raise (AssertFailure (lazy ("recursive_args:" ^ NCicPp.ppterm ~subst
+     ~metasenv ~context:[] t)))
 
-and get_new_safes ~subst (context, recfuns, x, safes as k) p rl =
+and get_new_safes ~subst (context, recfuns, x 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
+      let recfuns = (if b then [0,Safe] else []) @ recfuns in
       get_new_safes ~subst 
-        (shift_k (name,(C.Decl so)) (context, recfuns, x, safes)) ta tl
+        (shift_k (name,(C.Decl so)) (context, recfuns, x)) ta tl
   | C.Meta _ as e, _ | e, [] -> e, k
   | _ -> raise (AssertFailure (lazy "Ill formed pattern"))
 
@@ -1071,20 +1149,17 @@ and split_prods ~subst context n te =
        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 =
+and is_really_smaller 
+  r_uri r_len ~subst ~metasenv (context, recfuns, x 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.Rel m when is_safe m recfuns -> true
+ | C.Lambda (name, s, t) ->
+    is_really_smaller r_uri r_len ~subst ~metasenv (shift_k (name,C.Decl s) k) t
  | 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
+    is_really_smaller r_uri r_len ~subst ~metasenv k he
+ | C.Appl _
+ | C.Rel _ 
  | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false
  | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false
    (*| C.Fix (_, fl) ->
@@ -1105,24 +1180,27 @@ and is_really_smaller ~subst (context, recfuns, x, safes as k) te =
             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.Meta _ -> true 
  | 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
+    | C.Rel m | C.Appl (C.Rel m :: _ ) when is_safe m recfuns || m = x ->
+        (* TODO: add CoInd to references so that this call is useless *)
+        let isinductive, _, _, _, _ = E.get_checked_indtys ref in
         if not isinductive then
-          List.for_all (is_really_smaller ~subst k) pl
+          List.for_all (is_really_smaller r_uri r_len ~subst ~metasenv k) pl
         else
-          let c_ctx,len,cl = fix_lefts_in_constrs ~subst uri paramsno tl i in
+          let ty = typeof ~subst ~metasenv context term in
+          let itl_ctx,dcl= fix_lefts_in_constrs ~subst r_uri r_len context ty in
+          let start, stop = List.length context, List.length context + r_len in
+          let dc_ctx = context @ itl_ctx 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)
+           (fun p (_,dc) -> 
+             let rl = recursive_args ~subst ~metasenv dc_ctx start stop dc in
+             let e, k = get_new_safes ~subst k p rl in
+             is_really_smaller r_uri r_len ~subst ~metasenv k e)
+           pl dcl
+    | _ -> List.for_all (is_really_smaller r_uri r_len ~subst ~metasenv k) pl)
+ | _ -> assert false
 
 and returns_a_coinductive ~subst context ty =
   match R.whd ~subst context ty with
@@ -1143,8 +1221,6 @@ and type_of_constant ((Ref.Ref (_,uri,_)) as ref) =
        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
@@ -1152,7 +1228,7 @@ and type_of_constant ((Ref.Ref (_,uri,_)) as ref) =
       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 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
@@ -1168,46 +1244,66 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
       let _ = typeof ~subst ~metasenv [] ty in
       let ty_te = typeof ~subst ~metasenv [] te in
       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))))
+       raise (TypeCheckerFailure (lazy (Printf.sprintf (
+        "the type of the body is not convertible with the declared one.\n"^^
+        "inferred type:\n%s\nexpected type:\n%s")
+        (NCicPp.ppterm ~subst ~metasenv ~context:[] ty_te) 
+        (NCicPp.ppterm ~subst ~metasenv ~context:[] ty))))
    | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty)
-   | C.Inductive _ as obj -> check_mutual_inductive_defs obj
+   | C.Inductive (is_ind, leftno, tyl, _) -> 
+       check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl
    | C.Fixpoint (inductive,fl,_) ->
-      let types,kl,len =
+      let types, kl, len =
         List.fold_left
          (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 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 
+      let dfl, kl =   
+        List.split (List.map2 
+          (fun (_,_,_,_,bo) rno -> 
+             let dbo = debruijn uri len [] bo in
+             dbo, Evil rno)
+          fl kl)
+      in
+      List.iter2 (fun (_,name,x,ty,_) bo ->
+       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 ~metasenv types (x + 1) bo in
+          let r_uri, r_len =
+            let he =
+             match List.hd context with _,C.Decl t -> t | _ -> assert false
             in
-            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
-            | None ->
+            match R.whd ~subst (List.tl context) he with
+            | C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref)
+            | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref) :: _) ->
+                let _,_,itl,_,_ = E.get_checked_indtys ref in
+                  uri, List.length itl
+            | _ -> assert false
+          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 r_uri r_len 
+           ~subst ~metasenv context (enum_from (x+2) 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 ~metasenv
+                  types 0 len false bo [] uri)
+              then
                 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
+                 (lazy "CoFix: not guarded by constructors"))
+        ) fl dfl
 
 let typecheck_obj = check_obj_well_typed;;