Haskell-like custom parsers in quasiquotations?

Stream: lean4

[Kyra Brian]

Haskell supports custom concrete syntax in quasiquotations accepting user-supplied parsers.

Does anything like this exists in Lean 4?

If no, which approaches I'd may try to emulate this mechanism?

Any links and explanations would be greatly appreciated.

[Eric Wieser]

Do you want a Syntax quotation or an Expr quotation?

[Kyle Miller]

Could you give an example of what you want to do?

Lean does give you quasiquoters for user-defined parsers. It let's you use quasiquotations both for generating syntax and for matching against syntax.

[Kyra Brian]

Kyle Miller said:

Could you give an example of what you want to do?

Lean does give you quasiquoters for user-defined parsers. It let's you use quasiquotations both for generating syntax and for matching against syntax.

This

    getTimeDef = [cedecl|
      double get_time()
      {
          struct timeval t;
          struct timezone tzp;
          gettimeofday(&t, &tzp);
          return t.tv_sec + t.tv_usec*1e-6;
      }
      |]

is a real-life example (from Haskell imperative-edsl package, which uses language-c-quote package), and it may contain another nested quasiquotes and antiquotes too.

cedecl is a custom parser, which parses C code and returns a Haskell-defined C AST.

And language-c-quote package provides several other C parsers for other C-fragments, which return the same Haskell-defined C AST data.

[Sebastian Ullrich]

Does https://leanprover.github.io/lean4/doc/syntax_example.html help?

[Kyle Miller]

@Kyra Brian I've used cedecl long ago, and yeah, that's within the purview of Lean's metaprogramming abilities. You could potentially define a cedecl(...) elaborator that parses the ... using a C parser and then turns it into a Lean-defined C AST. Sebastian linked to an example using macro-defined transformation rules, and you can write more elaborate transformations as needed.

@Mac Malone seems to have written a C grammar in Lean here

[Kyra Brian]

Sebastian Ullrich said:

Does https://leanprover.github.io/lean4/doc/syntax_example.html help?

Yes, exactly. Thanks!

[Kyra Brian]

Exploring the theme further i've discovered this project.

After several unsuccessful attempts to build it against 4.0 release and the latest 4.3 pre, I've recognized it requires vcustom-tokens branch by @Sebastian Ullrich .

But the latter is 3 months old.

Thus I wonder how it all is going to be developed further.

Will the project be ported to "vanilla" Lean 4?

Or will vcustom-tokens branch be eventually merged into the main Lean repo?

Or something else?

[Sebastian Ullrich]

Or will vcustom-tokens branch be eventually merged into the main Lean repo?

Absolutely, there is an open PR for it. I'm just working on other things right now. But hearing people looking forward to it helps increase its priority a bit :)

[Mac Malone]

Sebastian Ullrich said:

But hearing people looking forward to it helps increase its priority a bit :)

I that case, I should note that I am also looking forward to it. It would help a lot with my experimental embedded language DSLs!