Antiquotations in Qq

Stream: lean4

[Eric Wieser]

Does Qq have antiquotations for expressions, or only free variables? This doesn't seem to work:

import Qq
import Mathlib.Data.Fin.Basic

open Qq

#check q(Fin $(2 + 1))

[Gabriel Ebner]

This works:

#check let n : Nat := 2 + 1; q(Fin $n)

Antiquotations are assumed to have type Q(_).

[Eric Wieser]

So is $(x) not the same as $x? Or is there a special rule above because n is a free variable of known type?

[Mario Carneiro]

the latter

[Eric Wieser]

Is this just a syntactic limitation, or are there good reasons to require it to use free variables?

[Eric Wieser]

Hmm, I'm still confused here:

import Qq
open scoped Qq

example (x : Nat) : Q(Nat) := q($x) -- ok
example (x : Nat) : Q(Nat) := q($(x)) -- ok
example (x : Nat) : Q(Nat) := q($((x))) -- error, type mismatch, got `Nat` expected `QQ _`

[Gabriel Ebner]

This is understandably confusing. $x is the same as $(x) (same syntax), but $((x)) is different (contains a parenthesis node). And quote4 transforms non-identifier antiquotations to let x' := (x); q($x').

[Eric Wieser]

What does quote4 do to identifiers? Is there a transformation toQ such that $(x) is equivalent to $(toQ x)?

[Eric Wieser]

(i.e. for when x : Nat)

[Gabriel Ebner]

The automatic toExpr is only applied to variables in the local context.

[Eric Wieser]

What I meant to ask is, can this be made to work?

example (x : ℕ) : Q(ℕ) := q($(Lean.toExpr x))

[Eric Wieser]

Or is Lean.toExpr the wrong function there?

[Eric Wieser]

Ah, q($((show Q(Nat) from Lean.toExpr x))) works

[Eric Wieser]

Do we have these functions?

def toTypeExprQ (α : Type u) [Lean.ToLevel.{u}] [Lean.ToExpr α] :
  Q(Sort $(Lean.toLevel.{u})) := Lean.toTypeExpr α

def toExprQ {α : Type u} [Lean.ToLevel.{u}] [Lean.ToExpr α] (x : α) :
  Q($(toTypeExprQ α)) := Lean.toExpr x

 -- works, but needs the :)
example (x : Nat) : Q(Nat) := q($((toExprQ x :)))

[Gabriel Ebner]

This works:

example (x : Nat) : Q(Nat) :=
  q($(@toExprQ _ (by exact inferInstance) _ x))

[Gabriel Ebner]

The ToLevel instances are obviously brittle, so I'd rather tend to a new ToExprQ Nat type class extending ToLevel.

[Eric Wieser]

#5952 contains the defs above, feel free to make the refactor you're suggesting

[Gabriel Ebner]

I've put in the refactor.