GROS COMMIT:

 - reduction du noyau (variables existentielles, fonctions auxiliaires
   pour inventer des noms, etc. deplacees hors de kernel/)
 - changement de noms de constructeurs des constr (suppression de "Is" et
   "Mut")


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

1 files changed, 45 insertions, 198 deletions

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 2aee7f420..dbaf36788 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -12,216 +12,63 @@
 open Names
 open Univ
 open Term
-open Sign
 open Declarations
 open Environ
-open Evd
 (*i*)
 
-(*s Inductives are accessible at several stages:
-
-A [mutual_inductive_body] contains all information about a
-declaration of mutual (co-)inductive types. These informations are
-closed (they depend on no free variables) and an instance of them
-corresponds to a [mutual_inductive_instance =
-mutual_inductive_body * constr list]. One inductive type in an
-instanciated packet corresponds to an [inductive_instance =
-mutual_inductive_instance * int]. Applying global parameters to an
-[inductive_instance] gives an [inductive_family = inductive_instance *
-constr list]. Finally, applying real parameters gives an
-[inductive_type = inductive_family * constr list]. At each level
-corresponds various appropriated functions *)
-
-type inductive_instance (* ex-[mind_specif] *)
-
-val build_mis : inductive -> mutual_inductive_body -> inductive_instance
-
-val mis_index : inductive_instance -> int
-val mis_ntypes : inductive_instance -> int
-val mis_nconstr : inductive_instance -> int
-val mis_nparams : inductive_instance -> int
-val mis_nrealargs : inductive_instance -> int
-val mis_kelim : inductive_instance -> sorts_family list
-val mis_recargs : inductive_instance -> (recarg list) array array
-val mis_recarg : inductive_instance -> (recarg list) array
-val mis_typename : inductive_instance -> identifier
-val mis_typepath : inductive_instance -> section_path
-val mis_is_recursive_subset : int list -> inductive_instance -> bool
-val mis_is_recursive : inductive_instance -> bool
-val mis_consnames : inductive_instance -> identifier array
-val mis_conspaths : inductive_instance -> section_path array
-val mis_inductive : inductive_instance -> inductive
-val mis_arity : inductive_instance -> types
-val mis_nf_arity : inductive_instance -> types
-val mis_params_ctxt : inductive_instance -> rel_context
-val mis_sort : inductive_instance -> sorts
-val mis_constructor_type : int -> inductive_instance -> types
-val mis_finite : inductive_instance -> bool 
-
-(* The ccl of constructor is pre-normalised in the following functions *)
-val mis_nf_lc : inductive_instance -> constr array
-
-(*s [inductive_family] = [inductive_instance] applied to global parameters *)
-type inductive_family = IndFamily of inductive_instance * constr list
-
-val make_ind_family : inductive_instance * constr list -> inductive_family
-val dest_ind_family : inductive_family -> inductive_instance * constr list
-
-val liftn_inductive_family :
-  int -> int -> inductive_family -> inductive_family
-val lift_inductive_family : 
-  int -> inductive_family -> inductive_family
-
-(*s [inductive_type] = [inductive_family] applied to ``real'' parameters *)
-type inductive_type = IndType of inductive_family * constr list
-
-val make_ind_type : inductive_family * constr list -> inductive_type
-val dest_ind_type : inductive_type -> inductive_family * constr list
-
-val mkAppliedInd : inductive_type -> constr
-
-val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
-val lift_inductive_type : int -> inductive_type -> inductive_type
-val substnl_ind_type : constr list -> int -> inductive_type -> inductive_type
-
-(*s A [constructor] is an [inductive] + an index; the following functions
-    destructs and builds [constructor] *)
-val inductive_of_constructor : constructor -> inductive
-val index_of_constructor : constructor -> int
-val ith_constructor_of_inductive : inductive -> int -> constructor
-
-(*s This type gathers useful informations about some instance of a constructor
-    relatively to some implicit context (the current one)
-
-    If [cs_cstr] is a constructor in [(I p1...pm a1...an)] then
-    [cs_params] is [p1...pm] and the type of [MutConstruct(cs_cstr)
-    p1...pn] is [(cs_args)(I p1...pm cs_concl_realargs)] where [cs_args]
-    and [cs_params] are relative to the current env and [cs_concl_realargs]
-    is relative to the current env enriched by [cs_args]
-*)
-
-type constructor_summary = {
-  cs_cstr : constructor;
-  cs_params : constr list;
-  cs_nargs : int;
-  cs_args : rel_context;
-  cs_concl_realargs : constr array
-}
-
-val lift_constructor : int -> constructor_summary -> constructor_summary
+exception Induc
 
-(*s Functions to build standard types related to inductive *)
+(*s Extracting an inductive type from a constructions *)
 
-(* This builds [(ci params (Rel 1)...(Rel ci_nargs))] which is the argument
-   of a dependent predicate in a Cases branch *)
-val build_dependent_constructor : constructor_summary -> constr
+(* [find_m*type env sigma c] coerce [c] to an recursive type (I args).
+   [find_rectype], [find_inductive] and [find_coinductive]
+   respectively accepts any recursive type, only an inductive type and
+   only a coinductive type.
+   They raise [Induc] if not convertible to a recursive type. *)
 
-(* 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
+val find_rectype     : env -> constr -> inductive * constr list
+val find_inductive   : env -> constr -> inductive * constr list
+val find_coinductive : env -> constr -> inductive * constr list
 
-(* 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 -> bool -> inductive_family -> sorts -> constr
+(*s Fetching information in the environment about an inductive type.
+    Raises Induc if the inductive type is not found. *)
+val lookup_mind_specif :
+  env -> inductive -> mutual_inductive_body * one_inductive_body
 
-(* [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 
+(*s Functions to build standard types related to inductive *)
 
+val type_of_inductive    : env -> inductive -> types
 
-(*s Extracting an inductive type from a constructions *)
+(* Return type as quoted by the user *)
+val type_of_constructor  : env -> constructor -> types
 
-exception Induc
+(* Return constructor types in normal form *)
+val arities_of_constructors : env -> inductive -> types array
 
-(* [extract_mrectype c] assumes [c] is syntactically an inductive type
-   applied to arguments then it returns its components; if not an
-   inductive type, it raises [Induc] *)
-val extract_mrectype  : constr -> inductive * constr list
 
-(* [find_m*type env sigma c] coerce [c] to an recursive type (I args).
-   [find_rectype], [find_inductive] and [find_coinductive]
-   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 Arity of (constr * constr * string) option
+
+(* [type_case_branches env (I,args) (p:A) c] computes useful types
+   about the following Cases expression:
+      <p>Cases (c :: (I args)) of b1..bn end
+   It computes the type of every branch (pattern variables are
+   introduced by products), the type for the whole expression, and
+   the universe constraints generated.
+ *)
+val type_case_branches :
+  env -> inductive * constr list -> unsafe_judgment -> constr
+    -> types array * types * constraints
+
+(* Check a case_info actually correspond to a Case expression on the
+   given inductive type. *)
+val check_case_info : env -> inductive -> case_info -> unit
+
+(*s Guard conditions for fix and cofix-points. *)
+val check_fix : env -> fixpoint -> unit
+val check_cofix : env -> cofixpoint -> unit
 
-val find_mrectype    : env -> 'a evar_map -> constr -> inductive * constr list
-val find_inductive   : env -> 'a evar_map -> constr -> inductive * constr list
-val find_coinductive : env -> 'a evar_map -> constr -> inductive * constr list
-
-val lookup_mind_specif : inductive -> env -> inductive_instance
-
-(* [find_rectype env sigma t] builds an [inductive_type] or raises
-   [Induc] if [t] is not a (co-)inductive type; The result is relative to
-   [env] and [sigma] *)
-
-val find_rectype : env -> 'a evar_map -> constr -> inductive_type
-
-(* [get_constructors_types indf] returns the array of the types of
-   constructors of the inductive\_family [indf], i.e. the types are
-   instantiated by the parameters of the family (the type may be not
-   in canonical form -- e.g. cf sets library) *)
-
-val get_constructors_types : inductive_family -> types array
-val get_constructor_type : inductive_family -> int -> types
-
-(* [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
-val get_constructor : inductive_family -> int -> constructor_summary
-
-(* [get_arity_type indf] returns the type of the arity of the
-   inductive family described by [indf]; global parameters are already
-   instanciated (but the type may be not in canonical form -- e.g. cf
-   sets library); the products signature is relative to the
-   environment definition of [indf]; the names of the products of the
-   constructors types are not renamed when [Anonymous]; [get_arity
-   indf] does the same but normalises and decomposes it as an arity *)
-
-val get_arity_type : inductive_family -> types
-val get_arity : inductive_family -> arity
-
-(* [get_arity_type indf] returns the type of the arity of the inductive
-   family described by [indf]; global parameters are already instanciated *)
-
-
-
-(* 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'], 
-\begin{quote}
-[find_rectype env sigma (listn bool (S x))] returns [IndType (indf, '(S x)')]
-\end{quote}
-where [indf = IndFamily ('listn',['bool'])].
-
-Then, [get_constructors indf] returns
-\begin{quote}
-[[| { 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)'|]} |]]
-\end{quote}
-and [get_arity indf] returns [[(Anonymous,'nat')],'Set'].
-\smallskip
-*)
-
-(*s [Cases] info *)
-
-val make_case_info : inductive_instance -> case_style option 
-  -> pattern_source array -> case_info
-val make_default_case_info : inductive_instance -> case_info
+(********************)
+(* TODO: remove (used in pretyping only...) *)
+val find_case_dep_nparams :
+  env -> constr * unsafe_judgment -> inductive * constr list ->
+    bool * constraints