Constructing Syntax

Stream: lean4

[Dan Velleman]

If I'm writing a tactic and I want it to call an existing tactic, I know that I can use evalTactic for that. For example, to call the rewrite tactic I can use:

evalTactic (← `(tactic| rewrite [not_imp_not]))

But now suppose I have myid : Syntax, which is an identifier for a hypothesis, and I want to apply the rewrite tactic to that hypothesis. I thought I first I could write:

evalTactic (← `(tactic| rewrite [not_imp_not] at $myid))

but that doesn't work. After studying the syntax for locations, I eventually determined that this works:

let mylocHyp := mkNode ``Parser.Tactic.locationHyp #[mkNode nullKind #[myid], mkNode nullKind #[]]
evalTactic (← `(tactic| rewrite [not_imp_not] at $mylocHyp))

But there must be an easier way that doesn't require getting so far into the details of how various kinds of Syntax are defined. Is there a better way to do this?

[Arthur Paulino]

I've thought about this in the past and the best solution I could think of was that we could have helpers to create terms of Syntax, like we do for terms of Expr

[Mario Carneiro]

you can usually get syntax quotations to do it. Does $myid:ident not work?

[Dan Velleman]

Thanks Mario. Yes, $myid:ident works, although I don't understand why. I don't think I really know what

← `( ...)

does.

[Mario Carneiro]

When you write something like ← `(tactic| rewrite [not_imp_not] at $myid), it is somewhat ambiguous what syntactic category $myid could live in. This is not a problem when you have an actual piece of syntax there like x but when it is an antiquotation it could be any subtree, and I think that the default behavior of an unadorned antiquotation is to be the largest subtree that would fit there, meaning in this case that it is the locationHyp, i.e. the piece corresponding to x y |-

[Mario Carneiro]

Using $stx:ident is saying "parse this as if it was an identifier", which ensures that the constructed locationHyp is of the form x or y or h rather than h1 h2 or h |-