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 Ltac
s that return values (as long as they don't have side-effects); how do I do the same with ltac2?
I could try resorting to CPS but it seems to me that returning values ought to be possible somehow...
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
yeah we have a hack based on that. it seems to break with name mangling though and generally just seems unnecessary hacky...
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".
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
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
you mean in my PR?
does it work if you eta expand Ltac string_to_ident x := let f := ltac2:(...) in f x
?
oh I didnt realize this Ltac1.lambda
approach needs your PR, I thought it should already work
Looking forward to that MR landing then. :) but for now I guess we'll use the CPS approach in Iris.
Last updated: Oct 13 2024 at 01:02 UTC