diff --git a/common/theories/Environment.v b/common/theories/Environment.v index f8de029a1..b7c5005fe 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,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. 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. diff --git a/examples/demo.v b/examples/demo.v index 12fd705f6..337197ef5 100644 --- a/examples/demo.v +++ b/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. diff --git a/examples/metacoq_tour.v b/examples/metacoq_tour.v index 02e69f5e7..f100e26e9 100644 --- a/examples/metacoq_tour.v +++ b/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).