Skip to content

Commit 6aeb645

Browse files
xavierleroyxavierleroy
committed
Add string_of_ident conversion
This is the left inverse of `ident_to_string`. Closes: #372
1 parent 600803c commit 6aeb645

File tree

1 file changed

+110
-0
lines changed

1 file changed

+110
-0
lines changed

‎exportclight/Clightdefs.v‎

Lines changed: 110 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -179,3 +179,113 @@ Ltac ident_of_string s :=
179179

180180
Notation "$ s" := (ltac:(ident_of_string s))
181181
(at level 1, only parsing) : string_scope.
182+
183+
(** The inverse conversion, from encoded strings to strings *)
184+
185+
Section DECODE_BITS.
186+
187+
Variable rec: positive -> string.
188+
189+
Fixpoint decode_n_bits (n: nat) (l: list bool) (p: positive) : string :=
190+
match n with
191+
| O =>
192+
match l with
193+
| b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: _ =>
194+
String (Ascii b7 b6 b5 b4 b3 b2 b1 b0) (rec p)
195+
| _ => EmptyString
196+
end
197+
| S n =>
198+
match p with
199+
| xO q => decode_n_bits n (false :: l) q
200+
| xI q => decode_n_bits n (true :: l) q
201+
| xH => EmptyString
202+
end
203+
end.
204+
205+
Definition decode_8_bits := Eval compute in (decode_n_bits 8%nat nil).
206+
207+
End DECODE_BITS.
208+
209+
Fixpoint string_of_ident (p: positive) : string :=
210+
match p with
211+
| xO (xO (xO (xO (xO (xO p))))) => String "0"%char (string_of_ident p)
212+
| xI (xO (xO (xO (xO (xO p))))) => String "1"%char (string_of_ident p)
213+
| xO (xI (xO (xO (xO (xO p))))) => String "2"%char (string_of_ident p)
214+
| xI (xI (xO (xO (xO (xO p))))) => String "3"%char (string_of_ident p)
215+
| xO (xO (xI (xO (xO (xO p))))) => String "4"%char (string_of_ident p)
216+
| xI (xO (xI (xO (xO (xO p))))) => String "5"%char (string_of_ident p)
217+
| xO (xI (xI (xO (xO (xO p))))) => String "6"%char (string_of_ident p)
218+
| xI (xI (xI (xO (xO (xO p))))) => String "7"%char (string_of_ident p)
219+
| xO (xO (xO (xI (xO (xO p))))) => String "8"%char (string_of_ident p)
220+
| xI (xO (xO (xI (xO (xO p))))) => String "9"%char (string_of_ident p)
221+
| xO (xI (xO (xI (xO (xO p))))) => String "a"%char (string_of_ident p)
222+
| xI (xI (xO (xI (xO (xO p))))) => String "b"%char (string_of_ident p)
223+
| xO (xO (xI (xI (xO (xO p))))) => String "c"%char (string_of_ident p)
224+
| xI (xO (xI (xI (xO (xO p))))) => String "d"%char (string_of_ident p)
225+
| xO (xI (xI (xI (xO (xO p))))) => String "e"%char (string_of_ident p)
226+
| xI (xI (xI (xI (xO (xO p))))) => String "f"%char (string_of_ident p)
227+
| xO (xO (xO (xO (xI (xO p))))) => String "g"%char (string_of_ident p)
228+
| xI (xO (xO (xO (xI (xO p))))) => String "h"%char (string_of_ident p)
229+
| xO (xI (xO (xO (xI (xO p))))) => String "i"%char (string_of_ident p)
230+
| xI (xI (xO (xO (xI (xO p))))) => String "j"%char (string_of_ident p)
231+
| xO (xO (xI (xO (xI (xO p))))) => String "k"%char (string_of_ident p)
232+
| xI (xO (xI (xO (xI (xO p))))) => String "l"%char (string_of_ident p)
233+
| xO (xI (xI (xO (xI (xO p))))) => String "m"%char (string_of_ident p)
234+
| xI (xI (xI (xO (xI (xO p))))) => String "n"%char (string_of_ident p)
235+
| xO (xO (xO (xI (xI (xO p))))) => String "o"%char (string_of_ident p)
236+
| xI (xO (xO (xI (xI (xO p))))) => String "p"%char (string_of_ident p)
237+
| xO (xI (xO (xI (xI (xO p))))) => String "q"%char (string_of_ident p)
238+
| xI (xI (xO (xI (xI (xO p))))) => String "r"%char (string_of_ident p)
239+
| xO (xO (xI (xI (xI (xO p))))) => String "s"%char (string_of_ident p)
240+
| xI (xO (xI (xI (xI (xO p))))) => String "t"%char (string_of_ident p)
241+
| xO (xI (xI (xI (xI (xO p))))) => String "u"%char (string_of_ident p)
242+
| xI (xI (xI (xI (xI (xO p))))) => String "v"%char (string_of_ident p)
243+
| xO (xO (xO (xO (xO (xI p))))) => String "w"%char (string_of_ident p)
244+
| xI (xO (xO (xO (xO (xI p))))) => String "x"%char (string_of_ident p)
245+
| xO (xI (xO (xO (xO (xI p))))) => String "y"%char (string_of_ident p)
246+
| xI (xI (xO (xO (xO (xI p))))) => String "z"%char (string_of_ident p)
247+
| xO (xO (xI (xO (xO (xI p))))) => String "A"%char (string_of_ident p)
248+
| xI (xO (xI (xO (xO (xI p))))) => String "B"%char (string_of_ident p)
249+
| xO (xI (xI (xO (xO (xI p))))) => String "C"%char (string_of_ident p)
250+
| xI (xI (xI (xO (xO (xI p))))) => String "D"%char (string_of_ident p)
251+
| xO (xO (xO (xI (xO (xI p))))) => String "E"%char (string_of_ident p)
252+
| xI (xO (xO (xI (xO (xI p))))) => String "F"%char (string_of_ident p)
253+
| xO (xI (xO (xI (xO (xI p))))) => String "G"%char (string_of_ident p)
254+
| xI (xI (xO (xI (xO (xI p))))) => String "H"%char (string_of_ident p)
255+
| xO (xO (xI (xI (xO (xI p))))) => String "I"%char (string_of_ident p)
256+
| xI (xO (xI (xI (xO (xI p))))) => String "J"%char (string_of_ident p)
257+
| xO (xI (xI (xI (xO (xI p))))) => String "K"%char (string_of_ident p)
258+
| xI (xI (xI (xI (xO (xI p))))) => String "L"%char (string_of_ident p)
259+
| xO (xO (xO (xO (xI (xI p))))) => String "M"%char (string_of_ident p)
260+
| xI (xO (xO (xO (xI (xI p))))) => String "N"%char (string_of_ident p)
261+
| xO (xI (xO (xO (xI (xI p))))) => String "O"%char (string_of_ident p)
262+
| xI (xI (xO (xO (xI (xI p))))) => String "P"%char (string_of_ident p)
263+
| xO (xO (xI (xO (xI (xI p))))) => String "Q"%char (string_of_ident p)
264+
| xI (xO (xI (xO (xI (xI p))))) => String "R"%char (string_of_ident p)
265+
| xO (xI (xI (xO (xI (xI p))))) => String "S"%char (string_of_ident p)
266+
| xI (xI (xI (xO (xI (xI p))))) => String "T"%char (string_of_ident p)
267+
| xO (xO (xO (xI (xI (xI p))))) => String "U"%char (string_of_ident p)
268+
| xI (xO (xO (xI (xI (xI p))))) => String "V"%char (string_of_ident p)
269+
| xO (xI (xO (xI (xI (xI p))))) => String "W"%char (string_of_ident p)
270+
| xI (xI (xO (xI (xI (xI p))))) => String "X"%char (string_of_ident p)
271+
| xO (xO (xI (xI (xI (xI p))))) => String "Y"%char (string_of_ident p)
272+
| xI (xO (xI (xI (xI (xI p))))) => String "Z"%char (string_of_ident p)
273+
| xO (xI (xI (xI (xI (xI p))))) => String "_"%char (string_of_ident p)
274+
| xI (xI (xI (xI (xI (xI p))))) => decode_8_bits string_of_ident p
275+
| _ => EmptyString
276+
end.
277+
278+
Lemma string_of_ident_of_string:
279+
forall s, string_of_ident (ident_of_string s) = s.
280+
Proof.
281+
induction s as [ | c s]; simpl.
282+
- auto.
283+
- rewrite <- IHs at 2. destruct c as [[] [] [] [] [] [] [] []]; reflexivity.
284+
Qed.
285+
286+
Corollary ident_of_string_injective:
287+
forall s1 s2, ident_of_string s1 = ident_of_string s2 -> s1 = s2.
288+
Proof.
289+
intros. rewrite <- (string_of_ident_of_string s1), <- (string_of_ident_of_string s2).
290+
congruence.
291+
Qed.

0 commit comments

Comments
 (0)