Commit graph

576 commits

Author SHA1 Message Date
Sebastian Ullrich
32bea73708 fix: ensure hygiene of double-quoted names
Fixes #586
2021-07-30 07:17:50 -07:00
Leonardo de Moura
fb3ea8109f fix: structure instance parser 2021-07-27 12:54:17 -07:00
Wojciech Nawrocki
cfb5d34dd3 fix: parser arity 2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
4a3c172ac9 feat: parametrised deriving handlers 2021-07-24 10:45:28 +02:00
Sebastian Ullrich
5866e2bbb7 chore: use register_parser_alias where possible
Fixes #494
2021-07-22 16:28:06 +02:00
Sebastian Ullrich
42e681a5a6 fix: make unterminated comments consume all input
Fixes #549
2021-07-22 15:55:12 +02:00
Sebastian Ullrich
8637220927 fix: make precedence mandatory for mixfix commands
Resolves #577
2021-07-19 13:18:58 -07:00
Wojciech Nawrocki
a8d599a955 fix: typo 2021-07-15 21:57:55 +02:00
Leonardo de Moura
f4a7ffd8c8 chore: fix codebase and tests 2021-06-29 17:14:52 -07:00
Leonardo de Moura
90a79a0b06 chore: remove command universes
Now, `universe` may declare many universes. The goal is to make it
consistent with the `variable` command
2021-06-29 17:01:07 -07:00
Sebastian Ullrich
3f4ab0a2af feat: implement elab_rules
TODO: infer category from quotation type
2021-06-21 10:17:26 -07:00
Sebastian Ullrich
9101c9d5da feat: support docstrings on syntax/macro/... 2021-06-21 10:17:26 -07:00
Sebastian Ullrich
619873c842 feat: make System.FilePath opaque 2021-05-28 14:19:59 +02:00
Sebastian Ullrich
e918e39ed0 feat: have: remove unnecessary whitespace check and allow name- and type-less have 2021-05-25 14:25:14 +02:00
Leonardo de Moura
8b4cdcfddd chore: fix mutable variable shadowing 2021-05-22 19:24:41 -07:00
Sebastian Ullrich
5b6051b15e feat: revise have syntax 2021-05-20 15:17:36 -07:00
Sebastian Ullrich
23f0c1051c feat: improve ToString/Quote Name 2021-05-19 09:34:01 +02:00
Leonardo de Moura
3b7bcdc449 feat: add endPos field to SourceInfo.original
We need an update stage0 before we use it.
2021-05-17 14:32:58 -07:00
Leonardo de Moura
71cd067e94 feat: add helper command 2021-05-13 22:10:35 -07:00
Sebastian Ullrich
baa2781eb0 chore: remove built-in emptyC syntax/elaborator 2021-05-06 22:07:03 +02:00
Leonardo de Moura
e8aa02cd51 feat: closes #415 2021-05-03 18:04:01 -07:00
Leonardo de Moura
f8ac5d25dd feat: add notation for helper elaboration function
This similar to `binrel%` but for binary operators.

See issue #382
2021-04-30 17:14:17 -07:00
tydeu
44f45f426c
feat: add scoped macro_rules (#432) 2021-04-30 09:05:09 +02:00
Sebastian Ullrich
f0960b7f89 fix: ignore antiquotations outside quotations 2021-04-29 13:33:48 +02:00
Sebastian Ullrich
73cf3533a1 fix: count quotation depth in parser correctly 2021-04-29 13:33:48 +02:00
Sebastian Ullrich
8119daeb18 feat: syntax & attribute for double-quoted quotations 2021-04-27 16:38:37 -07:00
Daniel Fabian
0238bf8c33 refactor: use Ordering inside of rbmap instead of lt. 2021-04-27 07:58:58 -07:00
Sebastian Ullrich
53b0e7dde8 fix: ban tabs
Fixes #339
2021-04-25 19:55:15 -07:00
Sebastian Ullrich
01f6cece2f chore: fix parser error message 2021-04-24 21:48:12 +02:00
Sebastian Ullrich
069bcf8933 fix: restore missing invariant 2021-04-24 21:46:48 +02:00
Leonardo de Moura
a076b5b89e feat: improved error recovery for interpolated strings 2021-04-24 10:24:57 -07:00
Leonardo de Moura
09d438ca1d chore: enforce notation parameter naming convention 2021-04-19 18:54:09 -07:00
Sebastian Ullrich
61f39d6088 chore: Parser.atomic: preserve partial output 2021-04-17 23:44:45 +02:00
Sebastian Ullrich
fd42b111fb chore: always push missing on a parser error 2021-04-17 23:44:43 +02:00
Leonardo de Moura
157ef80c5a feat: match auto generalization 2021-04-16 21:48:38 -07:00
Leonardo de Moura
1c23d68c6a feat: add (generalizing := true/false) optional attribute to match 2021-04-15 17:04:25 -07:00
Leonardo de Moura
abf78e162c feat: add notation for disabling implicit lambda feature
This notation will be useful for writing macros where
implicit lambdas are not desired.
2021-04-12 22:33:23 -07:00
Daniel Selsam
d35091da56 feat: parser alias for 'declVal' 2021-04-12 16:59:54 -07:00
Leonardo de Moura
578b3b822f fix: do not use nullKind for group combinator
We use `nullKind` for the `group` parser combinator.
When pattern matching `nullKind` nodes, we check their arities.
So, error recovery often fails for parsers that use the `group`
combinator.
For example, we have the parser
```
def whereDecls := leading_parser "where " >> many1Indent (group (letRecDecl >> optional ";"))
```
If there is syntax error at `letRecDecl`, the node corresponding to
```
group (letRecDecl >> optional ";")
```
will contain only one child, and the pattern matching at
```
def expandWhereDecls (whereDecls : Syntax) (body : Syntax) : MacroM Syntax :=
  match whereDecls with
  | `(whereDecls|where $[$decls:letRecDecl $[;]?]*) => `(let rec $decls:letRecDecl,*; $body)
  | _ => Macro.throwUnsupported
```
fails, and we can't elaborate the partial syntax tree for
`letRecDecl`, and auto-completion will not work there.

We address this issue by using a new kind for the `group` combinator.
The idea is to pattern match `group` as we pattern match `node`s with
proper syntax node kinds. This change is consistent with the way we
use `group` where it mainly a convenience for saving us the trouble of
defining a new parser definition that is used only once.
2021-04-07 22:30:51 -07:00
Leonardo de Moura
2b9df7d8b9 chore: make it clear that implementation relies on the fact that both branches of the if-then-else generate a node with the same kind
Motivation: we want to change the kind used in the `group` combinator.
2021-04-07 22:02:17 -07:00
Leonardo de Moura
6c0f3c277f fix: ignore syntactically incorrect commands that do not contain any symbol
This kind of broken command does not have a position information, and
was producing a panic message in the server because it makes the
reasonable assumption that every command returned by `parserCommand`
has a position.
2021-04-07 14:46:13 -07:00
Leonardo de Moura
0717c3d0b2 chore: adding helper parser completion
I am hitting many error recovery problems. This is an attempt to make
auto-completion more robust.
For example, we currently can't auto complete inside of parentheses.
The syntax tree for the syntactically incorrect tern `(s. , 0)` is
```
(Term.paren "(" [(Term.proj `s ".")])
```
The elaborator for `paren` fails to match this partial syntax tree and
returns an error. I considered adding code to the `else` branch of
this elaborator and handle partial trees there. However, we would
still be losing information for the other elements of the tuple.
Example: no hover information for them.
The helper parser makes sure we don't lose information.
2021-04-05 18:44:01 -07:00
Leonardo de Moura
f13bdd6869 fix: error recovery at sepBy combinator 2021-04-05 18:38:57 -07:00
Leonardo de Moura
fb38955be2 feat: improve command parser error recovery
After a parser error in a command, we are "swallowing" all command
parsing errors until a command was succesfully parsed.
This was producing counterintuitive behavior in the IDEs.
2021-04-05 12:31:33 -07:00
Leonardo de Moura
d6af843683 chore: remove completion auxiliary parser 2021-04-05 11:26:13 -07:00
Leonardo de Moura
e6dec2dd79 feat: don't allow whitespaces between . and field name 2021-04-05 07:11:14 -07:00
Sebastian Ullrich
98e1baabbd refactor: make trailingNode clean up after itself
Also resolves an issue with emitting both `left` and a partial tree
containing it
2021-04-05 13:51:03 +02:00
Sebastian Ullrich
6dc3e55c54 fix: longestMatchFn: do not discard partial syntax tree of first overload 2021-04-05 10:00:47 +02:00
Sebastian Ullrich
e5be9e7dd4 chore: helpers for parser debugging 2021-04-05 10:00:47 +02:00
Sebastian Ullrich
d0996fb945 chore: improve EOI error message 2021-04-03 11:56:26 +02:00