syntactic sugar for simple enumerated type definitions

Stream: new members

[Mark Aagaard]

I'm teaching a first-year course on logic and discrete math to computer engineers. I'd like to enable the students to write simple enumerated type definitions such as:

Typedef Ty1 := A1 | A2

and have this elaborate to:

inductive Ty1 where | A1 | A2
open Ty1

The issues I'm facing are:

1. Writing a macro for the | A1 | A2 expansion.
2. Writing a macro that expands to 2 commands (inductive and open)

For the | A1 | A2 expansion, I started with the simple case of just one constructor, (e.g., Typedef Ty1 := A1)

syntax "Typedef" ident " := " ident : command
macro_rules
  | `( Typedef $id:ident := $val1:ident ) => `( inductive $id where | $val1 )

This gives a syntax error just after $val1 of expected token. I get a similar message with multiple vals.

Any suggestions on how to write this macro?

For the second issue, is it possible to write a macro that expands to 2 commands?

-mark

[Aaron Liu]

It looks like the parser is expecting some docs#Lean.Parser.Command.declModifiers. It works if you annotate it.

syntax "Typedef" ident " := " ident : command
macro_rules
  | `( Typedef $id:ident := $val1:ident ) => `( inductive $id where | $val1:ident )

[Kyle Miller]

Mark Aagaard said:

For the second issue, is it possible to write a macro that expands to 2 commands?

Yes, you can put multiple commands into the `(...) syntax.

Or you can do something like

macro_rules
  | `( Typedef $id:ident := $val1:ident ) => do
    let cmd1 ← `(inductive $id where | $val1:ident )
    let cmd2 ← `(other command)
    return mkNullNode #[cmd1, cmd2]

This has the same effect. Null nodes can be processed by the command elaborator.

[Mark Aagaard]

Thanks, I didn't know that it was possible to put a declModifier on the rhs of a macro expansion.

Aaron- How did you identify that the parser was looking for a declModifier? Debugging macros is still more art than science for me.

-mark

[Aaron Liu]

Step 1

syntax "Typedef" ident " := " ident : command
macro_rules
  | `( Typedef $id:ident := $val1:ident ) => `( inductive $id where | $val1 /- expected token -/)

Step 2

syntax "Typedef" ident " := " ident : command
macro_rules
  | `( Typedef $id:ident := $val1:ident ) => `( inductive $id where | $val1 a /- i put a token -/)

Step 3

application type mismatch
  val1.raw
argument
  val1
has type
  Lean.TSyntax `ident : Type
but is expected to have type
  Lean.TSyntax `Lean.Parser.Command.declModifiers : Type

[Mark Aagaard]

Got it. Thanks!

[Kyle Miller]

Key tidbit: the lhs and rhs are both the same kind of syntax, known as syntax quotations. The quotations get interpreted in different ways depending on the context (e.g. as a pattern or as a value), but syntax quotations all have the same parsing rules.

[Aaron Liu]

Here's my attempt at making this.

import Lean

syntax "Typedef" ident ":=" sepBy(ident, "|") : command
macro_rules
  | `(Typedef $id := $[$vals]|*) => do
    let ctors ← vals.mapM fun val => `(Lean.Parser.Command.ctor| | $val:ident)
    `(inductive $id where $[$ctors]* open $id:ident)

[Kyle Miller]

Here's how you do it with a single syntax quotation:

macro_rules
  | `(Typedef $id:ident := $[$vals]|*) => do
    `(inductive $id where
        $[ | $vals:ident]*
      open $id:ident)

[Kyle Miller]

The syntax and macro_rules can also be done together using the macro command:

macro "Typedef" id:ident ":=" vals:sepBy(ident, "|") : command =>
  `(inductive $id where
      $[ | $vals:ident]*
    open $id:ident)