Stream: Coq users

Topic: ltac2/ltac1 interop


view this post on Zulip Armaël Guéneau (Nov 21 2020 at 12:10):

I'm kind of stuck trying to write some ltac2 tactics while reusing ltac1 tactics from an existing codebase. Is any of these things possible?

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 13:08):

You have to go full CPS, as is the norm in Ltac1 (à la ring)

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 13:09):

that is, given a Ltac1 CPS-style constr, if you want to extract the result you can pass it a Ltac2 function setting a Ltac2 reference

view this post on Zulip Armaël Guéneau (Nov 21 2020 at 13:09):

ah, that, I tried, but couldn't get to work

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 13:10):

Well, if you have a simple use case I can try to have a look.

view this post on Zulip Armaël Guéneau (Nov 21 2020 at 13:10):

I couldn't figure how to thread the name to the reference through the ltac2 callback into the ltac1 quotation

view this post on Zulip Armaël Guéneau (Nov 21 2020 at 13:10):

alright, I'll put something together

view this post on Zulip Armaël Guéneau (Nov 21 2020 at 13:15):

    From Ltac2 Require Import Ltac2.
    From Ltac2 Require Import Option.

     Ltac tac cont :=
       match goal with |- ?x = _ => cont x end.

  Goal 0 = 1.
    let r := { contents := None } in
    let set_r (c: constr) := r.(contents) := Some(c) in
    ltac1:(set_r |- tac set_r) set_r. (* does not work: set_r is not a Ltac1.t *)

view this post on Zulip Armaël Guéneau (Nov 21 2020 at 13:15):

something like this? I'm not sure how to turn the ltac2 callback into a Ltac1.t

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 13:49):

So indeed, I don't know how to pass higher-order values across quotations, and as such I think it's an instance of https://github.com/coq/coq/issues/12871

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 13:50):

The problem with this kind of feature request is that the runtime of Ltac1 is literal madness, and I am unsure of how expose this to Ltac2 without breaking soundness.

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 13:51):

Returning values from Ltac1 is quite tricky in general...

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 13:53):

I wonder if a function abstract : (Ltac1.t -> Ltac1.t) -> Ltac1.t would be enough...

view this post on Zulip Armaël Guéneau (Nov 21 2020 at 13:53):

right, I was thinking about that

view this post on Zulip Armaël Guéneau (Nov 21 2020 at 13:54):

(Ltac1.t list -> Ltac1.t) -> Ltac1.t maybe?

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 13:54):

The comment in the issue is correct, that is there is an asymmetry between Ltac1 and Ltac2.

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 13:54):

Since Ltac1 is untyped you can wreak havoc there.

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 13:54):

@Armaël Guéneau nope, you need the arity.

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 13:55):

so, int -> (Ltac1.t list -> Ltac1.t) -> Ltac1.t

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 13:55):

where the size of the list is guaranteed to be the integer argument.

view this post on Zulip Armaël Guéneau (Nov 21 2020 at 13:55):

ah, right. I think that would be very useful already

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 13:55):

but that function can be derived from the other one.

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 13:56):

(I wouldn't go as far as saying that nested functions behave as expected in Ltac1, but it seems not totally unreasonable)

view this post on Zulip Armaël Guéneau (Nov 21 2020 at 13:57):

oh, right…

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 13:57):

I insist: the Ltac1 runtime is a hellish nightmare.

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 13:58):

But this abstraction functions seems reasonable enough. If it's enough for your need then I can write a PR (hopefully fixing the other issue as well).

view this post on Zulip Armaël Guéneau (Nov 21 2020 at 13:59):

yeah, it would be enough for me! if you can make a PR that'd be awesome

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 14:01):

Writing that function is easy, but guaranteeing that it will behave as expected is not a strong promise.

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 14:09):

Hm, I am pretty sure there was a similar hack written somewhere in the codebase but I can't find it again.

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 14:12):

Found it: it's Tacentries.ml_val_tactic_extend.

view this post on Zulip Paolo Giarrusso (Nov 21 2020 at 14:48):

Since Ltac1 is untyped you can wreak havoc there.

view this post on Zulip Paolo Giarrusso (Nov 21 2020 at 14:50):

@Pierre-Marie Pédrot if it were that simple, at least you'd have the research on gradual typing to draw on

view this post on Zulip Paolo Giarrusso (Nov 21 2020 at 14:51):

But that only deals with runtime type errors, not with global mutable state or whatnot

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 19:05):

See https://github.com/coq/coq/pull/13442.

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2020 at 19:05):

As usual with Ltac1, there are a lots of hoop jumping.


Last updated: Jan 27 2023 at 01:03 UTC