The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

> 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