| Age | Commit message (Collapse) | Author |
|---|
|
We can use logical kind for the same purpose, which is mainly
dumpglob, so `goal_object_kind` was never matched against, making this
transformation safe.
|
|
We remove two flags that were seldom used in favor of named parameters.
|
|
They are clearly not at the same importance level, thus we use a named
parameter and isolate the kinds as to allow further improvements and
refactoring.
|
|
We move the bulk of `Decl_kinds` to a better place [namely
`interp/decls`] and refactor the use of this information quite a bit.
The information seems to be used almost only for `Dumpglob`, so it
certainly should end there to achieve a cleaner core.
Note the previous commits, as well as the annotations regarding the
dubious use of the "variable" data managed by the `Decls` file.
IMO this needs more work, but this should be a good start.
|
|
Reviewed-by: SkySkimmer
|
|
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
We make a few libobject constructions (Module, Module Type,
Include,...) first-class and rephrase their handling in direct style (removing
the inversion of control). This makes it easier to define iterators over
objects without hacks like inspecting the tags of dynamic objects.
|
|
|
|
State is still token except for proofs [due to the compat layer, would
be great if someone could port the STM], but this should be good for now.
|
|
|
|
We move special vernac-qed handling to a special function, making the
regular vernacular interpretation path uniform.
This is an important step as it paves the way up to export the vernac
DSL to clients, as there are no special vernacs anymore in the regular
interp path, except for Load, which should be handled separately due
to silly reasons, as morally it is a `VtNoProof` command.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
We turn the hook parameter into a record, making more explicit the
capture of data in hooks as they only take one parameter now
This is a fine-tuning but provides some small advantages, and allows
us to tweak the hook type with less breakage.
|
|
We move the stack of open lemmas from `Lemmas` to `Vernacstate`. The
`Lemmas` module doesn't deal with stacked proofs, so the stack can be
moved to to the proper place; this reduces the size of the API.
Note that `Lemmas` API is still quite imperative, it would be great if
we would return some more information on close proof, for example
about the global environment parts that were modified.
|
|
It is completely local to that file, there was no point to put it into
the unrelated Declare file.
|
|
It was never used actually.
|
|
theorems.
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
As noted in GitHub discussion, it is a good idea to make `poly` always
explicit, this PR does remove last case of `?(poly=false)` in the
codebase.
|
|
Followup on "[api] Remove `polymorphic` type alias, use labels instead."
|
|
These are only needed when closing / admitting a proof.
|
|
|
|
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.
|
|
This was already in the base proof object however not forwarded by
`close_proof`. thus it had to be stored twice.
There are more cases like this, like `poly`, all are covered by
subsequent commits.
|
|
|
|
Lemmas.info was a bit out of hand, as well as the parameters to the
`start_*` family. Most of the info is not needed and should hopefully
remain constrained to special cases, most callers only set the hook,
and obligations should be better served by a `start_obligation`
function soon.
|
|
|
|
Information about interactive mutually recursive proofs was stored as
a closure on an ad-hoc hook, then later made available to the hook
closing actions.
Instead, we put this information in the lemma state and incorporate
these declarations into the normal save path.
TODO: Should investigate what's going on with implicits, maybe submit
a separate PR.
|
|
Key information about an interactive lemma proof was stored as a
closure on an ad-hoc hook, then later made available to the hook
closing actions.
Instead, we put this information in the lemma state and incorporate
these declarations into the normal save path.
We prepare to put the information about rec_thms in the state too.
|
|
It was always the negation of the opacity flag.
|
|
This allows to desynchronize the kernel-facing API from the proof-facing one.
|
|
obligation ones.
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
We handle state restoration outside the main fail logic, as in the
future it could be that vernac execution is fully functional so we
could get rid of the second part.
|
|
We can now implement `Fail` in a direct style.
|
|
We place the check for unhandled exceptions in the `is_anomaly`
function, and consider all the exceptions non-handled by the printers
always anomalies.
This reworks the solution implemented in
ea3909466eaaf86ff212c0a002e5df11e4a979f5 , in particular
`allow_uncaught` cannot be used anymore, all exceptions must install a
printer.
In order to pass the test-suite CI we also had to register some
printers, that were not registered for no reason, forcing clients to
call a post-processing step on errors.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
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.
|
|
Reviewed-by: herbelin
|
|
Small refactoring to pass the `sigma` functionally.
|
|
Equation's terminator had exactly duplicated the shrink function used
in `Abstract`, we remove this duplicity.
|
|
We add the and routine the regular proof save path of Equations was
using.
I don't understand what is going on here, these are a few remarks:
- Equations does capture `sigma` at the time of `start_dependent_lemma`
- A custom hook is also captured, along with telescopes
- The shrink function seems like a duplicate with things already in Coq's
[abstract.ml / declareObl.ml]
I guess the preferred option would be to merge this with the
obligations save path; but I need help from experts.
|
|
Just a cleanup, should bring no functional code change.
|
|
We radically redesign how proof closing information is stored. Instead
of a user-defined closure, we now reify control into a single data
structure containing the needed information.
In this scheme, the `Lemmas` module can get extra information with
obligation info when opening the proof, and will correspondingly call
the right closing function based on this.
This is the start of what could be a much bigger unification of all
the proof save paths.
|
