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?
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: Nov 29 2023 at 21:01 UTC