Passed a big milestone towards bootstrapping Lean 4 today: After grafting the old elaborator (written in C++) onto the new frontend (written in Lean) in true Frankensteinian fashion, the new frontend can now process all 2176 lines of core.lean successfully!
Conversation
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. :)
1
4
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.
GLR can deal with ambiguous grammars (arbitrary CFGs in fact), but I think Stratego goes beyond CFGs for a few reasons having to do with extensible parsing, and IIRC one is to help prioritization?
1
OTOH real-world compilers often use hand-written recursive-descent parsers anyway?
1
1
Show replies
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
Show replies
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?
1
Show replies