X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=a77b293c1ae42d67ef8bdc0bdf09471441d431ef;hb=18d8d7128c16b5d4dd589d75a2e7c026ac7d405d;hp=63eacd93169afe311b071174d2a3f519e15de197;hpb=080122687296a86b1a0c1e1ed67fb7a79bd84ec6;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 63eacd931..a77b293c1 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -28,281 +28,9 @@ let shift_k e (c,rf,x,safes) =
 
 (* $Id: cicTypeChecker.ml 8213 2008-03-13 18:48:26Z sacerdot $ *)
 
-(*
-exception CicEnvironmentError;;
-
-(*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"))
-
-(* 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"))
-
-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))))
 
-(* 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'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
-
-(* 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.                            *)
@@ -603,16 +331,17 @@ let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) =
          (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 ~context s ^ " - Vs - " ^ NCicPp.ppterm
+          prerr_endline (NCicPp.ppterm ~subst ~metasenv ~context s ^ " - Vs - "
+          ^ NCicPp.ppterm ~subst ~metasenv
           ~context ty_arg);
-          prerr_endline (NCicPp.ppterm ~context (S.subst ~avoid_beta_redexes:true arg t));
+          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
@@ -620,13 +349,23 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty =
             raise 
               (TypeCheckerFailure 
                 (lazy (Printf.sprintf
-                  ("Appl: wrong parameter-type, expected %s, found %s")
-                  (NCicPp.ppterm ~subst ~metasenv ~context ty_arg) 
+                  ("Appl: wrong application of %s: the parameter %s has type"^^
+                   "\n%s\nbut it should have type \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))))
        | _ ->
           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
 ;;
@@ -671,6 +410,116 @@ let does_not_occur ~subst context n nn t =
    with DoesOccur -> false
 ;;
 
+(*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_mutind = C.Implicit `Hole in
+  (*CSC: mettere in cicSubstitution *)
+  let rec subst_inductive_type_with_dummy_mutind _ = function
+    | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy_mutind
+    | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl) when NUri.eq uri' uri ->
+       dummy_mutind
+    | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy_mutind 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 n dest ->
+       (* dummy abstraction, so we behave as in the anonimous case *)
+       strictly_positive ~subst context n nn
+        (subst_inductive_type_with_dummy_mutind () 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_mutind () source)&&
+         weakly_positive ~subst ((name,C.Decl source)::context)
+         (n + 1) (nn + 1) uri dest
+   | _ ->
+     raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
+
+(* 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 =
+  match c, params with
+  | c,[] -> c
+  | C.Prod (_,_,ta), he::tl -> instantiate_parameters tl (S.subst he ta)
+  | t,l -> raise (AssertFailure (lazy "1"))
+
+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) 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
+           | _ -> raise (TypeCheckerFailure (lazy 
+              ("Non-positive occurence in mutual inductive definition(s) [1]" ^
+              NUri.string_of_uri uri))))
+        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 n 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) ->
+      does_not_occur ~subst context n nn source &&
+       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 =
@@ -718,6 +567,7 @@ let rec typeof ~subst ~metasenv context term =
          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 
@@ -733,17 +583,20 @@ let rec typeof ~subst ~metasenv context term =
        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 ("HEAD: " ^ NCicPp.ppterm ~subst ~metasenv ~context ty_he);
        prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
-       ~context) (List.map snd args_with_ty)));
+       ~subst ~metasenv ~context) (List.map snd args_with_ty)));
        prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
-       ~context) (List.map fst args_with_ty)));
+       ~subst ~metasenv ~context) (List.map fst args_with_ty)));
 *)
-       eat_prods ~subst ~metasenv context ty_he 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 (_,_,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 =
@@ -774,16 +627,9 @@ let rec typeof ~subst ~metasenv context term =
         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 =
@@ -812,8 +658,8 @@ let rec typeof ~subst ~metasenv context term =
           (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 r)))
-          (NCicPp.ppterm ~metasenv ~subst ~context (List.nth pl (j-1)))
+            (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
@@ -959,34 +805,74 @@ 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 ~metasenv context n te =
   match (n, R.whd ~subst context te) with
@@ -1082,7 +968,7 @@ and guarded_by_destructors ~subst ~metasenv context recfuns t =
        ) fl true
 *)
 
-and guarded_by_constructors ~subst _ _ _ _ _ _ _ = assert false
+and guarded_by_constructors ~subst ~metasenv _ _ _ _ _ _ _ = true
 
 and recursive_args ~subst ~metasenv context n nn te =
   match R.whd context te with
@@ -1183,8 +1069,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
@@ -1218,7 +1102,8 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
         (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 =
         List.fold_left