writing a command to define (a family of) unexpanders

Stream: metaprogramming / tactics

[Chris Henson]

I have written a command that takes a bundled relation and a symbol to define notations, e.g. a ⭢ᵗ b or a ⭢ᶠ b. I would like to extend this to also defining a corresponding unexpander. Here is an mwe showing the issues I'm running into:

import Lean

open Lean Syntax Parser Command

structure ReductionSystem (Term : Type u) where
  Red : Term → Term → Prop

def rs_true : ReductionSystem Nat := ⟨fun _ _ => True⟩
def rs_false : ReductionSystem Nat := ⟨fun _ _ => False⟩

syntax "reduction_notation" ident notationItem : command
macro_rules
  | `(reduction_notation $rs $sym) =>
    `(notation:39 t " ⭢"$sym t' => (ReductionSystem.Red $rs) t t')

reduction_notation rs_true "ᵗ"
reduction_notation rs_false "ᶠ"

variable (m n : Nat)

/-- info: rs_true.Red m n : Prop -/
#guard_msgs in #check (m ⭢ᵗ n)

/-- info: rs_false.Red m n : Prop -/
#guard_msgs in #check (m ⭢ᶠ n)

-- this works individually
@[app_unexpander ReductionSystem.Red]
def rs_true_pp : PrettyPrinter.Unexpander := fun
  | `(ReductionSystem.Red rs_true $a $b) => `($a ⭢ᵗ $b)
  | _ => throw ()

@[app_unexpander ReductionSystem.Red]
def rs_false_pp : PrettyPrinter.Unexpander := fun
  | `(ReductionSystem.Red rs_false $a $b) => `($a ⭢ᶠ $b)
  | _ => throw ()

/-- info: m ⭢ᵗn : Prop -/
#guard_msgs in #check (m ⭢ᵗ n)

/-- info: m ⭢ᶠn : Prop -/
#guard_msgs in #check (m ⭢ᶠ n)

-- but I want a command that works with the notationItem used as a variable, here's what I tried
-- two problems here:
--   I don't know how to distinguish a nested antiquotation ($a and $b)
--   writing ⭢$sym tries to parse as the above notations (and if you remove them would still fail)
syntax "reduction_pp" ident notationItem : command
macro_rules
| `(reduction_pp $rs $sym) => do
  `(
    @[app_unexpander ReductionSystem.Red]
    def pp : PrettyPrinter.Unexpander := fun
      | `(ReductionSystem.Red $rs $a $b) => `($a ⭢$sym $b)
      | _ => throw ()
   )

reduction_pp rs_true "ᵗ"
reduction_pp rs_false "ᶠ"

I have the notion that it would be easier if I assembled the left and right hand sides of the match in the unexpander beforehand to avoid nested antiquotation, but I wasn't sure how to do this.

[Kyle Miller]

Conceptual question, do you mean to define a notation with ⭢ᵗ as an atom, or is the fact that m ⭢ ᵗ n parses ok?

notation doesn't support it, but if there were noWs between the two in the syntax then that would keep it from parsing if it has whitespace.

The notation command also requires that you give precedence levels to the terms that appear, since otherwise they default to max. I assume you want this to work like infix, in which case everything should have :39.

If you use notation3 from Mathlib, you get pretty printers for this for free:

import Lean
import Mathlib.Util.Notation3

open Lean Syntax Parser Command

structure ReductionSystem (Term : Type u) where
  Red : Term → Term → Prop

def rs_true : ReductionSystem Nat := ⟨fun _ _ => True⟩
def rs_false : ReductionSystem Nat := ⟨fun _ _ => False⟩

syntax "reduction_notation" ident str : command
macro_rules
  | `(reduction_notation $rs $sym) =>
    `(notation3:39 t:39 " ⭢" $sym:str t':39 => (ReductionSystem.Red $rs) t t')

reduction_notation rs_true "ᵗ "
reduction_notation rs_false "ᶠ "

variable (m n : Nat)

/-- info: m ⭢ᵗ n : Prop -/
#guard_msgs in #check (m ⭢ᵗ n)

/-- info: m ⭢ᶠ n : Prop -/
#guard_msgs in #check (m ⭢ᶠ n)

[Kyle Miller]

Here's a little improvement with the macro to get the pretty printing to have the right whitespace without needing to put it into the reduction_notation:

macro_rules
  | `(reduction_notation $rs $sym) => do
    let mut sym := sym
    unless sym.getString.endsWith " " do
      sym := Syntax.mkStrLit (sym.getString ++ " ")
    `(notation3:39 t:39 " ⭢" $sym:str t':39 => (ReductionSystem.Red $rs) t t')

reduction_notation rs_true "ᵗ"
reduction_notation rs_false "ᶠ"

[Kyle Miller]

Using unexpanders for this is unfortunately a bit problematic. The issue is that they match syntactically, so in ReductionSystem.Red rs_true m n, the rs_true might not refer to the constant you think it is. Or, if you switch namespaces, it might start pretty printing as SomeNS.rs_true, and the unexpander won't apply anymore.

[Chris Henson]

I see, thank you. I've not used notation3 before, that is helpful.

Can I ask though, if I did want to do this "manually" along the lines I started above, is it possible to have these nested antiquotations? My trying to do it that way came from seeing this example in LeanLTL that you linked to the other day. I didn't quite follow everything, but this seemed like what your antiquote function was helping to do? Where you have `($unexpandLHS) => $unexpandRHS, these include antiquotations, right?

[Kyle Miller]

Yes, I was just working out how to get this all to work using a slightly different scheme. Here are some nested antiquotations:

import Lean

open Lean Syntax Parser Command

structure ReductionSystem (Term : Type u) where
  Red : Term → Term → Prop

declare_syntax_cat reductionKind

syntax:39 (name := reductionArrowStx) term:39 " ⭢" noWs reductionKind ppSpace term:39 : term

syntax "reduction_notation" ident str : command
macro_rules
  | `(reduction_notation $rs $sym) => do
    let [(n, [])] ← Macro.resolveGlobalName rs.getId | Macro.throwErrorAt rs "could not resolve name"
    let redKind ← Macro.addMacroScope `redKind
    let redKindIdent := mkIdentFrom sym redKind
    `(syntax (name := $redKindIdent) $sym:str : reductionKind
      macro_rules (kind := $(mkIdent `reductionArrowStx))
      | `($$a:term ⭢$$k:reductionKind $$b:term) =>
        if k.raw.isOfKind $(quote redKind) then
          `(ReductionSystem.Red $(mkCIdentFrom rs n) $$a $$b)
        else
          Macro.throwUnsupported)


def rs_true : ReductionSystem Nat := ⟨fun _ _ => True⟩
def rs_false : ReductionSystem Nat := ⟨fun _ _ => False⟩

reduction_notation rs_true "ᵗ"
reduction_notation rs_false "ᶠ"

[Kyle Miller]

What you were running into with your unexpander is that each reduction notation defines its own arrow, with its own syntax kind, so you can't actually use quotations in that context.

Using a syntax category like this lets all the reduction arrows share the same syntax kind, but with different nodes at the reductionKind spot

[Kyle Miller]

(The resolveGlobalName isn't necessary yet, but its use will pop up when I add in the delaborator)

[Kyle Miller]

Got it:

import Lean

open Lean Syntax Parser Command

structure ReductionSystem (Term : Type u) where
  Red : Term → Term → Prop

declare_syntax_cat reductionKind

syntax:39 (name := reductionArrowStx) term:39 " ⭢" noWs reductionKind ppSpace term:39 : term

open Lean PrettyPrinter Delaborator SubExpr in
def delabReductionSystem (n : Name) (reduct : TSyntax `reductionKind) : Delab :=
  whenNotPPOption getPPExplicit <| whenPPOption getPPNotation do
    let e ← getExpr
    guard <| e.getAppNumArgs == 4
    let self := e.getArg! 1
    guard <| self.isConstOf n
    let a ← withAppFn <| withAppArg delab
    let b ← withAppArg delab
    `($a ⭢$reduct:reductionKind $b)

syntax "reduction_notation" ident str : command
macro_rules
  | `(reduction_notation $rs $sym) => do
    let [(n, [])] ← Macro.resolveGlobalName rs.getId | Macro.throwErrorAt rs "could not resolve name"
    let redKind ← Macro.addMacroScope `redKind
    let redKindIdent := mkIdentFrom sym redKind
    `(syntax (name := $redKindIdent) $sym:str : reductionKind
      macro_rules (kind := $(mkIdent `reductionArrowStx))
      | `($$a:term ⭢$$k:reductionKind $$b:term) =>
        if k.raw.isOfKind $(quote redKind) then
          `(ReductionSystem.Red $(mkCIdentFrom rs n) $$a $$b)
        else
          Macro.throwUnsupported
      @[app_delab $(mkIdent ``ReductionSystem.Red)]
      def delabReduction :=
        delabReductionSystem $(quote n) ⟨mkNode $(quote redKind) #[mkAtom .none $sym:str]⟩)

def rs_true : ReductionSystem Nat := ⟨fun _ _ => True⟩
def rs_false : ReductionSystem Nat := ⟨fun _ _ => False⟩

reduction_notation rs_true "ᵗ"
reduction_notation rs_false "ᶠ"

variable (m n : Nat)

/-- info: m ⭢ᵗ n : Prop -/
#guard_msgs in #check (m ⭢ᵗ n)

/-- info: m ⭢ᶠ n : Prop -/
#guard_msgs in #check (m ⭢ᶠ n)

[Kyle Miller]

That mkNode $(quote redKind) #[mkAtom .none $sym:str] hints at some of the difficulty here with creating syntax. The problem is that from within the macro, the syntax hasn't been run, so it can't be used to parse the rest of the quotation, so we have to create the node manually.

[Kyle Miller]

If you modify the delaborator like so

open Lean PrettyPrinter Delaborator SubExpr in
def delabReductionSystem (n : Name) (reduct : TSyntax `reductionKind) : Delab :=
  whenNotPPOption getPPExplicit <| whenPPOption getPPNotation do
    let e ← getExpr
    guard <| e.getAppNumArgs == 4
    let self := e.getArg! 1
    guard <| self.isConstOf n
    let a ← withAppFn <| withAppArg delab
    let b ← withAppArg delab
    -- Hack: treate `reduct` as a term and give it terminfo pointing to `self`
    let reduct : TSyntax `reductionKind := ⟨← withAppFn <| withAppFn <| withAppArg <| annotateTermInfo ⟨reduct.raw⟩ ⟩
    `($a ⭢$reduct:reductionKind $b)

then you also get hoverable reductionKinds in the pretty printed output:

image.png

[Chris Henson]

Yeah, I tried for a bit to figure out how to construct it manually since the errors hinted in that direction. Using a syntax category for the reduction arrow is also very helpful. Thanks again!

[Chris Henson]

Is it expected that these unexpanders would not work if there is a variable in the type of the ReductionSystem? For instance the following doesn't pretty print:

inductive Term (Var : Type)

variable {Var : Type}

def term_rel : ReductionSystem (Term Var) := ⟨λ _ _ ↦ True⟩

reduction_notation term_rel "β"

variable (a b : Term Var)

-- term_rel.Red a b : Prop
#check a ⭢β b

My guess was that this is because syntactically term_rel is @term_rel Var?

[Chris Henson]

Using notation3 works for this, so I suppose it is able to capture this case of implicit variables?

[Chris Henson]

I am looking at the notation3 source and trying to understand where this happens. I see in docs#Mathlib.Notation3.mkExprMatcher it mentions variables?

[Kyle Miller]

A big difference between notation and notation3 is that notation generates an unexpander (so a Syntax -> Syntax transformation for pretty printing) but notation3 generates a delaborator (so an Expr -> Syntax transformation). It elaborates the RHS of => to construct the Expr matcher. That matcher is generated in docs#exprToMatcher in particular.

With the macro I wrote earlier, the generated delaborator is looking for a plain constant (with isConstOf). Since term_rel elaborates to @term_rel Var, that's no longer a plain constant, but an application.

If you think that the head constant suffices to distinguish between different notations, you could change that line to guard <| self.getAppFn.isConstOf n I believe (didn't test it).

[Chris Henson]

That makes sense, thanks! I will likely just use notation3, but this has been a good exercise to understand unexpanders versus delaborators.