Stream: Ltac2

Topic: use Gallina string with ltac's fresh


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Philipp G. Haselwarter (May 11 2022 at 12:32):

@Michael Soegtrop could you give me a pointer to one such, for reference?

view this post on Zulip 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.

view this post on Zulip 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 ()).

view this post on Zulip Philipp G. Haselwarter (May 11 2022 at 17:17):

I had to pepper it with a few calls to eval cbv in ... where I called Coq functions, otherwise I'd get match failures.

view this post on Zulip Philipp G. Haselwarter (May 11 2022 at 17:17):

feedback appreciated, I haven't used Ltac2 much

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.


Last updated: Jan 31 2023 at 09:01 UTC