Merge pull request #1128 from MathisBD/update-inductive-doc

Update documentation in common/Environment.ml for inductive and constant declarations

common/theories/Environment.v

@@ -218,7 +218,9 @@ Module Environment (T : Term).
        decl_body := decl_body x;
        decl_type := decl_type x |}.
 
-  Fixpoint context_assumptions (Γ : context) :=
+  (** Count the number of assumptions in a context (i.e. declarations that do not 
+      contain a body). *)
+  Fixpoint context_assumptions (Γ : context) : nat :=
     match Γ with
     | [] => 0
     | d :: Γ =>
@@ -313,23 +315,35 @@ Module Environment (T : Term).
 
   (** *** Environments *)
 
+  (** Data associated to a single inductive constructor. *)
   Record constructor_body := {
+    (** Constructor name, without the module path. *)
     cstr_name : ident;
-    (* The arguments and indices are typeable under the context of
-      arities of the mutual inductive + parameters *)
+    (** Arguments of the constructor, which can depend on the inductives in the same block
+        and the parameters of the inductive : `ind_bodies ,,, ind_params |- cstr_args`. *)
     cstr_args : context;
+    (** Indices of the constructor, which can depend on the inductives in the same block,
+        the parameters of the inductive and the constructor arguments :
+        `ind_bodies ,,, ind_params ,,, cstr_args |- cstr_indices`. *)
     cstr_indices : list term;
+    (** Full type of the constructor, which can depend on the inductives in the same block :
+        `ind_bodies |- cstr_type`. This should be equal to 
+        `forall ind_params cstr_args, I ind_params cstr_indices` *)
     cstr_type : term;
-    (* Closed type: on well-formed constructors: forall params, cstr_args, I params cstr_indices *)
-    cstr_arity : nat; (* arity, w/o lets, w/o parameters *)
+    (** Number of arguments of the constructor, _without_ let-in arguments and _without_ parameters.
+        This should be equal to `context_assumptions cstr_args`. *)
+    cstr_arity : nat;
   }.
 
+  (** Data associated to a primitive projection. *)
   Record projection_body := {
+    (** Projection name, without the module path. *)
     proj_name : ident;
-    (* The arguments and indices are typeable under the context of
-      arities of the mutual inductive + parameters *)
+    (** Relevance of the projection. *)
     proj_relevance : relevance;
-    proj_type : term; (* Type under context of params and inductive object *)
+    (** Type of the projection, wich can depend on the parameters of the inductive 
+        and on the object we are projecting from : `ind_params ,,, x |- proj_type`. *)
+    proj_type : term;
   }.
 
   Definition map_constructor_body npars arities f c :=
@@ -341,23 +355,33 @@ Module Environment (T : Term).
        cstr_type := f arities c.(cstr_type);
        cstr_arity := c.(cstr_arity) |}.
 
-  (* Here npars should be the [context_assumptions] of the parameters context. *)
+  (** Here npars should be the `context_assumptions` of the parameters context. *)
   Definition map_projection_body npars f c :=
     {| proj_name := c.(proj_name);
        proj_relevance := c.(proj_relevance);
        proj_type := f (S npars) c.(proj_type)
     |}.
 
-  (** See [one_inductive_body] from [declarations.ml]. *)
+  (** Data associated to a single inductive in a mutual inductive block. *)
   Record one_inductive_body := {
-    ind_name : ident;
-    ind_indices : context; (* Indices of the inductive types, under params *)
-    ind_sort : Sort.t; (* Sort of the inductive. *)
-    ind_type : term; (* Closed arity = forall mind_params, ind_indices, tSort ind_sort *)
-    ind_kelim : allowed_eliminations; (* Allowed eliminations *)
+    (** Name of the inductive, without the module path. *)
+    ind_name : ident; 
+    (** Indices of the inductive, which can depend on the parameters :
+        `ind_params |- ind_indices`. *)
+    ind_indices : context;
+    (** Sort of the inductive. *) 
+    ind_sort : Sort.t; 
+    (** Full type of the inductive. This should be equal to
+        `forall ind_params ind_indices, tSort ind_sort` *)
+    ind_type : term; 
+    (** Allowed eliminations for the inductive. *)
+    ind_kelim : allowed_eliminations; 
+    (** Constructors of the inductive. Order is important. *)
     ind_ctors : list constructor_body;
-    ind_projs : list projection_body; (* names and types of projections, if any. *)
-    ind_relevance : relevance (* relevance of the inductive definition *) }.
+    (** Names and types of primitive projections, if any. *)
+    ind_projs : list projection_body; 
+    (** Relevance of the inductive. *)
+    ind_relevance : relevance }.
 
   Definition map_one_inductive_body npars arities f m :=
     match m with
@@ -369,20 +393,33 @@ Module Environment (T : Term).
                   (map (map_projection_body npars f) ind_projs) ind_relevance
     end.
 
-  (** See [mutual_inductive_body] from [declarations.ml]. *)
+  (** Data associated to a block of mutually inductive types. *)
   Record mutual_inductive_body := {
+    (** Whether the block is inductive, coinductive or non-recursive (Records). *)
     ind_finite : recursivity_kind;
+    (** Number of parameters (including non-uniform ones), _without_ counting let-in parameters.
+        This should be equal to `context_assumptions ind_params`. *)
     ind_npars : nat;
+    (** Context of parameters (including non-uniform ones), _with_ let-in parameters. *)
     ind_params : context;
+    (** Components of the mutual inductive block. Order is important. *)
     ind_bodies : list one_inductive_body ;
+    (** Whether the mutual inductive is universe monomorphic or universe polymorphic,
+        and information about the local universes if polymorphic. *)
     ind_universes : universes_decl;
+    (** Variance information. `None` when non-cumulative. *)
     ind_variance : option (list Universes.Variance.t) }.
 
-  (** See [constant_body] from [declarations.ml] *)
+  (** Data associated to a constant (definition, lemma or axiom). *)
   Record constant_body := {
+    (** Type of the constant. *)
     cst_type : term;
+    (** Body of the constant. For axioms this is [None]. *)
     cst_body : option term;
+    (** Whether the constant is universe monomorphic or polymorphic, and if polymorphic
+        information about its local universes. *)
     cst_universes : universes_decl;
+    (** Proof relevance of this constant. *)
     cst_relevance : relevance }.
 
   Definition map_constant_body f decl :=
@@ -399,6 +436,7 @@ Module Environment (T : Term).
     option_map f (cst_body decl) = cst_body (map_constant_body f decl).
   Proof. destruct decl; reflexivity. Qed.
 
+  (** A global declaration is a definition, lemma, axiom or mutual inductive. *)
   Inductive global_decl :=
   | ConstantDecl : constant_body -> global_decl
   | InductiveDecl : mutual_inductive_body -> global_decl.

common/theories/EnvironmentTyping.v

@@ -1261,7 +1261,7 @@ Module GlobalMaps (T: Term) (E: EnvironmentSig T) (TU : TermUtils T E) (ET: EnvT
     *)
 
     (** A constructor argument type [t] is positive w.r.t. an inductive block [mdecl]
-      when it's zeta-normal form is of the shape Π Δ. concl and:
+        when it's zeta-normal form is of the shape Π Δ. concl and:
         - [t] does not refer to any inductive in the block.
           In that case [t] must be a closed type under the context of parameters and
           previous arguments.

examples/demo.v

@@ -1,6 +1,7 @@
 (* Distributed under the terms of the MIT license. *)
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Template Require Import All.
+From Coq Require Init.
 
 Import MCMonadNotation.
 
@@ -19,7 +20,7 @@ MetaCoq Test Quote (let x := 2 in
               | S n => n
             end).
 
-MetaCoq Test Unquote (Ast.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Stdlib"], "nat") 0) 0 []).
+MetaCoq Test Unquote (Ast.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Corelib"], "nat") 0) 0 []).
 
 (** Build a definition **)
 Definition d : Ast.term.
@@ -71,7 +72,9 @@ MetaCoq Quote Definition eo_syntax := Eval compute in even.
 MetaCoq Quote Definition add'_syntax := Eval compute in add'.
 
 (** Reflecting definitions **)
-MetaCoq Unquote Definition zero_from_syntax := (Ast.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Stdlib"], "nat") 0) 0 []).
+Check Coq.Init.Datatypes.nat.
+MetaCoq Unquote Definition zero_from_syntax := 
+  (Ast.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Corelib"], "nat") 0) 0 []).
 Set Printing All.
 (* the function unquote_kn in reify.ml4 is not yet implemented *)
 
@@ -84,7 +87,9 @@ MetaCoq Unquote Definition add_from_syntax := add_syntax.
 MetaCoq Unquote Definition eo_from_syntax := eo_syntax.
 Print eo_from_syntax.
 
-Local Notation Nat_module := (MPfile ["Datatypes"; "Init"; "Stdlib"], "nat").
+Local Notation Nat_module := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat").
+
+
 
 MetaCoq Unquote Definition two_from_syntax := (Ast.tApp (Ast.tConstruct (Kernames.mkInd Nat_module 0) 1 nil)
    (Ast.tApp (Ast.tConstruct (Kernames.mkInd Nat_module 0) 1 nil)
@@ -221,7 +226,7 @@ Definition printInductive (q : qualid): TemplateMonad unit :=
   | _ => tmFail ("[" ^ q ^ "] is not an inductive")
   end.
 
-MetaCoq Run (printInductive "Stdlib.Init.Datatypes.nat").
+MetaCoq Run (printInductive "Init.Datatypes.nat").
 MetaCoq Run (printInductive "nat").
 
 CoInductive cnat : Set :=  O :cnat | S : cnat -> cnat.

examples/metacoq_tour.v

@@ -28,7 +28,7 @@ Definition foo := (fun x : nat => fun x : nat => x).
 MetaCoq Quote Definition reifx' := Eval compute in (fun x : nat => let y := x in fun x : nat => y).
 Print reifx'.
 MetaCoq Unquote Definition x :=
-  (Ast.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Stdlib"], "nat") 0) 0 []).
+  (Ast.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Corelib"], "nat") 0) 0 []).
 
 MetaCoq Run (tmBind (tmQuote (3 + 3)) tmPrint).