Inductive definition in macros

Stream: lean4

[Calvin Lee]

Is there any way to generate inductive definitions (and matches on those definitions) in a macro?
I'd like to do something like write a macro that creates an "enumerable" type with a list of identifiers, and the implements ToJson/FromJson using the string version of those identifiers

[Sebastian Ullrich]

You can create arbitrary syntax with a macro, including commands

[Calvin Lee]

So here was my first try to do just that

syntax identArr := "[" sepBy(ident, ", ") "]"
syntax "gen_enum_defs%" ident identArr : command -- TODO
syntax "gen_enum_json%" ident identArr : command
macro_rules
  | `(gen_enum_json% $id [$ids,*]) =>
    open Lean in --set_option trace.Meta.debug true in
      let ids : Array Syntax := ids
      if ids.size = 0 then
        return mkNullNode
      else
        `(| "$(quote ids[0])" => $(quote ids[0]) %gen_enum_json% $id [$(ids[1:]),*])

--syntax "gen_enum" identArr : command
macro "gen_enum" id:ident ids:identArr : command =>
  `(inductive $id where gen_enum_defs% $id $ids
    instance : FromJson $id where
      fromJson? j := do match (<-j.getStr?) with gen_enum_json% $id $ids)

But I'm getting some errors on the | which I think means it was invalid syntax

[Sebastian Ullrich]

You cannot use macros in that position, you have to insert the syntax directly using quotations. There is no documentation on complex quotations yet (oops), but you can find examples in Lean such as https://github.com/leanprover/lean4/blob/1af02dcaca3ca0665a37254aaa30ea196ec77c90/src/Lean/Elab/Quotation.lean#L457

[Sebastian Ullrich]

See also https://leanprover-community.github.io/lt2021/slides/sebastian-lean4-parsers-macros.pdf#page=23

[Calvin Lee]

I see, so if I had something like $[| $strs => $idents]* it would expand correctly into multiple patterns?

[Sebastian Ullrich]

Exactly!

[Calvin Lee]

Ok, then starting from square 1, if I try

syntax identArr := "[" sepBy(ident, ", ") "]"
syntax "gen_enum" ident identArr : command
macro_rules
  | `(gen_enum id [$ids,*]) =>`(inductive $id where $[| $ids ]*)

I get expected ) on the second $

[Calvin Lee]

Here is something that is mimicking the inductive definition more somewhat (and your example) but it's having trouble on the first $[| $ids]*

syntax "enum" ident " where " ("|" ident)* : command
macro_rules
  | `(enum $id where $[| $ids ]*) =>`(inductive $id where $[ $ids ]*)

[Sebastian Ullrich]

Ah, that looks like an issue with (stx)...

syntax myMatchAlt := "|" ident
syntax "enum" ident " where " myMatchAlt* : command
macro_rules
  | `(enum $id where $[| $ids:ident ]*) =>`(inductive $id where $[| $ids:ident ]*)

[Calvin Lee]

Ok, so I've tried to add it the FromJson and I'm getting a weird parenthesize: uncaught backtrack exception.
The code thus far is

syntax myMatchAlt := "|" ident
syntax "enum" ident " where " myMatchAlt* : command
macro_rules
  | `(enum $id where $[| $ids:ident ]*) =>
    open Lean in
      -- remove `
      let matchPatterns := ids.mapSepElems fun i => quote ((toString i).drop 1)
      let fromJson := id.getId.appendAfter "FromJson"
      `(inductive $id where $[| $ids:ident ]*
        instance $(mkIdentFrom id fromJson) : FromJson $id where
          fromJson? j := do match (<-j.getStr?) with
            $[| $matchPatterns => pure $ids ]*
            | _ => failure
        )

e.g. enum E where fails with the backtrace

  [Error pretty printing syntax: parenthesize: uncaught backtrack exception. Falling back to raw printer.]
  (Command.declaration
   (Command.declModifiers [] [] [] [] [] [])
   (Command.instance
    (Term.attrKind [])
    "instance"
    [`EFromJson]
    []
    (Command.declSig [] (Term.typeSpec ":" (Term.app `FromJson._@.Santorini.RPC._hyg.2104 [`E])))
    (Term.whereDecls
     "where"
     [[(Term.letRecDecl
        []
        []
        (Term.letDecl
         (Term.letIdDecl
          `fromJson?._@.Santorini.RPC._hyg.2104
          [(Term.simpleBinder [`j._@.Santorini.RPC._hyg.2104] [])]
          []
          ":="
          (Term.do
           "do"
           (Term.doSeqIndent
            [(Term.doSeqItem
              (Term.doMatch
               "match"
               [(Term.matchDiscr
                 []
                 (Term.paren "(" [(Term.liftMethod "<-" `j.getStr?._@.Santorini.RPC._hyg.2104) []] ")"))]
               []
               "with"
               (Term.matchAlts
                [(Term.matchAlt
                  "|"
                  [(Term.hole "_")]
                  "=>"
                  (Term.doSeqIndent [(Term.doSeqItem (Term.doExpr `failure._@.Santorini.RPC._hyg.2104) [])]))]))
              [])])))))
       []]])))

[Sebastian Ullrich]

Yes, the pretty printer often gives up when given invalid syntax. But that can't be the actual error message.

[Calvin Lee]

Ah, then the actual error message is unexpected syntax

[Sebastian Ullrich]

Try $matchPatterns:term. A general matchAlt has a comma-separated list of terms (patterns).

[Calvin Lee]

well I don't think that is causing this particular error beacuse in enum E where there should only be the _ pattern (I think this is shown in the raw printer)

[Sebastian Ullrich]

Ah, right. Then I'm not sure. Debugging syntax trees can be tough, unfortunately.

[Sebastian Ullrich]

It can help writing out the expected output and looking at its structure with set_option trace.Elab.command true in ...

[Calvin Lee]

How should I write . eliminated terms? i.e. if I have two names $a and $b$ is there a function that gives $a.$b or can i just write it like that?

[Sebastian Ullrich]

That only works for projections. Otherwise you need to concatenate them on the Name level

#eval `a ++ `b

[Calvin Lee]

Ahh ok that makes sense. Is there any way to get the Names themselves from Syntax variables?

[Sebastian Ullrich]

If it's an ident, Syntax.getId. Syntax.mkIdent is the reverse.

[Calvin Lee]

Thank you for working with me so much!
Is there some way to print trace messages myself?

[Calvin Lee]

OK this is somewhat working now! Here's my code

syntax myMatchAlt := "|" ident
syntax "enum" ident " where " myMatchAlt* : command
macro_rules
  | `(enum $id where $[| $ids:ident ]*) =>
    open Lean in do
      let matchPatterns := ids.map fun i => quote ((toString i).drop 1)
      let retPatterns := <-(ids.mapM (m := MacroM) fun i => `($(mkIdent $ id.getId ++ i.getId)))
      `(inductive $id where $[| $ids:ident ]*
        instance : FromJson $id where
          fromJson? j := do match (<-j.getStr?) with
            $[| $matchPatterns => pure ($retPatterns) ]*
            | _ => failure
        instance : ToJson $id where
          toJson e := match e with
            $[| $retPatterns:term => $matchPatterns ]*
      )

there were two interesting things... First, If I try creating an identifier to name the instance declarations it fails and I can't quite figure out why. Second, this was failing if I had more than one injection (e.g. enum E where | E1|E2) because for some reason mapSepElems and mapSepElemsM only mapped the first element and none of the others.... I had to change to map and mapM

[Sebastian Ullrich]

Nice!
Calvin Lee said:

First, If I try creating an identifier to name the instance declarations it fails and I can't quite figure out why.

Did you use :ident?

Second, this was failing if I had more than one injection (e.g. enum E where | E1|E2) because for some reason mapSepElems and mapSepElemsM only mapped the first element and none of the others.... I had to change to map and mapM

mapSepElems is for syntax created by sepBy (i.e. ,* etc), not many (i.e. *)

[Sebastian Ullrich]

Btw, it looks like you could have avoided the name concatenation with a open $id

[Calvin Lee]

did you try using :ident

oh I think that actually did it!
Also I did try open $id in... but it didn't seem to work, oh well

[Sebastian Ullrich]

Sebastian Ullrich said:

Ah, that looks like an issue with (stx)...

syntax myMatchAlt := "|" ident
syntax "enum" ident " where " myMatchAlt* : command
macro_rules
  | `(enum $id where $[| $ids:ident ]*) =>`(inductive $id where $[| $ids:ident ]*)

This is fixed now btw

[Andrew Kent]

@Calvin Lee Nice! :octopus: This is an awesome macro! I have thought several times about implementing something similar but have felt too busy or come up with other excuses, haha --- there's some embarrassing boilerplate in our code right now that basically manually creates an "enum" from an inductive type with all nullary constructors by mapping each constructor to a Nat to I can pretend they're an ordered/enumerable/etc type xD