Stream: Ltac2

Topic: Pass value from ltac2 back to ltac1


view this post on Zulip Ralf Jung (May 02 2023 at 18:00):

I am trying to finally use the nice Ltac1.of_ident function to let us pass an ident from Ltac2 to Ltac1, and use it in an ltac1 script... but I can't figure out how to do that. I tried this:

  Ltac string_to_ident :=
    ltac2:(s1 |- let s := get_opt (Ltac1.to_constr s1) in
                 let ident := coq_string_to_ident s in
                 Ltac1.of_ident ident).

but this shows a warning since the expression does not have type unit. In pure ltac1 I can declare Ltacs that return values (as long as they don't have side-effects); how do I do the same with ltac2?

view this post on Zulip Ralf Jung (May 02 2023 at 18:04):

I could try resorting to CPS but it seems to me that returning values ought to be possible somehow...

view this post on Zulip Jason Gross (May 02 2023 at 18:26):

I'm not sure if this is directly possible, but you can pass a constr back to Ltac1 via constr:(ltac2:(... exact <thing>)) and you can embed an ident in a constr by making fun x : Prop => x (you can use Constr.Unsafe to embed the ident) and then you can pull out the ident as match ltac2:(... let v := Constr.Unsafe.make (Constr.Unsafe.Lambda ...) in exact $v) with fun name => _ => <use name> end or something

view this post on Zulip Ralf Jung (May 02 2023 at 19:32):

yeah we have a hack based on that. it seems to break with name mangling though and generally just seems unnecessary hacky...

view this post on Zulip Rodolphe Lepigre (May 02 2023 at 21:41):

You can't pass a value back to Ltac via an Ltac2 quotation in an Ltac expression. The documentation (see https://coq.inria.fr/refman/proof-engine/ltac2.html#ltac2-from-ltac1) says that the Ltac2 expression in the quotation is "expected to have type unit".

view this post on Zulip Gaëtan Gilbert (May 05 2023 at 14:12):

https://github.com/coq/coq/pull/17575 allows to return values
I'm not sure if we can make it work properly with ltac2:(x |- ...) but ltac2:(Ltac1.lambda (fun x => ...)) seems to work fine

view this post on Zulip Ralf Jung (May 09 2023 at 11:34):

hm, I am now trying

  Ltac string_to_ident :=
    ltac2:(Ltac1.lambda (fun s1 =>
      let s := get_opt (Ltac1.to_constr s1) in
      let ident := coq_string_to_ident s in
      Ltac1.of_ident ident
    )).

but that fails with Illegal tactic application: got 1 extra argument.
I am not getting a clear error location

view this post on Zulip Gaëtan Gilbert (May 09 2023 at 11:36):

you mean in my PR?
does it work if you eta expand Ltac string_to_ident x := let f := ltac2:(...) in f x?

view this post on Zulip Ralf Jung (May 09 2023 at 11:37):

oh I didnt realize this Ltac1.lambda approach needs your PR, I thought it should already work

view this post on Zulip Ralf Jung (May 09 2023 at 11:38):

Looking forward to that MR landing then. :) but for now I guess we'll use the CPS approach in Iris.


Last updated: Jul 13 2024 at 03:01 UTC