How to supply variables to with an ident elab?

Stream: general

[Fernando Chu]

In the code below, my intention is that the constructor Foo.Bar has type (x : Term) → Foo x, but because the elab also captures identifiers, the type is instead (x : Term) → Foo (Term.var "x").

import Lean

inductive Term : Type where
  | var : String → Term

section
open Lean Elab Meta

declare_syntax_cat term_cat
syntax:0 ident : term_cat

partial def elabTerm : Syntax → MetaM Expr
  | `(term_cat| $i:ident) => mkAppM ``Term.var #[mkStrLit i.getId.toString]
  | _ => throwUnsupportedSyntax

elab "⟪" e:term_cat "⟫" : term => elabTerm e
end

inductive Foo : Term → Type where
  | Bar : (x : Term) → Foo ⟪ x ⟫

#check Foo.Bar

What is the right way to get my intended type for Foo.Bar, while still using the new syntax? Maybe is there a way to escape elabTerm inside the definition?

[Aaron Liu]

So do you want the identifiers to be escaped or not? If the answer is "sometimes", then how is Lean supposed to know which ones get escaped and which ones don't?

[Edward van de Meent]

Sounds like the syntax needs some sort of unquoting

[Kyle Miller]

Could you clarify what you mean by (x : Term) → Foo (Term.var x)? Term.var expects a string, so this isn't type correct.

[Fernando Chu]

@Kyle Miller my bad, I meant (x : Term) -> Foo x.

[Fernando Chu]

Aaron Liu said:

So do you want the identifiers to be escaped or not? If the answer is "sometimes", then how is Lean supposed to know which ones get escaped and which ones don't?

I want to be able to decide which of these cases it should be, as Edward suggested I could just extend the syntax to make everything more explicit, but I was hoping that there was a builtin way to do this easily.

[Kyle Miller]

Are you going to need complicated elaboration, or will macros suffice?

import Lean

inductive Term : Type where
  | var : String → Term

section
open Lean Elab Meta

declare_syntax_cat term_cat
syntax:0 ident : term_cat

syntax "⟪" term_cat "⟫" : term

macro_rules
  | `(⟪ $i:ident ⟫) => `($i)

end

inductive Foo : Term → Type where
  | Bar : (x : Term) → Foo ⟪ x ⟫

[Kyle Miller]

Here's a more complicated example. (Note that syntax:0 for ident causes parsing issues. There's no need to specify a precedence here, and it defaults to a high-precedence, which is probably what you want.)

import Lean

inductive Term : Type where
  | var : String → Term
  | add : Term → Term → Term

section
open Lean Elab Meta

declare_syntax_cat term_cat
syntax ident : term_cat
syntax:65 term_cat:65 " + " term_cat:66 : term_cat

syntax "⟪" term_cat "⟫" : term

macro_rules
  | `(⟪ $i:ident ⟫) => `($i)
  | `(⟪ $t1:term_cat + $t2:term_cat ⟫) => `(Term.add ⟪ $t1 ⟫ ⟪ $t2 ⟫)

end

inductive Foo : Term → Type where
  | Bar : (x : Term) → Foo ⟪ x ⟫
  | Baz : (x y : Term) → Foo ⟪ x + y ⟫

#check Foo.Bar
-- Foo.Bar (x : Term) : Foo x
#check Foo.Baz
-- Foo.Baz (x y : Term) : Foo (x.add y)

[Fernando Chu]

I think I will need elaboration at some point :'( But I'll try to push the macros as far as I can go and then see precisely what goes wrong. Thanks a lot for the suggestion!