Antiquot Splice

Stream: lean4

[Marcus Rossel]

I'm not sure if this title makes sense.
I'm trying to write a command that transforms something of the form

my_cmd [a : Nat, b : String, c : Bool × Prop]

into

example : IgnoreMe → Type :=
  fun x => match x with
    | a => Nat
    | b => String
    | c => Bool × Prop

My problem is that I don't know how to do the splicing in the antiquotation:

declare_syntax_cat interface_var
syntax ident " : " term : interface_var

macro "my_cmd" "[" vars:interface_var,* "]" : command => do
  `(
    example : IgnoreMe → Type :=
      fun x => match x with ???
  )

Is there a way to use $[ ]* for this?

[Mario Carneiro]

declare_syntax_cat interface_var
syntax ident " : " term : interface_var

macro "my_cmd" "[" vars:interface_var,* "]" : command => do
  let args := vars.getElems.map fun
    | `(interface_var| $x:ident : $t) => (x, t)
    | _ => panic! ""
  let (lhs, rhs) := args.unzip
  `(
    example : IgnoreMe → Type :=
      fun x => match x with
      $[| $lhs => $rhs]*
  )

[Marcus Rossel]

I've run straight into the next thing I can't figure out :sweat_smile:
Let's say I was trying to build a command my_multi which gets a sequence of lists and then runs my_cmd on each one:

import Lean
open Lean Macro

declare_syntax_cat interface_var
syntax ident " : " term : interface_var

declare_syntax_cat interface_scheme
syntax "[" interface_var,* "]" : interface_scheme

def getInterfaceVarComponents : (TSyntax `interface_var) → MacroM (Ident × Term)
  | `(interface_var| $i:ident : $t) => return (i, t)
  | _ => throwUnsupported

def getInterfaceSchemeVars : (TSyntax `interface_scheme) → MacroM (Array $ TSyntax `interface_var)
  | `(interface_scheme| [ $vars,* ]) => return vars
  | _ => throwUnsupported

macro "my_cmd" scheme:interface_scheme : command => do
  let vars ← getInterfaceSchemeVars scheme
  let components ← vars.mapM getInterfaceVarComponents
  let ⟨ids, types⟩ := components.unzip
  `(
    example : IgnoreMe → Type :=
      fun x => match x with $[| $ids => $types]*
  )

macro "my_multi" schemes:interface_scheme* : command => do
  `($[my_cmd $schemes:interface_scheme]*) -- Error

Then the last line here gives me multiple errors, e.g. elaboration function for 'commandMy_cmd_' has not been implemented.
Is this Lean telling mean that my_cmd is not implemented?

[Gabriel Ebner]

That's an ugly (and old) part of the syntax system.

[Gabriel Ebner]

`(foo) is sadly heavily overloaded. It can either produce:

• A term quotation (i.e., of category term)
• A command quotation (i.e., of category command), or
• A command list quotation (i.e., mkNullNode of commands)

[Gabriel Ebner]

Many places that accept commands also accept these "command lists", but not everywhere. Notably the pretty printer crashes on these hacky command lists:

import Lean
open Lean PrettyPrinter Elab Command
elab "foo" : command => do
  logInfo <| ← liftCoreM do ppCommand (← `(#check 0 #check 0))
foo -- unknown constant 'null'

(even though the quotation has type Syntax.Command)

[Gabriel Ebner]

More relevant in your case here: the command list version explicitly does not come with an antiquotation (it uses many1NoAntiquot). So you can't write `($[command]*) , no matter what command it is.

[Gabriel Ebner]

With that in mind, the solution is clear: all you need to do is call mkNullNode yourself.

macro "my_multi" schemes:interface_scheme* : command =>
  return mkNullNode (← schemes.mapM (`(my_cmd $(·))))

[Marcus Rossel]

Gabriel Ebner said:

That's an ugly (and old) part of the syntax system.

Haha, thank you for the history lesson :heart:️