| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
Followup on "[api] Remove `polymorphic` type alias, use labels instead."
|
|
This seems like the right location, a bit more refactoring should be
possible.
|
|
This is more in-line with attributes and the rest of the API, and
makes some code significantly clearer (as in `foo true false false`,
etc...)
|
|
This datatype does belong to this layer.
|
|
We split `{goal,declaration,assumption}_kind` into their
components. This makes sense as each part of this triple is handled by
a different layer, namely:
- `polymorphic` status: necessary for the lower engine layers;
- `locality`: only used in `vernac` top-level constants
- `kind`: merely used for cosmetic purposes [could indeed be removed /
pushed upwards]
We also profit from this refactoring to add some named parameters to
the top-level definition API which is quite parameter-hungry.
More refactoring is possible and will come in further commits, in
particular this is a step towards unifying the definition / lemma save path.
|
|
This information is already present on `Proof.t`, so we extract it
form there.
Moreover, this information is essential to the lower-level proof, as
opposed to the "kind" information which is only relevant to the vernac
layer; we will move it thus to its proper layer in subsequent commits.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
This enforces more invariants statically.
|
|
We had to move the private opaque constraints out of the constant declaration
into the opaque table. The API is not very pretty yet due to a pervasive
confusion between monomorphic global constraints and polymorphic local ones,
but once we get rid of futures in the kernel this should be magically solved.
|
|
Instead we get the symbols from a Environ.env.
We make them accessible to the produced code through a reference
managed by the kernel, similar to the return values except inverting
when it's written and when it's read.
|
|
We move the role data into the evarmap instead.
|
|
Preparing for it to be stored in an Environ.env.
|
|
Formerly, knowing if a declaration was to be discharged, to be global
but invisible at import, or to be global but visible at import was
obtained by combining the parser-level information (i.e. use of
Variable/Hypothesis/Let vs use of Axiom/Parameter/Definition/..., use
of Local vs Global) with the result of testing whether there were open
sections.
We change the meaning of the Discharge flag: it does not tell anymore
that it was syntactically a Variable/Hypothesis/Let, but tells the
expected semantics of the declaration (issuing a warning in the
parser-to-interpreter step if the semantics is not the one suggested
by the syntax). In particular, the interpretation/command engine
becomes independent of the parser.
The new "semantic" type is:
type import_status = ImportDefaultBehavior | ImportNeedQualified
type locality = Discharge | Global of import_status
In the process, we found a couple of inconsistencies in the treatment
of the locality status. See bug #8722 and test file LocalDefinition.v.
|
|
This is to avoid depending on the combination "Discharge" + no opened
section to trigger an automatic declaration of instance.
|
|
Since the introduction of delayed section substitution, the opaque table
was already containing the same information.
|
|
This will allow an easier removal of the discharge segment in a later
commit.
|
|
Instead we do that on a by-need basis by reusing the section info already
stored in the opaque proof.
|
|
This lets us avoid having to cache the SearchBlacklist.elements call
in search as we can just use the set module's for_all function.
|
|
Cooking
Reviewed-by: SkySkimmer
Ack-by: herbelin
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
This was virtually dead code. The only place really accessing this data was the
user pretty-printer, but actually the tables were not installed for vanilla vo
files.
In practice, that meant that the only case where an access to this table could
have been triggered would have been to print a term coming from a vio file,
or a vo file generated via vio2vo. In all other cases, the printer would not
have displayed the internal universes. While the latter might be considered
a bug, I am instead convinced that this notion of user-facing internal universes
needs to be handled by another mechanism, the current one making little sense.
The fact it was broken all along without anybody noticing proves my point.
|
|
We get rid of the future wrappers, as all callers are immediately forcing
the result.
|
|
|
|
We simply pass them as arguments, now that they are not called by the
kernel anymore.
The checker definitely needs to access the opaque proofs. In order not to
touch the API at all, I added a hook there, but it could also be provided
as an additional argument, at the cost of changing all the upwards callers.
|
|
This function is breaking the indirect opaque abstraction, so we move it
outside of the kernel. Unluckily, there is no better place to put it, so
we leave it in Global.
The checker uses it in a fundamental way, so we reimplement it there, but
this will eventually get removed.
|
|
Before, we would store futures, but it was actually ensured by the
upper layers that they were either evaluated or stored by the STM
somewhere else. We simply replace this type with an option, thus
removing the Future.computation type from vo/vio files.
This also enhances debug printing, as the latter is unable to properly
print futures.
|
|
vernac
Reviewed-by: maximedenes
|
|
|
|
generalization + cleanups
Reviewed-by: herbelin
|
|
We consolidate loadpath handling as a single `Loadpath` module from
parts in `Library` and `Mltop`, placing it at the `vernac` level [as
`Mltop`]
This idea was first suggested in https://github.com/coq/coq/pull/9808
, and indeed it makes sense as library resolution tends to be business
of the upper layers: IDE / build tools.
Logic could be pushed upwards, but this is good enough for now.
This consolidation has enabled some good and long overdue
refactorings, and the module should become self-contained enough as to
allow the resolution logic to be shared with `coqdep` in the future.
The `Mltop` module only cares now about ML-level modules, and should
go away once we rewrite the loader using `findlib` to solve
https://github.com/coq/coq/issues/7698 .
|
|
Ack-by: gares
Ack-by: herbelin
Reviewed-by: vbgl
|
|
This removes a lot of cruft breaking the opaque proof abstraction in
Safe_typing and similar.
|
|
|
|
|
|
The code was intricate due to the special handling of side-effects, while
it was sufficient to extrude the logical definition to make it clearer. We
thus declare a constant in two parts, first purely kernel-related, then
purely libobject-related.
|
|
|
|
We do it by consistently using variants of the "ensure_exists" policy
in compilation modes: vo (default), vio (-quick), vio2vo (-vio2vo) and
parallel vio2vo (schedule-vio2vo), vio checking (-check-vio-tasks) and
parallel vio checking (schedule-vio-checking).
For instance, coqc -vio2vo dir/file.vio now works, while before,
dir/file was expected.
Incidentally, this avoids the non-recommended Loadpath.locate_file.
|
|
Some of them are significant so presumably it will take a bit of
effort to fix overlays.
I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
|
|
Currently this env is only used to error for Printing If/Let on
non-2-constructor/non-1-constructor types so we could alternatively
remove it and not error / error later when trying to print.
Keeping the env and the error as-is should be fine though.
|
|
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
Fixes #6699
|
|
TODO coqproject handling (for now it can be done through -arg I guess)
|
|
This function seems unused.
|
|
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
|
|
|
