From 909d7c9edd05868d1fba2dae65e6ff775a41dcbe Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 14 Feb 2002 15:54:01 +0000
Subject: - Reforme de la gestion des args recursifs (via arbres reguliers) -
 coqtop -byte -opt bouclait!

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/declarations.ml  |  19 +++-
 kernel/declarations.mli |  12 +-
 kernel/environ.ml       |  92 ++++++++-------
 kernel/environ.mli      |  14 +--
 kernel/indtypes.ml      | 291 ++++++++++++++++++++++++------------------------
 kernel/indtypes.mli     |   1 -
 kernel/inductive.ml     | 235 +++++++++++++++++---------------------
 kernel/sign.ml          |  15 ++-
 kernel/sign.mli         |   1 +
 9 files changed, 340 insertions(+), 340 deletions(-)

(limited to 'kernel')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index a9b8737bb7..fca3e0a50c 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -31,10 +31,23 @@ type constant_body = {
     information). *)
 
 type recarg = 
-  | Param of int 
   | Norec 
   | Mrec of int 
-  | Imbr of inductive * (recarg list)
+  | Imbr of inductive
+
+type wf_paths = recarg Rtree.t
+
+let mk_norec = Rtree.mk_node Norec [||]
+
+let mk_paths r recargs =
+  Rtree.mk_node r
+    (Array.map (fun l -> Rtree.mk_node Norec (Array.of_list l)) recargs)
+
+let dest_recarg p = fst (Rtree.dest_node p)
+
+let dest_subterms p =
+  let (_,cstrs) = Rtree.dest_node p in
+  Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs
 
 (* [mind_typename] is the name of the inductive; [mind_arity] is
    the arity generalized over global parameters; [mind_lc] is the list
@@ -54,7 +67,7 @@ type one_inductive_body = {
   mind_consnames : identifier array;
   mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *)
   mind_user_lc : types array;
-  mind_listrec : (recarg list) array;
+  mind_recargs : wf_paths;
  }
 
 type mutual_inductive_body = {
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index a9b8737bb7..8a03e1cda3 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -31,10 +31,16 @@ type constant_body = {
     information). *)
 
 type recarg = 
-  | Param of int 
   | Norec 
   | Mrec of int 
-  | Imbr of inductive * (recarg list)
+  | Imbr of inductive
+
+type wf_paths = recarg Rtree.t
+
+val mk_norec : wf_paths
+val mk_paths : recarg -> wf_paths list array -> wf_paths
+val dest_recarg : wf_paths -> recarg
+val dest_subterms : wf_paths -> wf_paths list array
 
 (* [mind_typename] is the name of the inductive; [mind_arity] is
    the arity generalized over global parameters; [mind_lc] is the list
@@ -54,7 +60,7 @@ type one_inductive_body = {
   mind_consnames : identifier array;
   mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *)
   mind_user_lc : types array;
-  mind_listrec : (recarg list) array;
+  mind_recargs : wf_paths;
  }
 
 type mutual_inductive_body = {
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 7e638f5175..94303bada1 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -49,16 +49,23 @@ let universes env = env.env_universes
 let named_context env = env.env_named_context
 let rel_context env = env.env_rel_context
 
-(* Construction functions. *)
+(* Access functions. *)
 
-let named_context_app f env =
-  { env with
-      env_named_context = f env.env_named_context }
+let lookup_rel n env =
+  Sign.lookup_rel n env.env_rel_context
 
-let push_named_decl d   = named_context_app (add_named_decl d)
-let push_named_assum (id,ty) = push_named_decl (id,None,ty)
-let pop_named_decl id         = named_context_app (pop_named_decl id)
+let lookup_named id env =
+  Sign.lookup_named id env.env_named_context
+
+let lookup_constant sp env =
+  Spmap.find sp env.env_globals.env_constants
+
+let lookup_mind sp env =
+  Spmap.find sp env.env_globals.env_inductives
 
+(* Construction functions. *)
+
+(* Rel context *)
 let rel_context_app f env =
   { env with
       env_rel_context = f env.env_rel_context }
@@ -77,16 +84,6 @@ let reset_rel_context env =
   { env with
       env_rel_context = empty_rel_context }
 
-
-
-let fold_named_context f env ~init =
-  snd (Sign.fold_named_context
-	 (fun d (env,e) -> (push_named_decl d env, f env d e))
-         (named_context env) ~init:(reset_context env,init))
-
-let fold_named_context_reverse f ~init env =
-  Sign.fold_named_context_reverse f ~init:init (named_context env) 
-
 let push_rel d   = rel_context_app (add_rel_decl d)
 let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x
 let push_rel_assum (id,ty) = push_rel (id,None,ty)
@@ -102,6 +99,24 @@ let fold_rel_context f env ~init =
 	 (fun d (env,e) -> (push_rel d env, f env d e))
          (rel_context env) ~init:(reset_rel_context env,init))
 
+(* Named context *)
+let named_context_app f env =
+  { env with
+      env_named_context = f env.env_named_context }
+
+let push_named_decl d   = named_context_app (add_named_decl d)
+let push_named_assum (id,ty) = push_named_decl (id,None,ty)
+let pop_named_decl id         = named_context_app (pop_named_decl id)
+
+let fold_named_context f env ~init =
+  snd (Sign.fold_named_context
+	 (fun d (env,e) -> (push_named_decl d env, f env d e))
+         (named_context env) ~init:(reset_context env,init))
+
+let fold_named_context_reverse f ~init env =
+  Sign.fold_named_context_reverse f ~init:init (named_context env) 
+
+(* Universe constraints *)
 let set_universes g env =
   if env.env_universes == g then env else { env with env_universes = g }
 
@@ -111,7 +126,12 @@ let add_constraints c env =
   else 
     { env with env_universes = merge_constraints c env.env_universes }
 
+(* Global constants *)
 let add_constant sp cb env =
+  let _ =
+    try
+      let _ = lookup_constant sp env in failwith "already declared constant"
+    with Not_found -> () in
   let new_constants = Spmap.add sp cb env.env_globals.env_constants in
   let new_locals = (Constant,sp)::env.env_globals.env_locals in
   let new_globals = 
@@ -120,7 +140,12 @@ let add_constant sp cb env =
 	env_locals = new_locals } in
   { env with env_globals = new_globals }
 
+(* Mutual Inductives *)
 let add_mind sp mib env =
+  let _ =
+    try 
+      let _ = lookup_mind sp env in failwith "already defined inductive"
+    with Not_found -> () in
   let new_inds = Spmap.add sp mib env.env_globals.env_inductives in
   let new_locals = (Inductive,sp)::env.env_globals.env_locals in
   let new_globals = 
@@ -129,20 +154,6 @@ let add_mind sp mib env =
 	env_locals = new_locals } in
   { env with env_globals = new_globals }
 
-(* Access functions. *)
-
-let lookup_rel n env =
-  Sign.lookup_rel n env.env_rel_context
-
-let lookup_named id env =
-  Sign.lookup_named id env.env_named_context
-
-let lookup_constant sp env =
-  Spmap.find sp env.env_globals.env_constants
-
-let lookup_mind sp env =
-  Spmap.find sp env.env_globals.env_inductives
-
 (* Lookup of section variables *)
 let lookup_constant_variables c env =
   let cmap = lookup_constant c env in
@@ -208,13 +219,13 @@ let keep_hyps env needed =
 
 (* Constants *)
 
-(* Not taking opacity into account *)
-let defined_constant env sp =
-  match (lookup_constant sp env).const_body with
-      Some _ -> true
-    | None -> false
+let opaque_constant env sp = (lookup_constant sp env).const_opaque
+
+(* constant_type gives the type of a constant *)
+let constant_type env sp =
+  let cb = lookup_constant sp env in
+  cb.const_type  
 
-(* Taking opacity into account *)
 type const_evaluation_result = NoBody | Opaque
 
 exception NotEvaluableConst of const_evaluation_result
@@ -233,7 +244,7 @@ let constant_opt_value env cst =
 (* A global const is evaluable if it is defined and not opaque *)
 let evaluable_constant env cst =
   try let _  = constant_value env cst in true
-  with NotEvaluableConst _ -> false
+  with Not_found | NotEvaluableConst _ -> false
 
 (* A local const is evaluable if it is defined and not opaque *)
 let evaluable_named_decl env id =
@@ -252,11 +263,6 @@ let evaluable_rel_decl env n =
   with Not_found -> 
     false
 
-(* constant_type gives the type of a constant *)
-let constant_type env sp =
-  let cb = lookup_constant sp env in
-  cb.const_type  
-
 (*s Modules (i.e. compiled environments). *)
 
 type compiled_env = {
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 9a00f053ac..ecaa4d1082 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -71,14 +71,20 @@ val add_mind :
 (* raises [Not_found] if the index points out of the context *)
 val lookup_rel : int -> env -> rel_declaration
 
+val evaluable_rel_decl : env -> int -> bool
+
 (* Looks up in the context of local vars referred by names ([named_context]) *)
 (* raises [Not_found] if the identifier is not found *)
 val lookup_named : variable -> env -> named_declaration
 
+val evaluable_named_decl : env -> variable -> bool
+
 (* Looks up in the context of global constant names *)
 (* raises [Not_found] if the required path is not found *)
 val lookup_constant : constant -> env -> constant_body
 
+val evaluable_constant : env -> constant -> bool
+
 (*s [constant_value env c] raises [NotEvaluableConst Opaque] if
    [c] is opaque and [NotEvaluableConst NoBody] if it has no
    body and [Not_found] if it does not exist in [env] *)
@@ -102,14 +108,6 @@ val vars_of_global : env -> constr -> identifier list
 
 val keep_hyps : env -> Idset.t -> section_context
 
-(* A constant is defined when it has a body (theorems do) *)
-val defined_constant : env -> constant -> bool
-(* A constant is evaluable when delta reduction applies (theorems don't) *)
-val evaluable_constant : env -> constant -> bool
-
-val evaluable_named_decl : env -> variable -> bool
-val evaluable_rel_decl : env -> int -> bool
-
 (*s Modules. *)
 
 type compiled_env
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 746a942de9..96c2eaf987 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -27,7 +27,6 @@ open Typeops
 (*s Declaration. *)
 
 type one_inductive_entry = {
-  mind_entry_nparams : int;
   mind_entry_params : (identifier * local_entry) list;
   mind_entry_typename : identifier;
   mind_entry_arity : constr;
@@ -90,12 +89,6 @@ let mind_check_names mie =
   vue since inductive and constructors are not referred to by their
   name, but only by the name of the inductive packet and an index. *)
 
-(* [mind_extract_params mie] extracts the params from an inductive types
-   declaration, and checks that they are all present (and all the same)
-   for all the given types. *)
-
-let mind_extract_params = decompose_prod_n_assum
-
 let mind_check_arities env mie =
   let check_arity id c =
     if not (is_arity env c) then 
@@ -201,7 +194,7 @@ let infer_constructor_packet env_ar params arsort vc =
 
 (* Type-check an inductive definition. Does not check positivity
    conditions. *)
-let type_inductive env mie =
+let typecheck_inductive env mie =
   if mie.mind_entry_inds = [] then anomaly "empty inductive types declaration";
   (* Check unicity of names *)
   mind_check_names mie;
@@ -242,35 +235,19 @@ let type_inductive env mie =
 	 let (_,arsort) = dest_arity env full_arity in
 	 let lc = ind.mind_entry_lc in
 	 let (issmall,isunit,lc',cst') =
-	   infer_constructor_packet env_arities params arsort lc
-	 in
-	 let nparams = ind.mind_entry_nparams in
+	   infer_constructor_packet env_arities params arsort lc in
 	 let consnames = ind.mind_entry_consnames in
-	 let ind' = (params,nparams,id,full_arity,consnames,issmall,isunit,lc')
+	 let ind' = (params,id,full_arity,consnames,issmall,isunit,lc')
 	 in
 	 (ind'::inds, Constraint.union cst cst'))
       mie.mind_entry_inds
       params_arity_list
       ([],cst) in
-  (env_arities, inds, cst)
+  (env_arities, Array.of_list inds, cst)
 
 (***********************************************************************)
 (***********************************************************************)
-let all_sorts = [InProp;InSet;InType]
-let impredicative_sorts = [InProp;InSet]
-let logical_sorts = [InProp]
-
-let allowed_sorts issmall isunit = function
-  | Type _ -> all_sorts
-  | Prop Pos -> 
-      if issmall then all_sorts
-      else impredicative_sorts
-  | Prop Null -> 
-(* Added InType which is derivable :when the type is unit and small *)
-      if isunit then 
-	if issmall then all_sorts
-	else impredicative_sorts
-      else logical_sorts
+(* Positivity *)
 
 type ill_formed_ind =
   | LocalNonPos of int
@@ -280,6 +257,12 @@ type ill_formed_ind =
 
 exception IllFormedInd of ill_formed_ind
 
+(* [mind_extract_params mie] extracts the params from an inductive types
+   declaration, and checks that they are all present (and all the same)
+   for all the given types. *)
+
+let mind_extract_params = decompose_prod_n_assum
+
 let explain_ind_err ntyp env0 nbpar c err = 
   let (lpar,c') = mind_extract_params nbpar c in
   let env = push_rel_context lpar env0 in
@@ -305,7 +288,8 @@ let failwith_non_pos_vect n ntypes v =
   anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur in v"
 
 (* Check the inductive type is called with the expected parameters *)
-let check_correct_par env hyps nparams ntypes n l largs =
+let check_correct_par (env,n,ntypes,_) hyps l largs =
+  let nparams = rel_context_nhyps hyps in
   let largs = Array.of_list largs in
   if Array.length largs < nparams then 
     raise (IllFormedInd (LocalNotEnoughArgs l));
@@ -322,7 +306,8 @@ let check_correct_par env hyps nparams ntypes n l largs =
   if not (array_for_all (noccur_between n ntypes) largs') then 
     failwith_non_pos_vect n ntypes largs'
 
-(* This removes global parameters of the inductive types in lc *)
+(* This removes global parameters of the inductive types in lc (for
+   nested inductive types only ) *)
 let abstract_mind_lc env ntyps npars lc = 
   if npars = 0 then 
     lc
@@ -333,50 +318,58 @@ let abstract_mind_lc env ntyps npars lc =
     in 
     Array.map (substl make_abs) lc
 
+let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
+ (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra)
+
+let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) =
+  let auxntyp = 1 in
+  let env' =
+    push_rel (Anonymous,None,
+              hnf_prod_applist env (type_of_inductive env mi) lpar) env in
+  let ra_env' = 
+    (Imbr mi,Rtree.mk_param 0) ::
+    List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
+  (* New index of the inductive types *)
+  let newidx = n + auxntyp in
+  (env', newidx, ntypes, ra_env')
+
 (* The recursive function that checks positivity and builds the list
    of recursive arguments *)
-let check_positivity env ntypes hyps nparams i indlc =
-  let nhyps = List.length hyps in
+let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
+  let nparams = rel_context_length hyps in
   (* check the inductive types occur positively in [c] *)
-  let rec check_pos env n c = 
+  let rec check_pos (env, n, ntypes, ra_env as ienv) c = 
     let x,largs = decompose_app (whd_betadeltaiota env c) in
     match kind_of_term x with
       | Prod (na,b,d) ->
 	  assert (largs = []);
           if not (noccur_between n ntypes b) then
 	    raise (IllFormedInd (LocalNonPos n));
-	  check_pos (push_rel (na, None, b) env) (n+1) d
+	  check_pos (ienv_push_var ienv (na, b, mk_norec)) d
       | Rel k ->
-          if k >= n && k<n+ntypes then begin
-	    check_correct_par env hyps nparams ntypes n (k-n+1) largs;
-	    Mrec(n+ntypes-k-1)
-          end else if List.for_all (noccur_between n ntypes) largs then 
-	    if (n-nhyps) <= k & k <= (n-1) 
-	    then Param(n-1-k)
-            else Norec
-	  else
-	    raise (IllFormedInd (LocalNonPos n))
+          let (ra,rarg) =
+            try List.nth ra_env (k-1)
+            with Failure _ | Invalid_argument _ -> (Norec,mk_norec) in
+          (match ra with
+              Mrec _ -> check_correct_par ienv hyps (k-n+1) largs
+            | _ ->
+                if not (List.for_all (noccur_between n ntypes) largs)
+	        then raise (IllFormedInd (LocalNonPos n)));
+          rarg
       | Ind ind_sp ->
-          (* If the inductive type being defined or a parameter appears as
+          (* If the inductive type being defined appears in a
              parameter, then we have an imbricated type *)
-          if List.for_all (noccur_between n ntypes) largs then
-            (* If parameters are passed but occur negatively, then
-               the argument is considered non recursive *)
-            if List.for_all (noccur_between (n-nhyps) nhyps) largs 
-            then Norec
-            else
-              try check_positive_imbr env n ind_sp largs
-              with IllFormedInd _ -> Norec
-          else check_positive_imbr env n ind_sp largs
+          if List.for_all (noccur_between n ntypes) largs then mk_norec
+          else check_positive_imbr ienv (ind_sp, largs)
       | err -> 
 	  if noccur_between n ntypes x &&
              List.for_all (noccur_between n ntypes) largs 
-	  then Norec
+	  then mk_norec
 	  else raise (IllFormedInd (LocalNonPos n))
 
   (* accesses to the environment are not factorised, but does it worth
      it? *)
-  and check_positive_imbr env n mi largs =
+  and check_positive_imbr (env,n,ntypes,ra_env as ienv) (mi, largs) =
     let (mib,mip) = lookup_mind_specif env mi in
     let auxnpar = mip.mind_nparams in
     let (lpar,auxlargs) =
@@ -386,114 +379,115 @@ let check_positivity env ntypes hyps nparams i indlc =
        definition is not positive. *)
     if not (List.for_all (noccur_between n ntypes) auxlargs) then
       raise (IllFormedInd (LocalNonPos n));
-    (* If the inductive type appears non positively in the
-       parameters then the def is not positive *)
-    let lrecargs = List.map (check_weak_pos env n) lpar in
-    let auxlc = mip.mind_nf_lc in
-    let auxntyp = mib.mind_ntypes in 
     (* We do not deal with imbricated mutual inductive types *)
+    let auxntyp = mib.mind_ntypes in 
     if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
-    (* The abstract imbricated inductive type with parameters substituted *)
-    let auxlcvect = abstract_mind_lc env auxntyp auxnpar auxlc in
+    (* The nested inductive type with parameters removed *)
+    let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in
     (* Extends the environment with a variable corresponding to
        the inductive def *)
-    let env' =
-      push_rel (Anonymous,None,
-                hnf_prod_applist env (type_of_inductive env mi) lpar) env in
-    let newidx = n + auxntyp in
-    let _ = 
+    let (env',_,_,_ as ienv') = ienv_push_inductive ienv (mi,lpar) in
+    (* Parameters expressed in env' *)
+    let lpar' = List.map (lift auxntyp) lpar in
+    let irecargs = 
       (* fails if the inductive type occurs non positively *)
       (* when substituted *) 
       Array.map 
 	(function c -> 
-	  let c' = hnf_prod_applist env c (List.map (lift auxntyp) lpar) in 
-	  check_construct env' false newidx c') 
+	  let c' = hnf_prod_applist env' c lpar' in 
+	  check_constructors ienv' false c') 
 	auxlcvect
     in 
-    Imbr(mi,lrecargs)
-
-  (* The function check_weak_pos is exactly the same as check_pos, but
-     with an extra case for traversing abstractions, like in Marseille's
-     contribution about bisimulations:
-     
-     CoInductive strong_eq:process->process->Prop:=
-       str_eq:(p,q:process)((a:action)(p':process)(transition p a p')->
-          (Ex [q':process] (transition q a q')/\(strong_eq p' q')))->
-             ((a:action)(q':process)(transition q a q')->
-          (Ex [p':process] (transition p a p')/\(strong_eq p' q')))->
-          (strong_eq p q).
-
-     Abstractions may occur in imbricated recursive ocurrences, but I am
-     not sure if they make sense in a form of constructor. This is why I
-     chose to duplicated the code.  Eduardo 13/7/99. *)
-  (* Since Lambda can no longer occur after a product or a Ind,
-     I have branched the remaining cases on check_pos. HH 28/1/00 *)
-
-  and check_weak_pos env n c =
-    let x = whd_betadeltaiota env c in
-    match kind_of_term x with 
-      (* The extra case *)
-      | Lambda (na,b,d) -> 
-          if noccur_between n ntypes b
-          then check_weak_pos (push_rel (na,None,b) env) (n+1) d
-          else raise (IllFormedInd (LocalNonPos n))
-      (******************)
-      | _ -> check_pos env n x
+    (Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0)
   
   (* check the inductive types occur positively in the products of C, if
      check_head=true, also check the head corresponds to a constructor of
      the ith type *) 
 
-  and check_construct env check_head n c = 
-    let rec check_constr_rec env lrec n c = 
+  and check_constructors ienv check_head c = 
+    let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c = 
       let x,largs = decompose_app (whd_betadeltaiota env c) in
       match kind_of_term x with
 
         | Prod (na,b,d) -> 
 	    assert (largs = []);
-            let recarg = check_pos env n b in 
-	    check_constr_rec (push_rel (na, None, b) env)
-	      (recarg::lrec) (n+1) d
+            let recarg = check_pos ienv b in 
+            let ienv' = ienv_push_var ienv (na,b,mk_norec) in
+	    check_constr_rec ienv' (recarg::lrec) d
 
 	| hd ->
 	    if check_head then
-	      if hd = Rel (n+ntypes-i) then
-		check_correct_par env hyps nparams ntypes n (ntypes-i+1) largs
+	      if hd = Rel (n+ntypes-i-1) then
+		check_correct_par ienv hyps (ntypes-i) largs
 	      else
 		raise (IllFormedInd LocalNotConstructor)
 	    else
 	      if not (List.for_all (noccur_between n ntypes) largs)
               then raise (IllFormedInd (LocalNonPos n));
 	    List.rev lrec
-    in check_constr_rec env [] n c
+    in check_constr_rec ienv [] c
   in
-  Array.map
-    (fun c ->
-       let c = body_of_type c in
-       let sign, rawc = mind_extract_params nhyps c in
-       let env' = push_rel_context sign env in
-       try
-	 check_construct env' true (1+nhyps) rawc
-       with IllFormedInd err -> 
-	 explain_ind_err (ntypes-i+1) env nhyps c err)
-    indlc
+  mk_paths (Mrec i)
+    (Array.map
+      (fun c ->
+        let c = body_of_type c in
+        let sign, rawc = mind_extract_params nparams c in
+        let env' = push_rel_context sign env in
+        try
+	  check_constructors ienv true rawc
+        with IllFormedInd err -> 
+	  explain_ind_err (ntypes-i) env nparams c err)
+      indlc)
+
+let check_positivity env_ar inds =
+  let ntypes = Array.length inds in
+  let lra_ind =
+    List.rev (list_tabulate (fun j -> (Mrec j, Rtree.mk_param j)) ntypes) in
+  let check_one i (params,_,_,_,_,_,lc) =
+    let nparams = rel_context_length params in
+    let ra_env =
+      list_tabulate (fun _ -> (Norec,mk_norec)) nparams @ lra_ind in
+    let ienv = (env_ar, 1+nparams, ntypes, ra_env) in
+    check_positivity_one ienv params i lc in
+  Rtree.mk_rec (Array.mapi check_one inds)
+
+
+(***********************************************************************)
+(***********************************************************************)
+(* Build the inductive packet *)
     
-let is_recursive listind =
-  let rec one_is_rec rvec = 
+(* Elimination sorts *)
+let is_recursive = Rtree.is_infinite
+(*  let rec one_is_rec rvec = 
     List.exists (function Mrec(i) -> List.mem i listind 
-                   | Imbr(_,lvec) -> one_is_rec lvec
-                   | Norec -> false
-                   | Param _ -> false) rvec
+                   | Imbr(_,lvec) -> array_exists one_is_rec lvec
+                   | Norec -> false) rvec
   in 
   array_exists one_is_rec
+*)
+
+let all_sorts = [InProp;InSet;InType]
+let impredicative_sorts = [InProp;InSet]
+let logical_sorts = [InProp]
 
-(* Check positivity of an inductive definition *)
-let cci_inductive env env_ar finite inds cst =
-  let ntypes = List.length inds in
+let allowed_sorts issmall isunit = function
+  | Type _ -> all_sorts
+  | Prop Pos -> 
+      if issmall then all_sorts
+      else impredicative_sorts
+  | Prop Null -> 
+(* Added InType which is derivable :when the type is unit and small *)
+      if isunit then 
+	if issmall then all_sorts
+	else impredicative_sorts
+      else logical_sorts
+
+let build_inductive env env_ar finite inds recargs cst =
+  let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let ids = 
-    List.fold_left 
-      (fun acc (_,_,_,ar,_,_,_,lc) -> 
+    Array.fold_left 
+      (fun acc (_,_,ar,_,_,_,lc) -> 
 	 Idset.union (Environ.global_vars_set env (body_of_type ar))
 	   (Array.fold_left
 	      (fun acc c ->
@@ -503,37 +497,40 @@ let cci_inductive env env_ar finite inds cst =
       Idset.empty inds in
   let hyps = keep_hyps env ids in
   (* Check one inductive *)
-  let one_packet i (params,nparams,id,ar,cnames,issmall,isunit,lc) =
-    (* Check positivity *)
-    let recargs = check_positivity env_ar ntypes params nparams i lc in
+  let build_one_packet (params,id,ar,cnames,issmall,isunit,lc) recarg =
     (* Arity in normal form *)
+    let nparams = rel_context_length params in
     let (ar_sign,ar_sort) = dest_arity env ar in
     let nf_ar =
       if isArity (body_of_type ar) then ar
       else it_mkProd_or_LetIn (mkSort ar_sort) ar_sign in
-    (* Elimination sorts *)
-    let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in
-    let kelim = allowed_sorts issmall isunit ar_sort in
     (* Type of constructors in normal form *)
     let splayed_lc = Array.map (dest_prod_assum env_ar) lc in
     let nf_lc =
       array_map2 (fun (d,b) c -> it_mkProd_or_LetIn b d) splayed_lc lc in
     let nf_lc = if nf_lc = lc then lc else nf_lc in
-    (* Build the inductive *)
-    { mind_consnames = Array.of_list cnames;
-      mind_typename = id;
-      mind_user_lc = lc;
-      mind_nf_lc = nf_lc;
+    let carities =
+      Array.map
+        (fun (args,_) -> rel_context_length args - nparams) splayed_lc in
+    (* Elimination sorts *)
+    let isunit = isunit && ntypes = 1 && (not (is_recursive recargs.(0))) in
+    let kelim = allowed_sorts issmall isunit ar_sort in
+    (* Build the inductive packet *)
+    { mind_typename = id;
+      mind_nparams = rel_context_nhyps params;
+      mind_params_ctxt = params;
       mind_user_arity  = ar;
       mind_nf_arity = nf_ar;
       mind_nrealargs = rel_context_length ar_sign - nparams;
       mind_sort = ar_sort;
       mind_kelim = kelim;
-      mind_listrec = recargs;
-      mind_nparams = nparams;
-      mind_params_ctxt = params }
-  in
-  let packets = Array.of_list (list_map_i one_packet 1 inds) in
+      mind_consnames = Array.of_list cnames;
+      mind_user_lc = lc;
+      mind_nf_lc = nf_lc;
+      mind_recargs = recarg;
+    } in
+  let packets = array_map2 build_one_packet inds recargs in
+  (* Build the mutual inductive *)
   { mind_ntypes = ntypes;
     mind_finite = finite;
     mind_hyps = hyps;
@@ -545,7 +542,9 @@ let cci_inductive env env_ar finite inds cst =
 (***********************************************************************)
 
 let check_inductive env mie =
-  (* First type the inductive definition *)
-  let (env_arities, inds, cst) = type_inductive env mie in
-  (* Then check positivity *)
-  cci_inductive env env_arities mie.mind_entry_finite inds cst
+  (* First type-check the inductive definition *)
+  let (env_arities, inds, cst) = typecheck_inductive env mie in
+  (* Then check positivity conditions *)
+  let recargs = check_positivity env_arities inds in
+  (* Build the inductive packets *)
+  build_inductive env env_arities mie.mind_entry_finite inds recargs cst
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 7e803b11e8..532471ebcd 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -52,7 +52,6 @@ then, in $i^{th}$ block, [mind_entry_params] is [[xn:Xn;...;x1:X1]];
 *)
 
 type one_inductive_entry = {
-  mind_entry_nparams : int;
   mind_entry_params : (identifier * local_entry) list;
   mind_entry_typename : identifier;
   mind_entry_arity : constr;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index b45e501eb4..d98adbb37f 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -304,23 +304,21 @@ type guard_env =
     (* inductive of recarg of each fixpoint *)
     inds    : inductive array;
     (* the recarg information of inductive family *)
-    recvec  : recarg list array array;
+    recvec  : wf_paths array;
     (* dB of variables denoting subterms *)
-    lst     : (int * (size * recarg list array)) list;
+    genv    : (int * (size * wf_paths)) list;
   }
 
-let lookup_recargs env ind =
-  let (mib,mip) = lookup_mind_specif env ind in
-  Array.map (fun mip -> mip.mind_listrec) mib.mind_packets
-
 let make_renv env minds recarg (_,tyi as ind) =
-  let mind_recvec = lookup_recargs env ind in 
+  let (mib,mip) = lookup_mind_specif env ind in
+  let mind_recvec =
+    Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
   let lcx = mind_recvec.(tyi)  in
   { env = env;
     rel_min = recarg+2;
     inds = minds;
     recvec = mind_recvec;
-    lst = [(1,(Large,mind_recvec.(tyi)))] }
+    genv = [(1,(Large,mind_recvec.(tyi)))] }
 
 let map_lift_fst_n m = List.map (function (n,t)->(n+m,t))
 
@@ -328,26 +326,27 @@ let push_var_renv renv (x,ty) =
   { renv with 
     env = push_rel (x,None,ty) renv.env;
     rel_min = renv.rel_min+1;
-    lst = map_lift_fst_n 1 renv.lst }
+    genv = map_lift_fst_n 1 renv.genv }
 
 let push_ctxt_renv renv ctxt =
   let n = rel_context_length ctxt in
   { renv with 
     env = push_rel_context ctxt renv.env;
     rel_min = renv.rel_min+n;
-    lst = map_lift_fst_n n renv.lst }
+    genv = map_lift_fst_n n renv.genv }
 
 let push_fix_renv renv (_,v,_ as recdef) =
   let n = Array.length v in
   { renv with
     env = push_rec_types recdef renv.env;
     rel_min = renv.rel_min+n;
-    lst = map_lift_fst_n n renv.lst }
+    genv = map_lift_fst_n n renv.genv }
 
 (* Add a variable and mark it as strictly smaller with information [spec]. *)
 let add_recarg renv (x,a,spec) =
   let renv' = push_var_renv renv (x,a) in
-  { renv' with lst = (1,(Strict,spec))::renv'.lst }
+  if spec = mk_norec then renv'
+  else { renv' with genv = (1,(Strict,spec))::renv'.genv }
 
 (* Fetch recursive information about a variable *)
 let subterm_var p renv = 
@@ -355,7 +354,7 @@ let subterm_var p renv =
     | (a,ta)::l -> 
         if a < p then findrec l else if a = p then Some ta else None
     | _ -> None in
-  findrec renv.lst
+  findrec renv.genv
 
 
 (******************************)
@@ -373,38 +372,24 @@ let subterm_var p renv =
    correct envs and decreasing args.
 *)
 
-let lookup_subterms env (_,i as ind) =
-  (lookup_recargs env ind).(i)
-
-let imbr_recarg_expand env (sp,i as ind_sp) lrc =
-  let recargs = lookup_subterms env ind_sp in
-  let rec imbr_recarg ra = 
-    match ra with 
-      | Mrec(j)        -> Imbr((sp,j),lrc)
-      | Imbr(ind_sp,l) -> Imbr(ind_sp, List.map imbr_recarg l)
-      | Norec          -> Norec
-      | Param(k)       -> List.nth lrc k in
-  Array.map (List.map imbr_recarg) recargs
+let lookup_subterms env ind =
+  let (_,mip) = lookup_mind_specif env ind in
+  mip.mind_recargs
 
 
-let case_branches_specif renv = 
+let case_branches_specif renv spec lc = 
   let rec crec renv lrec c = 
     let c' = strip_outer_cast c in 
     match lrec, kind_of_term c' with 
       |	(ra::lr,Lambda (x,a,b)) ->
-          let renv' =
-            match ra with 
-	        Mrec(i) -> add_recarg renv (x,a,renv.recvec.(i))
-              | Imbr(ind_sp,lrc) ->
-                  let lc = imbr_recarg_expand renv.env ind_sp lrc in
-                  add_recarg renv (x,a,lc)
-	      | _ -> push_var_renv renv (x,a) in
+          let renv' = add_recarg renv (x,a,ra) in
           crec renv' lr b
       | (_,LetIn (x,c,a,b)) -> crec renv lrec (subst1 c b)
       (* Rq: if branch is not eta-long, then the recursive information
          is not propagated: *)
-      | (_,_) -> (renv,c')
-  in array_map2 (crec renv) 
+      | (_,_) -> (renv,c') in
+  if spec = mk_norec then Array.map (fun c -> (renv,c)) lc
+  else array_map2 (crec renv) (dest_subterms spec) lc
 
 (*********************************)
 
@@ -431,74 +416,70 @@ let inductive_of_fix env recarg body =
    - [Some lc] if [c] is a strict subterm of the rec. arg. (or a Meta) 
    - [None] otherwise
 *)
-let subterm_specif renv c ind = 
-  let rec crec renv c ind = 
-    let f,l = decompose_app (whd_betadeltaiota renv.env c) in
-    match kind_of_term f with 
-      | Rel k -> subterm_var k renv
-
-      | Case (ci,_,c,lbr) ->
-          if Array.length lbr = 0
-            (* New: if it is built by contadiction, it is OK *)
-          then Some (Strict,[||])
-          else
-            let def = Array.create (Array.length lbr) [] in
-            let lcv =
-              match crec renv c ci.ci_ind with
+let rec subterm_specif renv c ind = 
+  let f,l = decompose_app (whd_betadeltaiota renv.env c) in
+  match kind_of_term f with 
+    | Rel k -> subterm_var k renv
+
+    | Case (ci,_,c,lbr) ->
+        if Array.length lbr = 0
+        (* New: if it is built by contadiction, it is OK *)
+        then Some (Strict,mk_norec)
+        else
+          let lcv =
+            match subterm_specif renv c ci.ci_ind with
                 Some (_,lr) -> lr
-              | None -> def in 
-            let lbr' = case_branches_specif renv lcv lbr in
-            let stl  =
-              Array.map (fun (renv',br') -> crec renv' br' ind) lbr' in
-            let stl0 = stl.(0) in
-	    if array_for_all (fun st -> st=stl0) stl then stl0 
-            (* branches do not return objects with same spec *)
-            else None
+              | None -> mk_norec in 
+          let lbr' = case_branches_specif renv lcv lbr in
+          let stl  =
+            Array.map (fun (renv',br') -> subterm_specif renv' br' ind) lbr' in
+          let stl0 = stl.(0) in
+	  if array_for_all (fun st -> st=stl0) stl then stl0 
+          (* branches do not return objects with same spec *)
+          else None
 	       
-      | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
+    | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
 (* when proving that the fixpoint f(x)=e is less than n, it is enough
    to prove that e is less than n assuming f is less than n
    furthermore when f is applied to a term which is strictly less than
    n, one may assume that x itself is strictly less than n
 *)
-          let nbfix = Array.length typarray in
-          let recargs = lookup_subterms renv.env ind in
-          (* pushing the fixpoints *)
-          let renv' = push_fix_renv renv recdef in
-          let renv' =
-            { renv' with lst=(nbfix-i,(Strict,recargs))::renv'.lst } in
-          let decrArg = recindxs.(i) in 
-          let theBody = bodies.(i)   in
-          let nbOfAbst = decrArg+1 in
-          let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
-          (* pushing the fix parameters *)
-          let renv'' = push_ctxt_renv renv' sign in
-          let renv'' =
-            { renv'' with
-              lst =
-              if List.length l < nbOfAbst then renv''.lst
+        let nbfix = Array.length typarray in
+        let recargs = lookup_subterms renv.env ind in
+        (* pushing the fixpoints *)
+        let renv' = push_fix_renv renv recdef in
+        let renv' =
+          { renv' with genv=(nbfix-i,(Strict,recargs))::renv'.genv } in
+        let decrArg = recindxs.(i) in 
+        let theBody = bodies.(i)   in
+        let nbOfAbst = decrArg+1 in
+        let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
+        (* pushing the fix parameters *)
+        let renv'' = push_ctxt_renv renv' sign in
+        let renv'' =
+          { renv'' with
+            genv =
+              if List.length l < nbOfAbst then renv''.genv
               else
                 let decrarg_ind =
                   inductive_of_fix renv''.env decrArg theBody in
                 let theDecrArg  = List.nth l decrArg in
 	        try 
-	          match crec renv theDecrArg decrarg_ind with 
-		    (Some recArgsDecrArg) ->
-                      (1,recArgsDecrArg) :: renv''.lst 
-                  | None -> renv''.lst
-	        with Not_found -> renv''.lst } in
-	  crec renv'' strippedBody ind
+	          match subterm_specif renv theDecrArg decrarg_ind with 
+		      (Some recArgsDecrArg) ->
+                        (1,recArgsDecrArg) :: renv''.genv 
+                    | None -> renv''.genv
+	        with Not_found -> renv''.genv } in
+	subterm_specif renv'' strippedBody ind
 	    
-      | Lambda (x,a,b) -> 
-          assert (l=[]);
-          crec (push_var_renv renv (x,a)) b ind
-
-      (* A term with metas is considered OK *)
-      | Meta _ -> Some (Strict,lookup_subterms renv.env ind)
-      (* Other terms are not subterms *)
-      | _ -> None
-  in 
-  crec renv c ind
+    | Lambda (x,a,b) -> 
+        assert (l=[]);
+        subterm_specif (push_var_renv renv (x,a)) b ind
+
+    (* A term with metas is considered OK *)
+    | Meta _ -> Some (Strict,lookup_subterms renv.env ind)
+    (* Other terms are not subterms *)
+    | _ -> None
 
 (* Propagation of size information through Cases: if the matched
    object is a recursive subterm then compute the information
@@ -506,9 +487,7 @@ let subterm_specif renv c ind =
 let spec_subterm_large renv c ind = 
   match subterm_specif renv c ind with
     Some (_,lr) -> lr
-  | None ->
-      let nb = Array.length (lookup_subterms renv.env ind) in
-      Array.create nb []
+  | None -> mk_norec
 
 (* Check term c can be applied to one of the mutual fixpoints. *)
 let check_is_subterm renv c ind = 
@@ -632,7 +611,7 @@ let check_one_fix renv recpos def =
   and check_nested_fix_body renv decr recArgsDecrArg body =
     if decr = 0 then
       check_rec_call
-        { renv with lst=(1,recArgsDecrArg)::renv.lst } body
+        { renv with genv=(1,recArgsDecrArg)::renv.genv } body
     else
       match kind_of_term body with
 	| Lambda (x,a,b) ->
@@ -707,22 +686,17 @@ exception CoFixGuardError of guard_error
 let anomaly_ill_typed () =
   anomaly "check_one_cofix: too many arguments applied to constructor"
 
+let rec codomain_is_coind env c =
+  let b = whd_betadeltaiota env c in
+  match kind_of_term b with
+    | Prod (x,a,b) ->
+	codomain_is_coind (push_rel (x, None, a) env) b 
+    | _ -> 
+	(try find_coinductive env b
+        with Not_found ->
+	  raise (CoFixGuardError (CodomainNotInductiveType b)))
 
 let check_one_cofix env nbfix def deftype = 
-  let rec codomain_is_coind env c =
-    let b = whd_betadeltaiota env c in
-    match kind_of_term b with
-      | Prod (x,a,b) ->
-	  codomain_is_coind (push_rel (x, None, a) env) b 
-      | _ -> 
-	  (try find_coinductive env b
-           with Not_found ->
-	     raise (CoFixGuardError (CodomainNotInductiveType b)))
-  in
-  let (mind, _) = codomain_is_coind env deftype in
-  let (sp,tyi) = mind in
-  let lvlra = lookup_recargs env (sp,tyi) in
-  let vlra = lvlra.(tyi) in  
   let rec check_rec_call env alreadygrd n vlra  t =
     if noccur_with_meta n nbfix t then
       true 
@@ -749,29 +723,20 @@ let check_one_cofix env nbfix def deftype =
             let mI = inductive_of_constructor cstr_sp in
 	    let (mib,mip) = lookup_mind_specif env mI in
             let _,realargs = list_chop mip.mind_nparams args in
-            let rec process_args_of_constr l lra =
-              match l with
-                | [] -> true 
-                | t::lr ->
-		    (match lra  with 
-                       | [] -> anomaly_ill_typed () 
-                       |  (Mrec i)::lrar -> 
-                            let newvlra = lvlra.(i) in
-                            (check_rec_call env true n newvlra t) &&
-                            (process_args_of_constr lr lrar)
-			    
-                       |  (Imbr((sp,i) as ind_sp,lrc)::lrar)  ->
-                            let lc = imbr_recarg_expand env ind_sp lrc in
-                            check_rec_call env true n lc t &
-                            process_args_of_constr lr lrar
-				 
-                       |  _::lrar  -> 
-                            if (noccur_with_meta n nbfix t) 
-                            then (process_args_of_constr lr lrar)
-                            else raise (CoFixGuardError
-					  (RecCallInNonRecArgOfConstructor t)))
-            in (process_args_of_constr realargs lra)
-		 
+            let rec process_args_of_constr = function
+              | (t::lr), (rar::lrar) -> 
+                  if rar = mk_norec then
+                    if noccur_with_meta n nbfix t
+                    then process_args_of_constr (lr, lrar)
+                    else raise (CoFixGuardError
+		                 (RecCallInNonRecArgOfConstructor t))
+                  else
+                    let spec = dest_subterms rar in
+                    check_rec_call env true n spec t &&
+                    process_args_of_constr (lr, lrar)
+              | [],_ -> true 
+              | _ -> anomaly_ill_typed () 
+            in process_args_of_constr (realargs, lra)
 		 
 	| Lambda (x,a,b) ->
 	     assert (args = []);
@@ -808,10 +773,10 @@ let check_one_cofix env nbfix def deftype =
             else 
 	      raise (CoFixGuardError (RecCallInCasePred c))
               
-	| _    -> raise (CoFixGuardError NotGuardedForm)
-	      
-  in 
-  check_rec_call env false 1 vlra def
+	| _    -> raise (CoFixGuardError NotGuardedForm) in 
+  let (mind, _) = codomain_is_coind env deftype in
+  let vlra = lookup_subterms env mind in
+  check_rec_call env false 1 (dest_subterms vlra) def
 
 (* The  function which checks that the whole block of definitions 
    satisfies the guarded condition *)
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 20bd1e03a6..e1c9fbe4b0 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -20,13 +20,19 @@ type named_context = named_declaration list
 
 let empty_named_context = []
 
-let add_named_decl d sign = d::sign
 
 let rec lookup_named id = function
   | (id',_,_ as decl) :: _ when id=id' -> decl
   | _ :: sign -> lookup_named id sign
   | [] -> raise Not_found
 
+  
+let add_named_decl (id,_,_ as d) sign =
+  try
+    let _ = lookup_named id sign in 
+    failwith ("identifier "^string_of_id id^" already defined")
+  with _ -> d::sign
+
 let named_context_length = List.length
 
 let pop_named_decl id = function
@@ -66,6 +72,13 @@ let lookup_rel n sign =
 
 let rel_context_length = List.length
 
+let rel_context_nhyps hyps =
+  let rec nhyps acc = function
+    | [] -> acc
+    | (_,None,_)::hyps -> nhyps (1+acc) hyps
+    | (_,Some _,_)::hyps -> nhyps acc hyps in
+  nhyps 0 hyps
+
 let fold_rel_context f l ~init:x = List.fold_right f l x
 let fold_rel_context_reverse f ~init:x l = List.fold_left f x l
 
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 6667b598c3..a35f61d229 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -46,6 +46,7 @@ val add_rel_decl : rel_declaration -> rel_context -> rel_context
 
 val lookup_rel : int -> rel_context -> rel_declaration
 val rel_context_length : rel_context -> int
+val rel_context_nhyps : rel_context -> int
 
 val push_named_to_rel_context : named_context -> rel_context -> rel_context
 
-- 
cgit v1.2.3