Zulip Chat Archive

Stream: lean4

Topic: Inductive definition in macros


Calvin Lee (Mar 18 2021 at 17:32):

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 (Mar 18 2021 at 17:36):

You can create arbitrary syntax with a macro, including commands

Calvin Lee (Mar 18 2021 at 17:38):

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 (Mar 18 2021 at 17:44):

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 (Mar 18 2021 at 17:47):

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

Calvin Lee (Mar 18 2021 at 17:50):

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

Sebastian Ullrich (Mar 18 2021 at 17:50):

Exactly!

Calvin Lee (Mar 18 2021 at 18:00):

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 (Mar 18 2021 at 18:16):

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 (Mar 18 2021 at 20:13):

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 (Mar 18 2021 at 21:33):

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 (Mar 18 2021 at 21:42):

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

Calvin Lee (Mar 18 2021 at 21:49):

Ah, then the actual error message is unexpected syntax

Sebastian Ullrich (Mar 18 2021 at 21:50):

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

Calvin Lee (Mar 18 2021 at 21:53):

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 (Mar 18 2021 at 21:57):

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

Sebastian Ullrich (Mar 18 2021 at 21:59):

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

Calvin Lee (Mar 19 2021 at 01:17):

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 (Mar 19 2021 at 08:31):

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

#eval `a ++ `b

Calvin Lee (Mar 19 2021 at 17:15):

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

Sebastian Ullrich (Mar 19 2021 at 17:17):

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

Calvin Lee (Mar 19 2021 at 17:33):

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

Calvin Lee (Mar 19 2021 at 23:09):

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 (Mar 20 2021 at 09:08):

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 (Mar 20 2021 at 09:09):

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

Calvin Lee (Mar 20 2021 at 16:24):

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 (Mar 20 2021 at 17:24):

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 (Mar 20 2021 at 21:42):

@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


Last updated: Dec 20 2023 at 11:08 UTC