[declare] Refactor constant information into a record. - #12372
Merged
Conversation
ejgallego
added
kind: cleanup
ejgallego
force-pushed
the
proof+info
branch
3 times, most recently
from
May 25, 2020 13:12
fe87400 to
5e41e10
Compare
This was referenced Jun 18, 2020
ejgallego
force-pushed
the
proof+info
branch
5 times, most recently
from
June 23, 2020 19:50
bf9b69d to
5ac2c3e
Compare
ejgallego
added
the
needs: overlay
Contributor
Author
|
This is ready for review, overlays in preparation. |
ejgallego
marked this pull request as ready for review
June 23, 2020 21:01
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.
We move the advanced proof initialization routine to Declare, and stop exposing implementation internals in `Info.t` constructor.
The module is now a stub. We choose to be explicit on the parameters for now, this will improve in next commits with the refactoring of proof / constant information.
This improves the interface, and allows even more sealing of the API. This is yet work in progress.
This hides even more internals; we will reduce the API even more shortly.
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 is in preparation for the next commit which will clean-up the current API flow in `Declare`.
Step towards merging `Info / `CInfo`; the presentation order is now "final" in the sense of that we propose this API for the medium-term.
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.
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.
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.
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.
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.
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 is needed in rewriter as to avoid hack; indeed it makes sense to propagate this information to the callers of save.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
We refactor and consolidate handling of constant information in the
Declareinterface.This improves the interface, enforces some more invariants, and allows a significant sealing of the API.
The PR is large as it was a bit of titanic work to have everything fall in place and stabilize the API, no point on doing overlays for an interim version of the API IMO. Future PRs will rework the internals of declare and hopefully consolidate them, in particular regarding proof involving many constants, side-effects, etc...
I will also allow #12539 and #9004
Overlays: