blob: 45695ebb3e52890f6679bef7722feb545f136769 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 2.1 of *)
(* the License, or (at your option) any later version. *)
(* This file is also distributed under the terms of the *)
(* INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** Definitions used by the .v files generated by clightgen *)
From Coq Require Import Ascii String List ZArith.
From compcert Require Import Maps Errors AST Ctypes.
(** ** Short names for types *)
Definition tvoid := Tvoid.
Definition tschar := Tint I8 Signed noattr.
Definition tuchar := Tint I8 Unsigned noattr.
Definition tshort := Tint I16 Signed noattr.
Definition tushort := Tint I16 Unsigned noattr.
Definition tint := Tint I32 Signed noattr.
Definition tuint := Tint I32 Unsigned noattr.
Definition tbool := Tint IBool Unsigned noattr.
Definition tlong := Tlong Signed noattr.
Definition tulong := Tlong Unsigned noattr.
Definition tfloat := Tfloat F32 noattr.
Definition tdouble := Tfloat F64 noattr.
Definition tptr (t: type) := Tpointer t noattr.
Definition tarray (t: type) (sz: Z) := Tarray t sz noattr.
Definition volatile_attr := {| attr_volatile := true; attr_alignas := None |}.
Definition tattr (a: attr) (ty: type) :=
match ty with
| Tvoid => Tvoid
| Tint sz si _ => Tint sz si a
| Tlong si _ => Tlong si a
| Tfloat sz _ => Tfloat sz a
| Tpointer elt _ => Tpointer elt a
| Tarray elt sz _ => Tarray elt sz a
| Tfunction args res cc => Tfunction args res cc
| Tstruct id _ => Tstruct id a
| Tunion id _ => Tunion id a
end.
Definition tvolatile (ty: type) := tattr volatile_attr ty.
Definition talignas (n: N) (ty: type) :=
tattr {| attr_volatile := false; attr_alignas := Some n |} ty.
Definition tvolatile_alignas (n: N) (ty: type) :=
tattr {| attr_volatile := true; attr_alignas := Some n |} ty.
(** ** Encoding character strings as positive numbers *)
(** The following encoding of character strings as positive numbers
must be kept consistent with the OCaml function [Camlcoq.pos_of_string]. *)
Definition append_bit_pos (b: bool) (p: positive) : positive :=
if b then xI p else xO p.
Definition append_char_pos_default (c: ascii) (p: positive) : positive :=
let '(Ascii b7 b6 b5 b4 b3 b2 b1 b0) := c in
xI (xI (xI (xI (xI (xI
(append_bit_pos b0 (append_bit_pos b1
(append_bit_pos b2 (append_bit_pos b3
(append_bit_pos b4 (append_bit_pos b5
(append_bit_pos b6 (append_bit_pos b7 p))))))))))))).
Definition append_char_pos (c: ascii) (p: positive) : positive :=
match c with
| "0"%char => xO (xO (xO (xO (xO (xO p)))))
| "1"%char => xI (xO (xO (xO (xO (xO p)))))
| "2"%char => xO (xI (xO (xO (xO (xO p)))))
| "3"%char => xI (xI (xO (xO (xO (xO p)))))
| "4"%char => xO (xO (xI (xO (xO (xO p)))))
| "5"%char => xI (xO (xI (xO (xO (xO p)))))
| "6"%char => xO (xI (xI (xO (xO (xO p)))))
| "7"%char => xI (xI (xI (xO (xO (xO p)))))
| "8"%char => xO (xO (xO (xI (xO (xO p)))))
| "9"%char => xI (xO (xO (xI (xO (xO p)))))
| "a"%char => xO (xI (xO (xI (xO (xO p)))))
| "b"%char => xI (xI (xO (xI (xO (xO p)))))
| "c"%char => xO (xO (xI (xI (xO (xO p)))))
| "d"%char => xI (xO (xI (xI (xO (xO p)))))
| "e"%char => xO (xI (xI (xI (xO (xO p)))))
| "f"%char => xI (xI (xI (xI (xO (xO p)))))
| "g"%char => xO (xO (xO (xO (xI (xO p)))))
| "h"%char => xI (xO (xO (xO (xI (xO p)))))
| "i"%char => xO (xI (xO (xO (xI (xO p)))))
| "j"%char => xI (xI (xO (xO (xI (xO p)))))
| "k"%char => xO (xO (xI (xO (xI (xO p)))))
| "l"%char => xI (xO (xI (xO (xI (xO p)))))
| "m"%char => xO (xI (xI (xO (xI (xO p)))))
| "n"%char => xI (xI (xI (xO (xI (xO p)))))
| "o"%char => xO (xO (xO (xI (xI (xO p)))))
| "p"%char => xI (xO (xO (xI (xI (xO p)))))
| "q"%char => xO (xI (xO (xI (xI (xO p)))))
| "r"%char => xI (xI (xO (xI (xI (xO p)))))
| "s"%char => xO (xO (xI (xI (xI (xO p)))))
| "t"%char => xI (xO (xI (xI (xI (xO p)))))
| "u"%char => xO (xI (xI (xI (xI (xO p)))))
| "v"%char => xI (xI (xI (xI (xI (xO p)))))
| "w"%char => xO (xO (xO (xO (xO (xI p)))))
| "x"%char => xI (xO (xO (xO (xO (xI p)))))
| "y"%char => xO (xI (xO (xO (xO (xI p)))))
| "z"%char => xI (xI (xO (xO (xO (xI p)))))
| "A"%char => xO (xO (xI (xO (xO (xI p)))))
| "B"%char => xI (xO (xI (xO (xO (xI p)))))
| "C"%char => xO (xI (xI (xO (xO (xI p)))))
| "D"%char => xI (xI (xI (xO (xO (xI p)))))
| "E"%char => xO (xO (xO (xI (xO (xI p)))))
| "F"%char => xI (xO (xO (xI (xO (xI p)))))
| "G"%char => xO (xI (xO (xI (xO (xI p)))))
| "H"%char => xI (xI (xO (xI (xO (xI p)))))
| "I"%char => xO (xO (xI (xI (xO (xI p)))))
| "J"%char => xI (xO (xI (xI (xO (xI p)))))
| "K"%char => xO (xI (xI (xI (xO (xI p)))))
| "L"%char => xI (xI (xI (xI (xO (xI p)))))
| "M"%char => xO (xO (xO (xO (xI (xI p)))))
| "N"%char => xI (xO (xO (xO (xI (xI p)))))
| "O"%char => xO (xI (xO (xO (xI (xI p)))))
| "P"%char => xI (xI (xO (xO (xI (xI p)))))
| "Q"%char => xO (xO (xI (xO (xI (xI p)))))
| "R"%char => xI (xO (xI (xO (xI (xI p)))))
| "S"%char => xO (xI (xI (xO (xI (xI p)))))
| "T"%char => xI (xI (xI (xO (xI (xI p)))))
| "U"%char => xO (xO (xO (xI (xI (xI p)))))
| "V"%char => xI (xO (xO (xI (xI (xI p)))))
| "W"%char => xO (xI (xO (xI (xI (xI p)))))
| "X"%char => xI (xI (xO (xI (xI (xI p)))))
| "Y"%char => xO (xO (xI (xI (xI (xI p)))))
| "Z"%char => xI (xO (xI (xI (xI (xI p)))))
| "_"%char => xO (xI (xI (xI (xI (xI p)))))
| _ => append_char_pos_default c p
end.
Fixpoint ident_of_string (s: string) : ident :=
match s with
| EmptyString => xH
| String c s => append_char_pos c (ident_of_string s)
end.
(** The inverse conversion, from encoded strings to strings *)
Section DECODE_BITS.
Variable rec: positive -> string.
Fixpoint decode_n_bits (n: nat) (l: list bool) (p: positive) : string :=
match n with
| O =>
match l with
| b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: _ =>
String (Ascii b7 b6 b5 b4 b3 b2 b1 b0) (rec p)
| _ => EmptyString
end
| S n =>
match p with
| xO q => decode_n_bits n (false :: l) q
| xI q => decode_n_bits n (true :: l) q
| xH => EmptyString
end
end.
Definition decode_8_bits := Eval compute in (decode_n_bits 8%nat nil).
End DECODE_BITS.
Fixpoint string_of_ident (p: positive) : string :=
match p with
| xO (xO (xO (xO (xO (xO p))))) => String "0"%char (string_of_ident p)
| xI (xO (xO (xO (xO (xO p))))) => String "1"%char (string_of_ident p)
| xO (xI (xO (xO (xO (xO p))))) => String "2"%char (string_of_ident p)
| xI (xI (xO (xO (xO (xO p))))) => String "3"%char (string_of_ident p)
| xO (xO (xI (xO (xO (xO p))))) => String "4"%char (string_of_ident p)
| xI (xO (xI (xO (xO (xO p))))) => String "5"%char (string_of_ident p)
| xO (xI (xI (xO (xO (xO p))))) => String "6"%char (string_of_ident p)
| xI (xI (xI (xO (xO (xO p))))) => String "7"%char (string_of_ident p)
| xO (xO (xO (xI (xO (xO p))))) => String "8"%char (string_of_ident p)
| xI (xO (xO (xI (xO (xO p))))) => String "9"%char (string_of_ident p)
| xO (xI (xO (xI (xO (xO p))))) => String "a"%char (string_of_ident p)
| xI (xI (xO (xI (xO (xO p))))) => String "b"%char (string_of_ident p)
| xO (xO (xI (xI (xO (xO p))))) => String "c"%char (string_of_ident p)
| xI (xO (xI (xI (xO (xO p))))) => String "d"%char (string_of_ident p)
| xO (xI (xI (xI (xO (xO p))))) => String "e"%char (string_of_ident p)
| xI (xI (xI (xI (xO (xO p))))) => String "f"%char (string_of_ident p)
| xO (xO (xO (xO (xI (xO p))))) => String "g"%char (string_of_ident p)
| xI (xO (xO (xO (xI (xO p))))) => String "h"%char (string_of_ident p)
| xO (xI (xO (xO (xI (xO p))))) => String "i"%char (string_of_ident p)
| xI (xI (xO (xO (xI (xO p))))) => String "j"%char (string_of_ident p)
| xO (xO (xI (xO (xI (xO p))))) => String "k"%char (string_of_ident p)
| xI (xO (xI (xO (xI (xO p))))) => String "l"%char (string_of_ident p)
| xO (xI (xI (xO (xI (xO p))))) => String "m"%char (string_of_ident p)
| xI (xI (xI (xO (xI (xO p))))) => String "n"%char (string_of_ident p)
| xO (xO (xO (xI (xI (xO p))))) => String "o"%char (string_of_ident p)
| xI (xO (xO (xI (xI (xO p))))) => String "p"%char (string_of_ident p)
| xO (xI (xO (xI (xI (xO p))))) => String "q"%char (string_of_ident p)
| xI (xI (xO (xI (xI (xO p))))) => String "r"%char (string_of_ident p)
| xO (xO (xI (xI (xI (xO p))))) => String "s"%char (string_of_ident p)
| xI (xO (xI (xI (xI (xO p))))) => String "t"%char (string_of_ident p)
| xO (xI (xI (xI (xI (xO p))))) => String "u"%char (string_of_ident p)
| xI (xI (xI (xI (xI (xO p))))) => String "v"%char (string_of_ident p)
| xO (xO (xO (xO (xO (xI p))))) => String "w"%char (string_of_ident p)
| xI (xO (xO (xO (xO (xI p))))) => String "x"%char (string_of_ident p)
| xO (xI (xO (xO (xO (xI p))))) => String "y"%char (string_of_ident p)
| xI (xI (xO (xO (xO (xI p))))) => String "z"%char (string_of_ident p)
| xO (xO (xI (xO (xO (xI p))))) => String "A"%char (string_of_ident p)
| xI (xO (xI (xO (xO (xI p))))) => String "B"%char (string_of_ident p)
| xO (xI (xI (xO (xO (xI p))))) => String "C"%char (string_of_ident p)
| xI (xI (xI (xO (xO (xI p))))) => String "D"%char (string_of_ident p)
| xO (xO (xO (xI (xO (xI p))))) => String "E"%char (string_of_ident p)
| xI (xO (xO (xI (xO (xI p))))) => String "F"%char (string_of_ident p)
| xO (xI (xO (xI (xO (xI p))))) => String "G"%char (string_of_ident p)
| xI (xI (xO (xI (xO (xI p))))) => String "H"%char (string_of_ident p)
| xO (xO (xI (xI (xO (xI p))))) => String "I"%char (string_of_ident p)
| xI (xO (xI (xI (xO (xI p))))) => String "J"%char (string_of_ident p)
| xO (xI (xI (xI (xO (xI p))))) => String "K"%char (string_of_ident p)
| xI (xI (xI (xI (xO (xI p))))) => String "L"%char (string_of_ident p)
| xO (xO (xO (xO (xI (xI p))))) => String "M"%char (string_of_ident p)
| xI (xO (xO (xO (xI (xI p))))) => String "N"%char (string_of_ident p)
| xO (xI (xO (xO (xI (xI p))))) => String "O"%char (string_of_ident p)
| xI (xI (xO (xO (xI (xI p))))) => String "P"%char (string_of_ident p)
| xO (xO (xI (xO (xI (xI p))))) => String "Q"%char (string_of_ident p)
| xI (xO (xI (xO (xI (xI p))))) => String "R"%char (string_of_ident p)
| xO (xI (xI (xO (xI (xI p))))) => String "S"%char (string_of_ident p)
| xI (xI (xI (xO (xI (xI p))))) => String "T"%char (string_of_ident p)
| xO (xO (xO (xI (xI (xI p))))) => String "U"%char (string_of_ident p)
| xI (xO (xO (xI (xI (xI p))))) => String "V"%char (string_of_ident p)
| xO (xI (xO (xI (xI (xI p))))) => String "W"%char (string_of_ident p)
| xI (xI (xO (xI (xI (xI p))))) => String "X"%char (string_of_ident p)
| xO (xO (xI (xI (xI (xI p))))) => String "Y"%char (string_of_ident p)
| xI (xO (xI (xI (xI (xI p))))) => String "Z"%char (string_of_ident p)
| xO (xI (xI (xI (xI (xI p))))) => String "_"%char (string_of_ident p)
| xI (xI (xI (xI (xI (xI p))))) => decode_8_bits string_of_ident p
| _ => EmptyString
end.
Lemma string_of_ident_of_string:
forall s, string_of_ident (ident_of_string s) = s.
Proof.
induction s as [ | c s]; simpl.
- auto.
- rewrite <- IHs at 2. destruct c as [[] [] [] [] [] [] [] []]; reflexivity.
Qed.
Corollary ident_of_string_injective:
forall s1 s2, ident_of_string s1 = ident_of_string s2 -> s1 = s2.
Proof.
intros. rewrite <- (string_of_ident_of_string s1), <- (string_of_ident_of_string s2).
congruence.
Qed.
|
