Library iris.proofmode.string_ident
From Ltac2 Require Ltac2.
From Stdlib Require Import Strings.String.
From Stdlib Require Import Init.Byte Ascii.
Import List.ListNotations.
Local Open Scope list.
Module StringToIdent.
Import Ltac2.
Ltac2 Type exn ::= [ NotStringLiteral(constr) | InvalidIdent(string) ].
Ltac2 rocq_byte_to_int (b : constr) : int :=
match! b with
| x00 ⇒ 0 | x01 ⇒ 1 | x02 ⇒ 2 | x03 ⇒ 3 | x04 ⇒ 4 | x05 ⇒ 5 | x06 ⇒ 6 | x07 ⇒ 7 | x08 ⇒ 8 | x09 ⇒ 9 | x0a ⇒ 10 | x0b ⇒ 11 | x0c ⇒ 12 | x0d ⇒ 13 | x0e ⇒ 14 | x0f ⇒ 15 | x10 ⇒ 16 | x11 ⇒ 17 | x12 ⇒ 18 | x13 ⇒ 19 | x14 ⇒ 20 | x15 ⇒ 21 | x16 ⇒ 22 | x17 ⇒ 23 | x18 ⇒ 24 | x19 ⇒ 25 | x1a ⇒ 26 | x1b ⇒ 27 | x1c ⇒ 28 | x1d ⇒ 29 | x1e ⇒ 30 | x1f ⇒ 31 | x20 ⇒ 32 | x21 ⇒ 33 | x22 ⇒ 34 | x23 ⇒ 35 | x24 ⇒ 36 | x25 ⇒ 37 | x26 ⇒ 38 | x27 ⇒ 39 | x28 ⇒ 40 | x29 ⇒ 41 | x2a ⇒ 42 | x2b ⇒ 43 | x2c ⇒ 44 | x2d ⇒ 45 | x2e ⇒ 46 | x2f ⇒ 47 | x30 ⇒ 48 | x31 ⇒ 49 | x32 ⇒ 50 | x33 ⇒ 51 | x34 ⇒ 52 | x35 ⇒ 53 | x36 ⇒ 54 | x37 ⇒ 55 | x38 ⇒ 56 | x39 ⇒ 57 | x3a ⇒ 58 | x3b ⇒ 59 | x3c ⇒ 60 | x3d ⇒ 61 | x3e ⇒ 62 | x3f ⇒ 63 | x40 ⇒ 64 | x41 ⇒ 65 | x42 ⇒ 66 | x43 ⇒ 67 | x44 ⇒ 68 | x45 ⇒ 69 | x46 ⇒ 70 | x47 ⇒ 71 | x48 ⇒ 72 | x49 ⇒ 73 | x4a ⇒ 74 | x4b ⇒ 75 | x4c ⇒ 76 | x4d ⇒ 77 | x4e ⇒ 78 | x4f ⇒ 79 | x50 ⇒ 80 | x51 ⇒ 81 | x52 ⇒ 82 | x53 ⇒ 83 | x54 ⇒ 84 | x55 ⇒ 85 | x56 ⇒ 86 | x57 ⇒ 87 | x58 ⇒ 88 | x59 ⇒ 89 | x5a ⇒ 90 | x5b ⇒ 91 | x5c ⇒ 92 | x5d ⇒ 93 | x5e ⇒ 94 | x5f ⇒ 95 | x60 ⇒ 96 | x61 ⇒ 97 | x62 ⇒ 98 | x63 ⇒ 99 | x64 ⇒ 100 | x65 ⇒ 101 | x66 ⇒ 102 | x67 ⇒ 103 | x68 ⇒ 104 | x69 ⇒ 105 | x6a ⇒ 106 | x6b ⇒ 107 | x6c ⇒ 108 | x6d ⇒ 109 | x6e ⇒ 110 | x6f ⇒ 111 | x70 ⇒ 112 | x71 ⇒ 113 | x72 ⇒ 114 | x73 ⇒ 115 | x74 ⇒ 116 | x75 ⇒ 117 | x76 ⇒ 118 | x77 ⇒ 119 | x78 ⇒ 120 | x79 ⇒ 121 | x7a ⇒ 122 | x7b ⇒ 123 | x7c ⇒ 124 | x7d ⇒ 125 | x7e ⇒ 126 | x7f ⇒ 127 | x80 ⇒ 128 | x81 ⇒ 129 | x82 ⇒ 130 | x83 ⇒ 131 | x84 ⇒ 132 | x85 ⇒ 133 | x86 ⇒ 134 | x87 ⇒ 135 | x88 ⇒ 136 | x89 ⇒ 137 | x8a ⇒ 138 | x8b ⇒ 139 | x8c ⇒ 140 | x8d ⇒ 141 | x8e ⇒ 142 | x8f ⇒ 143 | x90 ⇒ 144 | x91 ⇒ 145 | x92 ⇒ 146 | x93 ⇒ 147 | x94 ⇒ 148 | x95 ⇒ 149 | x96 ⇒ 150 | x97 ⇒ 151 | x98 ⇒ 152 | x99 ⇒ 153 | x9a ⇒ 154 | x9b ⇒ 155 | x9c ⇒ 156 | x9d ⇒ 157 | x9e ⇒ 158 | x9f ⇒ 159 | xa0 ⇒ 160 | xa1 ⇒ 161 | xa2 ⇒ 162 | xa3 ⇒ 163 | xa4 ⇒ 164 | xa5 ⇒ 165 | xa6 ⇒ 166 | xa7 ⇒ 167 | xa8 ⇒ 168 | xa9 ⇒ 169 | xaa ⇒ 170 | xab ⇒ 171 | xac ⇒ 172 | xad ⇒ 173 | xae ⇒ 174 | xaf ⇒ 175 | xb0 ⇒ 176 | xb1 ⇒ 177 | xb2 ⇒ 178 | xb3 ⇒ 179 | xb4 ⇒ 180 | xb5 ⇒ 181 | xb6 ⇒ 182 | xb7 ⇒ 183 | xb8 ⇒ 184 | xb9 ⇒ 185 | xba ⇒ 186 | xbb ⇒ 187 | xbc ⇒ 188 | xbd ⇒ 189 | xbe ⇒ 190 | xbf ⇒ 191 | xc0 ⇒ 192 | xc1 ⇒ 193 | xc2 ⇒ 194 | xc3 ⇒ 195 | xc4 ⇒ 196 | xc5 ⇒ 197 | xc6 ⇒ 198 | xc7 ⇒ 199 | xc8 ⇒ 200 | xc9 ⇒ 201 | xca ⇒ 202 | xcb ⇒ 203 | xcc ⇒ 204 | xcd ⇒ 205 | xce ⇒ 206 | xcf ⇒ 207 | xd0 ⇒ 208 | xd1 ⇒ 209 | xd2 ⇒ 210 | xd3 ⇒ 211 | xd4 ⇒ 212 | xd5 ⇒ 213 | xd6 ⇒ 214 | xd7 ⇒ 215 | xd8 ⇒ 216 | xd9 ⇒ 217 | xda ⇒ 218 | xdb ⇒ 219 | xdc ⇒ 220 | xdd ⇒ 221 | xde ⇒ 222 | xdf ⇒ 223 | xe0 ⇒ 224 | xe1 ⇒ 225 | xe2 ⇒ 226 | xe3 ⇒ 227 | xe4 ⇒ 228 | xe5 ⇒ 229 | xe6 ⇒ 230 | xe7 ⇒ 231 | xe8 ⇒ 232 | xe9 ⇒ 233 | xea ⇒ 234 | xeb ⇒ 235 | xec ⇒ 236 | xed ⇒ 237 | xee ⇒ 238 | xef ⇒ 239 | xf0 ⇒ 240 | xf1 ⇒ 241 | xf2 ⇒ 242 | xf3 ⇒ 243 | xf4 ⇒ 244 | xf5 ⇒ 245 | xf6 ⇒ 246 | xf7 ⇒ 247 | xf8 ⇒ 248 | xf9 ⇒ 249 | xfa ⇒ 250 | xfb ⇒ 251 | xfc ⇒ 252 | xfd ⇒ 253 | xfe ⇒ 254 | xff ⇒ 255
end.
Ltac2 rocq_byte_to_char (b : constr) : char :=
Char.of_int (rocq_byte_to_int b).
Fixpoint rocq_string_to_list_byte (s : string) : list byte :=
match s with
| EmptyString ⇒ []
| String c s ⇒ Ascii.byte_of_ascii c :: rocq_string_to_list_byte s
end.
From Stdlib Require Import Strings.String.
From Stdlib Require Import Init.Byte Ascii.
Import List.ListNotations.
Local Open Scope list.
Module StringToIdent.
Import Ltac2.
Ltac2 Type exn ::= [ NotStringLiteral(constr) | InvalidIdent(string) ].
Ltac2 rocq_byte_to_int (b : constr) : int :=
match! b with
| x00 ⇒ 0 | x01 ⇒ 1 | x02 ⇒ 2 | x03 ⇒ 3 | x04 ⇒ 4 | x05 ⇒ 5 | x06 ⇒ 6 | x07 ⇒ 7 | x08 ⇒ 8 | x09 ⇒ 9 | x0a ⇒ 10 | x0b ⇒ 11 | x0c ⇒ 12 | x0d ⇒ 13 | x0e ⇒ 14 | x0f ⇒ 15 | x10 ⇒ 16 | x11 ⇒ 17 | x12 ⇒ 18 | x13 ⇒ 19 | x14 ⇒ 20 | x15 ⇒ 21 | x16 ⇒ 22 | x17 ⇒ 23 | x18 ⇒ 24 | x19 ⇒ 25 | x1a ⇒ 26 | x1b ⇒ 27 | x1c ⇒ 28 | x1d ⇒ 29 | x1e ⇒ 30 | x1f ⇒ 31 | x20 ⇒ 32 | x21 ⇒ 33 | x22 ⇒ 34 | x23 ⇒ 35 | x24 ⇒ 36 | x25 ⇒ 37 | x26 ⇒ 38 | x27 ⇒ 39 | x28 ⇒ 40 | x29 ⇒ 41 | x2a ⇒ 42 | x2b ⇒ 43 | x2c ⇒ 44 | x2d ⇒ 45 | x2e ⇒ 46 | x2f ⇒ 47 | x30 ⇒ 48 | x31 ⇒ 49 | x32 ⇒ 50 | x33 ⇒ 51 | x34 ⇒ 52 | x35 ⇒ 53 | x36 ⇒ 54 | x37 ⇒ 55 | x38 ⇒ 56 | x39 ⇒ 57 | x3a ⇒ 58 | x3b ⇒ 59 | x3c ⇒ 60 | x3d ⇒ 61 | x3e ⇒ 62 | x3f ⇒ 63 | x40 ⇒ 64 | x41 ⇒ 65 | x42 ⇒ 66 | x43 ⇒ 67 | x44 ⇒ 68 | x45 ⇒ 69 | x46 ⇒ 70 | x47 ⇒ 71 | x48 ⇒ 72 | x49 ⇒ 73 | x4a ⇒ 74 | x4b ⇒ 75 | x4c ⇒ 76 | x4d ⇒ 77 | x4e ⇒ 78 | x4f ⇒ 79 | x50 ⇒ 80 | x51 ⇒ 81 | x52 ⇒ 82 | x53 ⇒ 83 | x54 ⇒ 84 | x55 ⇒ 85 | x56 ⇒ 86 | x57 ⇒ 87 | x58 ⇒ 88 | x59 ⇒ 89 | x5a ⇒ 90 | x5b ⇒ 91 | x5c ⇒ 92 | x5d ⇒ 93 | x5e ⇒ 94 | x5f ⇒ 95 | x60 ⇒ 96 | x61 ⇒ 97 | x62 ⇒ 98 | x63 ⇒ 99 | x64 ⇒ 100 | x65 ⇒ 101 | x66 ⇒ 102 | x67 ⇒ 103 | x68 ⇒ 104 | x69 ⇒ 105 | x6a ⇒ 106 | x6b ⇒ 107 | x6c ⇒ 108 | x6d ⇒ 109 | x6e ⇒ 110 | x6f ⇒ 111 | x70 ⇒ 112 | x71 ⇒ 113 | x72 ⇒ 114 | x73 ⇒ 115 | x74 ⇒ 116 | x75 ⇒ 117 | x76 ⇒ 118 | x77 ⇒ 119 | x78 ⇒ 120 | x79 ⇒ 121 | x7a ⇒ 122 | x7b ⇒ 123 | x7c ⇒ 124 | x7d ⇒ 125 | x7e ⇒ 126 | x7f ⇒ 127 | x80 ⇒ 128 | x81 ⇒ 129 | x82 ⇒ 130 | x83 ⇒ 131 | x84 ⇒ 132 | x85 ⇒ 133 | x86 ⇒ 134 | x87 ⇒ 135 | x88 ⇒ 136 | x89 ⇒ 137 | x8a ⇒ 138 | x8b ⇒ 139 | x8c ⇒ 140 | x8d ⇒ 141 | x8e ⇒ 142 | x8f ⇒ 143 | x90 ⇒ 144 | x91 ⇒ 145 | x92 ⇒ 146 | x93 ⇒ 147 | x94 ⇒ 148 | x95 ⇒ 149 | x96 ⇒ 150 | x97 ⇒ 151 | x98 ⇒ 152 | x99 ⇒ 153 | x9a ⇒ 154 | x9b ⇒ 155 | x9c ⇒ 156 | x9d ⇒ 157 | x9e ⇒ 158 | x9f ⇒ 159 | xa0 ⇒ 160 | xa1 ⇒ 161 | xa2 ⇒ 162 | xa3 ⇒ 163 | xa4 ⇒ 164 | xa5 ⇒ 165 | xa6 ⇒ 166 | xa7 ⇒ 167 | xa8 ⇒ 168 | xa9 ⇒ 169 | xaa ⇒ 170 | xab ⇒ 171 | xac ⇒ 172 | xad ⇒ 173 | xae ⇒ 174 | xaf ⇒ 175 | xb0 ⇒ 176 | xb1 ⇒ 177 | xb2 ⇒ 178 | xb3 ⇒ 179 | xb4 ⇒ 180 | xb5 ⇒ 181 | xb6 ⇒ 182 | xb7 ⇒ 183 | xb8 ⇒ 184 | xb9 ⇒ 185 | xba ⇒ 186 | xbb ⇒ 187 | xbc ⇒ 188 | xbd ⇒ 189 | xbe ⇒ 190 | xbf ⇒ 191 | xc0 ⇒ 192 | xc1 ⇒ 193 | xc2 ⇒ 194 | xc3 ⇒ 195 | xc4 ⇒ 196 | xc5 ⇒ 197 | xc6 ⇒ 198 | xc7 ⇒ 199 | xc8 ⇒ 200 | xc9 ⇒ 201 | xca ⇒ 202 | xcb ⇒ 203 | xcc ⇒ 204 | xcd ⇒ 205 | xce ⇒ 206 | xcf ⇒ 207 | xd0 ⇒ 208 | xd1 ⇒ 209 | xd2 ⇒ 210 | xd3 ⇒ 211 | xd4 ⇒ 212 | xd5 ⇒ 213 | xd6 ⇒ 214 | xd7 ⇒ 215 | xd8 ⇒ 216 | xd9 ⇒ 217 | xda ⇒ 218 | xdb ⇒ 219 | xdc ⇒ 220 | xdd ⇒ 221 | xde ⇒ 222 | xdf ⇒ 223 | xe0 ⇒ 224 | xe1 ⇒ 225 | xe2 ⇒ 226 | xe3 ⇒ 227 | xe4 ⇒ 228 | xe5 ⇒ 229 | xe6 ⇒ 230 | xe7 ⇒ 231 | xe8 ⇒ 232 | xe9 ⇒ 233 | xea ⇒ 234 | xeb ⇒ 235 | xec ⇒ 236 | xed ⇒ 237 | xee ⇒ 238 | xef ⇒ 239 | xf0 ⇒ 240 | xf1 ⇒ 241 | xf2 ⇒ 242 | xf3 ⇒ 243 | xf4 ⇒ 244 | xf5 ⇒ 245 | xf6 ⇒ 246 | xf7 ⇒ 247 | xf8 ⇒ 248 | xf9 ⇒ 249 | xfa ⇒ 250 | xfb ⇒ 251 | xfc ⇒ 252 | xfd ⇒ 253 | xfe ⇒ 254 | xff ⇒ 255
end.
Ltac2 rocq_byte_to_char (b : constr) : char :=
Char.of_int (rocq_byte_to_int b).
Fixpoint rocq_string_to_list_byte (s : string) : list byte :=
match s with
| EmptyString ⇒ []
| String c s ⇒ Ascii.byte_of_ascii c :: rocq_string_to_list_byte s
end.
copy a list of Rocq byte constrs into a string (already of the right length)
Ltac2 rec rocq_byte_list_blit_list (pos : int) (ls : constr) (str : string) : unit :=
match! ls with
| nil ⇒ ()
| ?c :: ?ls ⇒
let b := rocq_byte_to_char c in
String.set str pos b; rocq_byte_list_blit_list (Int.add pos 1) ls str
end.
Ltac2 rec rocq_string_length (s : constr) : int :=
match! s with
| EmptyString ⇒ 0
| String _ ?s' ⇒ Int.add 1 (rocq_string_length s')
| _ ⇒ Control.throw (NotStringLiteral s)
end.
Ltac2 compute (c : constr) : constr :=
Std.eval_vm None c.
match! ls with
| nil ⇒ ()
| ?c :: ?ls ⇒
let b := rocq_byte_to_char c in
String.set str pos b; rocq_byte_list_blit_list (Int.add pos 1) ls str
end.
Ltac2 rec rocq_string_length (s : constr) : int :=
match! s with
| EmptyString ⇒ 0
| String _ ?s' ⇒ Int.add 1 (rocq_string_length s')
| _ ⇒ Control.throw (NotStringLiteral s)
end.
Ltac2 compute (c : constr) : constr :=
Std.eval_vm None c.
rocq_string_to_string converts a Gallina string in a constr to an Ltac2
native string
Ltac2 rocq_string_to_string (s : constr) : string :=
let l := rocq_string_length s in
let str := String.make l (Char.of_int 0) in
let bytes := compute constr:(rocq_string_to_list_byte $s) in
let _ := rocq_byte_list_blit_list 0 bytes str in
str.
Ltac2 string_to_ident (s : string) : ident :=
match Ident.of_string s with
| Some id ⇒ id
| None ⇒ Control.throw (InvalidIdent s)
end.
let l := rocq_string_length s in
let str := String.make l (Char.of_int 0) in
let bytes := compute constr:(rocq_string_to_list_byte $s) in
let _ := rocq_byte_list_blit_list 0 bytes str in
str.
Ltac2 string_to_ident (s : string) : ident :=
match Ident.of_string s with
| Some id ⇒ id
| None ⇒ Control.throw (InvalidIdent s)
end.
rocq_string_to_ident implements the ident to string conversion in Ltac2
Ltac2 rocq_string_to_ident (s : constr) : ident :=
string_to_ident (rocq_string_to_string s).
string_to_ident (rocq_string_to_string s).
We want to wrap rocq_string_to_ident in an Ltac1 API, but Ltac1-2 FFI
does not support returning values from Ltac2 to Ltac1. So we provide
string_to_ident_cps in CPS instead.
Ltac string_to_ident_cps :=
ltac2:(s1 r |- let s := Option.get (Ltac1.to_constr s1) in
let ident := rocq_string_to_ident s in
Ltac1.apply r [Ltac1.of_ident ident] Ltac1.run).
End StringToIdent.
Module IdentToString.
Import Ltac2.
Ltac2 get_bit (n : int) (i : int) : bool :=
Int.equal (Int.land (Int.lsr n i) 1) 1.
Ltac2 get_bit_rocq_bool (n : int) (i : int) : constr :=
if get_bit n i then constr:(true) else constr:(false).
Ltac2 char_to_rocq_ascii (c : char) : constr :=
let i := Char.to_int c in
let bs := Array.init 8 (get_bit_rocq_bool i) in
Constr.Unsafe.make (Constr.Unsafe.App constr:(Ascii) bs).
Ltac2 string_to_rocq_string (s : string) : constr :=
let len := String.length s in
let rec to_string i :=
if Int.equal i len then constr:(EmptyString) else
let tail := to_string (Int.add i 1) in
let head := char_to_rocq_ascii (String.get s i) in
constr:(String $head $tail)
in
to_string 0.
Ltac2 ident_to_string (id : ident) : constr :=
string_to_rocq_string (Ident.to_string id).
Ltac ident_to_string_cps :=
ltac2:(id r |- let id := Option.get (Ltac1.to_ident id) in
let s := ident_to_string id in
Ltac1.apply r [Ltac1.of_constr s] Ltac1.run).
End IdentToString.
Finally we wrap everything up intro a tactic that renames a variable given
by ident id into the name given by string s.
Ltac rename_by_string id s :=
StringToIdent.string_to_ident_cps s ltac:(fun x ⇒ rename id into x).
Ltac string_to_ident_cps := StringToIdent.string_to_ident_cps.
Ltac ident_to_string_cps := IdentToString.ident_to_string_cps.
StringToIdent.string_to_ident_cps s ltac:(fun x ⇒ rename id into x).
Ltac string_to_ident_cps := StringToIdent.string_to_ident_cps.
Ltac ident_to_string_cps := IdentToString.ident_to_string_cps.