I'd like to change the Hint Extern If
command to now take a self/continue
tactic argument. However to "inject" a unit Proofview.tactic
and bind it to the self
argument to interpret the rest of the tactic, I seem to need to refer to plugins/ltac's Tacarg.wit_tactic from the eauto/typeclasses eauto implementation. Doesn't this require moving Tacarg lower in the dependencies?
@Pierre-Marie Pédrot
wit_tactic is not the right thing to pass to that function
What you want to do is injecting an arbitrary OCaml value into an Ltac closure
So in any case you're living at the Val.t level, not the Genarg one.
But how do I produce such a Val.t ?
This is dark magic, I think.
If not with Geninterp.Val.inject
?
Yes and no, because what you want to do is evaluate the result, right?
how does Hint Extern 0 (P ?A) => bla A
bind A
?
This is a pattern, you don't have to cross FFI boundaries.
That's find, they are constrs so we already have the right wit:
let open Genarg in
let open Geninterp in
let inj c = match val_tag (topwit Stdarg.wit_constr) with
| Val.Base tag -> Val.Dyn (tag, c)
| _ -> assert false
in
wit != val
That's how those are injected though, and I can see wit_constr
there
there are val attached to wit, but the mapping is not injective
there is a val_tag function in the middle
which returns the runtime tag attached to wit_constr
Sure, I'm just saying I can't find a tag for my tactics
What I am saying is that it has nothing to do with wit because you're only living in the runtime.
I have to think a bit for the proper way to do this.
Ok, I understand. Can I build a tag myself?
Yes, but it won't work as a closure.
Right, this seems not so easy to implement :)
Ltac will fail saying something along the lines of "closure expected but found mytag"
The normal way is to register global callbacks, but here you want arbitrary code
You don't care about the return value, right?
So you can hack something with dummy closure + TacML + ad-hoc value as arguments.
Nope, it's always unit (I don't care about goal states or anything like that)
there must be a handful of examples in the code doing that already
Would it be easier / cleaner to assume that Hint Extern self is actually building a higher-order tactic ltac:(fun self => ...)
and use Ltac application instead?
It doesn't change the heart of the problem.
You can take inspiration from Tacentries.ml_tactic_extend maybe
Ok.
so the solution is the following : define a new Val.t that will hold the OCaml closure
(creating a fresh tag)
Register a global ML function to be passed to TacML, that expects one argument of that dynamic type
it unwraps the dyn value, and the ML code can do anything
Then pass this to the Hint Extern function as a dummy closure (see Tacinterp.Value.of_closure)
(both the tag creation / ML registration need to be global, beware)
I see. We only need to declare once one such global interpretation tactic then?
yup
It just acts as a bridge to decode my new tagged values
I am a bit surprised I didn't write this kind of boilerplate in tacentries
I wouldn't have access to tacentries anyway as I'm in typeclasses eauto, no?
plugins/ltac comes after it, I believe
probably not
which is kind of problematic
that means you're adding an Ltac hook into class_tactic hten
I don't remember how we handle this
Aren't extern hints arbitrary genargs?
Yes
They are
OK, so you have to register an additional function for this in class_tactics
the boilerplate goes into the Ltac plugin
You mean a forward reference in class tactics to inject the unit tactic
into the proper genarg?
And then the rest is done in plugins/ltac
no, you have to replace the interpetation function by something else
remember, you're living in the runtime
Look at Auto.conclPattern
The interpretation function for what? Hint Extern genargs?
there is a call to Geninterp.interp
Yes
so you get some dynamic runtime value
you don't know anything about this
so you need to register a table for dynamic types in Auto that provide a way to apply such a value to an arbitrary unit tactic
cause now you'd likely get what would correspond to an Ltac function of arity 1
(expect trouble with focussing also)
Oh ok, so you're saying I shouldn't use the ist
to bind self
, like is done for the pattern variables
Ah, no, indeed, this would work also...
Either we apply, or we extend the environment, I was thinking the later would be easier
yes, it's probably better
but you'll have to do a bit of magic on the ltac side
that is, self won't be an Ltac closure but an opaque type that needs to be wrapped off using a dedicated function.
So if in plugins/ltac I have a way to inject my unit tactic
into a Geninterp.Val.t
that is properly decoded, I should be fine
Yes, I understand that
try and see
Ok
nothing is ever given in Ltac
:)
I'm a bit confused, I need to create a genarg to be able to register an interpretation function, no?
At least that's what looking at Tacarg suggests
No no.
You have to create a Val tag
(if you need help we can have a quick visio)
(but I need to make tea first)
or do you want me to write a stub code?
Almost done writing a stub
Ok, now ?
ok
https://github.com/ppedrot/coq/tree/stub-auto-callback for the stub
Thanks, it just works!
There is something wrong with your pull request. It contains a bunch of unrelated commits.
A merge or a rebase gone wrong perhaps?
Last updated: Jun 05 2023 at 09:01 UTC