How can I prevent syntax from unfolding?

Stream: metaprogramming / tactics

[Syed Shaazib Tanvir]

I have declared some syntax syntax (name := state_expr) "{" state_decl,* "}" : term
This syntax works correctly in the source file but unfolds into its definition in the InfoView

example : (⟪ skip ⟫, {x ← 2, y ← 2}) ▷ {y ← 2, x ← 2}

becomes

(Program.skip, fun x =>
    (List.find? (fun y => x.ident == y.fst) [("y", Literal.nat 2), ("x", Literal.nat 2)]).elim (Value.nat 0) fun l =>
      l.snd.eval) ▷
  fun x =>
  (List.find? (fun y => x.ident == y.fst) [("y", Literal.nat 2), ("x", Literal.nat 2)]).elim (Value.nat 0) fun l =>
    l.snd.eval

Here's a MWE with a similar problem

syntax (name := evalExpr) "⟦" term ";" term "⟧" : term

macro_rules
  | `(⟦$a:term ; $b:term⟧) => `(Nat.add $a $b)

example : ⟦ 2; 3 ⟧ = 5 := by
  sorry

[František Silváši 🦉]

syntax does not automatically give you a pretty printer - it's only notation (and derivatives, like infix) that support this functionality.

You need to define a delaborator to tell lean how to turn the Expr back to Syntax for the user.

[Robin Arnez]

Well, Lean's elaboration pipeline looks like this:

$\text{String} \xrightarrow{\text{Parsers}} \text{Syntax} \xrightarrow{\text{Macros}} \text{Syntax} \xrightarrow{\text{Elaborators}} \text{Expr}$

and then what happens in the infoview is a similar process is reverse, called pretty-printing:

$\text{Expr} \xrightarrow{\text{Delaborators and unexpanders}} \text{Syntax} \xrightarrow{\text{Parenthesizers}} \text{Syntax} \xrightarrow{\text{Formatters}} \text{Format}$

where Syntax is docs#Lean.Syntax, the syntax tree macros and elaborators operate on, Expr is docs#Lean.Expr which is the raw tree of applications and lambda expressions (and some other stuff) and Format is docs#Std.Format, which is basically a string with indentation and line break information so it can print nicely at different line widths.

The problem here is that what the infoview shows comes after the part that expands all macros, so the infoview has no clue what macros were involved in the expression that shows up at the end. That's where delaborators and unexpanders come in though: They can look at the expression and turn it back into notation. The difference between delaborators and unexpanders here is that delaborators go directly from Expr to Syntax while unexpanders already take in Syntax and make it "prettier". For example the unexpander for Bool.not will take the syntax Bool.not a and turn it into the syntax !a. Now in your case, you're just using generic functions like List.find? and Nat.add which you maybe don't want to turn into your syntax in general, so you'd probably be better off using definitions:

def myAdd (a b : Nat) : Nat := a + b

notation "⟦ " a "; " b " ⟧" => myAdd a b

example : ⟦ 2; 3 ⟧ = 5 := by
  sorry -- shows ⟦ 2; 3 ⟧ = 5

what Lean does internally here is define the syntax, the macro expander and an unexpander:

def myAdd (a b : Nat) : Nat := a + b

syntax "⟦ " term "; " term " ⟧" : term

macro_rules
  | `(⟦$a:term ; $b:term⟧) => `(myAdd $a $b)

@[app_unexpander myAdd]
def unexpandMyAdd : Lean.PrettyPrinter.Unexpander := fun stx =>
  match stx with
  | `($_ $a $b) => `(⟦$a ; $b⟧)
  | _ => throw ()

example : ⟦ 2; 3 ⟧ = 5 := by
  sorry -- shows ⟦ 2; 3 ⟧ = 5

Now for your actual problem, you might need a more sophisticated unexpander and definition:

-- simplified definitions
inductive Literal where | nat (n : Nat)
inductive Value where | num (n : Nat)
structure Variable where ident : String
def Literal.eval : Literal → Value | .nat n => .num n

-- simplified syntax
syntax state_decl := ident " ← " num
syntax (name := state_expr) "{" state_decl,* "}" : term

def evalStateExpr (stateDecls : List (String × Literal)) : Variable → Value :=
  fun x => (List.find? (fun y => x.ident == y.fst) stateDecls).elim (Value.num 0)
    fun l => l.snd.eval

-- simplified macro
macro_rules
  | `({$[$x:ident ← $y:num],*}) =>
    let x := x.map fun ident => Lean.Syntax.mkStrLit ident.getId.toString
    `(evalStateExpr [$[($x:str, Literal.nat $y:num)],*])

-- run this with all the arguments pretty-printed if you see an application of `evalStateExpr`
@[app_unexpander evalStateExpr]
def unexpandEvalStateExpr : Lean.PrettyPrinter.Unexpander
  -- match an application of the form `something [("string", term), ...]`
  | `($_ [$[($x:str, $y:term)],*]) => do
    -- turn the strings into identifiers
    let x := x.map fun str => Lean.mkIdent (.mkStr1 str.getString)
    -- turn the literal terms back into literals, simplified from your actual case
    let y ← y.mapM fun term => do
      match term with
      | `(Literal.nat $n:num) => return n
      | _ => throw ()
    -- construct the final syntax
    `({$[$x:ident ← $y:num],*})
  | _ => throw () -- syntax is in the wrong shape, abort

#check {x ← 2, y ← 2} -- shows {x ← 2, y ← 2}

In case you're not sure what $[...],* means, it's a shorthand for matching on every element in the comma-separated list, producing an array for each of the results (so x becomes an array of string literals and y becomes an array of terms) or for constructing a comma-separated list with each element constructed by the quotation inside, taking in an array of each thing.

[Syed Shaazib Tanvir]

Thank You for this great explanation