How can I fix "'antiquot' has not been implemented"?

Stream: metaprogramming / tactics

[Youngju Song]

In the below code:

def xxx: Q(ℕ) := q(42)
def yyy: ℕ := $(xxx)

I am basically expecting $(q(·)) to be an identity function - q turns program to data (string), and $ turns data (string) to program.
However, the second line gives me the following error:

elaboration function for 'term.pseudo.antiquot' has not been implemented
  $(xxx)

How can I fix this issue, or am I doing something wrong here?

[Kyle Miller]

Antiquotations are only allowed inside a quotation. (Note that Lean doesn't operate on strings, it operates on more complex data structures, like Syntax and Expr.)

It's possible to do compile-time evaluation and reflection of the result though.

[Kyle Miller]

import Mathlib.Data.Nat.Notation
import Mathlib.Tactic.Eval
import Qq
import Lean

open Qq
open Lean Elab

/--
`expr% t` evaluates `t` (which should yield an expression) and then yields that expression as the result.
-/
elab "expr% " t:term : term => do
  let e ← Term.withSynthesize <| Term.elabTermEnsuringType t q(Expr)
  unsafe Lean.Meta.evalExpr Expr q(Expr) e (safety := .unsafe)

def xxx: Q(ℕ) := q(42)
def yyy: ℕ := expr% xxx

#eval yyy
-- 42

[Kyle Miller]

I guess that can actually be implemented using a macro:

/--
`expr% t` evaluates `t` (which should yield an expression) and then inserts the result.
-/
macro "expr% " t:term : term => `(by_elab return $t)

This is to say that to "antiquote" an expression, you can write

def yyy: ℕ := by_elab return xxx

[Youngju Song]

Thank you for the answer, @Kyle Miller !

Antiquotations are only allowed inside a quotation.

I am no expert in metaprogramming, but in the literature of staged programming, it seems it is possible to splice a term without it needing to be inside a quotation. For exmaple, the first three paragraph of this paper describes "staged programming 101" example, where at the end they splice the term $(mpower 3 <<2>>) which is not inside the quotation.
Thus the question: is there a reason that splicing is only allowed inside a quotation? (just out of curiosity, not being critical) Maybe the core Lean4's quotation doesn't bring enough type information for this to work safely. But wouldn't it be possible in Qq?

It's possible to do compile-time evaluation and reflection of the result though.
I guess that can actually be implemented using a macro:

Thanks, this looks really cool! I will try them out!

[Kyle Miller]

I think you could define the $(...) syntax to be a macro for by_elab return xxx. It's just not done for whatever reason (possibly because such level-zero splicings are very infrequently done)

[Kyle Miller]

Lean doesn't have the guarantees given at the end of the first paragraph of the introduction of that paper:

language support for multi-stage programming often provides additional guarantees (e.g. that well-typed generating programs generate only well-scoped and well-typed code).

Qq helps with this though. With more work the above expr% syntax could try to ensure type correctness at elaboration time.

[Sebastian Ullrich]

I left open the possibility of top-level quotations when implementing the parser but never implemented the corresponding elaborator for lack of use cases. There's also some unclear details on whether it should e.g. support both pure and monadic values.

[Eric Wieser]

Should the elaborator be implemented to just emit an error message like "top level antiquots are not supported"?

[Youngju Song]

@Kyle Miller @Sebastian Ullrich @Eric Wieser Thank you for the explanations, that makes very much sense.