Lexer for Agda - #1825
Lexer for Agda#1825ionathanch wants to merge 18 commits into
Conversation
|
Not sure the etiquette on this, but I would like to boost this. The support for agda here would be great! |
| state :hole do | ||
| rule %r/!}/, Comment::Special, :pop! | ||
| rule %r/{!/, Comment::Special, :hole | ||
| rule %r/./, Comment::Special |
There was a problem hiding this comment.
If possible, it's much better for performance to capture more than a single character at a time here. Maybe above this rule add one for %r/[^{!]+/? It avoids having to pop in and out of the regex engine on every character.
There was a problem hiding this comment.
(same goes for the other rules that use %r/./ - try to have a greedier regex first if possible)
|
To fix the Linelint error all you've gotta do is remove the extra blank line at the end of |
* Builtin pragmas always have the form `{#- BUILTIN <builtin> ... #-}`
* Other pragmas always have the form `{#- <pragma> ... #-}`
* Match as many chars as possible in block comments/holes
* Fix lexing line comments after many spaces
(More examples to follow)
| keywords %r/\w+/ do | ||
| rule BUILTINS, Keyword::Pseudo | ||
| end | ||
| rule %r/\s+/, Comment::Preproc |
There was a problem hiding this comment.
This is here twice for some reason, and in a bunch of the other rules.
There was a problem hiding this comment.
Do you mean the \s+ rules? That was to ensure that the builtin (and pragma below) keywords have to be followed by spaces
There was a problem hiding this comment.
That's unfortunately not how the lexer model works - keywords will end when the covering regex ends, so at the first non-\w character. If you really need a space (and not, e.g. a parenthesis or other punctuation), you can use a lookahead, like keywords %r/\w+(?=\s)/. I'm not super familiar with Agda, but I think that's unlikely to be correct.
There was a problem hiding this comment.
Ah I see... reading the lexer dev doc more closely, I've misunderstood how the states work. I think I need to move the keyword rule up to where the pragma rule is then
| rule BUILTINS, Keyword::Pseudo | ||
| end | ||
| rule %r/\s+/, Comment::Preproc | ||
| rule %r/.+#-}/, Comment::Preproc, :pop! |
There was a problem hiding this comment.
This will unfortunately break if the brace isn't closed. The way you had it before was fine, but it needed a negative capture to grab stuff a bit more greedily.
5 participants
[Issue #709] Based on Agda's lexer, I've filled out the remaining bits of the Agda lexer. It doesn't quite match the behaviour, especially in places where the semantics of the keywords matter (e.g. imports, pragmas), but this should be sufficient to cover most use cases and look nice, and I think Rouge should have at least some Agda support with improvements as needed later on. (And thanks @ayberkt for the initial work!)