Restructuration des outils pour les inductifs.

- Les déclarations (mutual_inductive_packet et mutual_inductive_body),
  utilisisées dans Environ vont dans Constant
- Instantiations du context local (mind_specif), instantiation des
  paramètres globaux (inductive_family) et instantiation complète
  (inductive_type, nouveau nom de inductive_summary) vont dans
  Inductive qui est déplacé après réduction
- Certaines fonctions de Typeops et celle traitant des inductifs dans Reduction
  sont regroupées dans Inductive


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@438 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 456 insertions, 359 deletions

diff --git a/kernel/constant.ml b/kernel/constant.ml
index dda7274af..7f45aae57 100644
--- a/kernel/constant.ml
+++ b/kernel/constant.ml
@@ -7,6 +7,8 @@ open Generic
 open Term
 open Sign
 
+(* Constant entries *)
+
 type lazy_constant_value =
   | Cooked of constr
   | Recipe of (unit -> constr)
@@ -34,3 +36,41 @@ type constant_entry = {
   const_entry_body : lazy_constant_value;
   const_entry_type : constr option }
 
+(* Inductive entries *)
+
+type recarg = 
+  | Param of int 
+  | Norec 
+  | Mrec of int 
+  | Imbr of inductive_path * recarg list
+
+type mutual_inductive_packet = {
+  mind_consnames : identifier array;
+  mind_typename : identifier;
+  mind_lc : constr;
+  mind_arity : typed_type;
+  mind_sort : sorts;
+  mind_nrealargs : int;
+  mind_kelim : sorts list;
+  mind_listrec : (recarg list) array;
+  mind_finite : bool }
+
+type mutual_inductive_body = {
+  mind_kind : path_kind;
+  mind_ntypes : int;
+  mind_hyps : typed_type signature;
+  mind_packets : mutual_inductive_packet array;
+  mind_constraints : constraints;
+  mind_singl : constr option;
+  mind_nparams : int }
+
+let mind_type_finite mib i = mib.mind_packets.(i).mind_finite
+
+(*s Declaration. *)
+
+type mutual_inductive_entry = {
+  mind_entry_nparams : int;
+  mind_entry_finite : bool;
+  mind_entry_inds : (identifier * constr * identifier list * constr) list }
+
+let mind_nth_type_packet mib n = mib.mind_packets.(n)
diff --git a/kernel/constant.mli b/kernel/constant.mli
index c24280c40..16894c735 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -36,3 +36,43 @@ type constant_entry= {
   const_entry_body : lazy_constant_value;
   const_entry_type : constr option }
 
+(* Inductive types (internal representation). *)
+
+type recarg = 
+  | Param of int 
+  | Norec 
+  | Mrec of int 
+  | Imbr of inductive_path * (recarg list)
+
+type mutual_inductive_packet = {
+  mind_consnames : identifier array;
+  mind_typename : identifier;
+  mind_lc : constr;
+  mind_arity : typed_type;
+  mind_sort : sorts;
+  mind_nrealargs : int;
+  mind_kelim : sorts list;
+  mind_listrec : (recarg list) array;
+  mind_finite : bool }
+
+type mutual_inductive_body = {
+  mind_kind : path_kind;
+  mind_ntypes : int;
+  mind_hyps : typed_type signature;
+  mind_packets : mutual_inductive_packet array;
+  mind_constraints : constraints;
+  mind_singl : constr option;
+  mind_nparams : int }
+
+val mind_type_finite : mutual_inductive_body -> int -> bool
+
+val mind_nth_type_packet : 
+  mutual_inductive_body -> int -> mutual_inductive_packet
+
+(*s Declaration of inductive types. *)
+
+type mutual_inductive_entry = {
+  mind_entry_nparams : int;
+  mind_entry_finite : bool;
+  mind_entry_inds : (identifier * constr * identifier list * constr) list }
+
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 512c4b43c..823e4e612 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -7,33 +7,9 @@ open Univ
 open Generic
 open Term
 open Sign
-
-type recarg = 
-  | Param of int 
-  | Norec 
-  | Mrec of int 
-  | Imbr of inductive_path * recarg list
-
-type mutual_inductive_packet = {
-  mind_consnames : identifier array;
-  mind_typename : identifier;
-  mind_lc : constr;
-  mind_arity : typed_type;
-  mind_nrealargs : int;
-  mind_kelim : sorts list;
-  mind_listrec : (recarg list) array;
-  mind_finite : bool }
-
-type mutual_inductive_body = {
-  mind_kind : path_kind;
-  mind_ntypes : int;
-  mind_hyps : typed_type signature;
-  mind_packets : mutual_inductive_packet array;
-  mind_constraints : constraints;
-  mind_singl : constr option;
-  mind_nparams : int }
-
-let mind_type_finite mib i = mib.mind_packets.(i).mind_finite
+open Constant
+open Environ
+open Reduction
 
 type mind_specif = {
   mis_sp : section_path;
@@ -43,6 +19,7 @@ type mind_specif = {
   mis_mip : mutual_inductive_packet }
 
 let mis_ntypes mis = mis.mis_mib.mind_ntypes
+let mis_index mis = mis.mis_tyi
 let mis_nconstr mis = Array.length (mis.mis_mip.mind_consnames)
 let mis_nparams mis = mis.mis_mib.mind_nparams
 let mis_nrealargs mis = mis.mis_mip.mind_nrealargs
@@ -54,6 +31,56 @@ let mis_typename mis = mis.mis_mip.mind_typename
 let mis_typepath mis =
   make_path (dirpath mis.mis_sp) mis.mis_mip.mind_typename CCI
 let mis_consnames mis = mis.mis_mip.mind_consnames
+let mis_inductive mis = ((mis.mis_sp,mis.mis_tyi),mis.mis_args)
+
+let mis_lc mis =
+  Instantiate.instantiate_constr
+    (ids_of_sign mis.mis_mib.mind_hyps) mis.mis_mip.mind_lc
+    (Array.to_list mis.mis_args)
+
+let mis_lc_without_abstractions mis = 
+  let rec strip_DLAM = function
+    | (DLAM (n,c1)) -> strip_DLAM c1 
+    | (DLAMV (n,v)) -> v
+    | _ -> assert false
+  in 
+  strip_DLAM (mis_lc mis)
+
+let mis_type_mconstructs mispec =
+  let specif = mis_lc mispec
+  and ntypes = mis_ntypes mispec
+  and nconstr = mis_nconstr mispec in
+  let make_Ik k = mkMutInd ((mispec.mis_sp,k),mispec.mis_args) 
+  and make_Ck k = mkMutConstruct (((mispec.mis_sp,mispec.mis_tyi),k+1),
+		       mispec.mis_args) in
+  (Array.init nconstr make_Ck, 
+   sAPPVList specif (list_tabulate make_Ik ntypes))
+
+let mis_typed_arity mis =
+  let idhyps = ids_of_sign mis.mis_mib.mind_hyps 
+  and largs = Array.to_list mis.mis_args in
+  Instantiate.instantiate_type idhyps mis.mis_mip.mind_arity largs
+
+let mis_arity mispec = incast_type (mis_typed_arity mispec)
+
+let mis_params_ctxt mispec =
+  let paramsign,_ =
+    decompose_prod_n mispec.mis_mib.mind_nparams
+      (body_of_type (mis_typed_arity mispec))
+  in paramsign
+
+let mis_sort mispec = mispec.mis_mip.mind_sort
+
+let liftn_inductive_instance n depth mis = {
+  mis_sp = mis.mis_sp;
+  mis_mib = mis.mis_mib;
+  mis_tyi = mis.mis_tyi;
+  mis_args = Array.map (liftn n depth) mis.mis_args;
+  mis_mip = mis.mis_mip
+}
+
+let lift_inductive_instance n = liftn_inductive_instance n 1
+
 
 type constructor_summary = {
   cs_cstr : constructor;
@@ -63,31 +90,58 @@ type constructor_summary = {
   cs_concl_realargs : constr array
 }
 
-(* A light version of mind_specif_of_mind with pre-splitted args *)
-(* and a receipt to build a summary of constructors *)
-type inductive_summary = {
+let lift_constructor n cs = {
+  cs_cstr = (let (csp,ctxt) = cs.cs_cstr in (csp,Array.map (lift n) ctxt));
+  cs_params = List.map (lift n) cs.cs_params;
+  cs_nargs = cs.cs_nargs;
+  cs_args = lift_context n cs.cs_args;
+  cs_concl_realargs = Array.map (liftn n (cs.cs_nargs+1)) cs.cs_concl_realargs
+}
+
+(* [inductive_family] = [inductive_instance] applied to global parameters *)
+type inductive_family = IndFamily of mind_specif * constr list
+(* = {
   mind : inductive;
   params : constr list;
-  realargs : constr list;
   nparams : int;
   nrealargs : int;
   nconstr : int;
-}
+  ind_kelim : sorts list;
+} *)
 
-let is_recursive listind = 
+type inductive_type = IndType of inductive_family * constr list
+
+let liftn_inductive_family n d (IndFamily (mis, params)) =
+  IndFamily (liftn_inductive_instance n d mis, List.map (liftn n d) params)
+let lift_inductive_family n = liftn_inductive_family n 1
+
+let liftn_inductive_type n d (IndType (indf, realargs)) =
+  IndType (liftn_inductive_family n d indf, List.map (liftn n d) realargs)
+let lift_inductive_type n = liftn_inductive_type n 1
+
+let make_ind_family (mis, params) = IndFamily (mis,params)
+let dest_ind_family (IndFamily (mis,params)) = (mis,params)
+
+let make_ind_type (indf, realargs) = IndType (indf,realargs)
+let dest_ind_type (IndType (indf,realargs)) = (indf,realargs)
+
+let mkAppliedInd (IndType (IndFamily (mis,params), realargs)) =
+  applist (mkMutInd (mis_inductive mis),params@realargs)
+
+let mis_is_recursive_subset listind mis = 
   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
+    List.exists
+      (function
+	 | Mrec i       -> List.mem i listind 
+         | Imbr(_,lvec) -> one_is_rec lvec
+         | Norec        -> false
+         | Param _      -> false) rvec
   in 
-  array_exists one_is_rec
+  array_exists one_is_rec (mis_recarg mis)
 
 let mis_is_recursive mis =
-  is_recursive (interval 0 ((mis_ntypes mis)-1)) (mis_recarg mis)
+  mis_is_recursive_subset (interval 0 ((mis_ntypes mis)-1)) mis
 
-let mind_nth_type_packet mib n = mib.mind_packets.(n)
 
 (* Annotation for cases *)
 let make_case_info mis style pats_source =
@@ -100,12 +154,7 @@ let make_case_info mis style pats_source =
 let make_default_case_info mis =
   make_case_info mis None (Array.init (mis_nconstr mis) (fun _ -> RegularPat))
 
-(*s Declaration. *)
-
-type mutual_inductive_entry = {
-  mind_entry_nparams : int;
-  mind_entry_finite : bool;
-  mind_entry_inds : (identifier * constr * identifier list * constr) list }
+(*s Useful functions *)
 
 let inductive_path_of_constructor_path (ind_sp,i) = ind_sp
 let ith_constructor_path_of_inductive_path ind_sp i = (ind_sp,i)
@@ -118,7 +167,82 @@ let build_dependent_constructor cs =
     (mkMutConstruct cs.cs_cstr,
      (List.map (lift cs.cs_nargs) cs.cs_params)@(rel_list 0 cs.cs_nargs))
 
-let build_dependent_inductive is =
+let build_dependent_inductive (IndFamily (mis, params)) =
+  let nrealargs = mis_nrealargs mis in
   applist 
-    (mkMutInd is.mind,
-     (List.map (lift is.nparams) is.params)@(rel_list 0 is.nrealargs))
+    (mkMutInd (mis_inductive mis),
+     (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
+
+exception Induc
+
+let find_mrectype env sigma c =
+  let (t,l) = whd_betadeltaiota_stack env sigma c [] in
+  match t with
+    | DOPN(MutInd ind_sp,args) ->  ((ind_sp,args),l)
+    | _ -> raise Induc
+
+let find_minductype env sigma c =
+  let (t,l) = whd_betadeltaiota_stack env sigma c [] in
+  match t with
+    | DOPN(MutInd (sp,i),_)
+        when mind_type_finite (lookup_mind sp env) i -> (destMutInd t,l)
+    | _ -> raise Induc
+
+let find_mcoinductype env sigma c =
+  let (t,l) = whd_betadeltaiota_stack env sigma c [] in
+  match t with
+    | DOPN(MutInd (sp,i),_)
+        when not (mind_type_finite (lookup_mind sp env) i) -> (destMutInd t,l)
+    | _ -> raise Induc
+
+(* raise Induc if not an inductive type *)
+let lookup_mind_specif ((sp,tyi),args) env =
+  let mib = lookup_mind sp env in
+  { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_args = args;
+    mis_mip = mind_nth_type_packet mib tyi }
+
+let find_inductive env sigma ty =
+  let (mind,largs) = find_minductype env sigma ty in
+  let mispec = lookup_mind_specif mind env in 
+  let nparams = mis_nparams mispec in
+  let (params,realargs) = list_chop nparams largs in
+  make_ind_type (make_ind_family (mispec,params),realargs)
+
+let get_constructors (IndFamily (mispec,params)) =
+  let specif = mis_lc mispec in
+  let make_ik i = DOPN (MutInd (mispec.mis_sp,i), mispec.mis_args) in
+  let types = sAPPVList specif (list_tabulate make_ik (mis_ntypes mispec)) in
+  let make_ck j =
+    let (args,ccl) = decompose_prod (prod_applist types.(j) params) in
+    let (_,vargs) = array_chop (mis_nparams mispec + 1) (destAppL (ensure_appl ccl)) in
+    { cs_cstr = ith_constructor_of_inductive (mis_inductive mispec) (j+1);
+      cs_params = params;
+      cs_nargs = List.length args;
+      cs_args = args;
+      cs_concl_realargs = vargs } in
+  Array.init (mis_nconstr mispec) make_ck
+
+let get_arity env sigma (IndFamily (mispec,params)) =
+  let arity = mis_arity mispec in
+  splay_arity env sigma (prod_applist arity params)
+
+(* builds the arity of an elimination predicate in sort [s] *)
+let make_arity env sigma dep indf s =
+  let (arsign,_) = get_arity env sigma indf in
+  if dep then
+    (* We need names everywhere *)
+    it_prod_name env
+      (mkArrow (build_dependent_inductive indf) (mkSort s)) arsign
+  else
+    (* No need to enforce names *)
+    prod_it (mkSort s) arsign
+
+(* [p] is the predicate and [cs] a constructor summary *)
+let build_branch_type env dep p cs =
+  let base = appvect (lift cs.cs_nargs p, cs.cs_concl_realargs) in
+  if dep then
+    it_prod_name env
+      (applist (base,[build_dependent_constructor cs]))
+      cs.cs_args
+  else
+    prod_it base cs.cs_args
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index f7d371417..51ea86f30 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -6,38 +6,11 @@ open Names
 open Univ
 open Term
 open Sign
+open Constant
+open Environ
+open Evd
 (*i*)
 
-(* Inductive types (internal representation). *)
-
-type recarg = 
-  | Param of int 
-  | Norec 
-  | Mrec of int 
-  | Imbr of inductive_path * (recarg list)
-
-type mutual_inductive_packet = {
-  mind_consnames : identifier array;
-  mind_typename : identifier;
-  mind_lc : constr;
-  mind_arity : typed_type;
-  mind_nrealargs : int;
-  mind_kelim : sorts list;
-  mind_listrec : (recarg list) array;
-  mind_finite : bool }
-
-type mutual_inductive_body = {
-  mind_kind : path_kind;
-  mind_ntypes : int;
-  mind_hyps : typed_type signature;
-  mind_packets : mutual_inductive_packet array;
-  mind_constraints : constraints;
-  mind_singl : constr option;
-  mind_nparams : int }
-
-val mind_type_finite : mutual_inductive_body -> int -> bool
-
-
 (*s To give a more efficient access to the informations related to a given
   inductive type, we introduce the following type [mind_specif], which
   contains all the informations about the inductive type, including its
@@ -50,6 +23,7 @@ type mind_specif = {
   mis_args : constr array;
   mis_mip : mutual_inductive_packet }
 
+val mis_index : mind_specif -> int
 val mis_ntypes : mind_specif -> int
 val mis_nconstr : mind_specif -> int
 val mis_nparams : mind_specif -> int
@@ -59,16 +33,17 @@ val mis_recargs : mind_specif -> (recarg list) array array
 val mis_recarg : mind_specif -> (recarg list) array
 val mis_typename : mind_specif -> identifier
 val mis_typepath : mind_specif -> section_path
-val is_recursive : int list -> recarg list array -> bool
+val mis_is_recursive_subset : int list -> mind_specif -> bool
 val mis_is_recursive : mind_specif -> bool
 val mis_consnames : mind_specif -> identifier array
-
-val mind_nth_type_packet : 
-  mutual_inductive_body -> int -> mutual_inductive_packet
-
-val make_case_info : mind_specif -> case_style option -> pattern_source array 
-      -> case_info
-val make_default_case_info : mind_specif -> case_info
+val mis_typed_arity : mind_specif -> typed_type
+val mis_inductive : mind_specif -> inductive
+val mis_arity : mind_specif -> constr
+val mis_lc : mind_specif -> constr
+val mis_lc_without_abstractions : mind_specif -> constr array
+val mis_type_mconstructs : mind_specif -> constr array * constr array
+val mis_params_ctxt : mind_specif -> (name * constr) list
+val mis_sort : mind_specif -> sorts
 
 (*s This type gathers useful informations about some instance of a constructor
     relatively to some implicit context (the current one)
@@ -88,6 +63,8 @@ type constructor_summary = {
   cs_concl_realargs : constr array
 }
 
+val lift_constructor : int -> constructor_summary -> constructor_summary
+
 (*s A variant of [mind_specif_of_mind] with pre-splitted args
 
    We recover the inductive type as \par
@@ -96,21 +73,25 @@ type constructor_summary = {
 
  *)
 
-type inductive_summary = {
-  mind : inductive;
-  params : constr list;
-  realargs : constr list;
-  nparams : int;
-  nrealargs : int;
-  nconstr : int;
-}
+(* [inductive_family] = [inductive_instance] applied to global parameters *)
+type inductive_family = IndFamily of mind_specif * constr list
+
+val make_ind_family : mind_specif * constr list -> inductive_family
+val dest_ind_family : inductive_family -> mind_specif * constr list
+
+(* [inductive_type] = [inductive_family] applied to ``real'' parameters *)
+type inductive_type = IndType of inductive_family * constr list
 
-(*s Declaration of inductive types. *)
+val make_ind_type : inductive_family * constr list -> inductive_type
+val dest_ind_type : inductive_type -> inductive_family * constr list
 
-type mutual_inductive_entry = {
-  mind_entry_nparams : int;
-  mind_entry_finite : bool;
-  mind_entry_inds : (identifier * constr * identifier list * constr) list }
+val mkAppliedInd : inductive_type -> constr
+
+val liftn_inductive_family : int -> int -> inductive_family -> inductive_family
+val lift_inductive_family : int -> inductive_family -> inductive_family
+
+val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
+val lift_inductive_type : int -> inductive_type -> inductive_type
 
 val inductive_of_constructor : constructor -> inductive
 
@@ -122,9 +103,93 @@ val ith_constructor_path_of_inductive_path :
   inductive_path -> int -> constructor_path
 
 (* This builds [(ci params (Rel 1)...(Rel ci_nargs))] which is the argument
-   of predicate in a cases branch *)
+   of a dependent predicate in a Cases branch *)
 val build_dependent_constructor : constructor_summary -> constr
 
-(* This builds [(I params (Rel 1)...(Rel nrealargs))] which is the argument
-   of predicate in a cases branch *)
-val build_dependent_inductive : inductive_summary -> constr
+(* This builds [(I params (Rel 1)...(Rel nrealargs))] which is the type of
+   the constructor argument of a dependent predicate in a cases branch *)
+val build_dependent_inductive : inductive_family -> constr
+
+(* if the arity for some inductive family [indf] associated to [(I
+   params)] is [(x1:A1)...(xn:An)sort'] then [make_arity env sigma dep
+   indf k] builds [(x1:A1)...(xn:An)sort] which is the arity of an
+   elimination predicate on sort [k]; if [dep=true] then it rather
+   builds [(x1:A1)...(xn:An)(I params x1...xn)->sort] *)
+val make_arity : env -> 'a evar_map -> bool -> inductive_family ->
+  sorts -> constr
+
+(* [build_branch_type env dep p cs] builds the type of the branch
+   associated to constructor [cs] in a Case with elimination predicate
+   [p]; if [dep=true], the predicate is assumed dependent *)
+val build_branch_type : env -> bool -> constr -> constructor_summary -> constr 
+
+(* [find_m*type env sigma c] coerce [c] to an recursive type (I args).
+   [find_mrectype], [find_minductype] and [find_mcoinductype]
+   respectively accepts any recursive type, only an inductive type and
+   only a coinductive type.
+   They raise [Induc] if not convertible to a recursive type. *)
+
+exception Induc
+val find_mrectype     : env -> 'a evar_map -> constr -> inductive * constr list
+val find_minductype   : env -> 'a evar_map -> constr -> inductive * constr list
+val find_mcoinductype : env -> 'a evar_map -> constr -> inductive * constr list
+
+val lookup_mind_specif : inductive -> env -> mind_specif
+
+(* [find_inductive env sigma t] builds an [inductive_type] or raises
+   [Induc] if [t] is not an inductive type; The result is relative to
+   [env] and [sigma] *)
+
+val find_inductive : env -> 'a evar_map -> constr -> inductive_type
+
+(* [get_constructors indf] build an array of [constructor_summary]
+   from some inductive type already analysed as an [inductive_family];
+   global parameters are already instanciated in the constructor
+   types; the resulting summaries are valid in the environment where
+   [indf] is valid the names of the products of the constructors types
+   are not renamed when [Anonymous] *)
+
+val get_constructors : inductive_family -> constructor_summary array
+
+(* [get_arity env sigma inf] returns the product and the sort of the
+   arity of the inductive family described by [is]; global parameters are
+   already instanciated; [indf] must be defined w.r.t. [env] and [sigma];
+   the products signature is relative to [env] and [sigma]; the names
+   of the products of the constructors types are not renamed when
+   [Anonymous] *)
+
+val get_arity : env -> 'a evar_map -> inductive_family ->
+      (name * constr) list * sorts
+
+(* Examples: assume
+  
+\begin{verbatim}
+Inductive listn [A:Set] : nat -> Set :=
+  niln : (listn A O)
+| consn : (n:nat)A->(listn A n)->(listn A (S n)).
+\end{verbatim}
+
+has been defined. Then in some env containing ['x:nat'], 
+
+[find_inductive env sigma (listn bool (S x))] returns
+
+[is = {mind = 'listn'; params = 'bool'; realargs = '(S x)';
+  nparams = 1; nrealargs = 1; nconstr = 2 }]
+
+then [get_constructors env sigma is] returns
+
+[[| { cs_cstr = 'niln'; cs_params = 'bool'; cs_nargs = 0;
+     cs_args = []; cs_concl_realargs = [|O|]};
+   { cs_cstr = 'consn'; cs_params = 'bool'; cs_nargs = 3;
+     cs_args = [(Anonymous,'(listn A n)'),(Anonymous,'A'),(Name n,'nat')];
+     cs_concl_realargs = [|'(S n)'|]} |]]
+
+and [get_arity env sigma is] returns [[(Anonymous,'nat')],'Set'].
+*)
+
+(* Cases info *)
+
+val make_case_info : mind_specif -> case_style option -> pattern_source array 
+      -> case_info
+val make_default_case_info : mind_specif -> case_info
+
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 235adffb4..51ba31504 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -9,7 +9,6 @@ open Term
 open Univ
 open Evd
 open Constant
-open Inductive
 open Environ
 open Instantiate
 open Closure
@@ -490,9 +489,6 @@ let contract_cofix = function
       sAPPViList bodynum (array_last bodyvect) (list_tabulate make_Fi nbodies)
   | _ -> assert false
 
-let mind_nparams env i =
-  let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams
-
 let reduce_mind_case mia =
   match mia.mconstr with
     | DOPN(MutConstruct (ind_sp,i as cstr_sp),args) ->
@@ -983,31 +979,27 @@ let instance s c =
  * if this does not work, then we use the string S as part of our
  * error message. *)
 
-let hnf_prod_app env sigma s t n =
+let hnf_prod_app env sigma t n =
   match whd_betadeltaiota env sigma t with
     | DOP2(Prod,_,b) -> sAPP b n
-    | _ ->
-	errorlabstrm s [< 'sTR"Needed a product, but didn't find one in " ;
-			  'sTR s ; 'fNL >]
+    | _ -> anomaly "hnf_prod_app: Need a product"
 
-let hnf_prod_appvect env sigma s t nl = 
-  Array.fold_left (hnf_prod_app env sigma s) t nl
+let hnf_prod_appvect env sigma t nl = 
+  Array.fold_left (hnf_prod_app env sigma) t nl
 
-let hnf_prod_applist env sigma s t nl = 
-  List.fold_left (hnf_prod_app env sigma s) t nl
+let hnf_prod_applist env sigma t nl = 
+  List.fold_left (hnf_prod_app env sigma) t nl
 				    
-let hnf_lam_app env sigma s t n =
+let hnf_lam_app env sigma t n =
   match whd_betadeltaiota env sigma t with
     | DOP2(Lambda,_,b) -> sAPP b n
-    | _ ->
-	errorlabstrm s [< 'sTR"Needed a product, but didn't find one in " ;
-			  'sTR s ; 'fNL >]
+    | _ -> anomaly "hnf_lam_app: Need an abstraction"
 
-let hnf_lam_appvect env sigma s t nl = 
-  Array.fold_left (hnf_lam_app env sigma s) t nl
+let hnf_lam_appvect env sigma t nl = 
+  Array.fold_left (hnf_lam_app env sigma) t nl
 
-let hnf_lam_applist env sigma s t nl = 
-  List.fold_left (hnf_lam_app env sigma s) t nl
+let hnf_lam_applist env sigma t nl = 
+  List.fold_left (hnf_lam_app env sigma) t nl
 
 let splay_prod env sigma = 
   let rec decrec m c =
@@ -1146,63 +1138,6 @@ let whd_programs_stack env sigma =
 
 let whd_programs env sigma x = applist (whd_programs_stack env sigma x [])
 
-exception Induc
-
-let find_mrectype env sigma c =
-  let (t,l) = whd_betadeltaiota_stack env sigma c [] in
-  match t with
-    | DOPN(MutInd ind_sp,args) ->  ((ind_sp,args),l)
-    | _ -> raise Induc
-
-let find_minductype env sigma c =
-  let (t,l) = whd_betadeltaiota_stack env sigma c [] in
-  match t with
-    | DOPN(MutInd (sp,i),_)
-        when mind_type_finite (lookup_mind sp env) i -> (destMutInd t,l)
-    | _ -> raise Induc
-
-let find_mcoinductype env sigma c =
-  let (t,l) = whd_betadeltaiota_stack env sigma c [] in
-  match t with
-    | DOPN(MutInd (sp,i),_)
-        when not (mind_type_finite (lookup_mind sp env) i) -> (destMutInd t,l)
-    | _ -> raise Induc
-
-(* raise Induc if not an inductive type *)
-let find_inductive env sigma ty =
-  let (mind,largs) = find_minductype env sigma ty in
-  let mispec = lookup_mind_specif mind env in 
-  let nparams = mis_nparams mispec in
-  let (params,realargs) = list_chop nparams largs in
-  let nconstr = mis_nconstr mispec in
-  let hyps = mispec.mis_mib.mind_hyps in
-  { mind     = mind;
-    params   = params;
-    realargs = realargs;
-    nparams  = nparams;
-    nrealargs = List.length realargs;
-    nconstr  = nconstr }
-
-let get_constructors env sigma is =
-  let mispec = lookup_mind_specif is.mind env in
-  let specif = mis_lc mispec in
-  let make_ik i = DOPN (MutInd (mispec.mis_sp,i), mispec.mis_args) in
-  let types = sAPPVList specif (list_tabulate make_ik (mis_ntypes mispec)) in
-  let make_ck j =
-    let (args,ccl) = decompose_prod (prod_applist types.(j) is.params) in
-    let (_,vargs) = array_chop (is.nparams + 1) (destAppL (ensure_appl ccl)) in
-    { cs_cstr = ith_constructor_of_inductive is.mind (j+1);
-      cs_params = is.params;
-      cs_nargs = List.length args;
-      cs_args = args;
-      cs_concl_realargs = vargs } in
-  Array.init (mis_nconstr mispec) make_ck
-
-let get_arity env sigma is =
-  let mispec = lookup_mind_specif is.mind env in
-  let arity = mis_arity mispec in
-  splay_arity env sigma (prod_applist arity is.params)
-
 exception IsType
 
 let is_arity env sigma = 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index c772ede66..a1c542199 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -81,18 +81,13 @@ val whd_evar : 'a reduction_function
 
 val beta_applist : (constr * constr list) -> constr
 
-val hnf_prod_app : 
-  env -> 'a evar_map -> string -> constr -> constr -> constr
-val hnf_prod_appvect : 
-  env -> 'a evar_map -> string -> constr -> constr array -> constr
-val hnf_prod_applist : 
-  env -> 'a evar_map -> string -> constr -> constr list -> constr
-val hnf_lam_app : 
-  env -> 'a evar_map -> string -> constr -> constr -> constr
-val hnf_lam_appvect : 
-  env -> 'a evar_map -> string -> constr -> constr array -> constr
-val hnf_lam_applist : 
-  env -> 'a evar_map -> string -> constr -> constr list -> constr
+val hnf_prod_app     : env -> 'a evar_map -> constr -> constr -> constr
+val hnf_prod_appvect : env -> 'a evar_map -> constr -> constr array -> constr
+val hnf_prod_applist : env -> 'a evar_map -> constr -> constr list -> constr
+val hnf_lam_app      : env -> 'a evar_map -> constr -> constr -> constr
+val hnf_lam_appvect  : env -> 'a evar_map -> constr -> constr array -> constr
+val hnf_lam_applist  : env -> 'a evar_map -> constr -> constr list -> constr
+
 val splay_prod : env -> 'a evar_map -> constr -> (name * constr) list * constr
 val splay_arity : env -> 'a evar_map -> constr -> (name * constr) list * sorts
 val sort_of_arity : env -> constr -> sorts
@@ -201,25 +196,3 @@ val whd_ise1_metas : 'a evar_map -> constr -> constr
 val hnf : env -> 'a evar_map -> constr -> constr * constr list
 val apprec : 'a stack_reduction_function
 val red_product : 'a reduction_function
-
-(* [find_m*type env sigma c] coerce [c] to an recursive type (I args).
-   [find_mrectype], [find_minductype] and [find_mcoinductype]
-   respectively accepts any recursive type, only an inductive type and
-   only a coinductive type.
-   They raise [Induc] if not convertible to a recursive type. *)
-
-exception Induc
-val find_mrectype     : env -> 'a evar_map -> constr -> inductive * constr list
-val find_minductype   : env -> 'a evar_map -> constr -> inductive * constr list
-val find_mcoinductype : env -> 'a evar_map -> constr -> inductive * constr list
-
-(* [find_inductive env sigma t] raises [Induc] if [t] is not an inductive type*)
-(* The resulting summary is relative to the current env *)
-open Inductive
-val find_inductive : env -> 'a evar_map -> constr -> inductive_summary
-
-val get_constructors : env -> 'a evar_map -> inductive_summary
-      -> constructor_summary array
-val get_arity : env -> 'a evar_map -> inductive_summary ->
-      (name * constr) list * sorts
-
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 4a89568dc..6e453b60b 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -8,11 +8,11 @@ open Univ
 open Generic
 open Term
 open Constant
-open Inductive
 open Sign
 open Environ
 open Reduction
-open Instantiate
+open Inductive
+
 open Type_errors
 
 let make_judge v tj =
@@ -91,7 +91,7 @@ let instantiate_arity mis =
   { body = instantiate_constr ids arity.body args;
     typ = arity.typ }
 *)
-let instantiate_arity = Instantiate.mis_typed_arity
+let instantiate_arity = mis_typed_arity
 
 let type_of_inductive env sigma i =
   let mis = lookup_mind_specif i env in
@@ -107,7 +107,7 @@ let instantiate_lc mis =
   let lc = mis.mis_mip.mind_lc in
   instantiate_constr (ids_of_sign hyps) lc (Array.to_list mis.mis_args)
 *)
-let instantiate_lc = Instantiate.mis_lc
+let instantiate_lc = mis_lc
 
 let type_of_constructor env sigma ((ind_sp,j),args as cstr) =
   let mind = inductive_of_constructor cstr in
@@ -151,19 +151,11 @@ let type_mconstruct env sigma i mind =
   let mis = lookup_mind_specif mind env in
   mis_type_mconstruct i mis
 
-let type_inst_construct env sigma i (mind,globargs) =
-  let mis = lookup_mind_specif mind env in
+let type_inst_construct i (IndFamily (mis,globargs)) =
   let tc = mis_type_mconstruct i mis in
-    hnf_prod_applist env sigma "Typing.type_construct" tc globargs
-
-let type_of_existential env sigma c =
-  let (ev,args) = destEvar c in
-  let evi = Evd.map sigma ev in
-  let hyps = var_context evi.Evd.evar_env in
-  let id = id_of_string ("?" ^ string_of_int ev) in
-  (* TODO: check args *)
-  instantiate_constr (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args)
+  prod_applist tc globargs
 
+let type_of_existential env sigma c = Instantiate.existential_value sigma c
 
 (* Case. *)
 
@@ -173,23 +165,6 @@ let rec mysort_of_arity env sigma c =
     | DOP2(Prod,_,DLAM(_,c2)) -> mysort_of_arity env sigma c2
     | _ -> invalid_arg "mysort_of_arity"
 
-let make_arity_dep env sigma k = 
-  let rec mrec c m = match whd_betadeltaiota env sigma c with 
-    | DOP0(Sort _) -> mkArrow m k
-    | DOP2(Prod,b,DLAM(n,c_0)) ->
-        prod_name env (n,b,mrec c_0 (applist(lift 1 m,[Rel 1])))
-    | _ -> invalid_arg "make_arity_dep"
-  in 
-  mrec
-
-let make_arity_nodep env sigma k = 
-  let rec mrec c = match whd_betadeltaiota env sigma c with 
-    | DOP0(Sort _) -> k
-    | DOP2(Prod,b,DLAM(x,c_0)) -> DOP2(Prod,b,DLAM(x,mrec c_0))
-    | _ -> invalid_arg "make_arity_nodep"
-  in 
-  mrec
-
 let error_elim_expln env sigma kp ki =
   if is_info_sort env sigma kp && not (is_info_sort env sigma ki) then
     "non-informative objects may not construct informative ones."
@@ -201,91 +176,52 @@ let error_elim_expln env sigma kp ki =
 
 exception Arity of (constr * constr * string) option
 
-let is_correct_arity env sigma kelim (c,p) = 
-  let rec srec ind (pt,t) =
-    try 
-      (match whd_betadeltaiota env sigma pt, whd_betadeltaiota env sigma t with
-	 | DOP2(Prod,a1,DLAM(_,a2)), DOP2(Prod,a1',DLAM(_,a2')) ->
-             if is_conv env sigma a1 a1' then
-               srec (applist(lift 1 ind,[Rel 1])) (a2,a2') 
-             else 
-	       raise (Arity None)
-	 | DOP2(Prod,a1,DLAM(_,a2)), ki -> 
-             let k = whd_betadeltaiota env sigma a2 in 
-             let ksort = (match k with DOP0(Sort s) -> s 
-			    | _ -> raise (Arity None)) in
-             if is_conv env sigma a1 ind then
-               if List.exists (base_sort_cmp CONV ksort) kelim then
-		 (true,k)
-               else 
-		 raise (Arity (Some(k,ki,error_elim_expln env sigma k ki)))
-	     else 
-	       raise (Arity None)
-	 | k, DOP2(Prod,_,_) ->
-	     raise (Arity None)
-	 | k, ki -> 
-	     let ksort = (match k with DOP0(Sort s) -> s 
-                            | _ ->  raise (Arity None)) in
-             if List.exists (base_sort_cmp CONV ksort) kelim then 
-	       false,k
-             else 
-	       raise (Arity (Some(k,ki,error_elim_expln env sigma k ki))))
-    with Arity kinds ->
-      let listarity =
-	(List.map 
-	   (fun s -> make_arity_dep env sigma (DOP0(Sort s)) t ind) kelim)
-	@(List.map 
-	    (fun s -> make_arity_nodep env sigma (DOP0(Sort s)) t) kelim)
-      in 
-      error_elim_arity CCI env ind listarity c p pt kinds
-  in 
-  srec
-
-let find_case_dep_nparams env sigma (c,p) (mind,largs) typP =
-  let mis = lookup_mind_specif mind env in
-  let nparams = mis_nparams mis
-  and kelim = mis_kelim mis
-  and t = body_of_type (instantiate_arity mis) in 
-  let (globargs,la) = list_chop nparams largs in
-  let glob_t = hnf_prod_applist env sigma "find_elim_boolean" t globargs in
-  let arity = applist(mkMutInd mind,globargs) in
-  let (dep,_) = is_correct_arity env sigma kelim (c,p) arity (typP,glob_t) in
-  dep
+let is_correct_arity env sigma kelim (c,p) indf (pt,t) = 
+  let rec srec (pt,t) =
+    match whd_betadeltaiota env sigma pt, whd_betadeltaiota env sigma t with
+      | DOP2(Prod,a1,DLAM(_,a2)), DOP2(Prod,a1',DLAM(_,a2')) ->
+          if is_conv env sigma a1 a1' then
+            srec (a2,a2') 
+          else 
+	    raise (Arity None)
+      | DOP2(Prod,a1,DLAM(_,a2)), ki -> 
+          let k = whd_betadeltaiota env sigma a2 in 
+          let ksort = (match k with DOP0(Sort s) -> s 
+			 | _ -> raise (Arity None)) in
+	  let ind = build_dependent_inductive indf in
+          if is_conv env sigma a1 ind then
+            if List.exists (base_sort_cmp CONV ksort) kelim then
+	      (true,k)
+            else 
+	      raise (Arity (Some(k,ki,error_elim_expln env sigma k ki)))
+	  else 
+	    raise (Arity None)
+      | k, DOP2(Prod,_,_) ->
+	  raise (Arity None)
+      | k, ki -> 
+	  let ksort = (match k with DOP0(Sort s) -> s 
+                         | _ ->  raise (Arity None)) in
+          if List.exists (base_sort_cmp CONV ksort) kelim then 
+	    false,k
+          else 
+	    raise (Arity (Some(k,ki,error_elim_expln env sigma k ki)))
+in 
+  try srec (pt,t)
+  with Arity kinds ->
+    let listarity =
+      (List.map (make_arity env sigma true indf) kelim)
+      @(List.map (make_arity env sigma false indf) kelim)
+    in 
+    let ind = mis_inductive (fst (dest_ind_family indf)) in
+    error_elim_arity CCI env ind listarity c p pt kinds
 
-let type_one_branch_dep env sigma (nparams,globargs,p) co t = 
-  let rec typrec n c =
-    match whd_betadeltaiota env sigma c with
-      | DOP2(Prod,a1,DLAM(x,a2)) -> prod_name env (x,a1,typrec (n+1) a2)
-      | x -> let lAV = destAppL (ensure_appl x) in
-             let (_,vargs) = array_chop (nparams+1) lAV in
-             applist 
-               (appvect ((lift n p),vargs),
-		[applist(co,((List.map (lift n) globargs)@(rel_list 0 n)))])
-  in 
-  typrec 0 (hnf_prod_applist env sigma "type_case" t globargs)
-
-let type_one_branch_nodep env sigma (nparams,globargs,p) t = 
-  let rec typrec n c =
-    match whd_betadeltaiota env sigma c with 
-      | DOP2(Prod,a1,DLAM(x,a2)) -> DOP2(Prod,a1,DLAM(x,typrec (n+1) a2))
-      | x -> let lAV = destAppL(ensure_appl x) in
-             let (_,vargs) = array_chop (nparams+1) lAV in
-             appvect (lift n p,vargs)
-  in 
-  typrec 0 (hnf_prod_applist env sigma "type_case" t globargs)
 
-(* [p] is the predicate and [cs] a constructor summary *)
-let mytype_one_branch dep env p cs =
-  if dep then
-    let n = cs.cs_nargs in
-    let ci =
-      applist
-	(mkMutConstruct cs.cs_cstr,
-	 (List.map (lift n) cs.cs_params)@(rel_list 0 n)) in
-    it_prod_name env (applist (appvect (lift n p,cs.cs_concl_realargs), [ci]))
-      cs.cs_args
-  else
-    prod_it (appvect (lift cs.cs_nargs p,cs.cs_concl_realargs)) cs.cs_args
+let find_case_dep_nparams env sigma (c,p) (IndFamily (mis,_) as indf) typP =
+  let kelim = mis_kelim mis in
+  let arsign,s = get_arity env sigma indf in
+  let glob_t = prod_it (mkSort s) arsign in
+  let (dep,_) = is_correct_arity env sigma kelim (c,p) indf (typP,glob_t) in
+  dep
 
 (* type_case_branches type un <p>Case c of ... end 
    ct = type de c, si inductif il a la forme APP(mI,largs), sinon raise Induc
@@ -294,21 +230,17 @@ let mytype_one_branch dep env p cs =
    attendus dans les branches du Case; lr est le type attendu du resultat
  *)
 
-let type_case_branches env sigma indspec pt p c =
-  let dep =
-    find_case_dep_nparams env sigma (c,p)
-      (indspec.mind,indspec.params@indspec.realargs) pt in
-  let constructs = get_constructors env sigma indspec in
-  let lc = Array.map (mytype_one_branch dep env p) constructs in
-  let la = indspec.realargs in
+let type_case_branches env sigma (IndType (indf,realargs)) pt p c =
+  let dep = find_case_dep_nparams env sigma (c,p) indf pt in
+  let constructs = get_constructors indf in
+  let lc = Array.map (build_branch_type env dep p) constructs in
   if dep then
-    (lc, beta_applist (p,(la@[c])))
+    (lc, beta_applist (p,(realargs@[c])))
   else 
-    (lc, beta_applist (p,la))
+    (lc, beta_applist (p,realargs))
 
 let check_branches_message env sigma (c,ct) (explft,lft) = 
-  let n = Array.length explft 
-  and expn = Array.length lft in
+  let expn = Array.length explft and n = Array.length lft in
   if n<>expn then error_number_branches CCI env c ct expn;
   for i = 0 to n-1 do
     if not (is_conv_leq env sigma lft.(i) (explft.(i))) then
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 2c93141cb..7ab2404f8 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -41,7 +41,7 @@ val type_of_case : env -> 'a evar_map -> case_info
     -> unsafe_judgment array -> unsafe_judgment
 
 val type_case_branches :
-  env -> 'a evar_map -> Inductive.inductive_summary -> constr -> constr
+  env -> 'a evar_map -> Inductive.inductive_type -> constr -> constr
     -> constr -> constr array * constr 
 
 val judge_of_prop_contents : contents -> unsafe_judgment
@@ -74,25 +74,13 @@ val control_only_guard : env -> 'a evar_map -> constr -> unit
 val type_fixpoint : env -> 'a evar_map -> name list -> typed_type array 
     -> unsafe_judgment array -> constraints
 
-val type_one_branch_dep : env -> 'a evar_map -> 
-  int * constr list * constr -> constr -> constr -> constr 
-
-val type_one_branch_nodep : env -> 'a evar_map -> 
-  int * constr list * constr -> constr -> constr 
-
-val make_arity_dep : 
-  env -> 'a evar_map -> constr -> constr -> constr -> constr 
-
-val make_arity_nodep : 
-  env -> 'a evar_map -> constr -> constr -> constr 
+open Inductive
 
 val find_case_dep_nparams :
-  env -> 'a evar_map -> constr * constr ->
-    inductive * constr list -> constr -> bool
+  env -> 'a evar_map -> constr * constr -> inductive_family -> constr -> bool
 
-(* The constr list is the global args list *)
-val type_inst_construct :
-  env -> 'a evar_map -> int -> inductive * constr list -> constr 
+(* Returns the type of the [i]$^{th}$ constructor of the inductive family *)
+val type_inst_construct : int -> inductive_family -> constr 
 
 val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool