Unexpanders: Book examples fail

Stream: metaprogramming / tactics

[Shreyas Srinivas]

Hello everyone,

I was struggling with errors with unexpanders after reading the "Pretty-Printing" chapter of the MPIL book and trying to apply them to my own simple language. Then I decided to try to the example language in the chapter of #mpil directly and I get the exact same type mismatch errors.

[Shreyas Srinivas]

Here's the book example annotated with my own comments marked ERROR

import Lean
open Lean Lean.Elab Term


declare_syntax_cat lang
syntax num   : lang
syntax ident : lang
syntax "let " ident " := " lang " in " lang: lang
syntax "[Lang| " lang "]" : term

inductive LangExpr
  | numConst : Nat → LangExpr
  | ident    : String → LangExpr
  | letE     : String → LangExpr → LangExpr → LangExpr

macro_rules
  | `([Lang| $x:num ]) => `(LangExpr.numConst $x)
  | `([Lang| $x:ident]) => `(LangExpr.ident $(Lean.quote (toString x.getId)))
  | `([Lang| let $x:ident := $v:lang in $b:lang]) => `(LangExpr.letE $(Lean.quote (toString x.getId)) [Lang| $v] [Lang| $b])

instance : Coe NumLit (TSyntax `lang) where
  coe s := ⟨s.raw⟩

instance : Coe Ident (TSyntax `lang) where
  coe s := ⟨s.raw⟩

-- LangExpr.letE "foo" (LangExpr.numConst 12)
--   (LangExpr.letE "bar" (LangExpr.ident "foo") (LangExpr.ident "foo")) : LangExpr
#check [Lang|
  let foo := 12 in
  let bar := foo in
  foo
]


@[app_unexpander LangExpr.numConst]
def unexpandNumConst : Unexpander
  | `(LangExpr.numConst $x:num) => `([Lang| $x]) -- ERROR: Big error here about type mismatch
  | _ => throw ()

@[app_unexpander LangExpr.ident]
def unexpandIdent : Unexpander
  | `(LangExpr.ident $x:str) =>               -- ERROR: Big error here about type mismatch
    let str := x.getString
    let name := mkIdent $ Name.mkSimple str
    `([Lang| $name])
  | _ => throw ()

@[app_unexpander LangExpr.letE]
def unexpandLet : Unexpander
  | `(LangExpr.letE $x:str [Lang| $v:lang] [Lang| $b:lang]) =>  -- ERROR: Big error here about type mismatch
    let str := x.getString
    let name := mkIdent $ Name.mkSimple str
    `([Lang| let $name := $v in $b])
  | _ => throw ()

-- [Lang| let foo := 12 in foo] : LangExpr
#check [Lang|
  let foo := 12 in foo
] --ERROR:  No unexpansion here ofc

[Shreyas Srinivas]

I have not touched unexpanders before. So I don't know whether (and if so then what) changed after this chapter was written.

[Shreyas Srinivas]

UPDATE: Found my mistake. All that was needed was open Lean.PrettyPrinter. But for some reason lean did not complain about the identifier not being there.