Feature: Ltac2 antiquotation shorthand for constr-producing expressions instead of only variables

[samuelgruetter]

The Ltac2 manual says:

In a Coq term, writing $x is semantically equivalent to ltac2:(Control.refine (fun () => x)), up to re-typechecking.

But why does x have to be a variable? I would find it useful if x could be any (parenthesized) Ltac2 expression of type constr, especially for cases where the surrounding Coq term is quite big, and the Ltac2 expression to be antiquoted is so small that creating a let-bindings far out for it makes code harder to read.

A potential reason for not implementing this would be to avoid having to make any decisions on the evaluation order, but it turns out that it has already been decided that the evaluation order is unspecified, according to the manual:

Relative orders of evaluation of antiquotations and quoted term are not specified.

So, in the already supported

constr:(some gallina code ltac2:(my first expr of type unit) more gallina ltac2:(my second expr of type unit))

I already don't know which of the Ltac2 expression is going to be evaluated first (which is fine for me), so it's not a problem if it's also unspecified in the proposed syntax

constr:(some gallina code $(my first expr of type constr) more gallina $(my second expr of type constr))

[SkySkimmer]

How would it work exactly? I guess we want to avoid generating an evar to use as goal since otherwse why not use ltac2:(). But then how do we get the context and expected type? Or is this only for when we don't care about them?

[samuelgruetter]

The use cases that I have in mind are antiquotations $e where e is of the shape myVerySimpleLtac2Func oneArgument, or myRecord.(fieldName), or other very simple constr-returning expressions that don't call Control.hyps or Control.goal. But indeed, in order to implement this feature, one needs to decide what Control.hyps and Control.goal would return when invoked inside such an antiquotation. Maybe just panicking (uncatchable failure) would be easiest? But as I said, it doesn't matter for my use cases.

[samuelgruetter]

However, Ltac2 functions that I'd like to call inside antiquotations might want to use constr:(...), which needs access to the context, so I would probably not be happy with an implementation that panics on Control.hyps.

[SkySkimmer]

Maybe we need a way to have gallina notations use the ltac2 entry? such that the user can write

Notation "${ e }" := (ltac2:(Control.refine (fun () => e))) (e ltac2).

Check ${ 'I } : True.