make the "inner cast" be a synonym for a strict cast#2352
Conversation
|
Why not remove it completely? |
|
As I have said elsewhere, it is not currently possible to strict-cast a term whose last production item is a non terminal. This feature is needed in order to disambiguate the particular rule that currently is using an inner cast as a workaround. Simply removing it entirely does not work because then that rule parses incorrectly. |
|
You mean this |
|
Logically, a strict cast doesn't pass through a bracket because strict casts only affect the term they are applied to, which in this case would be a bracket. The inside of the bracket would still be non strict, and thus the bracket essentially negates the strictness of the cast. I guess maybe you could make an argument that since this makes strict casting a bracket completely useless, that we should instead change the behavior of the type inferencer so that a term inside a bracket inside a strict cast is also strict. That requires a much more involved change to the type inferencer, but it's doable and then you would be able to write the rule in question using a strict cast. Is that what you would prefer to see instead? If we did that, we ought to be able to entirely delete the inner cast syntax. It might break some existing definitions in theory, because of the modified behavior of strict casts, though. This change is much more backwards compatible. I'm willing to be flexible. Make your arguments for or against each idea. |
|
By the way, one argument against making strictness pass through casts is that someone could theoretically write a grammar where the bracket itself needed to be strict casted in order to disambiguate it, which would no longer be possible without unintended side effects if we made such a change to the inferencer. Now such a grammar is highly unlikely in practice, but it is a limitation on the expressivity of k in terms of the set of grammars it is able to faithfully represent, so if you're concerned about theoretical completeness in the design of the parser, it's probably worth keeping the inferencer code the way it is in this PR instead. |
This PR cleans up a few issues related to the `{...}<:S` syntax for
strict casts. Specifically,
- Add a section to Lesson 1.11 explaining the need for the braced strict
cast syntax
- Change the klabel from `#InnerCast` to `#SyntacticCastBraced`
- `#InnerCast` was a holdover from prior to #2352
- Opinionatedly, change the syntax from `{...}<:S` to `{...}::S`
- Makes it more obvious this is just an alternative syntax for strict
casts `::S`
- To me, the syntax `<:S` is misleading in that it reads as "subsort of
`S`", but the actual meaning is "exactly the sort `S` and not a proper
subsort".
- Minimal fallout - there is only one rule in `rv-match` and two tests
in `pyk` where this needs to be changed
(https://github.com/search?q=org%3Aruntimeverification+%7D%3C%3A&type=code)
The commit history is clean and I can just drop the last commit if we
don't want to change the syntax.
---------
Co-authored-by: rv-jenkins <admin@runtimeverification.com>
3 participants
This would close the "type loophole" that lets you put a term of any sort anywhere. Since when you did this, a bunch of stuff broke, we don't really have more than the single instance in any of our semantics of this actually being used. Hence the reason this PR is so small.
The singular usage is on line 1649 of domains.k.