Auxiliary information for delaboration

Stream: metaprogramming / tactics

[Sergei Stepanenko]

Hi! I'm working with an embedding of a programming language with binders. The variables in this language are abstract. However, for readability purposes, I want to store concrete names somewhere to use them during delaboration.

What are the options for that? My current solution is wrong, because it breaks the abstraction:

MWE

import Lean
import Qq

inductive Expr : Type u → Type (u + 1)
| unit : {X : Type u} → Expr X
| var : {X : Type u} → Lean.Name → X → Expr X
| lam : {X : Type u} → Lean.Name → Expr (Option X) → Expr X
| app : {X : Type u} → Expr X → Expr X → Expr X

open Expr

declare_syntax_cat term_lang
syntax "⊤" : term_lang
syntax "(" term_lang ")" : term_lang
syntax ident : term_lang
syntax "λ " ident " . " term_lang : term_lang
syntax term_lang term_lang : term_lang

section Elab
  open Lean Elab Meta PrettyPrinter Delaborator SubExpr Qq

  abbrev ElabCtx := Vector Name

  def getIdx? (ctx : ElabCtx n) (name : Name) : Option (Fin n) :=
    Vector.finIdxOf? (Vector.reverse ctx) name

  abbrev TmElabM n := ReaderT (ElabCtx n) TermElabM

  def TmElabM.run {n} (Γ : ElabCtx n)
    (x : TmElabM n α) : TermElabM α :=
    ReaderT.run x Γ

  def getTmCtx (n : Nat) : TmElabM n (ElabCtx n) :=
    read

  def constructDom (T : Type u) (n : Nat) : Type u :=
    match n with
    | 0 => T
    | .succ n => Option (constructDom T n)

  def constructVar (n : Nat) (m : Fin n) (T : Type u) : constructDom T n :=
    match n with
    | 0 => Fin.elim0 m
    | .succ n => Fin.induction none (fun p _ => some (constructVar n p T)) m

  def quoteName (name : Name) : Q(Name) := q($name)

  partial def elabTM (l : Level) (n : Nat)
    (Γ : Q(Type l))
    : TSyntax `term_lang →
    TmElabM n Q(Expr $Γ)
    | `(term_lang| ($t:term_lang)) =>
      elabTM l n Γ t
    | `(term_lang| ⊤ ) => do
      return q(Expr.unit)
    | `(term_lang| $id:ident) => do
      let p := id.getId
      let Ψ ← getTmCtx n
      let R ← Qq.mkFreshExprMVarQ (q(Type l))
      let p' := quoteName p
      if let some m := getIdx? Ψ p then
        let Γ' := q(constructDom $R $n)
        let ⟨_⟩ ← assertDefEqQ (u := l) Γ Γ'
        let v := q(constructVar $n $m $R)
        return q(Expr.var $p' $v)
      else
        throwError "Unbound variable used: {id}"
    | `(term_lang| λ $id:ident . $t:term_lang) => do
      let id := id.getId
      let p' := quoteName id
      let m ← getTmCtx n
      let e ← (elabTM l (n + 1) q(Option $Γ) t).run (m.push id)
      return q(Expr.lam $p' $e)
    | `(term_lang| $t:term_lang $e:term_lang) => do
      let a ← elabTM l n Γ t
      let b ← elabTM l n Γ e
      return q(Expr.app $a $b)
    | _ => throwUnsupportedSyntax

  elab "⟪" t:term_lang "⟫" : term => do
    let u ← mkFreshLevelMVar
    let R ← Qq.mkFreshExprMVarQ (q(Type u))
    let T ← elabTM u 0 R t |>.run (Vector.ofFn (fun i => Fin.elim0 i))
    reduce T

  @[delab app.Expr.unit]
  def delabUnit : Delab := do
    `(⟪ ⊤ ⟫)

  @[delab app.Expr.var]
  def delabVar : Delab := do
    let e ← getExpr
    guard $ e.isAppOfArity' `Expr.var 3
    let P := mkIdent (e.getArg! 1).name?.get!
    `(⟪ $P:ident ⟫)

  @[delab app.Expr.app]
  def delabApp : Delab := do
    let e ← getExpr
    guard $ e.isAppOfArity' `Expr.app 3
    match ← delab (e.getArg! 1), ← delab (e.getArg! 2) with
    | `(⟪$x⟫), `(⟪$y⟫) => `(⟪$x $y⟫)
    | _, _ => failure

  @[delab app.Expr.lam]
  def delabLam : Delab := do
    let e ← getExpr
    guard $ e.isAppOfArity' `Expr.lam 3
    let P := mkIdent (e.getArg! 1).name?.get!
    match ← delab (e.getArg! 2) with
    | `(⟪$x⟫) => `(⟪ λ $P . $x:term_lang ⟫)
    | _ => failure
end Elab

def someterm : Expr Empty := ⟪ λ y. y ⟫

theorem test : ⟪λ x. x⟫ = someterm := by
  unfold someterm
  congr
  . sorry
  . sorry

Is it possible to make Lean.Name to be irrelevant, but still use it for delaboration? I guess, one possible solution is to construct terms manually, and insert mdata for lambdas and variables, but probably there is something better.

[Sergei Stepanenko]

Probably not the best solution, but I ended up just attaching mdata to places where I need to save variable names and writing delaborators for certain keys.

import Lean
import Qq

inductive Expr : Type u → Type (u + 1)
| unit : {X : Type u} → Expr X
| var : {X : Type u} → X → Expr X
| lam : {X : Type u} → Expr (Option X) → Expr X
| app : {X : Type u} → Expr X → Expr X → Expr X

open Expr

declare_syntax_cat term_lang
syntax "⊤" : term_lang
syntax "(" term_lang ")" : term_lang
syntax ident : term_lang
syntax "λ " ident " . " term_lang : term_lang
syntax term_lang term_lang : term_lang

section Elab
  open Lean Elab Meta PrettyPrinter Delaborator SubExpr Qq

  abbrev ElabCtx := Vector Name

  def getIdx? (ctx : ElabCtx n) (name : Name) : Option (Fin n) :=
    Vector.finIdxOf? (Vector.reverse ctx) name

  abbrev TmElabM n := ReaderT (ElabCtx n) TermElabM

  def TmElabM.run {n} (Γ : ElabCtx n)
    (x : TmElabM n α) : TermElabM α :=
    ReaderT.run x Γ

  def getTmCtx (n : Nat) : TmElabM n (ElabCtx n) :=
    read

  def constructDom (T : Type u) (n : Nat) : Type u :=
    match n with
    | 0 => T
    | .succ n => Option (constructDom T n)

  def constructVar (n : Nat) (m : Fin n) (T : Type u) : constructDom T n :=
    match n with
    | 0 => Fin.elim0 m
    | .succ n => Fin.induction none (fun p _ => some (constructVar n p T)) m

  def quoteName (name : Name) : Q(Name) := q($name)

  partial def elabTM (l : Level) (n : Nat) (Γ : Q(Type l))
    : TSyntax `term_lang →
    TmElabM n Q(Expr $Γ)
    | `(term_lang| ($t:term_lang)) =>
      elabTM l n Γ t
    | `(term_lang| ⊤ ) => do
      return q(Expr.unit)
    | `(term_lang| $id:ident) => do
      let id := id.getId
      let Ψ ← getTmCtx n
      let R := q(PEmpty.{l + 1})
      if let some m := getIdx? Ψ id then
        let Γ' := q(constructDom $R $n)
        let ⟨_⟩ ← assertDefEqQ (u := l) Γ Γ'
        let v := q(constructVar $n $m $R)
        return Expr.mdata (MData.empty.insert `Var (DataValue.ofName id)) q(Expr.var $v)
      else
        throwError "Unbound variable used: {id}"
    | `(term_lang| λ $id:ident . $t:term_lang) => do
      let id := id.getId
      let m ← getTmCtx n
      let e ← (elabTM l (n + 1) q(Option $Γ) t).run (m.push id)
      return Expr.mdata (MData.empty.insert `Binder (DataValue.ofName id)) q(Expr.lam $e)
    | `(term_lang| $t:term_lang $e:term_lang) => do
      let a ← elabTM l n Γ t
      let b ← elabTM l n Γ e
      return q(Expr.app $a $b)
    | _ => throwUnsupportedSyntax

  elab "⟪" t:term_lang "⟫" : term => do
    let u ← mkFreshLevelMVar
    let R ← Qq.mkFreshExprMVarQ (q(Type u))
    let T ← elabTM u 0 R t |>.run (Vector.ofFn (fun i => Fin.elim0 i))
    pure T

  @[delab app.Expr.unit]
  def delabUnit : Delab := do
    `(⟪ ⊤ ⟫)

  @[delab app.Expr.app]
  def delabApp : Delab := do
    let e ← getExpr
    guard $ e.isAppOfArity' `Expr.app 3
    match ← delab (e.getArg! 1), ← delab (e.getArg! 2) with
    | `(⟪$x:term_lang⟫), `(⟪$y:term_lang⟫) => `(⟪$x $y⟫)
    | _, _ => failure

  @[delab mdata.Binder]
  def delabMDataLam : Delab := do
    let .mdata d e ← SubExpr.getExpr | failure
    let .some (.ofName x) := d.find `Binder | failure
    guard $ e.isAppOfArity' `Expr.lam 2
    let P := mkIdent x
    match ← delab (e.getArg! 2) with
    | `(⟪$x:term_lang⟫) => `(⟪ λ $P . $x:term_lang ⟫)
    | _ => failure

  @[delab mdata.Var]
  def delabMDataVar : Delab := do
    let .mdata d e ← SubExpr.getExpr | failure
    let .some (.ofName x) := d.find `Var | failure
    guard $ e.isAppOfArity' `Expr.var 2
    let P := mkIdent x
    `(⟪ $P:ident ⟫)

end Elab

def test1 := ⟪ λ y. y ⟫
def test2 := ⟪ λ x. x ⟫

example : test1 = test2 := by
  unfold test1 test2
  rfl

def test3 := ⟪ λ y. λ z. z ⟫
def test4 := ⟪ λ x. λ w. w ⟫

example : test3 = test4 := by
  unfold test3 test4
  rfl

[Robin Arnez]

What about using

inductive Expr : Type u → Type (u + 1)
  | unit : {X : Type u} → Expr X
  | var' : {X : Type u} → X → Expr X
  | lam' : {X : Type u} → Expr (Option X) → Expr X
  | app : {X : Type u} → Expr X → Expr X → Expr X

def Expr.var (_nm : Lean.Name) : X → Expr X := Expr.var'
def Expr.lam (_nm : Lean.Name) : Expr (Option X) → Expr X := Expr.lam'

and

  elab "⟪" t:term_lang "⟫" : term => do
    let u ← mkFreshLevelMVar
    let R ← Qq.mkFreshExprMVarQ (q(Type u))
    elabTM u 0 R t |>.run #v[]

with the old version?

[Sergei Stepanenko]

Robin Arnez said:

What about using

inductive Expr : Type u → Type (u + 1)
  | unit : {X : Type u} → Expr X
  | var' : {X : Type u} → X → Expr X
  | lam' : {X : Type u} → Expr (Option X) → Expr X
  | app : {X : Type u} → Expr X → Expr X → Expr X

def Expr.var (_nm : Lean.Name) : X → Expr X := Expr.var'
def Expr.lam (_nm : Lean.Name) : Expr (Option X) → Expr X := Expr.lam'

and

  elab "⟪" t:term_lang "⟫" : term => do
    let u ← mkFreshLevelMVar
    let R ← Qq.mkFreshExprMVarQ (q(Type u))
    elabTM u 0 R t |>.run #v[]

with the old version?

Thanks!
I think that is actually better!

I just started to learn about metaprogramming in Lean, so I might be wrong, but I didn't find any guarantees about mdata being preserved by tactics. On the other hand, here it is possible to provide some api, and seal Expr.var and Expr.lam, so there're no hidden conversions.

[Jannis Limperg]

Yes, mdata is completely unstable and even core tactics make no real effort to preserve it.