How is TacticM lifted to TermElabM?

Stream: metaprogramming / tactics

[nrs]

I'm trying to make a macro or elaborator that would produce the same term as does beta% clear% (by reduce x; exact x), so I'm trying to figure out how it is that a tactic block gets embedded within a term. Is there a coercion that lifts TacticM to TermElabM or something of the sort? Is there any place in source I should take a look at to further investigate the question?

[nrs]

looks like Term.Elab.Tactic.run is responsible for this

[Kyle Miller]

Was it not sufficient making a macro?

[nrs]

Kyle Miller said:

Was it not sufficient making a macro?

Was having a hard time using TSynx `Lean.Parser.Tactic.location to make ... => `(beta% clear% (by reduce $x; exact $x). Went to sleep straight after reading that you can make a coercion from term to that parser, will report back after testing this

[nrs]

hm even so, the problem with

syntax (name := reduce) "reduce%" term : term

@[macro reduce]
def reduceImpl : Macro
| `(reduce% $t:term) => `(beta% clear% (by reduce $t; exact $t))
| _ => Macro.throwUnsupported

seems to be that beta% and clear% are immediately elaborated within the syntax quotation, any clue how to prevent this? i.e. they need to be passed as literals instead (i think?)
edit: I think you can do this with the Syntax.mk... API

[Kyle Miller]

They're definitely not elaborated within the quotation, the issue is that reduce $t with t : Term is not syntax. In your other thread, you were using reduce at x

[Kyle Miller]

I'm also really not sure what clear% is meant to be doing here. Are you wanting to clear a variable, or is that a typo for clean%?

[Kyle Miller]

Anyway, without it, this is how you could make a macro:

macro "reduce%" t:term : term =>
  `(beta% (by have x := $t; reduce at x; exact x))

[nrs]

whoops yeah I meant %clean!

[nrs]

ah I see, thank you very much for taking the time!