Philipp G. Haselwarter (May 11 2022 at 07:42): Philipp G. Haselwarter (May 11 2022 at 07:42):Hi, I have a constructor C taking a string argument "foo" in my goal, and essentially I want to perform set (foo := "foo"). Naturally I would try something like match goal with | |- context [ C ?foo_string ] => let x := fresh foo_string in set (x := C foo_string) end, but here foo_string is a gallina string, while fresh expects an identifier or an Ltac string (at least that's what the error message makes me think). Is there a conversion function?
Michael Soegtrop (May 11 2022 at 10:20):Ltac2 has a function to convert Ltac2 strings to identifiers here Ltac2-ident and it shouldn't be hard to create an Ltac2 string from a gallina string. I am not aware of an Ltac1 way to do this, but you can mix Ltac2 into Ltac1.
Michael Soegtrop (May 11 2022 at 10:24):For any serious automation I would anyway recommend Ltac2 - it is a bit terse in features especially in documentation, but Ltac2 tactics are much easier to maintain and grow because it is an ML like strictly typed language.
Philipp G. Haselwarter (May 11 2022 at 11:50):cheers Michael, that's what I ended up doing. It just seems like someone must already have written the boilerplate to convert gallina types to their ltac2 equivalent
Michael Soegtrop (May 11 2022 at 12:11):Philipp G. Haselwarter said:
cheers Michael, that's what I ended up doing. It just seems like someone must already have written the boilerplate to convert gallina types to their ltac2 equivalent
I have it for quite a few, but not for strings.
Philipp G. Haselwarter (May 11 2022 at 12:32):@Michael Soegtrop could you give me a pointer to one such, for reference?
Michael Soegtrop (May 11 2022 at 12:58):Nothing you can find online. Here is an example:
Ltac2 rec ltac_int_of_pos (p : constr) : int :=
let res :=lazy_match! p with
| xH => 1
| xO ?p' => Int.mul 2 (ltac_int_of_pos p')
| xI ?p' => Int.add (Int.mul 2 (ltac_int_of_pos p')) 1
end in
if Int.lt res 0
then throw_invalid_argument_sc "ltac_int_of_pos: value is too large: " p
else res.
Ltac2 ltac_int_of_Z (z : constr) : int :=
lazy_match! z with
| Z0 => 0
| Zpos ?p => ltac_int_of_pos p
| Zneg ?p => Int.sub 0 (ltac_int_of_pos p)
end.
The throw_invalid_argument_scis pre Ltac2-printf and requires a bit of boilerplate - I still need to write throw convenience functions with printf style parameters.
Philipp G. Haselwarter (May 11 2022 at 17:16):@Michael Soegtrop thank you, that was very useful. Here's what I came up with, where the notation $$ i stands for the constructor C I originally mentioned.
From Ltac2 Require Ltac2 Printf.
From Ltac2 Require String Char Fresh Ident.
From Coq Require Ascii.
Module jtac.
Import Ltac2.Ltac2 Ltac2.Printf.
Ltac2 rec ltac_int_of_pos (p : constr) : int :=
let res :=
lazy_match! p with
| xH => 1
| xO ?p' => Int.mul 2 (ltac_int_of_pos p')
| xI ?p' => Int.add (Int.mul 2 (ltac_int_of_pos p')) 1
end in
if Int.lt res 0
then Control.throw (Out_of_bounds (Some (fprintf "ltac_int_of_pos: value is too large: %t" p)))
else res.
Ltac2 ltac_int_of_Z (z : constr) : int :=
lazy_match! z with
| Z0 => 0
| Zpos ?p => ltac_int_of_pos p
| Zneg ?p => Int.sub 0 (ltac_int_of_pos p)
end.
Ltac2 ltac_char_of_ascii (c : constr) : char :=
let c := constr:(Z.of_nat (Ascii.nat_of_ascii $c)) in
let c := eval cbv in $c in
Char.of_int (ltac_int_of_Z c).
Ltac2 ltac_string_of_string (s : constr) : string :=
let s := eval cbv in $s in
let rec ltac_copy_to_string (s : constr) (out : string) (i : int) : unit :=
lazy_match! s with
| EmptyString => ()
| String ?c ?s => String.set out i (ltac_char_of_ascii c) ;
ltac_copy_to_string s out (Int.add i 1)
end
in
let len := constr:(Z.of_nat (String.length $s)) in
let len := eval cbv in $len in
let out := String.make (ltac_int_of_Z len) (Char.of_int 0) in
ltac_copy_to_string s out 0 ;
out.
Ltac2 base_length (s : string) : int :=
let full_stop := 46 in
let n := String.length s in
let rec f i len_ext :=
if Int.equal i 0
then None
else
let i := Int.sub i 1 in
let c := String.get s i in
let len_ext := Int.add 1 len_ext in
if Int.equal full_stop (Char.to_int c)
then Some len_ext
else f i len_ext
in
match f n 0 with
| None => n
| Some l => Int.sub n l end.
Ltac2 basename (s : string) : string :=
let len := base_length s in
if Int.equal len 0 then s else
let s' := String.make len (Char.of_int 0) in
let rec cp i :=
if Int.equal i 0 then () else
let i := Int.sub i 1 in
String.set s' i (String.get s i) ; cp i
in cp len ;
s'.
Ltac2 setjvars () :=
lazy_match! goal with
| [ |- context [ $$ ?i ] ] =>
let s := basename (ltac_string_of_string i) in
match Ident.of_string s with
| None => Control.throw (Tactic_failure (Some (fprintf "Not a valid ident: %s (was: %t)" s i)))
| Some id =>
let x := Fresh.fresh (Fresh.Free.of_goal ()) id in
set ($x := $$ $i)
end
end.
End jtac.
Ltac setjvars := ltac2:(jtac.setjvars ()).
I had to pepper it with a few calls to eval cbv in ... where I called Coq functions, otherwise I'd get match failures.
Philipp G. Haselwarter (May 11 2022 at 17:17):feedback appreciated, I haven't used Ltac2 much
Michael Soegtrop (May 11 2022 at 17:56):I can't say I can easily follow from base_length on (spec missing), but up to ltac_string_of_string it looks good to me.
Notification Bot (May 11 2022 at 17:58):This topic was moved here from #Coq users > use Gallina string with ltac's fresh by Michael Soegtrop.
Philipp G. Haselwarter (May 12 2022 at 09:16):base_length is an auxiliary function used in basename, which in turn removes an extension from a string, e.g. basename "foo.bar" = "foo", basename "foo" = "foo", basename ".bar" = "". The length of the output string has to be precomputed so that it can be allocated before copying the characters, that's what base_length does. I'm using basename because the strings I'm trying to turn into identifiers are of the form "x.143", and x.143 is not a valid identifier.
Notification Bot (May 16 2022 at 08:43):Philipp G. Haselwarter has marked this topic as resolved.
Last updated: May 28 2023 at 18:29 UTC