[api] Refactor most of Decl_kinds
#10419
Merged
Conversation
This file contains 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
ejgallego
added
kind: cleanup
|
Sadly this had to depend on the previous kind cleanup, last 4 commits are the relevant ones. |
|
cc: #10417 |
ejgallego
force-pushed
the
heads+test
branch
11 times, most recently
from
5c0729d
to
cbe628a
Compare
ejgallego
removed
the
needs: merge of dependency
|
Ok, this may still need some thinking but IMHO the bulk is ready for review. This PR also answers a question posed by @maximedenes about |
ejgallego
requested review from
amahboubi,
aspiwack,
forestjulien,
mattam82,
silene and
a team
as code owners
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.
The whole business of cst_kind is fishy tho, it seems to me that it should be removed from the libobject path.
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 remove two flags that were seldom used in favor of named parameters.
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.
`declare_definition` didn't improve a lot the declare path and was used only once on interesting code. Also, it had many optional parameters. The declare path is critical enough as to care about a tidy API.
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Jul 1, 2019
SkySkimmer
reviewed
Jul 2, 2019
SkySkimmer
reviewed
Jul 2, 2019
| val variable_opacity : variable -> bool | ||
|
|
||
| (* Used in declare, very dubious *) | ||
| val variable_context : variable -> Univ.ContextSet.t | ||
| val variable_polymorphic : variable -> bool |
There was a problem hiding this comment.
These 2 can be removed: #10461.
SkySkimmer
reviewed
Jul 2, 2019
|
|
||
| val add_variable_data : variable -> variable_data -> unit | ||
|
|
||
| (* Not used *) | ||
| val variable_path : variable -> DirPath.t |
There was a problem hiding this comment.
I though we could address the refactoring of this module in its own PR.
We cleanup a few imports on Declare, and indeed we find a suspicious exception `AlreadyDeclared` present in `CErrors` where it should not be there. We move it to `Declare`, waiting for more investigation.
We should have this in the check target, but meanwhile we have to do manual housekeeping here.
|
Wrong label for exception fixed. |
ejgallego
added a commit
to ejgallego/Mtac2
that referenced
this pull request
Jul 2, 2019
|
Bench said: https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/740/console |
SkySkimmer
added a commit
to SkySkimmer/coq
that referenced
this pull request
Jul 3, 2019
Reviewed-by: SkySkimmer Ack-by: herbelin
SkySkimmer
added a commit
to coq-community/paramcoq
that referenced
this pull request
Jul 3, 2019
[coq] Overlay for coq/coq#10419
bors bot
added a commit
to Mtac2/Mtac2
that referenced
this pull request
Jul 3, 2019
218: [coq] Overlay for coq/coq#10419 r=Janno a=ejgallego Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
gares
added a commit
to LPCIC/coq-elpi
that referenced
this pull request
Jul 3, 2019
[coq] Overlay for coq/coq#10419
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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 move the bulk of
Decl_kindsto a better place [namelyinterp/decls] and refactor the use of this information quite a bit.The information seems to be used almost only for
Dumpglob, so itcertainly should end there to achieve a cleaner core.
In particular the use of "variable" data stored in Decls seems very suspicious.
IMO this may need a bit more work, but this should be a good start, I wonder what people who know more about this
variable datastuff can say.Overlays: