source: driver/extracted/i8051.ml @ 3106

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