elaborator not declared even tho elaborator is declared

Stream: general

[Frederick Pu]

Hi,
I'm working through implmenting the do unchained paper, and the lean compiler seems to be saying that I haven't implemented an elaborator even though i did implment it.

Here's a mwe to reproduce the bug.

import Lean

declare_syntax_cat stmt
syntax "do'" stmt : term

syntax "d!" stmt : term
syntax term : stmt

-- (D1)
macro_rules | `(d! $t:term) => `(term| $t)

declare_syntax_cat expander
syntax "expand!" expander "in" stmt : stmt
syntax "return" : expander
syntax "return'" term : stmt

-- (1')
macro_rules | `(term| do' $s) => `(term| ExceptCpsT.runCatch (d! expand! return in $s))

-- (R1)
macro_rules
| `(stmt| expand! return in return' $e) => `(term| throw $e)

def f (n : Nat) : Nat := Id.run <| d! expand! return in return' 10
/-
elaboration function for 'termD!_' has not been implemented
  d! expand! return in return' 10
-/

[Sebastian Ullrich]

Macro expansion works top-down, so no rule is applicable at the given term. Nested macros need to be expanded recursively as in https://github.com/Kha/do-supplement/blob/master/Do/Basic.lean.

[Frederick Pu]

How come when I set it up like this I still get the same error?

import Lean

declare_syntax_cat stmt
syntax "do'" stmt : term

syntax "d!" stmt : term
syntax term : stmt

declare_syntax_cat expander
syntax "expand!" expander "in" stmt : stmt
syntax "return" : expander
syntax "return'" term : stmt


macro_rules
| `(stmt| expand! return in return' $e) => `(term| throw $e) -- (1')
| `(d! $t:term) => `(term| $t) -- (D1)

macro_rules
| `(term| do' $s) => `(term| ExceptCpsT.runCatch (d! expand! return in $s)) -- (R1)

def f (n : Nat) : Nat := Id.run <| d! expand! return in return' 10
/-
elaboration function for 'termD!_' has not been implemented
  d! expand! return in return' 10
-/

[Sebastian Ullrich]

The order of rules doesn't matter when there are no overlapping patterns. What I mean by top-down is that expansion starts of the root of the syntax tree but there is no rule that matches d! expand! ...

[Frederick Pu]

k thxs that makes a lot of sense.
Now i can get the elaboration to work but it won't recognize throw for some reason

open Lean
declare_syntax_cat stmt
syntax "do'" stmt : term

syntax "d!" stmt : term
syntax term : stmt

declare_syntax_cat expander
syntax "expand!" expander "in" stmt : stmt
syntax "return" : expander
syntax "return" term : stmt

-- helper function; see usage below
def expandStmt (s : TSyntax `stmt) : MacroM (TSyntax `stmt) := do
  let s' ← expandMacros s
  if s == s' then
    Macro.throwUnsupported
  else
    -- There is no static guarantee that `expandMacros` stays in the `stmt` category,
    -- but it is true for all our macros
    return TSyntax.mk s'

macro_rules
| `(d! $e:term) => `(term| $e)
| `(stmt| expand! return in return $e) => `(term| (throw $e)) -- (1')
| `(d! $t) => do
    -- fallback rule: try to expand abbreviation
    let t ← expandStmt t
    `(d! $t)

macro_rules
| `(term| do' $s) => `(term| ExceptCpsT.runCatch (d! expand! return in $s)) -- (R1)

def f (n : Nat) : Nat := Id.run <| d! expand! return in return 10

/-
  elaboration function for 'termD!_' has not been implemented
  d! throw✝ 10
-/

[Frederick Pu]

why is throw getting shadowed?

[Sebastian Ullrich]

Likely your rule 1' is creating an invalid syntax tree as it returns a term where a stmt is expected - while it is possible to embed the former into the latter, the former is not structurally a subset of the latter. `(stmt| throw $e) might work.

[Frederick Pu]

yeah that fixed it thanks.
now im getting
failed to synthesize instance MonadExcept ?m.10774 Id
what is an example of a monad that actually supports throw? would ExceptT Nat work?