The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

> In the same vein, I would be glad if a tactic such as ‘is_var' would not be a tactic but a function returning a boolean.

Ltac is_var_bool x := tryif is_var x then constr:(true) else constr:(false).

Does that work?  Otherwise:

Class is_var_bool {T} (x : T) := decide_is_var : bool.
Hint Extern 0 (is_var_bool ?x) => first [ is_var x; exact true | exact false ] : typeclass_instances.
Ltac is_var_bool x := constr:(_ : is_var_bool x).

On Wed, Sep 21, 2016, 5:01 AM Frédéric Besson <frederic.besson AT inria.fr> wrote:

> On 20 Sep 2016, at 16:41, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:
>
>
>
> On 20/09/2016 12:09, Frédéric Besson wrote:
>> I know that you can extend Ltac with a ml tactic. I am wondering
>> whether someone knows how to extend the *functional *language of Ltac
>> with a ml function. For instance, the ml function would perform some
>> computation over an argument Coq term and return another Coq term.
>
> It's not possible currently, because of the limitations of Ltac
> semantics (namely, the TacML node is evaluated by-value). I think we
> could hack around that by defining a generic argument whose
> interpretation function would precisely be the ML function you want to
> use, but this is reaaaaaally ugly. If you've got an urgent usecase, you
> can probably tell it on this list so we can help you.

I do not quite get why this would be that ugly.
Isn’t it something very similar to TACTIC EXTEND with a different return type?
My understanding of Ltac internals is probably still naive...
For my current usage, returning a constr would be sufficient — there might be other relevant cases.

For the urgency. On various occasions, I  have wished this feature.
I tend to write as much as possible functional Ltac code.
Yet, when Ltac  hits its limits, I would be glad to port the relevant pieces into OCaml.

In the same vein, I would be glad if a tactic such as ‘is_var' would not be a tactic but a function returning a boolean.

So, yes, if you can guide me through the relevant part of the code, I would like to give it a try.
BTW, if successful, would such an experiment have any chance of being eventually integrated ?

Anyway, your help would be greatly appreciated.

After a quite grep of the source tree, it seems that:
* tacexpr: there should be a new constructor e.g TacMLFUN
* tacinterp and tacintern seem to be responsible for the evaluation
  (I have no idea what kinds of terms are manipulated there.)
* Something should also happen in the parser? I have no idea where it is done...


Thanks in advance,
—
Frédéric