From f689bade7dc0ccd21d71731792f7daedb112c723 Mon Sep 17 00:00:00 2001 From: MathisBD Date: Thu, 12 Dec 2024 14:34:40 +0100 Subject: [PATCH] add documentation in common/Environment.v --- common/theories/Environment.v | 73 +++++++++++++++++++++-------- common/theories/EnvironmentTyping.v | 2 +- 2 files changed, 55 insertions(+), 20 deletions(-) diff --git a/common/theories/Environment.v b/common/theories/Environment.v index f8de029a1..b5c0a3298 100644 --- a/common/theories/Environment.v +++ b/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,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 := @@ -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 @@ -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 := @@ -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. diff --git a/common/theories/EnvironmentTyping.v b/common/theories/EnvironmentTyping.v index ff7df2e95..720e4eb00 100644 --- a/common/theories/EnvironmentTyping.v +++ b/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.