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