diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 43 |
1 files changed, 20 insertions, 23 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index b7427d20..61fcb483 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -46,18 +46,6 @@ type inline = int option (** A constant can have no body (axiom/parameter), or a transparent body, or an opaque one *) -(** Projections are a particular kind of constant: - always transparent. *) - -type projection_body = { - proj_ind : MutInd.t; - proj_npars : int; - proj_arg : int; - proj_type : types; (* Type under params *) - proj_eta : constr * types; (* Eta-expanded term and type *) - proj_body : constr; (* For compatibility with VMs only, the match version *) -} - (* Global declarations (i.e. constants) can be either: *) type constant_def = | Undef of inline (** a global assumption *) @@ -77,17 +65,17 @@ type typing_flags = { points are assumed to be total. *) check_universes : bool; (** If [false] universe constraints are not checked *) conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *) + share_reduction : bool; (** Use by-need reduction algorithm *) } (* some contraints are in constant_constraints, some other may be in * the OpaqueDef *) type constant_body = { - const_hyps : Context.Named.t; (** New: younger hyp at top *) + const_hyps : Constr.named_context; (** New: younger hyp at top *) const_body : constant_def; const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; - const_proj : projection_body option; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for @@ -112,13 +100,22 @@ v} *) (** Record information: - If the record is not primitive, then None - Otherwise, we get: + If the type is not a record, then NotRecord + If the type is a non-primitive record, then FakeRecord + If it is a primitive record, for every type in the block, we get: - The identifier for the binder name of the record in primitive projections. - The constants associated to each projection. - - The checked projection bodies. *) + - The projection types (under parameters). + + The kernel does not exploit the difference between [NotRecord] and + [FakeRecord]. It is mostly used by extraction, and should be extruded from + the kernel at some point. +*) -type record_body = (Id.t * Constant.t array * projection_body array) option +type record_info = +| NotRecord +| FakeRecord +| PrimRecord of (Id.t * Label.t array * types array) array type regular_inductive_arity = { mind_user_arity : types; @@ -132,7 +129,7 @@ type one_inductive_body = { mind_typename : Id.t; (** Name of the type: [Ii] *) - mind_arity_ctxt : Context.Rel.t; (** Arity context of [Ii] with parameters: [forall params, Ui] *) + mind_arity_ctxt : Constr.rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *) mind_arity : inductive_arity; (** Arity sort and original user arity *) @@ -167,7 +164,7 @@ type one_inductive_body = { mind_nb_args : int; (** number of no constant constructor *) - mind_reloc_tbl : Cbytecodes.reloc_table; + mind_reloc_tbl : Vmvalues.reloc_table; } type abstract_inductive_universes = @@ -184,19 +181,19 @@ type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) - mind_record : record_body option; (** The record information *) + mind_record : record_info; (** The record information *) mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *) mind_ntypes : int; (** Number of types in the block *) - mind_hyps : Context.Named.t; (** Section hypotheses on which the block depends *) + mind_hyps : Constr.named_context; (** Section hypotheses on which the block depends *) mind_nparams : int; (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *) mind_nparams_rec : int; (** Number of recursively uniform (i.e. ordinary) parameters *) - mind_params_ctxt : Context.Rel.t; (** The context of parameters (includes let-in declaration) *) + mind_params_ctxt : Constr.rel_context; (** The context of parameters (includes let-in declaration) *) mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) |