Is there a place we can go to have a sneak peek at this work? Super interested to see how one goes about implementing an elaborator for Lean in Lean. :)
Conversation
Not quite yet, unfortunately. Though rewriting the (term-level) elaborator in Lean is the one big task we haven't even started yet. Thus Frankenstein, for the time being.
1
3
Haha, no worries! I was actually attempting to look for the source code of your Lean parser in Lean the other day, but also couldn't find it either. Is that also a WIP?
1
2
Yes, it's all part of Lean 4. "We are currently developing Lean 4 in a new (private) repository. The Lean 4 source code will be released here when ready." :) github.com/leanprover/lean
1
3
Ahhh righto! Hehe, I'm so excited! Super interested to see what you've all learned.
Specifically atm I'm learning about in Top-Down Operator Precedence (Pratt) parsing and wondering if it's the right approach to be making. Having extensible syntax would be nice!
1
3
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.
2
3
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
Why must those two be distinguished? If B doesn’t mention x, it’s not dependent
1
1
I guess perhaps if you don't want you parser to know about name binding? Or are you saying you could remove the non-dependent function arrow, and always require a name for the parameter?
Yeah, the latter. Then post-processing would determine if it’s dependent or not based on whether the bound name is used on the RHS of the arrow or not. But my only context here is this thread so I might just be missing something!