metaprogramming: escape from elaborator

Stream: general

[Quinn]

I have an aggressive elaborator that coerces identifiers to strings, which makes sense for my usecase but is leading to heartbreak when I try to prepend the type/syntax category i'm elaborating with a quantified variable. This is a minimal reproducer

import Lean

open Lean Elab Meta

def Env : Type := String → Int
def Assertion : Type := Env → Prop
def Assert (assertion : Assertion) (σ : Env) : Prop := assertion σ

declare_syntax_cat assertion
syntax ident "=" num : assertion
syntax ident "=" ident : assertion
@[simp] def strIntEq (x : String) (y : Int) : Assertion := fun σ => σ x = y
@[simp] def strStrEq (x y : String) : Assertion := fun σ => σ x = σ y
def elabAssertionLit : Syntax → MetaM Expr
  | `(assertion| $x:ident = $n:num) => do
    let x <- pure $ mkStrLit x.getId.toString
    let n <- pure $ mkIntLit n.getNat
    mkAppM ``strIntEq  #[x, n]
  | `(assertion| $x:ident = $y:ident) => do
    let x <- pure $ mkStrLit x.getId.toString
    let y <- pure $ mkStrLit y.getId.toString
    mkAppM ``strStrEq #[x, y]
  | _ => throwUnsupportedSyntax
elab "astn " a:assertion : term => elabAssertionLit a

#reduce astn x = 2 -- good
-- Want: escape
#reduce forall (n : Int), Assert (astn n = x) (fun s => if s == "x" then 1 else 0) --bad: "unused variable: `n`"
-- I would like to be able to say `forall n, Assert (astn ~n = x) σ`, where the `~` _escapes_ to the quantified Int instead of getting interpreted as a string

I desire to figure out the escape, as i think the aggressive elaborator is right for most of my needed functionality

[Kyle Miller]

You can add ~term as additional syntax. I broke your syntax up into an assertionTerm category to reduce the number of cases to make. With a bit more effort, you could simplify elabAssertionLit by having some assertionTerm elaborator.

import Lean

open Lean Elab Meta

def Env : Type := String → Int
def Assertion : Type := Env → Prop
def Assert (assertion : Assertion) (σ : Env) : Prop := assertion σ

declare_syntax_cat assertionTerm
syntax ident : assertionTerm
syntax num : assertionTerm
syntax "~" term:max : assertionTerm
declare_syntax_cat assertion
syntax assertionTerm "=" assertionTerm : assertion

@[simp] def strIntEq (x : String) (y : Int) : Assertion := fun σ => σ x = y
@[simp] def strStrEq (x y : String) : Assertion := fun σ => σ x = σ y
@[simp] def strIntEqStr (x : Int) (y : String) : Assertion := fun σ => x = σ y
def elabAssertionLit : Syntax → TermElabM Expr
  | `(assertion| $x:ident = $n:num) => do
    let x <- pure $ mkStrLit x.getId.toString
    let n <- pure $ mkIntLit n.getNat
    mkAppM ``strIntEq  #[x, n]
  | `(assertion| $x:ident = $y:ident) => do
    let x <- pure $ mkStrLit x.getId.toString
    let y <- pure $ mkStrLit y.getId.toString
    mkAppM ``strStrEq #[x, y]
  | `(assertion| ~$t:term = $y:ident) => do
    let x <- Term.elabTermEnsuringType t (some <| .const ``Int [])
    let y <- pure $ mkStrLit y.getId.toString
    mkAppM ``strIntEqStr #[x, y]
  | _ => throwUnsupportedSyntax
elab "astn " a:assertion : term => elabAssertionLit a

#reduce astn x = 2
#reduce forall (n : Int), Assert (astn ~n = x) (fun s => if s == "x" then 1 else 0)

[Quinn]

woah thanks a ton! i'll take a look. During the meanwhile i cooked up this

  | `(assertion| $n:num != $x:ident) => do
    let n <- pure $ mkIntLit n.getNat
    let localDecls ← getLCtx
    match localDecls.findFromUserName? x.getId with
    | some decl =>
      let x <- pure $ decl.toExpr
      mkAppM ``valValNe #[x, n]
    | none =>
      let x <- pure $ mkStrLit x.getId.toString
      mkAppM ``strValNe  #[x, n]

which got me a lot closer, but yours is probably better

[Quinn]

heck yeah! got the exact right functionality from your suggestion.

[Quinn]

i'm disappointed that mkAppM doesn't accept a quoted lambda, like \\`(fun x y => x + y). forcing me to define def plus ... outside of scope (for some reason it also didn't allow the use of a local let`)

[Kyle Miller]

It looks like you could implement all of this with a macro rather than an elaborator.

The mkAppM function is rather low-level. You can also construct syntax using syntax quotations and pass it to elabTerm instead, which is more flexible (and sort of like making a macro from within an elaborator).

Re why not using a local let, when metaprogramming you have to think about what exists when and what representations they have. The mkAppM function creates an Expr by looking at the type of a constant, then creates an application of that constant. With a local let, that only exists at elaboration time and it's thrown away. (And at runtime it's an actual value, not an expression.) Theoretically one could write something to extract a let binding and turn it into an Expr, but that's not something mkAppM could do.