How to call the declaration elaborator

Stream: lean4

[Simon Hudon]

Note: in the process of writing up this question, I found the answer but I think it was an interesting problem and I thought I'd share the problem and the solution here.

I'm defining a command syntax for opaque definitions. I'm defining the parser by calling the «def» parser and my elaborator begins calling the declaration elaborator on the (slightly massaged) syntax tree.

I get into a funny situation where the declaration elaborator fails when the definition has a non-atomic (e.g. foo.bar) name. However the Lean syntax does allow such definitions. Am I missing a step where the name has to be expanded?

#mwe

import Lean.Elab.Declaration

namespace Lean
namespace Parser
namespace Command

open Elab.Command

syntax (name := opaqueDef)
   declModifiers "opaque " «def» : command

@[commandElab opaqueDef]
def elabOpaqueDef : CommandElab := λ stx => do
  let mods := stx[0]
  let kw := stx[1]
  let «def» := stx[2]
  print_vars![«def».getKind, stx.getKind]
  let stx := stx.setArgs #[mods, «def»]
  Lean.Elab.Command.elabDeclaration stx

opaque def x := 3   -- works
def x.x := 3        -- works
opaque def x.y := 3 -- does not works
                    -- Error: atomic identifier expected 'x.y'

(solution coming in a moment)

[Simon Hudon]

There are two problems with the way my code just plainly calls elabDeclaration on my home made declaration syntax:

0. Minor problem: it does not set the kind of the node. elabDeclaration checks the kind to see which one of ``Lean.Parser.Command.«def» or ``Lean.Parser.Command.«instance» etc.

1. While elabDeclaration does handle namespace expansion, when it encounters a complex name, after it rewrites the syntax tree with the right constructs (a namespace command and a declaration with an atomic name), it calls elabCommand on it which starts the elaboration all over again. In my code, I rewrite the syntax tree to make it more digestible by elabDeclaration by removing the keyword opaque. That means that restarting the elaboration does not end up calling my own elaborator.

The consequence for the #mwe I showed is that, I created a syntax tree that I thought would be more digestible

[Simon Hudon]

Here is what the code snippet becomes:

Fixing namespace expansion

import Lean.Elab.Declaration

namespace Lean
namespace Parser
namespace Command

open Elab.Command

syntax (name := opaqueDef)
   declModifiers "opaque " «def» : command

def expandOpaqueDefNamespace? (stx : Syntax) : Option (Name × Syntax) :=
    let decl := stx[2]
    let k := decl.getKind
    match expandDeclIdNamespace? decl[1] with
    | some (ns, declId) => some (ns, stx.setArg 2 (decl.setArg 1 declId))
    | none              => none

@[commandElab opaqueDef]
def elabOpaqueDef : CommandElab := λ stx => do
  match expandOpaqueDefNamespace? stx with
  | some (ns, newStx) => do
    let ns := mkIdentFrom stx ns
    let newStx ← `(namespace $ns:ident $newStx end $ns:ident)
    withMacroExpansion stx newStx $ elabCommand newStx
  | none => do
    let mods := stx[0]
    let kw := stx[1]
    let «def» := stx[2]
    let stx' := stx.setArgs #[mods, «def»]
    elabMutualDef #[stx'] (getTerminationHints stx')

opaque def x := 3   -- works
def x.x := 3        -- works
opaque def x.y := 3 -- now works! Yay!

#check x -- x : Nat
#check x.x -- x.x : Nat
#check x.y -- x.y : Nat

Explanation

Instead of calling elabDeclaration, we call elabMutualDef after doing the namespace expansion, possibly restarting the elaboration as a result. We mimic the structure of elabDeclaration.

[Leonardo de Moura]

@Simon Hudon The key problem in your example is that you are constructing an invalid syntax tree at

  let stx := stx.setArgs #[mods, «def»]

If you create a proper declaration syntax object, everything works.

import Lean.Elab.Declaration

namespace Lean
namespace Parser
namespace Command

open Elab.Command

syntax (name := opaqueDef)
   declModifiers "opaque " «def» : command

@[commandElab opaqueDef]
def elabOpaqueDef : CommandElab := λ stx => do
  let mods  := stx[0]
  let kw    := stx[1]
  let «def» := stx[2]
  let stx   := mkNode ``Lean.Parser.Command.declaration #[mods, «def»]  -- <<< FIxed here
  Lean.Elab.Command.elabDeclaration stx

opaque def x := 3   -- works
def x.x := 3        -- works
opaque def x.y := 3 -- works

[Simon Hudon]

In this context, that's true but if I need to do something special during elaboration because of the opaque keyword, when elabDeclaration calls elabCommand, it will not see the opaque keyword anymore.

[Simon Hudon]

Addendum: ok, I see how to get around that. In hindsight, it looks like more fuss than was needed. Sorry about that

[Simon Hudon]

Thanks for your help!

[Gabriel Ebner]

@Simon Hudon you might be interested in https://github.com/leanprover-community/mathlib4/blob/89fab7c0c4b59709dbafe212a9e02261c73b7d09/Mathlib/Tactic/IrreducibleDef.lean

[Simon Hudon]

Nice! Thanks! My version does something similar and also transports the equations produced by the equation compiler. It does not register them as equations but they can still be useful

[Simon Hudon]

I'm also preparing a feature where writing:

opaque namespace MyOpaqueDef
...
end MyOpaqueDef

lets you write definitions in terms of your definition as if it was not opaque (as long as the types work out when you transport them)