Unexpected token when pretty printing something

Stream: lean4

[xiao]

I defined a context to be a partial map from variables to natural numbers like the following.

inductive Context where
  | empty: Context
  | update: Context -> String -> Nat -> Context
  | merge: Context -> Context -> Context
  deriving Repr

I also wanted to add some customized syntax for it, so I did the following.

declare_syntax_cat context
syntax "[]": context
syntax term: context
syntax ident " : " term: context
syntax "[" term "]" " : " term: context
syntax context ", " context: context
syntax "[ctx| " context " ]": term

macro_rules
  | `([ctx| [] ]) => `(Context.empty)
  | `([ctx| $t:term ]) => `($t)
  | `([ctx| $x:ident : $n]) => `(
      Context.update .empty $(Lean.quote (toString x.getId)) $n
    )
  | `([ctx| [$x:term]: $n]) => `(Context.empty.update $x $n)
  | `([ctx| $c1, $c2 ]) => `(Context.merge [ctx| $c1] [ctx| $c2])

Here, [ctx| x: 0] is defined to be Context.empty.update "x" 0, while sometimes x may be some Lean term, so I defined an escape bracket, i.e. [ctx| [s]: 0] is Context.empty.update s 0`.

def s := "some_name"
#check [ctx| []] -- Context.empty
#check [ctx| x: 3, y: 4, [s]: 8] -- (Context.empty.update "x" 3).merge ((Context.empty.update "y" 4).merge (Context.empty.update s 8))

Certainly, I wanted to pretty print it, so I added the following unexpanders.

@[app_unexpander Context.empty]
def unexpandContext_empty: Lean.PrettyPrinter.Unexpander
  | `($_) => `([ctx| [] ])


@[app_unexpander Context.update]
def unexpandContext_update: Lean.PrettyPrinter.Unexpander
  | `($_ $_ $x:term $v) => `([ctx| [$x] : $v ])
  | _ => throw ()


@[app_unexpander Context.merge]
def unexpandContext_merge: Lean.PrettyPrinter.Unexpander
  | `($_ [ctx| $x] [ctx| $y]) => `([ctx| $x, $y ])
  | _ => throw ()

They worked well except that [ctx| x: 4] is pretty printed as [ctx| ["x"]: 4].

def s := "some_name"
#check [ctx| []]  -- [ctx| [] ]
#check [ctx| x: 3, y: 4, [s]: 8]  -- [ctx| ["x"] : 3, ["y"] : 4, [s] : 8 ]

I wanted it pretty-printed exactly as how I wrote it, i.e., [ctx|x: 4], so I changed the unexpandContext_update a little bit.

@[app_unexpander Context.update]
def unexpandContext_update: Lean.PrettyPrinter.Unexpander
  | `($_ $_ $x:str $v) =>
    let ident := Lean.mkIdent (Lean.Name.mkSimple x.getString)
    `([ctx| $ident : $v ])
  | `($_ $_ $x:term $v) => `([ctx| [$x] : $v ])
  | _ => throw ()

Then, Lean complained unexpected token ':'; expected ']' at the : of `([ctx| $ident : $v ]).

What's the reason for that and how can I fixe it? I was following the meta-programming book. The error still occurred when I changed the : to some other symbol.

[xiao]

You can find the code here.

[Robin Arnez]

You often need to be explicit about what syntax kind you have:

`([ctx| $ident:ident : $v ])

should work

[xiao]

Robin Arnez 发言道：

You often need to be explicit about what syntax kind you have:

`([ctx| $ident:ident : $v ])

should work

I see. It works. Thank you!.