Stream: Coq devs & plugin devs

Topic: Binding a tactic in a Hint Extern


view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:04):

@Pierre-Marie Pédrot

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:05):

wit_tactic is not the right thing to pass to that function

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:07):

But how do I produce such a Val.t ?

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:07):

This is dark magic, I think.

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:07):

If not with Geninterp.Val.inject ?

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:08):

Yes and no, because what you want to do is evaluate the result, right?

view this post on Zulip Gaëtan Gilbert (Mar 25 2021 at 11:08):

how does Hint Extern 0 (P ?A) => bla A bind A?

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:08):

This is a pattern, you don't have to cross FFI boundaries.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:09):

wit != val

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:09):

That's how those are injected though, and I can see wit_constr there

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:09):

there are val attached to wit, but the mapping is not injective

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:10):

there is a val_tag function in the middle

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:10):

which returns the runtime tag attached to wit_constr

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:10):

Sure, I'm just saying I can't find a tag for my tactics

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:11):

I have to think a bit for the proper way to do this.

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:11):

Ok, I understand. Can I build a tag myself?

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:11):

Yes, but it won't work as a closure.

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:12):

Right, this seems not so easy to implement :)

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:12):

Ltac will fail saying something along the lines of "closure expected but found mytag"

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:12):

The normal way is to register global callbacks, but here you want arbitrary code

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:12):

You don't care about the return value, right?

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:13):

So you can hack something with dummy closure + TacML + ad-hoc value as arguments.

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:13):

Nope, it's always unit (I don't care about goal states or anything like that)

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:13):

there must be a handful of examples in the code doing that already

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:15):

It doesn't change the heart of the problem.

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:15):

You can take inspiration from Tacentries.ml_tactic_extend maybe

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:15):

Ok.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:15):

(creating a fresh tag)

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:16):

it unwraps the dyn value, and the ML code can do anything

view this post on Zulip 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)

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:18):

(both the tag creation / ML registration need to be global, beware)

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:18):

I see. We only need to declare once one such global interpretation tactic then?

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:18):

yup

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:18):

It just acts as a bridge to decode my new tagged values

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:19):

I wouldn't have access to tacentries anyway as I'm in typeclasses eauto, no?

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:19):

plugins/ltac comes after it, I believe

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:19):

probably not

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:20):

which is kind of problematic

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:20):

that means you're adding an Ltac hook into class_tactic hten

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:20):

I don't remember how we handle this

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:20):

Aren't extern hints arbitrary genargs?

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:20):

Yes

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:20):

They are

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:21):

OK, so you have to register an additional function for this in class_tactics

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:21):

the boilerplate goes into the Ltac plugin

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:23):

And then the rest is done in plugins/ltac

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:23):

no, you have to replace the interpetation function by something else

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:23):

remember, you're living in the runtime

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:24):

Look at Auto.conclPattern

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:24):

The interpretation function for what? Hint Extern genargs?

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:24):

there is a call to Geninterp.interp

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:25):

Yes

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:25):

so you get some dynamic runtime value

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:25):

you don't know anything about this

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:27):

(expect trouble with focussing also)

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:28):

Ah, no, indeed, this would work also...

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:29):

Either we apply, or we extend the environment, I was thinking the later would be easier

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:29):

yes, it's probably better

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:30):

but you'll have to do a bit of magic on the ltac side

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:31):

Yes, I understand that

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:31):

try and see

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:31):

Ok

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 11:31):

nothing is ever given in Ltac

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 11:33):

:)

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 12:44):

At least that's what looking at Tacarg suggests

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 12:44):

No no.

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 12:44):

You have to create a Val tag

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 12:45):

(if you need help we can have a quick visio)

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 12:45):

(but I need to make tea first)

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 12:51):

or do you want me to write a stub code?

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 13:07):

Almost done writing a stub

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 13:14):

Ok, now ?

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 13:15):

ok

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 13:15):

https://github.com/ppedrot/coq/tree/stub-auto-callback for the stub

view this post on Zulip Matthieu Sozeau (Mar 25 2021 at 14:14):

Thanks, it just works!

view this post on Zulip Guillaume Melquiond (Mar 25 2021 at 15:44):

There is something wrong with your pull request. It contains a bunch of unrelated commits.

view this post on Zulip Guillaume Melquiond (Mar 25 2021 at 15:45):

A merge or a rebase gone wrong perhaps?


Last updated: Oct 21 2021 at 21:03 UTC