Armaël Guéneau (Nov 21 2020 at 12:10): 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?
Pierre-Marie Pédrot (Nov 21 2020 at 13:08):You have to go full CPS, as is the norm in Ltac1 (à la ring)
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
Armaël Guéneau (Nov 21 2020 at 13:09):ah, that, I tried, but couldn't get to work
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.
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
Armaël Guéneau (Nov 21 2020 at 13:10):alright, I'll put something together
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 *)
something like this? I'm not sure how to turn the ltac2 callback into a Ltac1.t
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
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.
Pierre-Marie Pédrot (Nov 21 2020 at 13:51):Returning values from Ltac1 is quite tricky in general...
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...
Armaël Guéneau (Nov 21 2020 at 13:53):right, I was thinking about that
Armaël Guéneau (Nov 21 2020 at 13:54):(Ltac1.t list -> Ltac1.t) -> Ltac1.t maybe?
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.
Pierre-Marie Pédrot (Nov 21 2020 at 13:54):Since Ltac1 is untyped you can wreak havoc there.
Pierre-Marie Pédrot (Nov 21 2020 at 13:54):@Armaël Guéneau nope, you need the arity.
Pierre-Marie Pédrot (Nov 21 2020 at 13:55):so, int -> (Ltac1.t list -> Ltac1.t) -> Ltac1.t
Pierre-Marie Pédrot (Nov 21 2020 at 13:55):where the size of the list is guaranteed to be the integer argument.
Armaël Guéneau (Nov 21 2020 at 13:55):ah, right. I think that would be very useful already
Pierre-Marie Pédrot (Nov 21 2020 at 13:55):but that function can be derived from the other one.
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)
Armaël Guéneau (Nov 21 2020 at 13:57):oh, right…
Pierre-Marie Pédrot (Nov 21 2020 at 13:57):I insist: the Ltac1 runtime is a hellish nightmare.
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).
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
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.
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.
Pierre-Marie Pédrot (Nov 21 2020 at 14:12):Found it: it's Tacentries.ml_val_tactic_extend.
Paolo Giarrusso (Nov 21 2020 at 14:48):Since Ltac1 is untyped you can wreak havoc there.
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
Paolo Giarrusso (Nov 21 2020 at 14:51):But that only deals with runtime type errors, not with global mutable state or whatnot
Pierre-Marie Pédrot (Nov 21 2020 at 19:05):See https://github.com/coq/coq/pull/13442.
Pierre-Marie Pédrot (Nov 21 2020 at 19:05):As usual with Ltac1, there are a lots of hoop jumping.
Last updated: Oct 13 2024 at 01:02 UTC