Documentation mutual_inductive_body

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

1 files changed, 77 insertions, 23 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index d4f840b14..10559ffe1 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -23,8 +23,8 @@ open Mod_subst
 
 type engagement = ImpredicativeSet
 
-
-(*s Constants (Definition/Axiom) *)
+(**********************************************************************)
+(*s Representation of constants (Definition/Axiom)                    *)
 
 type constr_substituted
 
@@ -42,8 +42,8 @@ type constant_body = {
 
 val subst_const_body : substitution -> constant_body -> constant_body
 
-(*s Inductive types (internal representation with redundant
-    information). *)
+(**********************************************************************)
+(*s Representation of mutual inductive types in the kernel            *)
 
 type recarg = 
   | Norec 
@@ -62,48 +62,102 @@ val recarg_length : wf_paths -> int -> int
 
 val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
-(* [mind_typename] is the name of the inductive; [mind_arity] is
-   the arity generalized over global parameters; [mind_lc] is the list
-   of types of constructors generalized over global parameters and
-   relative to the global context enriched with the arities of the
-   inductives *) 
+(*
+\begin{verbatim}
+   Inductive I1 (params) : U1 := c11 : T11 | ... | c1p1 : T1p1
+   ...
+   with      In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn
+\end{verbatim}
+*)
 
 type one_inductive_body = {
+
+(* Primitive datas *)
+
+ (* Name of the type: [Ii] *)
     mind_typename : identifier;
-    mind_nrealargs : int;
-    mind_nf_arity : types;
+
+ (* Arity of [Ii] with parameters: [forall params, Ui] *)
     mind_user_arity : types;
-    mind_sort : sorts;
-    mind_kelim : sorts_family list;
+
+ (* Names of the constructors: [cij] *)
     mind_consnames : identifier array;
-    mind_consnrealargs : int array; (* length of constructs, let-in included *)
-    mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *)
+
+ (* Types of the constructors with parameters: [forall params, Tij],
+    where the Ik are replaced by de Bruijn index in the context
+    I1:forall params, U1 ..  In:forall params, Un *)
     mind_user_lc : types array;
+
+(* Derived datas *)
+
+ (* Head normalized arity so that the conclusion is a sort *)
+    mind_nf_arity : types;
+
+ (* Number of expected real arguments of the type (no let, no params) *)
+    mind_nrealargs : int;
+
+ (* Conclusion of the arity *)
+    mind_sort : sorts;
+
+ (* List of allowed elimination sorts *)
+    mind_kelim : sorts_family list;
+
+ (* Head normalized constructor types so that their conclusion is atomic *)
+    mind_nf_lc : types array;
+
+ (* Number of expected (real) arg of the constructors (no let, no params) *)
+    mind_consnrealargs : int array;
+
+ (* Signature of recursive arguments in the constructors *)
     mind_recargs : wf_paths;
-    mind_nb_constant : int; (* number of constant constructor *)
-    mind_nb_args : int; (* number of no constant constructor *)
+
+(* Datas for bytecode compilation *)
+
+ (* number of constant constructor *)
+    mind_nb_constant : int;
+
+ (* number of no constant constructor *)
+    mind_nb_args : int;
+
     mind_reloc_tbl :  Cbytecodes.reloc_table; 
   }
 
+type mutual_inductive_body = {
 
+  (* The component of the mutual inductive block *)
+    mind_packets : one_inductive_body array;
 
-type mutual_inductive_body = {
-    mind_record : bool; 
+  (* Whether the inductive type has been declared as a record *)
+    mind_record : bool;
+
+  (* Whether the type is inductive or coinductive *)
     mind_finite : bool;
+
+  (* Number of types in the block *)
     mind_ntypes : int;
+
+  (* Section hypotheses on which the block depends *)
     mind_hyps : section_context;
+
+  (* Number of expected parameters *)
     mind_nparams : int;
+
+  (* Number of non recursively uniform parameters *)
     mind_nparams_rec : int;
+
+  (* The context of parameters (includes let-in declaration) *)
     mind_params_ctxt : rel_context;
-    mind_packets : one_inductive_body array;
+
+  (* Universes constraints enforced by the inductive declaration *)
     mind_constraints : constraints;
-    mind_equiv : kernel_name option;
-  }
 
+  (* Source of the inductive block when aliased in a module *)
+    mind_equiv : kernel_name option
+  }
 
 val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
 
-
+(**********************************************************************)
 (*s Modules: signature component specifications, module types, and
   module declarations *)