Directly typed parsing #14
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
The previous level (89) of match branches was below the level of the sequence (;), thus one almost always had to wrap the value of match branches in braces. I see no need for this restriction, as match branches are clearly seperated by '|' characters.
This notation works like an if but with a lower precedence. It will check the given condition and wrap the whole remaining block into the 'true'-branch, thus making sure the condition holds for the current block. A block can be understood intuitively as everything that may possibly belong to the assert. A block only ends if something is closed that was started before the assert e.g. a paranthesis or a match arm end. This precedence gives the assert the ability to de-nest code as the 'true'-block after the condition does not have to be indented, making code more redable.
The bit vector syntax defined in Vect.v for constr and the syntax defined in Parsing.v for koika are very similar. However, for some reason the koika syntax does not support 'Ob' for an empty bitvector. I see no reason why it shouldn't exists, so I added it.
This commit brings the notations into a more logical order
maxkurze1
force-pushed
the
directly_typed_parsing
branch
from
d28c678 to
f4af9a3
Compare
This commit cleans up all notations concerning literals. This includes their typed/untyped koika and constr versions.
maxkurze1
force-pushed
the
directly_typed_parsing
branch
from
c974525 to
18ce599
Compare
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.
Again, more reworks on parsing