Rename wc to goal - #453
Open
System625 wants to merge 2 commits into
Open
Conversation
`Wc` is the "predicate or combinator" level of the proof language: an
atomic `Predicate`, a `for<..>`, or an `if ..`. Everything that consumes
it already calls that a goal -- `prove(.., assumptions, goal)`, the
"Goal(s) to prove ..." doc comments on `Wcs::all_eq` and friends,
`TypeckEnv::prove_goal` -- so name the type after what it is rather than
after the `WhereClause` syntax it happens to be lowered from.
Wc -> Goal (grammar/wc.rs -> grammar/goal.rs)
Wcs -> Goals
ToWcs -> ToGoals, to_wcs -> to_goals, to_wc -> to_goal
`WhereClause` is untouched: it remains the syntactic level and lowers
into `Goal`s via `ToGoals`. Pure rename, no behavioural change, and no
snapshot moves.
Follows the type rename: `prove_wc` proves one `Goal`, and `prove_wc_list`
proves a list of them.
prove_wc -> prove_goal (prove/prove_wc.rs -> prove/prove_goal.rs)
prove_wc_list -> prove_goal_list (likewise)
A judgment's source file appears in failure output, so the 16 snapshot
lines reading `the rule "trait implied bound" at (prove_wc.rs)` now read
`(prove_goal.rs)`. Nothing else in the snapshots moves: no judgment
changed line number.
Collaborator
|
Thanks for contributing to formality! :) |
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.
What does this PR do?
Part of #417, after #445 and #450. Step 4 of the issue says to collapse
WcintoPredicate, the distinction between atomic predicates and combinators is kept as discussed, so this renames that second level instead of merging it.After this PR:
Predicate= atomic (the six original variants plus the four relations merged in Merge Relation into Predicate #450)Goal=Predicate|for<..>|if ..WhereClause= unchanged, still the syntactic level, still lowering intoGoals viaToGoalsI picked
Goal/Goalsbecause it is already what the code calls these things (prove(.., assumptions, goal), the "Goal(s) to prove ..." doc comments onWcs::all_eqand friends,TypeckEnv::prove_goal), and it lines up with chalk, whereGoalis the quantifier/implication layer sitting over atomicDomainGoals.How does it work, what questions do you have?
I renamed prove_wc.rs to prove_goal.rs and the associated judgment. Snapshot churn is 16 lines: the rule "trait implied bound" at (prove_wc.rs) becomes (prove_goal.rs). I edited these by hand rather than running UPDATE_EXPECT=1. expect-test rewrites an entire block when any line in it changes, and three blocks in tests/borrowck.rs are indented deeper than its canonical output, so running it turns 16 changes into a 646-line diff. Then the indentation is trimmed before comparison, so tests will still pass. Only other movement is cargo fmt re-sorting the mod prove_*; list in prove.rs.
AI disclosure