Macros that introduce non-level parameters

Stream: metaprogramming / tactics

[Anthony Vandikas]

The Type* macro in mathlib introduces a fresh level metavariable and then converts it to a parameter using Elab.Term.levelMVarToParam. Is there any way to achieve the same thing for normal (non-level) parameters?

For instance, I'd like to write a macro HOM* such that

def foo {Hom : HOM*} (x : Hom A B) := ...

expands to

def foo.{u} {Hom : Obj → Obj → Type u} (x : Hom A B) := ...

which then becomes (via autoImplicits)

def foo.{u} {Obj : Type v} {A B : Obj} {Hom : Obj → Obj → Type u} (x : Hom A B) := ...

so that I may avoid declaring Obj whenever possible. Such a thing might also be useful for implementing a crude version of RFC: reimplementing class abbrev #8279.

[Kyle Miller]

This works, so long as Obj isn't a constant that's already in scope:

macro "HOM*" : term => do
  let o := mkIdent `Obj
  `($o → $o → Type _)

example (hom : HOM*) : True := by
  /-
  Obj : Sort u_1
  hom : Obj → Obj → Type u_2
  ⊢ True
  -/
  sorry

[Kyle Miller]

The mkIdent prevents the identifier from being made hygienic, and autoImplicits checks to see that identifiers are not hygienic (I think because that's a proxy for "written by the user")

[Anthony Vandikas]

Thank you! This was exactly what I needed to proceed.

Aside, I needed the names to be unique as I sometimes need to deal with more than one HOM*. I achieved this by re-implementing this using the elab command and generating the names based off a global counter.

open Lean Elab.Term in
elab "HOM[*]" : term => do
  let e ← getEnv
  let n := objCounter.getState e
  setEnv (objCounter.setState e (n + 1))
  let o := mkIdent (.str .anonymous ("Obj" ++ n.toSubscriptString))
  elabTerm (←`($o → $o → Type _)) .none

In another file:

initialize objCounter : Lean.EnvExtension Nat ← Lean.registerEnvExtension (pure 0)

[Robin Arnez]

Do you need to refer to the name of the Obj? If yes then it feels like this is a bit weird (a global counter? won't that throw off everything if you add HOM[*] somewhere?), if no then ​`(Obj → Obj → Type*) would also do the trick

[Anthony Vandikas]

I don't need to refer to the name. When I do, I have an alternate macro HOM[Obj] which is just equivalent to Obj → Obj → Type*.

if no then ​`(Obj → Obj → Type*) would also do the trick

If I do that, I get unknown identifier 'Obj✝' at the use site.

[Robin Arnez]

I'm confused; you say you sometimes have more than one; how do you distinguish?

[Robin Arnez]

I mean at the use site; I suppose you won't just x : Obj_12754

[Robin Arnez]

Oh wait you mean that hygienic identifiers don't get auto-implicits? That might be the case

[Robin Arnez]

Hmm you're right it might not be as easy to make something like this if you don't do what you did

[Kyle Miller]

If you're using a term elaborator, then you have access to the local context, and you can avoid using a global counter by instead finding an unused name.

[Kyle Miller]

Robin Arnez said:

Oh wait you mean that hygienic identifiers don't get auto-implicits? That might be the case

Kyle Miller said:

autoImplicits checks to see that identifiers are not hygienic

In particular it checks that the name is an atomic string. (isValidAutoBoundImplicitName)