| Age | Commit message (Collapse) | Author |
|---|
|
PR #13183 introduced quite a bit of duplicate code, we refactor it and
expose less internals on the way. That should make the API more
robust.
|
|
We use the new `Declare.Info` structure to uniformly add properties to
the handling of constants. In this case, per-constant typing flags.
The internal code may want to see some further refactoring, including
pushing the flags down to `Safe_typing.add_constant` , but the changes
in the interface should be definitive.
This will allow #12539 and #9004 using attributes.
|
|
After the previous commit, the stm should correctly pass proof
information, thus we make `proof_object` carry it removing a bunch of
internal code.
|
|
Since 8.5, the STM could not delegate proof information it was
contained inside a closure. This could potentially create some
problems, as witnessed in #12586.
Recent refactoring have reified however much of this state, so it
seems a good idea to use bits of the state now, at the cost of
introducing some safeguards in `declare.ml` w.r.t. `Ephemerons`.
|
|
|
|
|
|
|
|
- take just a ugraph instead of the whole env
- rename to update_sigma_univs
- push global env lookup a bit further up
- fix vernacinterp call to update all surrounding proofs, not just the
top one
- flip argument order for nicer partial applications
|
|
|
|
This is an alternative to #12663 ; much preferable as the kind
information is already stored in the constant object.
|
|
|
|
This is also needed in equations.
|
|
This is for use in Equations. At some point we should make all hook aware
of state, but this should suffice for now.
Note the comments as the role of hooks here, this may need further
cleanup indeed.
|
|
In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.
Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.
We make this manipulation explicit by handling the program state
functionally, in a similar way than we already do for lemmas.
This requires to extend the proof DSL a bit; but IMO changes are
acceptable given the gain.
Most of the PR is routine; only remarkable change is that the hook is
called explicitly in `finish_admitted` as it had to learn about the
different types of proof_endings.
Note that we could have gone deeper and use the type system to refine
the core proof type; IMO it is still too preliminary so it is better
to do this step as an intermediate one towards a deeper unification.
|
|
This is essential to allow hooks to modify state.
|
|
This is needed in rewriter as to avoid hack; indeed it makes sense to
propagate this information to the callers of save.
|
|
|
|
This completes the refactoring [for now] of the core `Declare`
interface, and will allow much internal refactoring in the future.
In particular, we remove the low-level Proof_ending type, and instead
introduce higher-level constructors for the several declare users.
Future PRs will change the internal representation of proof handling
to better enforce some invariants that should hold for specific
proofs.
|
|
This allows us to remove a large chunk of the internal API, and is the
pre-requisite to get rid of [Proof_ending], and even more refactoring
on the declare path.
|
|
Now that the interface has mostly stabilized, we move code around to
respect internal dependency order.
This will allow us to start sharing more code in the 4 principal
cases, and also paves the way for the full merging of obligations and
the removal of the Proof_ending type in favor of stronger type
abstraction.
|
|
We unify information about constants so it is shared among all the
paths [interactive, NI, obligations].
IMHO the current setup looks pretty good, with information split into
a per-constant record `CInfo.t` and variables affecting mutual
definitions at once, which live in `Info.t`.
Main information outside our `Info` record is `opaque`, which is
provided at different moments in several cases.
There are a few nits regarding interactive proofs, which will go away
in the next commits.
|
|
This removes so ad-hoc tuples, and encapsulates the API a bit.
It is a step towards:
- Pushing some `to_constr` from the upper layers to the declare code
itself [which will remove code duplication, in particular making the
interactive / non-interactive path more uniform, and make the API
easier to use]
- Further refactoring of the constant information, as `Recthm.t`
contains almost now what we would call "primitive constant
information"; thus we will be able to distinguish next better between
mutual declarations and single-constant ones.
|
|
When declaring a lemma, the code path is quite different depending on
whether the lemma is inferred to be a mutually-defined lemma or not.
We refactor the code path in declare to reflect that; this will allow
to better organize constant information and to reuse the `Recthm.t`
type in particular.
|
|
|
|
|
|
|
|
Step towards merging `Info / `CInfo`; the presentation order is now
"final" in the sense of that we propose this API for the medium-term.
|
|
This is in preparation for the next commit which will clean-up the
current API flow in `Declare`.
|
|
|
|
|
|
The previous refactoring in `Declare` to add `CInfo.t` makes this a
good moment to clean overlays up w.r.t. deprecation.
All cases but one is just a matter of simple renaming, for the other
the use of an internal API is replaced by newer API.
|
|
This hides even more internals; we will reduce the API even more
shortly.
|
|
This improves the interface, and allows even more sealing of the API.
This is yet work in progress.
|
|
We move the advanced proof initialization routine to Declare, and stop
exposing implementation internals in `Info.t` constructor.
|
|
At this point the record in lemmas was just a stub; next commit will
stop exposing the internals of mutual information, and pave the way
for the refactoring of `Info.t` handling in the Declare interface.
|
|
It makes sense to require it to be uni-goal; this also removes some
duplication.
See the caveat with the handling of `~sign` tho.
|
|
In the current proof save path, the kernel can raise an exception when
checking a proof wrapped into a future.
However, in this case, the future itself will "fix" the produced
exception, with the mandatory handler set at the future's creation
time.
Thus, there is no need for the declare layer to mess with exceptions
anymore, if my logic is correct. Note that the `fix_exn` parameter to
the `Declare` API was not used anymore.
This undoes 77cf18eb844b45776b2ec67be9f71e8dd4ca002c which comes from
pre-github times, so unfortunately I didn't have access to the
discussion.
We need to be careful in `perform_buildp` as to catch the `Qed` error
and properly notify the STM about it with `State.exn_on`; this was
previously done by the declare layer using a hack [grabbing internal
state of the future, that the future itself was not using as it was
already forced], but we now do it in the caller in a more principled
way.
This has been tested in the case that tactics succeed but Qed fails
asynchronously.
|
|
In particular this avoids exposing `Evd.side_effects proof_entry` in
the API.
|
|
This is not needed outside of `Declare` now.
|
|
|
|
This reduces the amount of exported internals, in particular
w.r.t. proof delaying and side effects which we will need in future
refactorings.
Actually turning the type from `Evd.side_effects proof_entry` to `unit
proof_entry` is left for the next commits.
|
|
This removes a use of internal obligation data `prg_poly` and a couple
of duplicate lines.
|
|
|
|
Not necessary anymore after the merge of obligation declaration into
the main path.
|
|
|
|
We complete some arduous refactoring in order to bring all the
internals and code of constant / proof saving into the same module.
In particular, this PR moves the remaining parts of proof saving from
`Lemmas` to `Declare`.
The reduction in exposed internals is considerable; in particular, we
remove the export of the internals of `proof_entry` and `proof_object`
[used in delayed proofs], which will allow us to start to address many
issues with the current setup, such as #10363 .
There are still some TODOs, that will be addressed in subsequent PRs:
- Remove `declare_constant` in favor of higher-level APIs
- Then, remove access to `proof_entry` entirely
- Refactor current very verbose handling of proof info.
- Remove compat modules / API.
- Rework handling of delayed proofs [this may be hard due to state and the STM]
- Reify Hook API for the case where it acts as a continuation [that is to say, declaring constants from the Hook]
List of remaining offenders for `proof_entry` / `declare_constant` in
the codebase:
- File "vernac/comHints.ml"
- File "vernac/indschemes.ml"
- File "vernac/comProgramFixpoint.ml"
- File "vernac/comAssumption.ml"
- File "vernac/record.ml"
- File "plugins/ltac/leminv.ml"
- File "plugins/setoid_ring/newring.ml"
- File "plugins/funind/recdef.ml"
- File "plugins/funind/gen_principle.ml"
|
|
This is needed as a first step to refactor and unify the obligation
save path and state; in particular `Equations` is a heavy user of
Hooks to modify obligations state, thus in order to make the hook
aware of this we need to place the obligation state before the hook.
As a good side-effect, `inline_private_constants` and `Hook.call` are
not exported from `Declare` anymore.
|
|
The API in `DeclareDef` should become the recommended API in `Declare`.
This greatly reduces the exposure of internals; we still have a large
offender in `Lemmas` but that will be taken care of in the next
commit; effectively removing quite some chunks from `declare.mli`.
This PR originally introduced a dependency cycle due to:
- `Declare`: uses `Vernacexpr.decl_notation list`
- `Vernacexpr`: uses `ComHint.hint_expr`
- `ComHint`: uses `Declare.declare_constant`
This is a real cycle in the sense that `ComHint` would have also move
to `DeclareDef` in the medium term.
There were quite a few ways to solve it, we have chosen to
move the hints ast to `Vernacexpr` as it is not very invasive
and seems consistent with the current style.
Alternatives, which could be considered at a later stage are for
example moving the notations AST to `Metasyntax`, having `Declare` not
to depend on `Vernacexpr` [which seems actually a good thing to do in
the medium term], reworking notation support more deeply...
|
|
|
|
This is needed to make this low-level entry structures privates;
moreover, the code seems much clearer using the higher-level API.
Some more cleanup needs to be done but this is clearly a step forward
IMHO.
|
