From `syntax` to function

Stream: lean4

[Patrick Massot]

In the following code

import Lean

open Lean

declare_syntax_cat foo
syntax (name := foo.stx₁) term " foo " term : foo

def mkFooStx₁ (a b : Term) : CoreM (TSyntax `foo) :=
`(foo|$a:term foo $b:term)

Is there any way to automate the definition of mkFooStx₁ (or even better of a non-monadic version of it)? The syntax command does not seem to generate such a function.

[Eric Wieser]

Regarding the non-monadic version; if you write it as

def mkFooStx₁ {m} [Monad m] [MonadRef m] [MonadQuotation m] (a b : Term) : m (TSyntax `foo) :=
`(foo|$a:term foo $b:term)

then the caller can always escape the monadicity with Unhygienic.run

[Patrick Massot]

Do you mean

def mkFooStx₁' (a b : Term) : TSyntax `foo :=
Unhygienic.run (mkFooStx₁ a b)

[Patrick Massot]

What is this new magic trick?

[Adam Topaz]

It seems that Unhygienic is just some readerT monad on top of a state monad, and the instances Eric mentioned let you run such things in this monad. The direct non-monadic version works as well:

def mkFooStx₁ (a b : Term) : TSyntax `foo :=
  Unhygienic.run `(foo|$a:term foo $b:term)

this is a nice trick!

[Eric Wieser]

(deleted, I can't read)

[Kyle Miller]

"Unhygienic" means that it's not going to do anything to prevent name capture. If your syntax that you're creating doesn't have any binders, this is probably ok.

[Sebastian Ullrich]

See also its docstring https://leanprover-community.github.io/mathlib4_docs/Lean/Hygiene.html#Lean.Unhygienic

[Patrick Massot]

Thanks Sebastian. Do you see an easy way to autogenerate my function?

[Mario Carneiro]

Patrick Massot said:

The syntax command does not seem to generate such a function.

When you use macro or elab, it will actually generate the syntax for that quotation as part of the pattern. But these take slightly different input, viz. elab a:term " foo " b:term : foo instead of syntax term " foo " term : foo.

[Patrick Massot]

I don’t understand your message. Do you claim that elab creates the function I want?

[Sebastian Ullrich]

It does something similar, but not exactly what you want, no. And it is not an easy task unfortunately.

[Sebastian Ullrich]

Could you say a bit more about what advantages you see over using quotations directly? I can imagine some would like to hear more

[Patrick Massot]

The advantage is being more robust to irrelevant syntax changes. It is all in the context of my controlled natural language tactics. There I have syntax with lots of strings that could change but the actual parameters are much more stable.

[Patrick Massot]

Things like

elab "By " e:maybeApplied " we get " colGt news:newStuffEN : tactic => do
obtainTac (← maybeAppliedToTerm e) (newStuffENToArray news)

elab "By " e:maybeApplied " we choose " colGt news:newStuffEN : tactic => do
chooseTac (← maybeAppliedToTerm e) (newStuffENToArray news)

elab "By " e:maybeApplied " it suffices to prove " "that "? colGt arg:term : tactic => do
bySufficesTac (← maybeAppliedToTerm e) #[arg]

elab "By " e:maybeApplied " it suffices to prove " "that "? colGt "["args:term,*"]" : tactic => do
bySufficesTac (← maybeAppliedToTerm e) args.getElems

[Patrick Massot]

But this is not crucial. I can define those functions by hand, it simply feels a bit boiler plate-y.