Update documentation on syntax and semantics of Kore #2266
Merged
Conversation
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
"Introduction to Matching Logic" is those parts of "The Semantics of K" which are still relevent to present-day Kore.
ttuegel
force-pushed
the
doc--intro-matching-logic
branch
2 times, most recently
from
868db6a to
bcca2b6
Compare
ttuegel
force-pushed
the
doc--intro-matching-logic
branch
from
bcca2b6 to
a501cf0
Compare
There was a problem hiding this comment.
I only noticed one issue in kore-syntax, and the rest looks good to me. But, before I approve this, I have a question. I think the introduction-to-matching-logic document used to be part of the old semantics-of-k document, is that correct? Does this PR make any changes to it?
| <set-variable> | ||
| ::= <set-variable-id> ":" <sort> | ||
| ::= <set-variable-identifier> ":" <sort> |
There was a problem hiding this comment.
Aren't set variables required to be prefixed with @?
There was a problem hiding this comment.
That's part of <set-variable-identifier>.
Co-authored-by: Andrei Burdușa <[email protected]>
| Note that, by default, symbols are interpreted as relations in matching logic. | ||
| It is often the case, though, that we want symbols to be interpreted as | ||
| \emph{functions}. | ||
| This can be easily done by axiomatically constraining those symbols to evaluate to |
There was a problem hiding this comment.
I think it can be confusing that function in this context means evaluating to exactly one value, while the glossary describes it as evaluating to at most one value.
ana-pantilie
approved these changes
Nov 17, 2020
andreiburdusa
approved these changes
Nov 17, 2020
MirceaS
approved these changes
Nov 19, 2020
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.
Reviewer checklist
stack test --coveragestack haddock