diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-17 16:07:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-23 01:38:33 +0200 |
| commit | 6007579ade085a60664e6b0d4596ff98c51aabf9 (patch) | |
| tree | 58c0b5ae6c6f77b31df07e0bd906f56c23ec044a /kernel/declarations.ml | |
| parent | c3318ad8408b1ceb0bfd4c2bfedec63ce9324698 (diff) | |
Using more general information for primitive records.
This brings more compatibility with handling of mutual primitive records
in the kernel.
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index bb81f7514..58fb5d66b 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -109,13 +109,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 checked projection bodies. -type record_body = (Id.t * Constant.t array * projection_body array) option + 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_info = +| NotRecord +| FakeRecord +| PrimRecord of (Id.t * Constant.t array * projection_body array) array type regular_inductive_arity = { mind_user_arity : types; @@ -181,7 +190,7 @@ 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 *) |