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?
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.
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.
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
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.
@Michael Soegtrop could you give me a pointer to one such, for reference?
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_sc
is pre Ltac2-printf and requires a bit of boilerplate - I still need to write throw convenience functions with printf style parameters.
@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.
feedback appreciated, I haven't used Ltac2 much
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.
This topic was moved here from #Coq users > use Gallina string with ltac's fresh by Michael Soegtrop.
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.
Philipp G. Haselwarter has marked this topic as resolved.
Last updated: May 28 2023 at 18:29 UTC