source: extracted/i8051.ml @ 2717

Last change on this file since 2717 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 32.9 KB
Line 
1open Preamble
2
3open Bool
4
5open Hints_declaration
6
7open Core_notation
8
9open Pts
10
11open Logic
12
13open Relations
14
15open Nat
16
17open Jmeq
18
19open Exp
20
21open Extranat
22
23open Vector
24
25open Div_and_mod
26
27open Russell
28
29open Types
30
31open List
32
33open Util
34
35open FoldStuff
36
37open BitVector
38
39open Arithmetic
40
41(** val int_size : BitVector.bitVector **)
42let int_size =
43  Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
44    (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)
45
46(** val ptr_size : BitVector.bitVector **)
47let ptr_size =
48  Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
49    (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S Nat.O))
50
51(** val alignment : 'a1 Types.option **)
52let alignment =
53  Types.None
54
55type register =
56| Register00
57| Register01
58| Register02
59| Register03
60| Register04
61| Register05
62| Register06
63| Register07
64| Register10
65| Register11
66| Register12
67| Register13
68| Register14
69| Register15
70| Register16
71| Register17
72| Register20
73| Register21
74| Register22
75| Register23
76| Register24
77| Register25
78| Register26
79| Register27
80| Register30
81| Register31
82| Register32
83| Register33
84| Register34
85| Register35
86| Register36
87| Register37
88| RegisterA
89| RegisterB
90| RegisterDPL
91| RegisterDPH
92| RegisterCarry
93
94(** val register_rect_Type4 :
95    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
96    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
97    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
98    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **)
99let rec register_rect_Type4 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function
100| Register00 -> h_Register00
101| Register01 -> h_Register01
102| Register02 -> h_Register02
103| Register03 -> h_Register03
104| Register04 -> h_Register04
105| Register05 -> h_Register05
106| Register06 -> h_Register06
107| Register07 -> h_Register07
108| Register10 -> h_Register10
109| Register11 -> h_Register11
110| Register12 -> h_Register12
111| Register13 -> h_Register13
112| Register14 -> h_Register14
113| Register15 -> h_Register15
114| Register16 -> h_Register16
115| Register17 -> h_Register17
116| Register20 -> h_Register20
117| Register21 -> h_Register21
118| Register22 -> h_Register22
119| Register23 -> h_Register23
120| Register24 -> h_Register24
121| Register25 -> h_Register25
122| Register26 -> h_Register26
123| Register27 -> h_Register27
124| Register30 -> h_Register30
125| Register31 -> h_Register31
126| Register32 -> h_Register32
127| Register33 -> h_Register33
128| Register34 -> h_Register34
129| Register35 -> h_Register35
130| Register36 -> h_Register36
131| Register37 -> h_Register37
132| RegisterA -> h_RegisterA
133| RegisterB -> h_RegisterB
134| RegisterDPL -> h_RegisterDPL
135| RegisterDPH -> h_RegisterDPH
136| RegisterCarry -> h_RegisterCarry
137
138(** val register_rect_Type5 :
139    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
140    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
141    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
142    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **)
143let rec register_rect_Type5 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function
144| Register00 -> h_Register00
145| Register01 -> h_Register01
146| Register02 -> h_Register02
147| Register03 -> h_Register03
148| Register04 -> h_Register04
149| Register05 -> h_Register05
150| Register06 -> h_Register06
151| Register07 -> h_Register07
152| Register10 -> h_Register10
153| Register11 -> h_Register11
154| Register12 -> h_Register12
155| Register13 -> h_Register13
156| Register14 -> h_Register14
157| Register15 -> h_Register15
158| Register16 -> h_Register16
159| Register17 -> h_Register17
160| Register20 -> h_Register20
161| Register21 -> h_Register21
162| Register22 -> h_Register22
163| Register23 -> h_Register23
164| Register24 -> h_Register24
165| Register25 -> h_Register25
166| Register26 -> h_Register26
167| Register27 -> h_Register27
168| Register30 -> h_Register30
169| Register31 -> h_Register31
170| Register32 -> h_Register32
171| Register33 -> h_Register33
172| Register34 -> h_Register34
173| Register35 -> h_Register35
174| Register36 -> h_Register36
175| Register37 -> h_Register37
176| RegisterA -> h_RegisterA
177| RegisterB -> h_RegisterB
178| RegisterDPL -> h_RegisterDPL
179| RegisterDPH -> h_RegisterDPH
180| RegisterCarry -> h_RegisterCarry
181
182(** val register_rect_Type3 :
183    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
184    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
185    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
186    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **)
187let rec register_rect_Type3 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function
188| Register00 -> h_Register00
189| Register01 -> h_Register01
190| Register02 -> h_Register02
191| Register03 -> h_Register03
192| Register04 -> h_Register04
193| Register05 -> h_Register05
194| Register06 -> h_Register06
195| Register07 -> h_Register07
196| Register10 -> h_Register10
197| Register11 -> h_Register11
198| Register12 -> h_Register12
199| Register13 -> h_Register13
200| Register14 -> h_Register14
201| Register15 -> h_Register15
202| Register16 -> h_Register16
203| Register17 -> h_Register17
204| Register20 -> h_Register20
205| Register21 -> h_Register21
206| Register22 -> h_Register22
207| Register23 -> h_Register23
208| Register24 -> h_Register24
209| Register25 -> h_Register25
210| Register26 -> h_Register26
211| Register27 -> h_Register27
212| Register30 -> h_Register30
213| Register31 -> h_Register31
214| Register32 -> h_Register32
215| Register33 -> h_Register33
216| Register34 -> h_Register34
217| Register35 -> h_Register35
218| Register36 -> h_Register36
219| Register37 -> h_Register37
220| RegisterA -> h_RegisterA
221| RegisterB -> h_RegisterB
222| RegisterDPL -> h_RegisterDPL
223| RegisterDPH -> h_RegisterDPH
224| RegisterCarry -> h_RegisterCarry
225
226(** val register_rect_Type2 :
227    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
228    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
229    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
230    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **)
231let rec register_rect_Type2 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function
232| Register00 -> h_Register00
233| Register01 -> h_Register01
234| Register02 -> h_Register02
235| Register03 -> h_Register03
236| Register04 -> h_Register04
237| Register05 -> h_Register05
238| Register06 -> h_Register06
239| Register07 -> h_Register07
240| Register10 -> h_Register10
241| Register11 -> h_Register11
242| Register12 -> h_Register12
243| Register13 -> h_Register13
244| Register14 -> h_Register14
245| Register15 -> h_Register15
246| Register16 -> h_Register16
247| Register17 -> h_Register17
248| Register20 -> h_Register20
249| Register21 -> h_Register21
250| Register22 -> h_Register22
251| Register23 -> h_Register23
252| Register24 -> h_Register24
253| Register25 -> h_Register25
254| Register26 -> h_Register26
255| Register27 -> h_Register27
256| Register30 -> h_Register30
257| Register31 -> h_Register31
258| Register32 -> h_Register32
259| Register33 -> h_Register33
260| Register34 -> h_Register34
261| Register35 -> h_Register35
262| Register36 -> h_Register36
263| Register37 -> h_Register37
264| RegisterA -> h_RegisterA
265| RegisterB -> h_RegisterB
266| RegisterDPL -> h_RegisterDPL
267| RegisterDPH -> h_RegisterDPH
268| RegisterCarry -> h_RegisterCarry
269
270(** val register_rect_Type1 :
271    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
272    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
273    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
274    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **)
275let rec register_rect_Type1 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function
276| Register00 -> h_Register00
277| Register01 -> h_Register01
278| Register02 -> h_Register02
279| Register03 -> h_Register03
280| Register04 -> h_Register04
281| Register05 -> h_Register05
282| Register06 -> h_Register06
283| Register07 -> h_Register07
284| Register10 -> h_Register10
285| Register11 -> h_Register11
286| Register12 -> h_Register12
287| Register13 -> h_Register13
288| Register14 -> h_Register14
289| Register15 -> h_Register15
290| Register16 -> h_Register16
291| Register17 -> h_Register17
292| Register20 -> h_Register20
293| Register21 -> h_Register21
294| Register22 -> h_Register22
295| Register23 -> h_Register23
296| Register24 -> h_Register24
297| Register25 -> h_Register25
298| Register26 -> h_Register26
299| Register27 -> h_Register27
300| Register30 -> h_Register30
301| Register31 -> h_Register31
302| Register32 -> h_Register32
303| Register33 -> h_Register33
304| Register34 -> h_Register34
305| Register35 -> h_Register35
306| Register36 -> h_Register36
307| Register37 -> h_Register37
308| RegisterA -> h_RegisterA
309| RegisterB -> h_RegisterB
310| RegisterDPL -> h_RegisterDPL
311| RegisterDPH -> h_RegisterDPH
312| RegisterCarry -> h_RegisterCarry
313
314(** val register_rect_Type0 :
315    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
316    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
317    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
318    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **)
319let rec register_rect_Type0 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function
320| Register00 -> h_Register00
321| Register01 -> h_Register01
322| Register02 -> h_Register02
323| Register03 -> h_Register03
324| Register04 -> h_Register04
325| Register05 -> h_Register05
326| Register06 -> h_Register06
327| Register07 -> h_Register07
328| Register10 -> h_Register10
329| Register11 -> h_Register11
330| Register12 -> h_Register12
331| Register13 -> h_Register13
332| Register14 -> h_Register14
333| Register15 -> h_Register15
334| Register16 -> h_Register16
335| Register17 -> h_Register17
336| Register20 -> h_Register20
337| Register21 -> h_Register21
338| Register22 -> h_Register22
339| Register23 -> h_Register23
340| Register24 -> h_Register24
341| Register25 -> h_Register25
342| Register26 -> h_Register26
343| Register27 -> h_Register27
344| Register30 -> h_Register30
345| Register31 -> h_Register31
346| Register32 -> h_Register32
347| Register33 -> h_Register33
348| Register34 -> h_Register34
349| Register35 -> h_Register35
350| Register36 -> h_Register36
351| Register37 -> h_Register37
352| RegisterA -> h_RegisterA
353| RegisterB -> h_RegisterB
354| RegisterDPL -> h_RegisterDPL
355| RegisterDPH -> h_RegisterDPH
356| RegisterCarry -> h_RegisterCarry
357
358(** val register_inv_rect_Type4 :
359    register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
360    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
361    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
362    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
363    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
364    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
365    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
366    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
367let register_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =
368  let hcut =
369    register_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15
370      h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33
371      h34 h35 h36 h37 hterm
372  in
373  hcut __
374
375(** val register_inv_rect_Type3 :
376    register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
377    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
378    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
379    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
380    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
381    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
382    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
383    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
384let register_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =
385  let hcut =
386    register_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15
387      h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33
388      h34 h35 h36 h37 hterm
389  in
390  hcut __
391
392(** val register_inv_rect_Type2 :
393    register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
394    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
395    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
396    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
397    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
398    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
399    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
400    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
401let register_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =
402  let hcut =
403    register_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15
404      h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33
405      h34 h35 h36 h37 hterm
406  in
407  hcut __
408
409(** val register_inv_rect_Type1 :
410    register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
411    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
412    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
413    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
414    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
415    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
416    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
417    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
418let register_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =
419  let hcut =
420    register_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15
421      h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33
422      h34 h35 h36 h37 hterm
423  in
424  hcut __
425
426(** val register_inv_rect_Type0 :
427    register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
428    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
429    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
430    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
431    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
432    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
433    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
434    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
435let register_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =
436  let hcut =
437    register_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15
438      h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33
439      h34 h35 h36 h37 hterm
440  in
441  hcut __
442
443(** val register_discr : register -> register -> __ **)
444let register_discr x y =
445  Logic.eq_rect_Type2 x
446    (match x with
447     | Register00 -> Obj.magic (fun _ dH -> dH)
448     | Register01 -> Obj.magic (fun _ dH -> dH)
449     | Register02 -> Obj.magic (fun _ dH -> dH)
450     | Register03 -> Obj.magic (fun _ dH -> dH)
451     | Register04 -> Obj.magic (fun _ dH -> dH)
452     | Register05 -> Obj.magic (fun _ dH -> dH)
453     | Register06 -> Obj.magic (fun _ dH -> dH)
454     | Register07 -> Obj.magic (fun _ dH -> dH)
455     | Register10 -> Obj.magic (fun _ dH -> dH)
456     | Register11 -> Obj.magic (fun _ dH -> dH)
457     | Register12 -> Obj.magic (fun _ dH -> dH)
458     | Register13 -> Obj.magic (fun _ dH -> dH)
459     | Register14 -> Obj.magic (fun _ dH -> dH)
460     | Register15 -> Obj.magic (fun _ dH -> dH)
461     | Register16 -> Obj.magic (fun _ dH -> dH)
462     | Register17 -> Obj.magic (fun _ dH -> dH)
463     | Register20 -> Obj.magic (fun _ dH -> dH)
464     | Register21 -> Obj.magic (fun _ dH -> dH)
465     | Register22 -> Obj.magic (fun _ dH -> dH)
466     | Register23 -> Obj.magic (fun _ dH -> dH)
467     | Register24 -> Obj.magic (fun _ dH -> dH)
468     | Register25 -> Obj.magic (fun _ dH -> dH)
469     | Register26 -> Obj.magic (fun _ dH -> dH)
470     | Register27 -> Obj.magic (fun _ dH -> dH)
471     | Register30 -> Obj.magic (fun _ dH -> dH)
472     | Register31 -> Obj.magic (fun _ dH -> dH)
473     | Register32 -> Obj.magic (fun _ dH -> dH)
474     | Register33 -> Obj.magic (fun _ dH -> dH)
475     | Register34 -> Obj.magic (fun _ dH -> dH)
476     | Register35 -> Obj.magic (fun _ dH -> dH)
477     | Register36 -> Obj.magic (fun _ dH -> dH)
478     | Register37 -> Obj.magic (fun _ dH -> dH)
479     | RegisterA -> Obj.magic (fun _ dH -> dH)
480     | RegisterB -> Obj.magic (fun _ dH -> dH)
481     | RegisterDPL -> Obj.magic (fun _ dH -> dH)
482     | RegisterDPH -> Obj.magic (fun _ dH -> dH)
483     | RegisterCarry -> Obj.magic (fun _ dH -> dH)) y
484
485(** val register_jmdiscr : register -> register -> __ **)
486let register_jmdiscr x y =
487  Logic.eq_rect_Type2 x
488    (match x with
489     | Register00 -> Obj.magic (fun _ dH -> dH)
490     | Register01 -> Obj.magic (fun _ dH -> dH)
491     | Register02 -> Obj.magic (fun _ dH -> dH)
492     | Register03 -> Obj.magic (fun _ dH -> dH)
493     | Register04 -> Obj.magic (fun _ dH -> dH)
494     | Register05 -> Obj.magic (fun _ dH -> dH)
495     | Register06 -> Obj.magic (fun _ dH -> dH)
496     | Register07 -> Obj.magic (fun _ dH -> dH)
497     | Register10 -> Obj.magic (fun _ dH -> dH)
498     | Register11 -> Obj.magic (fun _ dH -> dH)
499     | Register12 -> Obj.magic (fun _ dH -> dH)
500     | Register13 -> Obj.magic (fun _ dH -> dH)
501     | Register14 -> Obj.magic (fun _ dH -> dH)
502     | Register15 -> Obj.magic (fun _ dH -> dH)
503     | Register16 -> Obj.magic (fun _ dH -> dH)
504     | Register17 -> Obj.magic (fun _ dH -> dH)
505     | Register20 -> Obj.magic (fun _ dH -> dH)
506     | Register21 -> Obj.magic (fun _ dH -> dH)
507     | Register22 -> Obj.magic (fun _ dH -> dH)
508     | Register23 -> Obj.magic (fun _ dH -> dH)
509     | Register24 -> Obj.magic (fun _ dH -> dH)
510     | Register25 -> Obj.magic (fun _ dH -> dH)
511     | Register26 -> Obj.magic (fun _ dH -> dH)
512     | Register27 -> Obj.magic (fun _ dH -> dH)
513     | Register30 -> Obj.magic (fun _ dH -> dH)
514     | Register31 -> Obj.magic (fun _ dH -> dH)
515     | Register32 -> Obj.magic (fun _ dH -> dH)
516     | Register33 -> Obj.magic (fun _ dH -> dH)
517     | Register34 -> Obj.magic (fun _ dH -> dH)
518     | Register35 -> Obj.magic (fun _ dH -> dH)
519     | Register36 -> Obj.magic (fun _ dH -> dH)
520     | Register37 -> Obj.magic (fun _ dH -> dH)
521     | RegisterA -> Obj.magic (fun _ dH -> dH)
522     | RegisterB -> Obj.magic (fun _ dH -> dH)
523     | RegisterDPL -> Obj.magic (fun _ dH -> dH)
524     | RegisterDPH -> Obj.magic (fun _ dH -> dH)
525     | RegisterCarry -> Obj.magic (fun _ dH -> dH)) y
526
527(** val nat_of_register : register -> Nat.nat **)
528let nat_of_register = function
529| Register00 -> Nat.O
530| Register01 -> Nat.S Nat.O
531| Register02 -> Nat.S (Nat.S Nat.O)
532| Register03 -> Nat.S (Nat.S (Nat.S Nat.O))
533| Register04 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
534| Register05 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
535| Register06 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
536| Register07 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
537| Register10 ->
538  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
539| Register11 ->
540  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
541| Register12 ->
542  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
543    Nat.O)))))))))
544| Register13 ->
545  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
546    Nat.O))))))))))
547| Register14 ->
548  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
549    (Nat.S Nat.O)))))))))))
550| Register15 ->
551  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
552    (Nat.S (Nat.S Nat.O))))))))))))
553| Register16 ->
554  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
555    (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))
556| Register17 ->
557  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
558    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))
559| Register20 ->
560  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
561    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))
562| Register21 ->
563  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
564    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
565| Register22 ->
566  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
567    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))
568| Register23 ->
569  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
570    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
571    Nat.O))))))))))))))))))
572| Register24 ->
573  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
574    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
575    Nat.O)))))))))))))))))))
576| Register25 ->
577  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
578    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
579    Nat.O))))))))))))))))))))
580| Register26 ->
581  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
582    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
583    (Nat.S Nat.O)))))))))))))))))))))
584| Register27 ->
585  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
586    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
587    (Nat.S (Nat.S Nat.O))))))))))))))))))))))
588| Register30 ->
589  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
590    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
591    (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))
592| Register31 ->
593  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
594    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
595    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))
596| Register32 ->
597  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
598    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
599    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))))
600| Register33 ->
601  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
602    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
603    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))
604| Register34 ->
605  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
606    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
607    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
608    Nat.O)))))))))))))))))))))))))))
609| Register35 ->
610  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
611    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
612    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
613    Nat.O))))))))))))))))))))))))))))
614| Register36 ->
615  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
616    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
617    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
618    Nat.O)))))))))))))))))))))))))))))
619| Register37 ->
620  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
621    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
622    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
623    Nat.O))))))))))))))))))))))))))))))
624| RegisterA ->
625  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
626    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
627    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
628    (Nat.S Nat.O)))))))))))))))))))))))))))))))
629| RegisterB ->
630  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
631    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
632    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
633    (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))))
634| RegisterDPL ->
635  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
636    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
637    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
638    (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))))))))))))
639| RegisterDPH ->
640  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
641    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
642    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
643    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))))))
644| RegisterCarry ->
645  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
646    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
647    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
648    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
649    Nat.O)))))))))))))))))))))))))))))))))))
650
651(** val physical_register_count : Nat.nat **)
652let physical_register_count =
653  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
654    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
655    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
656    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
657    Nat.O)))))))))))))))))))))))))))))))))))
658
659(** val bitvector_of_register : register -> BitVector.bitVector **)
660let bitvector_of_register register0 =
661  Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
662    Nat.O)))))) (nat_of_register register0)
663
664(** val eq_Register : register -> register -> Bool.bool **)
665let eq_Register r s =
666  let r_as_nat = nat_of_register r in
667  let s_as_nat = nat_of_register s in Nat.eqb r_as_nat s_as_nat
668
669(** val registerSST : register **)
670let registerSST =
671  Register10
672
673(** val registerST0 : register **)
674let registerST0 =
675  Register02
676
677(** val registerST1 : register **)
678let registerST1 =
679  Register03
680
681(** val registerST2 : register **)
682let registerST2 =
683  Register04
684
685(** val registerST3 : register **)
686let registerST3 =
687  Register05
688
689(** val registerSTS : register List.list **)
690let registerSTS =
691  List.Cons (registerST0, (List.Cons (registerST1, (List.Cons (registerST2,
692    (List.Cons (registerST3, List.Nil)))))))
693
694(** val registerSPL : register **)
695let registerSPL =
696  Register06
697
698(** val registerSPH : register **)
699let registerSPH =
700  Register07
701
702(** val registerParams : register List.list **)
703let registerParams =
704  List.Cons (Register30, (List.Cons (Register31, (List.Cons (Register32,
705    (List.Cons (Register33, (List.Cons (Register34, (List.Cons (Register35,
706    (List.Cons (Register36, (List.Cons (Register37, List.Nil)))))))))))))))
707
708(** val registers : register List.list **)
709let registers =
710  List.Cons (Register00, (List.Cons (Register01, (List.Cons (Register02,
711    (List.Cons (Register03, (List.Cons (Register04, (List.Cons (Register05,
712    (List.Cons (Register06, (List.Cons (Register07, (List.Cons (Register10,
713    (List.Cons (Register11, (List.Cons (Register12, (List.Cons (Register13,
714    (List.Cons (Register14, (List.Cons (Register15, (List.Cons (Register16,
715    (List.Cons (Register17, (List.Cons (Register20, (List.Cons (Register21,
716    (List.Cons (Register22, (List.Cons (Register23, (List.Cons (Register24,
717    (List.Cons (Register25, (List.Cons (Register26, (List.Cons (Register27,
718    (List.Cons (Register30, (List.Cons (Register31, (List.Cons (Register32,
719    (List.Cons (Register33, (List.Cons (Register34, (List.Cons (Register35,
720    (List.Cons (Register36, (List.Cons (Register37, (List.Cons (RegisterA,
721    (List.Cons (RegisterB, (List.Cons (RegisterDPL, (List.Cons (RegisterDPH,
722    (List.Cons (registerSPL, (List.Cons (registerSPH, (List.Cons
723    (registerST0, (List.Cons (registerST1, (List.Cons (registerSST,
724    List.Nil)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
725
726(** val registerRets : register List.list **)
727let registerRets =
728  List.Cons (RegisterDPL, (List.Cons (RegisterDPH, (List.Cons (Register00,
729    (List.Cons (Register01, List.Nil)))))))
730
731(** val registerCallerSaved : register List.list **)
732let registerCallerSaved =
733  List.Cons (Register00, (List.Cons (Register01, (List.Cons (Register02,
734    (List.Cons (Register03, (List.Cons (Register04, (List.Cons (Register05,
735    (List.Cons (Register06, (List.Cons (Register07, (List.Cons (Register10,
736    (List.Cons (Register11, (List.Cons (Register12, (List.Cons (Register13,
737    (List.Cons (Register14, (List.Cons (Register15, (List.Cons (Register16,
738    (List.Cons (Register17, (List.Cons (Register30, (List.Cons (Register31,
739    (List.Cons (Register32, (List.Cons (Register33, (List.Cons (Register34,
740    (List.Cons (Register35, (List.Cons (Register36, (List.Cons (Register37,
741    List.Nil)))))))))))))))))))))))))))))))))))))))))))))))
742
743(** val registerCalleeSaved : register List.list **)
744let registerCalleeSaved =
745  List.Cons (Register20, (List.Cons (Register21, (List.Cons (Register22,
746    (List.Cons (Register23, (List.Cons (Register24, (List.Cons (Register25,
747    (List.Cons (Register26, (List.Cons (Register27, List.Nil)))))))))))))))
748
749(** val registersForbidden : register List.list **)
750let registersForbidden =
751  List.Cons (RegisterA, (List.Cons (RegisterB, (List.Cons (RegisterDPL,
752    (List.Cons (RegisterDPH, (List.Cons (registerSPL, (List.Cons
753    (registerSPH, (List.Cons (registerST0, (List.Cons (registerST1,
754    (List.Cons (registerST2, (List.Cons (registerST3, (List.Cons
755    (registerSST, List.Nil)))))))))))))))))))))
756
757(** val registersAllocatable : register List.list **)
758let registersAllocatable =
759  List.Cons (Register00, (List.Cons (Register01, (List.Cons (Register02,
760    (List.Cons (Register03, (List.Cons (Register04, (List.Cons (Register05,
761    (List.Cons (Register06, (List.Cons (Register07, (List.Cons (Register10,
762    (List.Cons (Register11, (List.Cons (Register12, (List.Cons (Register13,
763    (List.Cons (Register14, (List.Cons (Register15, (List.Cons (Register16,
764    (List.Cons (Register17, (List.Cons (Register20, (List.Cons (Register21,
765    (List.Cons (Register22, (List.Cons (Register23, (List.Cons (Register24,
766    (List.Cons (Register25, (List.Cons (Register26, (List.Cons (Register27,
767    (List.Cons (Register30, (List.Cons (Register31, (List.Cons (Register32,
768    (List.Cons (Register33, (List.Cons (Register34, (List.Cons (Register35,
769    (List.Cons (Register36, (List.Cons (Register37,
770    List.Nil)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
771
Note: See TracBrowser for help on using the repository browser.