Yep, we're still doing Pratt parsing! Only realistic alternative I'm aware of is Isabelle's Early parsing, but having to specify a formal, context-free priority grammar is pretty far from our approach of "everything goes" parser combinators.
Conversation
2
2
I've seen GLR, but not investigated too deeply! That's what tree-sitter uses, right? tree-sitter.github.io/tree-sitter/
2
I was starting on a hand-rolled parser because over the LR parser generator I was using because `(x : A) -> B` is ambiguous. It could either be parsed as:
- a dependent function type
- a non-dependent function with the input type annotated
I want to prioritise the former.
3
1
1
Do you have a pointer to the grammar ? Would be interesting as a case for priorities in SDF3
1
1
This is the grammar that they tend to use:
term ::= var
| term term
| "(" term ")"
| term ":" term
| term "->" term
| ( "(" var+ ":" term ")" )+ "->" term
Coming up with good precendences is left as an exercise 😊
1
3
I have an issue for it here: github.com/pikelet-lang/p
1
Quote Tweet
Replying to @brendanzab
seems like the real issue is overloading of parens!
1
Looks like an inherent ambiguity that is not solvable by priorities, since those select between a re-ordering of the tree using the same productions. Will do an experiment with SDF3
2
2
The grammar above is indeed inherently ambiguous. For example, how would you parse `z (a : b)(c : d) -> e f` ?
2
Yeah, I'm curious what Agda does there. I would expect a language to at least say 'help, add parens here please!'
Oh, Agda lacks `:` for type annotation, again getting around this issue. 🤔
2
I wonder if has a thought. In some ways type annotation in terms being related to proof search? Assuming / hypothesis vs proof cut? Idk.
1
1
Show replies