Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
73 changes: 54 additions & 19 deletions common/theories/Environment.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 :: Γ =>
Expand Down Expand Up @@ -313,23 +315,33 @@ 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. *)
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. *)
cstr_indices : list term;
(** Full type of the constructor, which can depend on the inductives in the same block.
This should be equal to `forall mind_params cstr_args, I mind_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. *)
proj_type : term;
}.

Definition map_constructor_body npars arities f c :=
Expand All @@ -341,23 +353,32 @@ 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 type, which can depend on the parameters of the inductive. *)
ind_indices : context;
(** Sort of the inductive. *)
ind_sort : Sort.t;
(** Full type of the inductive. This should be equal to
`forall mind_params ind_indices, tSort ind_sort` *)
ind_type : term;
(** Allowed eliminations for this inductive. *)
ind_kelim : allowed_eliminations;
(** Constructors of this 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 definition. *)
ind_relevance : relevance }.

Definition map_one_inductive_body npars arities f m :=
match m with
Expand All @@ -369,20 +390,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 mutual inductive is inductive, coinductive or non-recursive. *)
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, axiom). *)
Record constant_body := {
(** Type of this constant. *)
cst_type : term;
(** Body of this 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;
(** Relevance of this constant. *)
cst_relevance : relevance }.

Definition map_constant_body f decl :=
Expand All @@ -399,6 +433,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.
Expand Down
2 changes: 1 addition & 1 deletion common/theories/EnvironmentTyping.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
Loading