Conversation
See https://hal.science/hal-03294999v1 for more information on the High Level Language
| u2bin | ||
| unsigned | ||
| with | ||
| X) |
There was a problem hiding this comment.
I'm having trouble finding this in the docs - are these keywords case insensitive, or are only the cases listed here (like true, True, TRUE) valid? If it's case-insensitive, it's probably better to upcase or downcase before checking inclusion in this set.
There was a problem hiding this comment.
Only the cases listed here are valid. In https://hal.science/hal-03356342v1/, you can see in Appendix B the correct spellings. Therefore, as you mention, I don't think it's necessary to downcase before checking.
spec/visual/samples/hll
Outdated
| b := ALL i:[0, NOF_PIGEONS-1] SOME j:[0, NOF_HOLES-1] (P[i,j]); | ||
|
|
||
| proof obligations: | ||
| ~(a & b); |
There was a problem hiding this comment.
If it's possible, it's best to really stress-test the lexer here, rather than pasting the same example from the demo.
There was a problem hiding this comment.
I created a new stress test that should cover most common syntax constructions. Don't hesitate to tell me if you prefer an even more complete coverage.
- Lex built in functions - Lex more operators (those containing !) - Lex binary and hexadecimal literals
|
Thanks for the review and the suggestions ! I also made the lexer more complete over the HLL grammar. |
2 participants
This pull requests adds a lexer for the High Level Language (a.k.a. HLL), a language used in formal verification for railway systems. The specification is available here or there.