source: extracted/aSM.ml @ 2620

Last change on this file since 2620 was 2620, checked in by campbell, 8 years ago

Sufficient hacking to run the extracted Clight semantics.

File size: 199.9 KB
RevLine 
[2601]1open Preamble
2
3open Char
4
5open String
6
7open Extranat
8
9open Vector
10
11open Div_and_mod
12
13open Jmeq
14
15open Russell
16
17open Types
18
19open List
20
21open Util
22
23open FoldStuff
24
25open Bool
26
27open Hints_declaration
28
29open Core_notation
30
31open Pts
32
33open Logic
34
35open Relations
36
37open Nat
38
39open BitVector
40
41open Proper
42
43open PositiveMap
44
45open Deqsets
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Setoids
54
55open Monad
56
57open Option
58
59open Lists
60
61open Positive
62
63open Identifiers
64
65open Coqlib
66
67open Floats
68
69open Arithmetic
70
71open Integers
72
73open AST
74
75open CostLabel
76
77open LabelledObjects
78
79(** val aSMTag : String.string **)
80let aSMTag = "ASMTag"
81  (* failwith "AXIOM TO BE REALIZED" *)
82
83type identifier0 = PreIdentifiers.identifier
84
85(** val toASM_ident :
86    String.string -> PreIdentifiers.identifier -> identifier0 **)
87let toASM_ident t i =
88  let id = i in id
89
90type addressing_mode =
91| DIRECT of BitVector.byte
92| INDIRECT of BitVector.bit
93| EXT_INDIRECT of BitVector.bit
94| REGISTER of BitVector.bitVector
95| ACC_A
96| ACC_B
97| DPTR
98| DATA of BitVector.byte
99| DATA16 of BitVector.word
100| ACC_DPTR
101| ACC_PC
102| EXT_INDIRECT_DPTR
103| INDIRECT_DPTR
104| CARRY
105| BIT_ADDR of BitVector.byte
106| N_BIT_ADDR of BitVector.byte
107| RELATIVE of BitVector.byte
108| ADDR11 of BitVector.word11
109| ADDR16 of BitVector.word
110
111(** val addressing_mode_rect_Type4 :
112    (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
113    'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 ->
114    (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1
115    -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) ->
116    (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
117    -> 'a1) -> addressing_mode -> 'a1 **)
118let rec addressing_mode_rect_Type4 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
119| DIRECT x_14702 -> h_DIRECT x_14702
120| INDIRECT x_14703 -> h_INDIRECT x_14703
121| EXT_INDIRECT x_14704 -> h_EXT_INDIRECT x_14704
122| REGISTER x_14705 -> h_REGISTER x_14705
123| ACC_A -> h_ACC_A
124| ACC_B -> h_ACC_B
125| DPTR -> h_DPTR
126| DATA x_14706 -> h_DATA x_14706
127| DATA16 x_14707 -> h_DATA16 x_14707
128| ACC_DPTR -> h_ACC_DPTR
129| ACC_PC -> h_ACC_PC
130| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
131| INDIRECT_DPTR -> h_INDIRECT_DPTR
132| CARRY -> h_CARRY
133| BIT_ADDR x_14708 -> h_BIT_ADDR x_14708
134| N_BIT_ADDR x_14709 -> h_N_BIT_ADDR x_14709
135| RELATIVE x_14710 -> h_RELATIVE x_14710
136| ADDR11 x_14711 -> h_ADDR11 x_14711
137| ADDR16 x_14712 -> h_ADDR16 x_14712
138
139(** val addressing_mode_rect_Type5 :
140    (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
141    'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 ->
142    (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1
143    -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) ->
144    (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
145    -> 'a1) -> addressing_mode -> 'a1 **)
146let rec addressing_mode_rect_Type5 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
147| DIRECT x_14733 -> h_DIRECT x_14733
148| INDIRECT x_14734 -> h_INDIRECT x_14734
149| EXT_INDIRECT x_14735 -> h_EXT_INDIRECT x_14735
150| REGISTER x_14736 -> h_REGISTER x_14736
151| ACC_A -> h_ACC_A
152| ACC_B -> h_ACC_B
153| DPTR -> h_DPTR
154| DATA x_14737 -> h_DATA x_14737
155| DATA16 x_14738 -> h_DATA16 x_14738
156| ACC_DPTR -> h_ACC_DPTR
157| ACC_PC -> h_ACC_PC
158| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
159| INDIRECT_DPTR -> h_INDIRECT_DPTR
160| CARRY -> h_CARRY
161| BIT_ADDR x_14739 -> h_BIT_ADDR x_14739
162| N_BIT_ADDR x_14740 -> h_N_BIT_ADDR x_14740
163| RELATIVE x_14741 -> h_RELATIVE x_14741
164| ADDR11 x_14742 -> h_ADDR11 x_14742
165| ADDR16 x_14743 -> h_ADDR16 x_14743
166
167(** val addressing_mode_rect_Type3 :
168    (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
169    'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 ->
170    (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1
171    -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) ->
172    (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
173    -> 'a1) -> addressing_mode -> 'a1 **)
174let rec addressing_mode_rect_Type3 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
175| DIRECT x_14764 -> h_DIRECT x_14764
176| INDIRECT x_14765 -> h_INDIRECT x_14765
177| EXT_INDIRECT x_14766 -> h_EXT_INDIRECT x_14766
178| REGISTER x_14767 -> h_REGISTER x_14767
179| ACC_A -> h_ACC_A
180| ACC_B -> h_ACC_B
181| DPTR -> h_DPTR
182| DATA x_14768 -> h_DATA x_14768
183| DATA16 x_14769 -> h_DATA16 x_14769
184| ACC_DPTR -> h_ACC_DPTR
185| ACC_PC -> h_ACC_PC
186| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
187| INDIRECT_DPTR -> h_INDIRECT_DPTR
188| CARRY -> h_CARRY
189| BIT_ADDR x_14770 -> h_BIT_ADDR x_14770
190| N_BIT_ADDR x_14771 -> h_N_BIT_ADDR x_14771
191| RELATIVE x_14772 -> h_RELATIVE x_14772
192| ADDR11 x_14773 -> h_ADDR11 x_14773
193| ADDR16 x_14774 -> h_ADDR16 x_14774
194
195(** val addressing_mode_rect_Type2 :
196    (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
197    'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 ->
198    (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1
199    -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) ->
200    (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
201    -> 'a1) -> addressing_mode -> 'a1 **)
202let rec addressing_mode_rect_Type2 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
203| DIRECT x_14795 -> h_DIRECT x_14795
204| INDIRECT x_14796 -> h_INDIRECT x_14796
205| EXT_INDIRECT x_14797 -> h_EXT_INDIRECT x_14797
206| REGISTER x_14798 -> h_REGISTER x_14798
207| ACC_A -> h_ACC_A
208| ACC_B -> h_ACC_B
209| DPTR -> h_DPTR
210| DATA x_14799 -> h_DATA x_14799
211| DATA16 x_14800 -> h_DATA16 x_14800
212| ACC_DPTR -> h_ACC_DPTR
213| ACC_PC -> h_ACC_PC
214| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
215| INDIRECT_DPTR -> h_INDIRECT_DPTR
216| CARRY -> h_CARRY
217| BIT_ADDR x_14801 -> h_BIT_ADDR x_14801
218| N_BIT_ADDR x_14802 -> h_N_BIT_ADDR x_14802
219| RELATIVE x_14803 -> h_RELATIVE x_14803
220| ADDR11 x_14804 -> h_ADDR11 x_14804
221| ADDR16 x_14805 -> h_ADDR16 x_14805
222
223(** val addressing_mode_rect_Type1 :
224    (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
225    'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 ->
226    (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1
227    -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) ->
228    (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
229    -> 'a1) -> addressing_mode -> 'a1 **)
230let rec addressing_mode_rect_Type1 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
231| DIRECT x_14826 -> h_DIRECT x_14826
232| INDIRECT x_14827 -> h_INDIRECT x_14827
233| EXT_INDIRECT x_14828 -> h_EXT_INDIRECT x_14828
234| REGISTER x_14829 -> h_REGISTER x_14829
235| ACC_A -> h_ACC_A
236| ACC_B -> h_ACC_B
237| DPTR -> h_DPTR
238| DATA x_14830 -> h_DATA x_14830
239| DATA16 x_14831 -> h_DATA16 x_14831
240| ACC_DPTR -> h_ACC_DPTR
241| ACC_PC -> h_ACC_PC
242| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
243| INDIRECT_DPTR -> h_INDIRECT_DPTR
244| CARRY -> h_CARRY
245| BIT_ADDR x_14832 -> h_BIT_ADDR x_14832
246| N_BIT_ADDR x_14833 -> h_N_BIT_ADDR x_14833
247| RELATIVE x_14834 -> h_RELATIVE x_14834
248| ADDR11 x_14835 -> h_ADDR11 x_14835
249| ADDR16 x_14836 -> h_ADDR16 x_14836
250
251(** val addressing_mode_rect_Type0 :
252    (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
253    'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 ->
254    (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1
255    -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) ->
256    (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
257    -> 'a1) -> addressing_mode -> 'a1 **)
258let rec addressing_mode_rect_Type0 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
259| DIRECT x_14857 -> h_DIRECT x_14857
260| INDIRECT x_14858 -> h_INDIRECT x_14858
261| EXT_INDIRECT x_14859 -> h_EXT_INDIRECT x_14859
262| REGISTER x_14860 -> h_REGISTER x_14860
263| ACC_A -> h_ACC_A
264| ACC_B -> h_ACC_B
265| DPTR -> h_DPTR
266| DATA x_14861 -> h_DATA x_14861
267| DATA16 x_14862 -> h_DATA16 x_14862
268| ACC_DPTR -> h_ACC_DPTR
269| ACC_PC -> h_ACC_PC
270| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
271| INDIRECT_DPTR -> h_INDIRECT_DPTR
272| CARRY -> h_CARRY
273| BIT_ADDR x_14863 -> h_BIT_ADDR x_14863
274| N_BIT_ADDR x_14864 -> h_N_BIT_ADDR x_14864
275| RELATIVE x_14865 -> h_RELATIVE x_14865
276| ADDR11 x_14866 -> h_ADDR11 x_14866
277| ADDR16 x_14867 -> h_ADDR16 x_14867
278
279(** val addressing_mode_inv_rect_Type4 :
280    addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __
281    -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ ->
282    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte ->
283    __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
284    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
285    'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
286    (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **)
287let addressing_mode_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
288  let hcut =
289    addressing_mode_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
290      h15 h16 h17 h18 h19 hterm
291  in
292  hcut __
293
294(** val addressing_mode_inv_rect_Type3 :
295    addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __
296    -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ ->
297    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte ->
298    __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
299    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
300    'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
301    (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **)
302let addressing_mode_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
303  let hcut =
304    addressing_mode_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
305      h15 h16 h17 h18 h19 hterm
306  in
307  hcut __
308
309(** val addressing_mode_inv_rect_Type2 :
310    addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __
311    -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ ->
312    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte ->
313    __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
314    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
315    'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
316    (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **)
317let addressing_mode_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
318  let hcut =
319    addressing_mode_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
320      h15 h16 h17 h18 h19 hterm
321  in
322  hcut __
323
324(** val addressing_mode_inv_rect_Type1 :
325    addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __
326    -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ ->
327    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte ->
328    __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
329    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
330    'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
331    (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **)
332let addressing_mode_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
333  let hcut =
334    addressing_mode_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
335      h15 h16 h17 h18 h19 hterm
336  in
337  hcut __
338
339(** val addressing_mode_inv_rect_Type0 :
340    addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __
341    -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ ->
342    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte ->
343    __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
344    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
345    'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
346    (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **)
347let addressing_mode_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
348  let hcut =
349    addressing_mode_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
350      h15 h16 h17 h18 h19 hterm
351  in
352  hcut __
353
354(** val addressing_mode_discr : addressing_mode -> addressing_mode -> __ **)
355let addressing_mode_discr x y =
356  Logic.eq_rect_Type2 x
357    (match x with
358     | DIRECT a0 -> Obj.magic (fun _ dH -> dH __)
359     | INDIRECT a0 -> Obj.magic (fun _ dH -> dH __)
360     | EXT_INDIRECT a0 -> Obj.magic (fun _ dH -> dH __)
361     | REGISTER a0 -> Obj.magic (fun _ dH -> dH __)
362     | ACC_A -> Obj.magic (fun _ dH -> dH)
363     | ACC_B -> Obj.magic (fun _ dH -> dH)
364     | DPTR -> Obj.magic (fun _ dH -> dH)
365     | DATA a0 -> Obj.magic (fun _ dH -> dH __)
366     | DATA16 a0 -> Obj.magic (fun _ dH -> dH __)
367     | ACC_DPTR -> Obj.magic (fun _ dH -> dH)
368     | ACC_PC -> Obj.magic (fun _ dH -> dH)
369     | EXT_INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH)
370     | INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH)
371     | CARRY -> Obj.magic (fun _ dH -> dH)
372     | BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __)
373     | N_BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __)
374     | RELATIVE a0 -> Obj.magic (fun _ dH -> dH __)
375     | ADDR11 a0 -> Obj.magic (fun _ dH -> dH __)
376     | ADDR16 a0 -> Obj.magic (fun _ dH -> dH __)) y
377
378(** val addressing_mode_jmdiscr :
379    addressing_mode -> addressing_mode -> __ **)
380let addressing_mode_jmdiscr x y =
381  Logic.eq_rect_Type2 x
382    (match x with
383     | DIRECT a0 -> Obj.magic (fun _ dH -> dH __)
384     | INDIRECT a0 -> Obj.magic (fun _ dH -> dH __)
385     | EXT_INDIRECT a0 -> Obj.magic (fun _ dH -> dH __)
386     | REGISTER a0 -> Obj.magic (fun _ dH -> dH __)
387     | ACC_A -> Obj.magic (fun _ dH -> dH)
388     | ACC_B -> Obj.magic (fun _ dH -> dH)
389     | DPTR -> Obj.magic (fun _ dH -> dH)
390     | DATA a0 -> Obj.magic (fun _ dH -> dH __)
391     | DATA16 a0 -> Obj.magic (fun _ dH -> dH __)
392     | ACC_DPTR -> Obj.magic (fun _ dH -> dH)
393     | ACC_PC -> Obj.magic (fun _ dH -> dH)
394     | EXT_INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH)
395     | INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH)
396     | CARRY -> Obj.magic (fun _ dH -> dH)
397     | BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __)
398     | N_BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __)
399     | RELATIVE a0 -> Obj.magic (fun _ dH -> dH __)
400     | ADDR11 a0 -> Obj.magic (fun _ dH -> dH __)
401     | ADDR16 a0 -> Obj.magic (fun _ dH -> dH __)) y
402
403(** val eq_addressing_mode :
404    addressing_mode -> addressing_mode -> Bool.bool **)
405let eq_addressing_mode a b =
406  match a with
407  | DIRECT d ->
408    (match b with
409     | DIRECT e0 ->
410       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
411         (Nat.S Nat.O)))))))) d e0
412     | INDIRECT x -> Bool.False
413     | EXT_INDIRECT x -> Bool.False
414     | REGISTER x -> Bool.False
415     | ACC_A -> Bool.False
416     | ACC_B -> Bool.False
417     | DPTR -> Bool.False
418     | DATA x -> Bool.False
419     | DATA16 x -> Bool.False
420     | ACC_DPTR -> Bool.False
421     | ACC_PC -> Bool.False
422     | EXT_INDIRECT_DPTR -> Bool.False
423     | INDIRECT_DPTR -> Bool.False
424     | CARRY -> Bool.False
425     | BIT_ADDR x -> Bool.False
426     | N_BIT_ADDR x -> Bool.False
427     | RELATIVE x -> Bool.False
428     | ADDR11 x -> Bool.False
429     | ADDR16 x -> Bool.False)
430  | INDIRECT b' ->
431    (match b with
432     | DIRECT x -> Bool.False
433     | INDIRECT e0 -> BitVector.eq_b b' e0
434     | EXT_INDIRECT x -> Bool.False
435     | REGISTER x -> Bool.False
436     | ACC_A -> Bool.False
437     | ACC_B -> Bool.False
438     | DPTR -> Bool.False
439     | DATA x -> Bool.False
440     | DATA16 x -> Bool.False
441     | ACC_DPTR -> Bool.False
442     | ACC_PC -> Bool.False
443     | EXT_INDIRECT_DPTR -> Bool.False
444     | INDIRECT_DPTR -> Bool.False
445     | CARRY -> Bool.False
446     | BIT_ADDR x -> Bool.False
447     | N_BIT_ADDR x -> Bool.False
448     | RELATIVE x -> Bool.False
449     | ADDR11 x -> Bool.False
450     | ADDR16 x -> Bool.False)
451  | EXT_INDIRECT b' ->
452    (match b with
453     | DIRECT x -> Bool.False
454     | INDIRECT x -> Bool.False
455     | EXT_INDIRECT e0 -> BitVector.eq_b b' e0
456     | REGISTER x -> Bool.False
457     | ACC_A -> Bool.False
458     | ACC_B -> Bool.False
459     | DPTR -> Bool.False
460     | DATA x -> Bool.False
461     | DATA16 x -> Bool.False
462     | ACC_DPTR -> Bool.False
463     | ACC_PC -> Bool.False
464     | EXT_INDIRECT_DPTR -> Bool.False
465     | INDIRECT_DPTR -> Bool.False
466     | CARRY -> Bool.False
467     | BIT_ADDR x -> Bool.False
468     | N_BIT_ADDR x -> Bool.False
469     | RELATIVE x -> Bool.False
470     | ADDR11 x -> Bool.False
471     | ADDR16 x -> Bool.False)
472  | REGISTER bv ->
473    (match b with
474     | DIRECT x -> Bool.False
475     | INDIRECT x -> Bool.False
476     | EXT_INDIRECT x -> Bool.False
477     | REGISTER bv' -> BitVector.eq_bv (Nat.S (Nat.S (Nat.S Nat.O))) bv bv'
478     | ACC_A -> Bool.False
479     | ACC_B -> Bool.False
480     | DPTR -> Bool.False
481     | DATA x -> Bool.False
482     | DATA16 x -> Bool.False
483     | ACC_DPTR -> Bool.False
484     | ACC_PC -> Bool.False
485     | EXT_INDIRECT_DPTR -> Bool.False
486     | INDIRECT_DPTR -> Bool.False
487     | CARRY -> Bool.False
488     | BIT_ADDR x -> Bool.False
489     | N_BIT_ADDR x -> Bool.False
490     | RELATIVE x -> Bool.False
491     | ADDR11 x -> Bool.False
492     | ADDR16 x -> Bool.False)
493  | ACC_A ->
494    (match b with
495     | DIRECT x -> Bool.False
496     | INDIRECT x -> Bool.False
497     | EXT_INDIRECT x -> Bool.False
498     | REGISTER x -> Bool.False
499     | ACC_A -> Bool.True
500     | ACC_B -> Bool.False
501     | DPTR -> Bool.False
502     | DATA x -> Bool.False
503     | DATA16 x -> Bool.False
504     | ACC_DPTR -> Bool.False
505     | ACC_PC -> Bool.False
506     | EXT_INDIRECT_DPTR -> Bool.False
507     | INDIRECT_DPTR -> Bool.False
508     | CARRY -> Bool.False
509     | BIT_ADDR x -> Bool.False
510     | N_BIT_ADDR x -> Bool.False
511     | RELATIVE x -> Bool.False
512     | ADDR11 x -> Bool.False
513     | ADDR16 x -> Bool.False)
514  | ACC_B ->
515    (match b with
516     | DIRECT x -> Bool.False
517     | INDIRECT x -> Bool.False
518     | EXT_INDIRECT x -> Bool.False
519     | REGISTER x -> Bool.False
520     | ACC_A -> Bool.False
521     | ACC_B -> Bool.True
522     | DPTR -> Bool.False
523     | DATA x -> Bool.False
524     | DATA16 x -> Bool.False
525     | ACC_DPTR -> Bool.False
526     | ACC_PC -> Bool.False
527     | EXT_INDIRECT_DPTR -> Bool.False
528     | INDIRECT_DPTR -> Bool.False
529     | CARRY -> Bool.False
530     | BIT_ADDR x -> Bool.False
531     | N_BIT_ADDR x -> Bool.False
532     | RELATIVE x -> Bool.False
533     | ADDR11 x -> Bool.False
534     | ADDR16 x -> Bool.False)
535  | DPTR ->
536    (match b with
537     | DIRECT x -> Bool.False
538     | INDIRECT x -> Bool.False
539     | EXT_INDIRECT x -> Bool.False
540     | REGISTER x -> Bool.False
541     | ACC_A -> Bool.False
542     | ACC_B -> Bool.False
543     | DPTR -> Bool.True
544     | DATA x -> Bool.False
545     | DATA16 x -> Bool.False
546     | ACC_DPTR -> Bool.False
547     | ACC_PC -> Bool.False
548     | EXT_INDIRECT_DPTR -> Bool.False
549     | INDIRECT_DPTR -> Bool.False
550     | CARRY -> Bool.False
551     | BIT_ADDR x -> Bool.False
552     | N_BIT_ADDR x -> Bool.False
553     | RELATIVE x -> Bool.False
554     | ADDR11 x -> Bool.False
555     | ADDR16 x -> Bool.False)
556  | DATA b' ->
557    (match b with
558     | DIRECT x -> Bool.False
559     | INDIRECT x -> Bool.False
560     | EXT_INDIRECT x -> Bool.False
561     | REGISTER x -> Bool.False
562     | ACC_A -> Bool.False
563     | ACC_B -> Bool.False
564     | DPTR -> Bool.False
565     | DATA e0 ->
566       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
567         (Nat.S Nat.O)))))))) b' e0
568     | DATA16 x -> Bool.False
569     | ACC_DPTR -> Bool.False
570     | ACC_PC -> Bool.False
571     | EXT_INDIRECT_DPTR -> Bool.False
572     | INDIRECT_DPTR -> Bool.False
573     | CARRY -> Bool.False
574     | BIT_ADDR x -> Bool.False
575     | N_BIT_ADDR x -> Bool.False
576     | RELATIVE x -> Bool.False
577     | ADDR11 x -> Bool.False
578     | ADDR16 x -> Bool.False)
579  | DATA16 w ->
580    (match b with
581     | DIRECT x -> Bool.False
582     | INDIRECT x -> Bool.False
583     | EXT_INDIRECT x -> Bool.False
584     | REGISTER x -> Bool.False
585     | ACC_A -> Bool.False
586     | ACC_B -> Bool.False
587     | DPTR -> Bool.False
588     | DATA x -> Bool.False
589     | DATA16 e0 ->
590       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
591         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
592         Nat.O)))))))))))))))) w e0
593     | ACC_DPTR -> Bool.False
594     | ACC_PC -> Bool.False
595     | EXT_INDIRECT_DPTR -> Bool.False
596     | INDIRECT_DPTR -> Bool.False
597     | CARRY -> Bool.False
598     | BIT_ADDR x -> Bool.False
599     | N_BIT_ADDR x -> Bool.False
600     | RELATIVE x -> Bool.False
601     | ADDR11 x -> Bool.False
602     | ADDR16 x -> Bool.False)
603  | ACC_DPTR ->
604    (match b with
605     | DIRECT x -> Bool.False
606     | INDIRECT x -> Bool.False
607     | EXT_INDIRECT x -> Bool.False
608     | REGISTER x -> Bool.False
609     | ACC_A -> Bool.False
610     | ACC_B -> Bool.False
611     | DPTR -> Bool.False
612     | DATA x -> Bool.False
613     | DATA16 x -> Bool.False
614     | ACC_DPTR -> Bool.True
615     | ACC_PC -> Bool.False
616     | EXT_INDIRECT_DPTR -> Bool.False
617     | INDIRECT_DPTR -> Bool.False
618     | CARRY -> Bool.False
619     | BIT_ADDR x -> Bool.False
620     | N_BIT_ADDR x -> Bool.False
621     | RELATIVE x -> Bool.False
622     | ADDR11 x -> Bool.False
623     | ADDR16 x -> Bool.False)
624  | ACC_PC ->
625    (match b with
626     | DIRECT x -> Bool.False
627     | INDIRECT x -> Bool.False
628     | EXT_INDIRECT x -> Bool.False
629     | REGISTER x -> Bool.False
630     | ACC_A -> Bool.False
631     | ACC_B -> Bool.False
632     | DPTR -> Bool.False
633     | DATA x -> Bool.False
634     | DATA16 x -> Bool.False
635     | ACC_DPTR -> Bool.False
636     | ACC_PC -> Bool.True
637     | EXT_INDIRECT_DPTR -> Bool.False
638     | INDIRECT_DPTR -> Bool.False
639     | CARRY -> Bool.False
640     | BIT_ADDR x -> Bool.False
641     | N_BIT_ADDR x -> Bool.False
642     | RELATIVE x -> Bool.False
643     | ADDR11 x -> Bool.False
644     | ADDR16 x -> Bool.False)
645  | EXT_INDIRECT_DPTR ->
646    (match b with
647     | DIRECT x -> Bool.False
648     | INDIRECT x -> Bool.False
649     | EXT_INDIRECT x -> Bool.False
650     | REGISTER x -> Bool.False
651     | ACC_A -> Bool.False
652     | ACC_B -> Bool.False
653     | DPTR -> Bool.False
654     | DATA x -> Bool.False
655     | DATA16 x -> Bool.False
656     | ACC_DPTR -> Bool.False
657     | ACC_PC -> Bool.False
658     | EXT_INDIRECT_DPTR -> Bool.True
659     | INDIRECT_DPTR -> Bool.False
660     | CARRY -> Bool.False
661     | BIT_ADDR x -> Bool.False
662     | N_BIT_ADDR x -> Bool.False
663     | RELATIVE x -> Bool.False
664     | ADDR11 x -> Bool.False
665     | ADDR16 x -> Bool.False)
666  | INDIRECT_DPTR ->
667    (match b with
668     | DIRECT x -> Bool.False
669     | INDIRECT x -> Bool.False
670     | EXT_INDIRECT x -> Bool.False
671     | REGISTER x -> Bool.False
672     | ACC_A -> Bool.False
673     | ACC_B -> Bool.False
674     | DPTR -> Bool.False
675     | DATA x -> Bool.False
676     | DATA16 x -> Bool.False
677     | ACC_DPTR -> Bool.False
678     | ACC_PC -> Bool.False
679     | EXT_INDIRECT_DPTR -> Bool.False
680     | INDIRECT_DPTR -> Bool.True
681     | CARRY -> Bool.False
682     | BIT_ADDR x -> Bool.False
683     | N_BIT_ADDR x -> Bool.False
684     | RELATIVE x -> Bool.False
685     | ADDR11 x -> Bool.False
686     | ADDR16 x -> Bool.False)
687  | CARRY ->
688    (match b with
689     | DIRECT x -> Bool.False
690     | INDIRECT x -> Bool.False
691     | EXT_INDIRECT x -> Bool.False
692     | REGISTER x -> Bool.False
693     | ACC_A -> Bool.False
694     | ACC_B -> Bool.False
695     | DPTR -> Bool.False
696     | DATA x -> Bool.False
697     | DATA16 x -> Bool.False
698     | ACC_DPTR -> Bool.False
699     | ACC_PC -> Bool.False
700     | EXT_INDIRECT_DPTR -> Bool.False
701     | INDIRECT_DPTR -> Bool.False
702     | CARRY -> Bool.True
703     | BIT_ADDR x -> Bool.False
704     | N_BIT_ADDR x -> Bool.False
705     | RELATIVE x -> Bool.False
706     | ADDR11 x -> Bool.False
707     | ADDR16 x -> Bool.False)
708  | BIT_ADDR b' ->
709    (match b with
710     | DIRECT x -> Bool.False
711     | INDIRECT x -> Bool.False
712     | EXT_INDIRECT x -> Bool.False
713     | REGISTER x -> Bool.False
714     | ACC_A -> Bool.False
715     | ACC_B -> Bool.False
716     | DPTR -> Bool.False
717     | DATA x -> Bool.False
718     | DATA16 x -> Bool.False
719     | ACC_DPTR -> Bool.False
720     | ACC_PC -> Bool.False
721     | EXT_INDIRECT_DPTR -> Bool.False
722     | INDIRECT_DPTR -> Bool.False
723     | CARRY -> Bool.False
724     | BIT_ADDR e0 ->
725       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
726         (Nat.S Nat.O)))))))) b' e0
727     | N_BIT_ADDR x -> Bool.False
728     | RELATIVE x -> Bool.False
729     | ADDR11 x -> Bool.False
730     | ADDR16 x -> Bool.False)
731  | N_BIT_ADDR b' ->
732    (match b with
733     | DIRECT x -> Bool.False
734     | INDIRECT x -> Bool.False
735     | EXT_INDIRECT x -> Bool.False
736     | REGISTER x -> Bool.False
737     | ACC_A -> Bool.False
738     | ACC_B -> Bool.False
739     | DPTR -> Bool.False
740     | DATA x -> Bool.False
741     | DATA16 x -> Bool.False
742     | ACC_DPTR -> Bool.False
743     | ACC_PC -> Bool.False
744     | EXT_INDIRECT_DPTR -> Bool.False
745     | INDIRECT_DPTR -> Bool.False
746     | CARRY -> Bool.False
747     | BIT_ADDR x -> Bool.False
748     | N_BIT_ADDR e0 ->
749       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
750         (Nat.S Nat.O)))))))) b' e0
751     | RELATIVE x -> Bool.False
752     | ADDR11 x -> Bool.False
753     | ADDR16 x -> Bool.False)
754  | RELATIVE n ->
755    (match b with
756     | DIRECT x -> Bool.False
757     | INDIRECT x -> Bool.False
758     | EXT_INDIRECT x -> Bool.False
759     | REGISTER x -> Bool.False
760     | ACC_A -> Bool.False
761     | ACC_B -> Bool.False
762     | DPTR -> Bool.False
763     | DATA x -> Bool.False
764     | DATA16 x -> Bool.False
765     | ACC_DPTR -> Bool.False
766     | ACC_PC -> Bool.False
767     | EXT_INDIRECT_DPTR -> Bool.False
768     | INDIRECT_DPTR -> Bool.False
769     | CARRY -> Bool.False
770     | BIT_ADDR x -> Bool.False
771     | N_BIT_ADDR x -> Bool.False
772     | RELATIVE e0 ->
773       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
774         (Nat.S Nat.O)))))))) n e0
775     | ADDR11 x -> Bool.False
776     | ADDR16 x -> Bool.False)
777  | ADDR11 w ->
778    (match b with
779     | DIRECT x -> Bool.False
780     | INDIRECT x -> Bool.False
781     | EXT_INDIRECT x -> Bool.False
782     | REGISTER x -> Bool.False
783     | ACC_A -> Bool.False
784     | ACC_B -> Bool.False
785     | DPTR -> Bool.False
786     | DATA x -> Bool.False
787     | DATA16 x -> Bool.False
788     | ACC_DPTR -> Bool.False
789     | ACC_PC -> Bool.False
790     | EXT_INDIRECT_DPTR -> Bool.False
791     | INDIRECT_DPTR -> Bool.False
792     | CARRY -> Bool.False
793     | BIT_ADDR x -> Bool.False
794     | N_BIT_ADDR x -> Bool.False
795     | RELATIVE x -> Bool.False
796     | ADDR11 e0 ->
797       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
798         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))) w e0
799     | ADDR16 x -> Bool.False)
800  | ADDR16 w ->
801    (match b with
802     | DIRECT x -> Bool.False
803     | INDIRECT x -> Bool.False
804     | EXT_INDIRECT x -> Bool.False
805     | REGISTER x -> Bool.False
806     | ACC_A -> Bool.False
807     | ACC_B -> Bool.False
808     | DPTR -> Bool.False
809     | DATA x -> Bool.False
810     | DATA16 x -> Bool.False
811     | ACC_DPTR -> Bool.False
812     | ACC_PC -> Bool.False
813     | EXT_INDIRECT_DPTR -> Bool.False
814     | INDIRECT_DPTR -> Bool.False
815     | CARRY -> Bool.False
816     | BIT_ADDR x -> Bool.False
817     | N_BIT_ADDR x -> Bool.False
818     | RELATIVE x -> Bool.False
819     | ADDR11 x -> Bool.False
820     | ADDR16 e0 ->
821       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
822         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
823         Nat.O)))))))))))))))) w e0)
824
825type addressing_mode_tag =
826| Direct
827| Indirect
828| Ext_indirect
829| Registr
830| Acc_a
831| Acc_b
832| Dptr
833| Data
834| Data16
835| Acc_dptr
836| Acc_pc
837| Ext_indirect_dptr
838| Indirect_dptr
839| Carry
840| Bit_addr
841| N_bit_addr
842| Relative
843| Addr11
844| Addr16
845
846(** val addressing_mode_tag_rect_Type4 :
847    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
848    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
849    addressing_mode_tag -> 'a1 **)
850let rec addressing_mode_tag_rect_Type4 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function
851| Direct -> h_direct
852| Indirect -> h_indirect
853| Ext_indirect -> h_ext_indirect
854| Registr -> h_registr
855| Acc_a -> h_acc_a
856| Acc_b -> h_acc_b
857| Dptr -> h_dptr
858| Data -> h_data
859| Data16 -> h_data16
860| Acc_dptr -> h_acc_dptr
861| Acc_pc -> h_acc_pc
862| Ext_indirect_dptr -> h_ext_indirect_dptr
863| Indirect_dptr -> h_indirect_dptr
864| Carry -> h_carry
865| Bit_addr -> h_bit_addr
866| N_bit_addr -> h_n_bit_addr
867| Relative -> h_relative
868| Addr11 -> h_addr11
869| Addr16 -> h_addr16
870
871(** val addressing_mode_tag_rect_Type5 :
872    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
873    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
874    addressing_mode_tag -> 'a1 **)
875let rec addressing_mode_tag_rect_Type5 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function
876| Direct -> h_direct
877| Indirect -> h_indirect
878| Ext_indirect -> h_ext_indirect
879| Registr -> h_registr
880| Acc_a -> h_acc_a
881| Acc_b -> h_acc_b
882| Dptr -> h_dptr
883| Data -> h_data
884| Data16 -> h_data16
885| Acc_dptr -> h_acc_dptr
886| Acc_pc -> h_acc_pc
887| Ext_indirect_dptr -> h_ext_indirect_dptr
888| Indirect_dptr -> h_indirect_dptr
889| Carry -> h_carry
890| Bit_addr -> h_bit_addr
891| N_bit_addr -> h_n_bit_addr
892| Relative -> h_relative
893| Addr11 -> h_addr11
894| Addr16 -> h_addr16
895
896(** val addressing_mode_tag_rect_Type3 :
897    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
898    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
899    addressing_mode_tag -> 'a1 **)
900let rec addressing_mode_tag_rect_Type3 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function
901| Direct -> h_direct
902| Indirect -> h_indirect
903| Ext_indirect -> h_ext_indirect
904| Registr -> h_registr
905| Acc_a -> h_acc_a
906| Acc_b -> h_acc_b
907| Dptr -> h_dptr
908| Data -> h_data
909| Data16 -> h_data16
910| Acc_dptr -> h_acc_dptr
911| Acc_pc -> h_acc_pc
912| Ext_indirect_dptr -> h_ext_indirect_dptr
913| Indirect_dptr -> h_indirect_dptr
914| Carry -> h_carry
915| Bit_addr -> h_bit_addr
916| N_bit_addr -> h_n_bit_addr
917| Relative -> h_relative
918| Addr11 -> h_addr11
919| Addr16 -> h_addr16
920
921(** val addressing_mode_tag_rect_Type2 :
922    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
923    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
924    addressing_mode_tag -> 'a1 **)
925let rec addressing_mode_tag_rect_Type2 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function
926| Direct -> h_direct
927| Indirect -> h_indirect
928| Ext_indirect -> h_ext_indirect
929| Registr -> h_registr
930| Acc_a -> h_acc_a
931| Acc_b -> h_acc_b
932| Dptr -> h_dptr
933| Data -> h_data
934| Data16 -> h_data16
935| Acc_dptr -> h_acc_dptr
936| Acc_pc -> h_acc_pc
937| Ext_indirect_dptr -> h_ext_indirect_dptr
938| Indirect_dptr -> h_indirect_dptr
939| Carry -> h_carry
940| Bit_addr -> h_bit_addr
941| N_bit_addr -> h_n_bit_addr
942| Relative -> h_relative
943| Addr11 -> h_addr11
944| Addr16 -> h_addr16
945
946(** val addressing_mode_tag_rect_Type1 :
947    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
948    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
949    addressing_mode_tag -> 'a1 **)
950let rec addressing_mode_tag_rect_Type1 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function
951| Direct -> h_direct
952| Indirect -> h_indirect
953| Ext_indirect -> h_ext_indirect
954| Registr -> h_registr
955| Acc_a -> h_acc_a
956| Acc_b -> h_acc_b
957| Dptr -> h_dptr
958| Data -> h_data
959| Data16 -> h_data16
960| Acc_dptr -> h_acc_dptr
961| Acc_pc -> h_acc_pc
962| Ext_indirect_dptr -> h_ext_indirect_dptr
963| Indirect_dptr -> h_indirect_dptr
964| Carry -> h_carry
965| Bit_addr -> h_bit_addr
966| N_bit_addr -> h_n_bit_addr
967| Relative -> h_relative
968| Addr11 -> h_addr11
969| Addr16 -> h_addr16
970
971(** val addressing_mode_tag_rect_Type0 :
972    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
973    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
974    addressing_mode_tag -> 'a1 **)
975let rec addressing_mode_tag_rect_Type0 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function
976| Direct -> h_direct
977| Indirect -> h_indirect
978| Ext_indirect -> h_ext_indirect
979| Registr -> h_registr
980| Acc_a -> h_acc_a
981| Acc_b -> h_acc_b
982| Dptr -> h_dptr
983| Data -> h_data
984| Data16 -> h_data16
985| Acc_dptr -> h_acc_dptr
986| Acc_pc -> h_acc_pc
987| Ext_indirect_dptr -> h_ext_indirect_dptr
988| Indirect_dptr -> h_indirect_dptr
989| Carry -> h_carry
990| Bit_addr -> h_bit_addr
991| N_bit_addr -> h_n_bit_addr
992| Relative -> h_relative
993| Addr11 -> h_addr11
994| Addr16 -> h_addr16
995
996(** val addressing_mode_tag_inv_rect_Type4 :
997    addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
998    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
999    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
1000    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
1001    'a1) -> (__ -> 'a1) -> 'a1 **)
1002let addressing_mode_tag_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
1003  let hcut =
1004    addressing_mode_tag_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1005      h14 h15 h16 h17 h18 h19 hterm
1006  in
1007  hcut __
1008
1009(** val addressing_mode_tag_inv_rect_Type3 :
1010    addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
1011    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
1012    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
1013    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
1014    'a1) -> (__ -> 'a1) -> 'a1 **)
1015let addressing_mode_tag_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
1016  let hcut =
1017    addressing_mode_tag_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1018      h14 h15 h16 h17 h18 h19 hterm
1019  in
1020  hcut __
1021
1022(** val addressing_mode_tag_inv_rect_Type2 :
1023    addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
1024    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
1025    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
1026    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
1027    'a1) -> (__ -> 'a1) -> 'a1 **)
1028let addressing_mode_tag_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
1029  let hcut =
1030    addressing_mode_tag_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1031      h14 h15 h16 h17 h18 h19 hterm
1032  in
1033  hcut __
1034
1035(** val addressing_mode_tag_inv_rect_Type1 :
1036    addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
1037    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
1038    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
1039    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
1040    'a1) -> (__ -> 'a1) -> 'a1 **)
1041let addressing_mode_tag_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
1042  let hcut =
1043    addressing_mode_tag_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1044      h14 h15 h16 h17 h18 h19 hterm
1045  in
1046  hcut __
1047
1048(** val addressing_mode_tag_inv_rect_Type0 :
1049    addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
1050    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
1051    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
1052    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
1053    'a1) -> (__ -> 'a1) -> 'a1 **)
1054let addressing_mode_tag_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
1055  let hcut =
1056    addressing_mode_tag_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1057      h14 h15 h16 h17 h18 h19 hterm
1058  in
1059  hcut __
1060
1061(** val addressing_mode_tag_discr :
1062    addressing_mode_tag -> addressing_mode_tag -> __ **)
1063let addressing_mode_tag_discr x y =
1064  Logic.eq_rect_Type2 x
1065    (match x with
1066     | Direct -> Obj.magic (fun _ dH -> dH)
1067     | Indirect -> Obj.magic (fun _ dH -> dH)
1068     | Ext_indirect -> Obj.magic (fun _ dH -> dH)
1069     | Registr -> Obj.magic (fun _ dH -> dH)
1070     | Acc_a -> Obj.magic (fun _ dH -> dH)
1071     | Acc_b -> Obj.magic (fun _ dH -> dH)
1072     | Dptr -> Obj.magic (fun _ dH -> dH)
1073     | Data -> Obj.magic (fun _ dH -> dH)
1074     | Data16 -> Obj.magic (fun _ dH -> dH)
1075     | Acc_dptr -> Obj.magic (fun _ dH -> dH)
1076     | Acc_pc -> Obj.magic (fun _ dH -> dH)
1077     | Ext_indirect_dptr -> Obj.magic (fun _ dH -> dH)
1078     | Indirect_dptr -> Obj.magic (fun _ dH -> dH)
1079     | Carry -> Obj.magic (fun _ dH -> dH)
1080     | Bit_addr -> Obj.magic (fun _ dH -> dH)
1081     | N_bit_addr -> Obj.magic (fun _ dH -> dH)
1082     | Relative -> Obj.magic (fun _ dH -> dH)
1083     | Addr11 -> Obj.magic (fun _ dH -> dH)
1084     | Addr16 -> Obj.magic (fun _ dH -> dH)) y
1085
1086(** val addressing_mode_tag_jmdiscr :
1087    addressing_mode_tag -> addressing_mode_tag -> __ **)
1088let addressing_mode_tag_jmdiscr x y =
1089  Logic.eq_rect_Type2 x
1090    (match x with
1091     | Direct -> Obj.magic (fun _ dH -> dH)
1092     | Indirect -> Obj.magic (fun _ dH -> dH)
1093     | Ext_indirect -> Obj.magic (fun _ dH -> dH)
1094     | Registr -> Obj.magic (fun _ dH -> dH)
1095     | Acc_a -> Obj.magic (fun _ dH -> dH)
1096     | Acc_b -> Obj.magic (fun _ dH -> dH)
1097     | Dptr -> Obj.magic (fun _ dH -> dH)
1098     | Data -> Obj.magic (fun _ dH -> dH)
1099     | Data16 -> Obj.magic (fun _ dH -> dH)
1100     | Acc_dptr -> Obj.magic (fun _ dH -> dH)
1101     | Acc_pc -> Obj.magic (fun _ dH -> dH)
1102     | Ext_indirect_dptr -> Obj.magic (fun _ dH -> dH)
1103     | Indirect_dptr -> Obj.magic (fun _ dH -> dH)
1104     | Carry -> Obj.magic (fun _ dH -> dH)
1105     | Bit_addr -> Obj.magic (fun _ dH -> dH)
1106     | N_bit_addr -> Obj.magic (fun _ dH -> dH)
1107     | Relative -> Obj.magic (fun _ dH -> dH)
1108     | Addr11 -> Obj.magic (fun _ dH -> dH)
1109     | Addr16 -> Obj.magic (fun _ dH -> dH)) y
1110
1111(** val eq_a : addressing_mode_tag -> addressing_mode_tag -> Bool.bool **)
1112let eq_a a b =
1113  match a with
1114  | Direct ->
1115    (match b with
1116     | Direct -> Bool.True
1117     | Indirect -> Bool.False
1118     | Ext_indirect -> Bool.False
1119     | Registr -> Bool.False
1120     | Acc_a -> Bool.False
1121     | Acc_b -> Bool.False
1122     | Dptr -> Bool.False
1123     | Data -> Bool.False
1124     | Data16 -> Bool.False
1125     | Acc_dptr -> Bool.False
1126     | Acc_pc -> Bool.False
1127     | Ext_indirect_dptr -> Bool.False
1128     | Indirect_dptr -> Bool.False
1129     | Carry -> Bool.False
1130     | Bit_addr -> Bool.False
1131     | N_bit_addr -> Bool.False
1132     | Relative -> Bool.False
1133     | Addr11 -> Bool.False
1134     | Addr16 -> Bool.False)
1135  | Indirect ->
1136    (match b with
1137     | Direct -> Bool.False
1138     | Indirect -> Bool.True
1139     | Ext_indirect -> Bool.False
1140     | Registr -> Bool.False
1141     | Acc_a -> Bool.False
1142     | Acc_b -> Bool.False
1143     | Dptr -> Bool.False
1144     | Data -> Bool.False
1145     | Data16 -> Bool.False
1146     | Acc_dptr -> Bool.False
1147     | Acc_pc -> Bool.False
1148     | Ext_indirect_dptr -> Bool.False
1149     | Indirect_dptr -> Bool.False
1150     | Carry -> Bool.False
1151     | Bit_addr -> Bool.False
1152     | N_bit_addr -> Bool.False
1153     | Relative -> Bool.False
1154     | Addr11 -> Bool.False
1155     | Addr16 -> Bool.False)
1156  | Ext_indirect ->
1157    (match b with
1158     | Direct -> Bool.False
1159     | Indirect -> Bool.False
1160     | Ext_indirect -> Bool.True
1161     | Registr -> Bool.False
1162     | Acc_a -> Bool.False
1163     | Acc_b -> Bool.False
1164     | Dptr -> Bool.False
1165     | Data -> Bool.False
1166     | Data16 -> Bool.False
1167     | Acc_dptr -> Bool.False
1168     | Acc_pc -> Bool.False
1169     | Ext_indirect_dptr -> Bool.False
1170     | Indirect_dptr -> Bool.False
1171     | Carry -> Bool.False
1172     | Bit_addr -> Bool.False
1173     | N_bit_addr -> Bool.False
1174     | Relative -> Bool.False
1175     | Addr11 -> Bool.False
1176     | Addr16 -> Bool.False)
1177  | Registr ->
1178    (match b with
1179     | Direct -> Bool.False
1180     | Indirect -> Bool.False
1181     | Ext_indirect -> Bool.False
1182     | Registr -> Bool.True
1183     | Acc_a -> Bool.False
1184     | Acc_b -> Bool.False
1185     | Dptr -> Bool.False
1186     | Data -> Bool.False
1187     | Data16 -> Bool.False
1188     | Acc_dptr -> Bool.False
1189     | Acc_pc -> Bool.False
1190     | Ext_indirect_dptr -> Bool.False
1191     | Indirect_dptr -> Bool.False
1192     | Carry -> Bool.False
1193     | Bit_addr -> Bool.False
1194     | N_bit_addr -> Bool.False
1195     | Relative -> Bool.False
1196     | Addr11 -> Bool.False
1197     | Addr16 -> Bool.False)
1198  | Acc_a ->
1199    (match b with
1200     | Direct -> Bool.False
1201     | Indirect -> Bool.False
1202     | Ext_indirect -> Bool.False
1203     | Registr -> Bool.False
1204     | Acc_a -> Bool.True
1205     | Acc_b -> Bool.False
1206     | Dptr -> Bool.False
1207     | Data -> Bool.False
1208     | Data16 -> Bool.False
1209     | Acc_dptr -> Bool.False
1210     | Acc_pc -> Bool.False
1211     | Ext_indirect_dptr -> Bool.False
1212     | Indirect_dptr -> Bool.False
1213     | Carry -> Bool.False
1214     | Bit_addr -> Bool.False
1215     | N_bit_addr -> Bool.False
1216     | Relative -> Bool.False
1217     | Addr11 -> Bool.False
1218     | Addr16 -> Bool.False)
1219  | Acc_b ->
1220    (match b with
1221     | Direct -> Bool.False
1222     | Indirect -> Bool.False
1223     | Ext_indirect -> Bool.False
1224     | Registr -> Bool.False
1225     | Acc_a -> Bool.False
1226     | Acc_b -> Bool.True
1227     | Dptr -> Bool.False
1228     | Data -> Bool.False
1229     | Data16 -> Bool.False
1230     | Acc_dptr -> Bool.False
1231     | Acc_pc -> Bool.False
1232     | Ext_indirect_dptr -> Bool.False
1233     | Indirect_dptr -> Bool.False
1234     | Carry -> Bool.False
1235     | Bit_addr -> Bool.False
1236     | N_bit_addr -> Bool.False
1237     | Relative -> Bool.False
1238     | Addr11 -> Bool.False
1239     | Addr16 -> Bool.False)
1240  | Dptr ->
1241    (match b with
1242     | Direct -> Bool.False
1243     | Indirect -> Bool.False
1244     | Ext_indirect -> Bool.False
1245     | Registr -> Bool.False
1246     | Acc_a -> Bool.False
1247     | Acc_b -> Bool.False
1248     | Dptr -> Bool.True
1249     | Data -> Bool.False
1250     | Data16 -> Bool.False
1251     | Acc_dptr -> Bool.False
1252     | Acc_pc -> Bool.False
1253     | Ext_indirect_dptr -> Bool.False
1254     | Indirect_dptr -> Bool.False
1255     | Carry -> Bool.False
1256     | Bit_addr -> Bool.False
1257     | N_bit_addr -> Bool.False
1258     | Relative -> Bool.False
1259     | Addr11 -> Bool.False
1260     | Addr16 -> Bool.False)
1261  | Data ->
1262    (match b with
1263     | Direct -> Bool.False
1264     | Indirect -> Bool.False
1265     | Ext_indirect -> Bool.False
1266     | Registr -> Bool.False
1267     | Acc_a -> Bool.False
1268     | Acc_b -> Bool.False
1269     | Dptr -> Bool.False
1270     | Data -> Bool.True
1271     | Data16 -> Bool.False
1272     | Acc_dptr -> Bool.False
1273     | Acc_pc -> Bool.False
1274     | Ext_indirect_dptr -> Bool.False
1275     | Indirect_dptr -> Bool.False
1276     | Carry -> Bool.False
1277     | Bit_addr -> Bool.False
1278     | N_bit_addr -> Bool.False
1279     | Relative -> Bool.False
1280     | Addr11 -> Bool.False
1281     | Addr16 -> Bool.False)
1282  | Data16 ->
1283    (match b with
1284     | Direct -> Bool.False
1285     | Indirect -> Bool.False
1286     | Ext_indirect -> Bool.False
1287     | Registr -> Bool.False
1288     | Acc_a -> Bool.False
1289     | Acc_b -> Bool.False
1290     | Dptr -> Bool.False
1291     | Data -> Bool.False
1292     | Data16 -> Bool.True
1293     | Acc_dptr -> Bool.False
1294     | Acc_pc -> Bool.False
1295     | Ext_indirect_dptr -> Bool.False
1296     | Indirect_dptr -> Bool.False
1297     | Carry -> Bool.False
1298     | Bit_addr -> Bool.False
1299     | N_bit_addr -> Bool.False
1300     | Relative -> Bool.False
1301     | Addr11 -> Bool.False
1302     | Addr16 -> Bool.False)
1303  | Acc_dptr ->
1304    (match b with
1305     | Direct -> Bool.False
1306     | Indirect -> Bool.False
1307     | Ext_indirect -> Bool.False
1308     | Registr -> Bool.False
1309     | Acc_a -> Bool.False
1310     | Acc_b -> Bool.False
1311     | Dptr -> Bool.False
1312     | Data -> Bool.False
1313     | Data16 -> Bool.False
1314     | Acc_dptr -> Bool.True
1315     | Acc_pc -> Bool.False
1316     | Ext_indirect_dptr -> Bool.False
1317     | Indirect_dptr -> Bool.False
1318     | Carry -> Bool.False
1319     | Bit_addr -> Bool.False
1320     | N_bit_addr -> Bool.False
1321     | Relative -> Bool.False
1322     | Addr11 -> Bool.False
1323     | Addr16 -> Bool.False)
1324  | Acc_pc ->
1325    (match b with
1326     | Direct -> Bool.False
1327     | Indirect -> Bool.False
1328     | Ext_indirect -> Bool.False
1329     | Registr -> Bool.False
1330     | Acc_a -> Bool.False
1331     | Acc_b -> Bool.False
1332     | Dptr -> Bool.False
1333     | Data -> Bool.False
1334     | Data16 -> Bool.False
1335     | Acc_dptr -> Bool.False
1336     | Acc_pc -> Bool.True
1337     | Ext_indirect_dptr -> Bool.False
1338     | Indirect_dptr -> Bool.False
1339     | Carry -> Bool.False
1340     | Bit_addr -> Bool.False
1341     | N_bit_addr -> Bool.False
1342     | Relative -> Bool.False
1343     | Addr11 -> Bool.False
1344     | Addr16 -> Bool.False)
1345  | Ext_indirect_dptr ->
1346    (match b with
1347     | Direct -> Bool.False
1348     | Indirect -> Bool.False
1349     | Ext_indirect -> Bool.False
1350     | Registr -> Bool.False
1351     | Acc_a -> Bool.False
1352     | Acc_b -> Bool.False
1353     | Dptr -> Bool.False
1354     | Data -> Bool.False
1355     | Data16 -> Bool.False
1356     | Acc_dptr -> Bool.False
1357     | Acc_pc -> Bool.False
1358     | Ext_indirect_dptr -> Bool.True
1359     | Indirect_dptr -> Bool.False
1360     | Carry -> Bool.False
1361     | Bit_addr -> Bool.False
1362     | N_bit_addr -> Bool.False
1363     | Relative -> Bool.False
1364     | Addr11 -> Bool.False
1365     | Addr16 -> Bool.False)
1366  | Indirect_dptr ->
1367    (match b with
1368     | Direct -> Bool.False
1369     | Indirect -> Bool.False
1370     | Ext_indirect -> Bool.False
1371     | Registr -> Bool.False
1372     | Acc_a -> Bool.False
1373     | Acc_b -> Bool.False
1374     | Dptr -> Bool.False
1375     | Data -> Bool.False
1376     | Data16 -> Bool.False
1377     | Acc_dptr -> Bool.False
1378     | Acc_pc -> Bool.False
1379     | Ext_indirect_dptr -> Bool.False
1380     | Indirect_dptr -> Bool.True
1381     | Carry -> Bool.False
1382     | Bit_addr -> Bool.False
1383     | N_bit_addr -> Bool.False
1384     | Relative -> Bool.False
1385     | Addr11 -> Bool.False
1386     | Addr16 -> Bool.False)
1387  | Carry ->
1388    (match b with
1389     | Direct -> Bool.False
1390     | Indirect -> Bool.False
1391     | Ext_indirect -> Bool.False
1392     | Registr -> Bool.False
1393     | Acc_a -> Bool.False
1394     | Acc_b -> Bool.False
1395     | Dptr -> Bool.False
1396     | Data -> Bool.False
1397     | Data16 -> Bool.False
1398     | Acc_dptr -> Bool.False
1399     | Acc_pc -> Bool.False
1400     | Ext_indirect_dptr -> Bool.False
1401     | Indirect_dptr -> Bool.False
1402     | Carry -> Bool.True
1403     | Bit_addr -> Bool.False
1404     | N_bit_addr -> Bool.False
1405     | Relative -> Bool.False
1406     | Addr11 -> Bool.False
1407     | Addr16 -> Bool.False)
1408  | Bit_addr ->
1409    (match b with
1410     | Direct -> Bool.False
1411     | Indirect -> Bool.False
1412     | Ext_indirect -> Bool.False
1413     | Registr -> Bool.False
1414     | Acc_a -> Bool.False
1415     | Acc_b -> Bool.False
1416     | Dptr -> Bool.False
1417     | Data -> Bool.False
1418     | Data16 -> Bool.False
1419     | Acc_dptr -> Bool.False
1420     | Acc_pc -> Bool.False
1421     | Ext_indirect_dptr -> Bool.False
1422     | Indirect_dptr -> Bool.False
1423     | Carry -> Bool.False
1424     | Bit_addr -> Bool.True
1425     | N_bit_addr -> Bool.False
1426     | Relative -> Bool.False
1427     | Addr11 -> Bool.False
1428     | Addr16 -> Bool.False)
1429  | N_bit_addr ->
1430    (match b with
1431     | Direct -> Bool.False
1432     | Indirect -> Bool.False
1433     | Ext_indirect -> Bool.False
1434     | Registr -> Bool.False
1435     | Acc_a -> Bool.False
1436     | Acc_b -> Bool.False
1437     | Dptr -> Bool.False
1438     | Data -> Bool.False
1439     | Data16 -> Bool.False
1440     | Acc_dptr -> Bool.False
1441     | Acc_pc -> Bool.False
1442     | Ext_indirect_dptr -> Bool.False
1443     | Indirect_dptr -> Bool.False
1444     | Carry -> Bool.False
1445     | Bit_addr -> Bool.False
1446     | N_bit_addr -> Bool.True
1447     | Relative -> Bool.False
1448     | Addr11 -> Bool.False
1449     | Addr16 -> Bool.False)
1450  | Relative ->
1451    (match b with
1452     | Direct -> Bool.False
1453     | Indirect -> Bool.False
1454     | Ext_indirect -> Bool.False
1455     | Registr -> Bool.False
1456     | Acc_a -> Bool.False
1457     | Acc_b -> Bool.False
1458     | Dptr -> Bool.False
1459     | Data -> Bool.False
1460     | Data16 -> Bool.False
1461     | Acc_dptr -> Bool.False
1462     | Acc_pc -> Bool.False
1463     | Ext_indirect_dptr -> Bool.False
1464     | Indirect_dptr -> Bool.False
1465     | Carry -> Bool.False
1466     | Bit_addr -> Bool.False
1467     | N_bit_addr -> Bool.False
1468     | Relative -> Bool.True
1469     | Addr11 -> Bool.False
1470     | Addr16 -> Bool.False)
1471  | Addr11 ->
1472    (match b with
1473     | Direct -> Bool.False
1474     | Indirect -> Bool.False
1475     | Ext_indirect -> Bool.False
1476     | Registr -> Bool.False
1477     | Acc_a -> Bool.False
1478     | Acc_b -> Bool.False
1479     | Dptr -> Bool.False
1480     | Data -> Bool.False
1481     | Data16 -> Bool.False
1482     | Acc_dptr -> Bool.False
1483     | Acc_pc -> Bool.False
1484     | Ext_indirect_dptr -> Bool.False
1485     | Indirect_dptr -> Bool.False
1486     | Carry -> Bool.False
1487     | Bit_addr -> Bool.False
1488     | N_bit_addr -> Bool.False
1489     | Relative -> Bool.False
1490     | Addr11 -> Bool.True
1491     | Addr16 -> Bool.False)
1492  | Addr16 ->
1493    (match b with
1494     | Direct -> Bool.False
1495     | Indirect -> Bool.False
1496     | Ext_indirect -> Bool.False
1497     | Registr -> Bool.False
1498     | Acc_a -> Bool.False
1499     | Acc_b -> Bool.False
1500     | Dptr -> Bool.False
1501     | Data -> Bool.False
1502     | Data16 -> Bool.False
1503     | Acc_dptr -> Bool.False
1504     | Acc_pc -> Bool.False
1505     | Ext_indirect_dptr -> Bool.False
1506     | Indirect_dptr -> Bool.False
1507     | Carry -> Bool.False
1508     | Bit_addr -> Bool.False
1509     | N_bit_addr -> Bool.False
1510     | Relative -> Bool.False
1511     | Addr11 -> Bool.False
1512     | Addr16 -> Bool.True)
1513
1514type member_addressing_mode_tag = __
1515
1516(** val is_a : addressing_mode_tag -> addressing_mode -> Bool.bool **)
1517let rec is_a d a =
1518  match d with
1519  | Direct ->
1520    (match a with
1521     | DIRECT x -> Bool.True
1522     | INDIRECT x -> Bool.False
1523     | EXT_INDIRECT x -> Bool.False
1524     | REGISTER x -> Bool.False
1525     | ACC_A -> Bool.False
1526     | ACC_B -> Bool.False
1527     | DPTR -> Bool.False
1528     | DATA x -> Bool.False
1529     | DATA16 x -> Bool.False
1530     | ACC_DPTR -> Bool.False
1531     | ACC_PC -> Bool.False
1532     | EXT_INDIRECT_DPTR -> Bool.False
1533     | INDIRECT_DPTR -> Bool.False
1534     | CARRY -> Bool.False
1535     | BIT_ADDR x -> Bool.False
1536     | N_BIT_ADDR x -> Bool.False
1537     | RELATIVE x -> Bool.False
1538     | ADDR11 x -> Bool.False
1539     | ADDR16 x -> Bool.False)
1540  | Indirect ->
1541    (match a with
1542     | DIRECT x -> Bool.False
1543     | INDIRECT x -> Bool.True
1544     | EXT_INDIRECT x -> Bool.False
1545     | REGISTER x -> Bool.False
1546     | ACC_A -> Bool.False
1547     | ACC_B -> Bool.False
1548     | DPTR -> Bool.False
1549     | DATA x -> Bool.False
1550     | DATA16 x -> Bool.False
1551     | ACC_DPTR -> Bool.False
1552     | ACC_PC -> Bool.False
1553     | EXT_INDIRECT_DPTR -> Bool.False
1554     | INDIRECT_DPTR -> Bool.False
1555     | CARRY -> Bool.False
1556     | BIT_ADDR x -> Bool.False
1557     | N_BIT_ADDR x -> Bool.False
1558     | RELATIVE x -> Bool.False
1559     | ADDR11 x -> Bool.False
1560     | ADDR16 x -> Bool.False)
1561  | Ext_indirect ->
1562    (match a with
1563     | DIRECT x -> Bool.False
1564     | INDIRECT x -> Bool.False
1565     | EXT_INDIRECT x -> Bool.True
1566     | REGISTER x -> Bool.False
1567     | ACC_A -> Bool.False
1568     | ACC_B -> Bool.False
1569     | DPTR -> Bool.False
1570     | DATA x -> Bool.False
1571     | DATA16 x -> Bool.False
1572     | ACC_DPTR -> Bool.False
1573     | ACC_PC -> Bool.False
1574     | EXT_INDIRECT_DPTR -> Bool.False
1575     | INDIRECT_DPTR -> Bool.False
1576     | CARRY -> Bool.False
1577     | BIT_ADDR x -> Bool.False
1578     | N_BIT_ADDR x -> Bool.False
1579     | RELATIVE x -> Bool.False
1580     | ADDR11 x -> Bool.False
1581     | ADDR16 x -> Bool.False)
1582  | Registr ->
1583    (match a with
1584     | DIRECT x -> Bool.False
1585     | INDIRECT x -> Bool.False
1586     | EXT_INDIRECT x -> Bool.False
1587     | REGISTER x -> Bool.True
1588     | ACC_A -> Bool.False
1589     | ACC_B -> Bool.False
1590     | DPTR -> Bool.False
1591     | DATA x -> Bool.False
1592     | DATA16 x -> Bool.False
1593     | ACC_DPTR -> Bool.False
1594     | ACC_PC -> Bool.False
1595     | EXT_INDIRECT_DPTR -> Bool.False
1596     | INDIRECT_DPTR -> Bool.False
1597     | CARRY -> Bool.False
1598     | BIT_ADDR x -> Bool.False
1599     | N_BIT_ADDR x -> Bool.False
1600     | RELATIVE x -> Bool.False
1601     | ADDR11 x -> Bool.False
1602     | ADDR16 x -> Bool.False)
1603  | Acc_a ->
1604    (match a with
1605     | DIRECT x -> Bool.False
1606     | INDIRECT x -> Bool.False
1607     | EXT_INDIRECT x -> Bool.False
1608     | REGISTER x -> Bool.False
1609     | ACC_A -> Bool.True
1610     | ACC_B -> Bool.False
1611     | DPTR -> Bool.False
1612     | DATA x -> Bool.False
1613     | DATA16 x -> Bool.False
1614     | ACC_DPTR -> Bool.False
1615     | ACC_PC -> Bool.False
1616     | EXT_INDIRECT_DPTR -> Bool.False
1617     | INDIRECT_DPTR -> Bool.False
1618     | CARRY -> Bool.False
1619     | BIT_ADDR x -> Bool.False
1620     | N_BIT_ADDR x -> Bool.False
1621     | RELATIVE x -> Bool.False
1622     | ADDR11 x -> Bool.False
1623     | ADDR16 x -> Bool.False)
1624  | Acc_b ->
1625    (match a with
1626     | DIRECT x -> Bool.False
1627     | INDIRECT x -> Bool.False
1628     | EXT_INDIRECT x -> Bool.False
1629     | REGISTER x -> Bool.False
1630     | ACC_A -> Bool.False
1631     | ACC_B -> Bool.True
1632     | DPTR -> Bool.False
1633     | DATA x -> Bool.False
1634     | DATA16 x -> Bool.False
1635     | ACC_DPTR -> Bool.False
1636     | ACC_PC -> Bool.False
1637     | EXT_INDIRECT_DPTR -> Bool.False
1638     | INDIRECT_DPTR -> Bool.False
1639     | CARRY -> Bool.False
1640     | BIT_ADDR x -> Bool.False
1641     | N_BIT_ADDR x -> Bool.False
1642     | RELATIVE x -> Bool.False
1643     | ADDR11 x -> Bool.False
1644     | ADDR16 x -> Bool.False)
1645  | Dptr ->
1646    (match a with
1647     | DIRECT x -> Bool.False
1648     | INDIRECT x -> Bool.False
1649     | EXT_INDIRECT x -> Bool.False
1650     | REGISTER x -> Bool.False
1651     | ACC_A -> Bool.False
1652     | ACC_B -> Bool.False
1653     | DPTR -> Bool.True
1654     | DATA x -> Bool.False
1655     | DATA16 x -> Bool.False
1656     | ACC_DPTR -> Bool.False
1657     | ACC_PC -> Bool.False
1658     | EXT_INDIRECT_DPTR -> Bool.False
1659     | INDIRECT_DPTR -> Bool.False
1660     | CARRY -> Bool.False
1661     | BIT_ADDR x -> Bool.False
1662     | N_BIT_ADDR x -> Bool.False
1663     | RELATIVE x -> Bool.False
1664     | ADDR11 x -> Bool.False
1665     | ADDR16 x -> Bool.False)
1666  | Data ->
1667    (match a with
1668     | DIRECT x -> Bool.False
1669     | INDIRECT x -> Bool.False
1670     | EXT_INDIRECT x -> Bool.False
1671     | REGISTER x -> Bool.False
1672     | ACC_A -> Bool.False
1673     | ACC_B -> Bool.False
1674     | DPTR -> Bool.False
1675     | DATA x -> Bool.True
1676     | DATA16 x -> Bool.False
1677     | ACC_DPTR -> Bool.False
1678     | ACC_PC -> Bool.False
1679     | EXT_INDIRECT_DPTR -> Bool.False
1680     | INDIRECT_DPTR -> Bool.False
1681     | CARRY -> Bool.False
1682     | BIT_ADDR x -> Bool.False
1683     | N_BIT_ADDR x -> Bool.False
1684     | RELATIVE x -> Bool.False
1685     | ADDR11 x -> Bool.False
1686     | ADDR16 x -> Bool.False)
1687  | Data16 ->
1688    (match a with
1689     | DIRECT x -> Bool.False
1690     | INDIRECT x -> Bool.False
1691     | EXT_INDIRECT x -> Bool.False
1692     | REGISTER x -> Bool.False
1693     | ACC_A -> Bool.False
1694     | ACC_B -> Bool.False
1695     | DPTR -> Bool.False
1696     | DATA x -> Bool.False
1697     | DATA16 x -> Bool.True
1698     | ACC_DPTR -> Bool.False
1699     | ACC_PC -> Bool.False
1700     | EXT_INDIRECT_DPTR -> Bool.False
1701     | INDIRECT_DPTR -> Bool.False
1702     | CARRY -> Bool.False
1703     | BIT_ADDR x -> Bool.False
1704     | N_BIT_ADDR x -> Bool.False
1705     | RELATIVE x -> Bool.False
1706     | ADDR11 x -> Bool.False
1707     | ADDR16 x -> Bool.False)
1708  | Acc_dptr ->
1709    (match a with
1710     | DIRECT x -> Bool.False
1711     | INDIRECT x -> Bool.False
1712     | EXT_INDIRECT x -> Bool.False
1713     | REGISTER x -> Bool.False
1714     | ACC_A -> Bool.False
1715     | ACC_B -> Bool.False
1716     | DPTR -> Bool.False
1717     | DATA x -> Bool.False
1718     | DATA16 x -> Bool.False
1719     | ACC_DPTR -> Bool.True
1720     | ACC_PC -> Bool.False
1721     | EXT_INDIRECT_DPTR -> Bool.False
1722     | INDIRECT_DPTR -> Bool.False
1723     | CARRY -> Bool.False
1724     | BIT_ADDR x -> Bool.False
1725     | N_BIT_ADDR x -> Bool.False
1726     | RELATIVE x -> Bool.False
1727     | ADDR11 x -> Bool.False
1728     | ADDR16 x -> Bool.False)
1729  | Acc_pc ->
1730    (match a with
1731     | DIRECT x -> Bool.False
1732     | INDIRECT x -> Bool.False
1733     | EXT_INDIRECT x -> Bool.False
1734     | REGISTER x -> Bool.False
1735     | ACC_A -> Bool.False
1736     | ACC_B -> Bool.False
1737     | DPTR -> Bool.False
1738     | DATA x -> Bool.False
1739     | DATA16 x -> Bool.False
1740     | ACC_DPTR -> Bool.False
1741     | ACC_PC -> Bool.True
1742     | EXT_INDIRECT_DPTR -> Bool.False
1743     | INDIRECT_DPTR -> Bool.False
1744     | CARRY -> Bool.False
1745     | BIT_ADDR x -> Bool.False
1746     | N_BIT_ADDR x -> Bool.False
1747     | RELATIVE x -> Bool.False
1748     | ADDR11 x -> Bool.False
1749     | ADDR16 x -> Bool.False)
1750  | Ext_indirect_dptr ->
1751    (match a with
1752     | DIRECT x -> Bool.False
1753     | INDIRECT x -> Bool.False
1754     | EXT_INDIRECT x -> Bool.False
1755     | REGISTER x -> Bool.False
1756     | ACC_A -> Bool.False
1757     | ACC_B -> Bool.False
1758     | DPTR -> Bool.False
1759     | DATA x -> Bool.False
1760     | DATA16 x -> Bool.False
1761     | ACC_DPTR -> Bool.False
1762     | ACC_PC -> Bool.False
1763     | EXT_INDIRECT_DPTR -> Bool.True
1764     | INDIRECT_DPTR -> Bool.False
1765     | CARRY -> Bool.False
1766     | BIT_ADDR x -> Bool.False
1767     | N_BIT_ADDR x -> Bool.False
1768     | RELATIVE x -> Bool.False
1769     | ADDR11 x -> Bool.False
1770     | ADDR16 x -> Bool.False)
1771  | Indirect_dptr ->
1772    (match a with
1773     | DIRECT x -> Bool.False
1774     | INDIRECT x -> Bool.False
1775     | EXT_INDIRECT x -> Bool.False
1776     | REGISTER x -> Bool.False
1777     | ACC_A -> Bool.False
1778     | ACC_B -> Bool.False
1779     | DPTR -> Bool.False
1780     | DATA x -> Bool.False
1781     | DATA16 x -> Bool.False
1782     | ACC_DPTR -> Bool.False
1783     | ACC_PC -> Bool.False
1784     | EXT_INDIRECT_DPTR -> Bool.False
1785     | INDIRECT_DPTR -> Bool.True
1786     | CARRY -> Bool.False
1787     | BIT_ADDR x -> Bool.False
1788     | N_BIT_ADDR x -> Bool.False
1789     | RELATIVE x -> Bool.False
1790     | ADDR11 x -> Bool.False
1791     | ADDR16 x -> Bool.False)
1792  | Carry ->
1793    (match a with
1794     | DIRECT x -> Bool.False
1795     | INDIRECT x -> Bool.False
1796     | EXT_INDIRECT x -> Bool.False
1797     | REGISTER x -> Bool.False
1798     | ACC_A -> Bool.False
1799     | ACC_B -> Bool.False
1800     | DPTR -> Bool.False
1801     | DATA x -> Bool.False
1802     | DATA16 x -> Bool.False
1803     | ACC_DPTR -> Bool.False
1804     | ACC_PC -> Bool.False
1805     | EXT_INDIRECT_DPTR -> Bool.False
1806     | INDIRECT_DPTR -> Bool.False
1807     | CARRY -> Bool.True
1808     | BIT_ADDR x -> Bool.False
1809     | N_BIT_ADDR x -> Bool.False
1810     | RELATIVE x -> Bool.False
1811     | ADDR11 x -> Bool.False
1812     | ADDR16 x -> Bool.False)
1813  | Bit_addr ->
1814    (match a with
1815     | DIRECT x -> Bool.False
1816     | INDIRECT x -> Bool.False
1817     | EXT_INDIRECT x -> Bool.False
1818     | REGISTER x -> Bool.False
1819     | ACC_A -> Bool.False
1820     | ACC_B -> Bool.False
1821     | DPTR -> Bool.False
1822     | DATA x -> Bool.False
1823     | DATA16 x -> Bool.False
1824     | ACC_DPTR -> Bool.False
1825     | ACC_PC -> Bool.False
1826     | EXT_INDIRECT_DPTR -> Bool.False
1827     | INDIRECT_DPTR -> Bool.False
1828     | CARRY -> Bool.False
1829     | BIT_ADDR x -> Bool.True
1830     | N_BIT_ADDR x -> Bool.False
1831     | RELATIVE x -> Bool.False
1832     | ADDR11 x -> Bool.False
1833     | ADDR16 x -> Bool.False)
1834  | N_bit_addr ->
1835    (match a with
1836     | DIRECT x -> Bool.False
1837     | INDIRECT x -> Bool.False
1838     | EXT_INDIRECT x -> Bool.False
1839     | REGISTER x -> Bool.False
1840     | ACC_A -> Bool.False
1841     | ACC_B -> Bool.False
1842     | DPTR -> Bool.False
1843     | DATA x -> Bool.False
1844     | DATA16 x -> Bool.False
1845     | ACC_DPTR -> Bool.False
1846     | ACC_PC -> Bool.False
1847     | EXT_INDIRECT_DPTR -> Bool.False
1848     | INDIRECT_DPTR -> Bool.False
1849     | CARRY -> Bool.False
1850     | BIT_ADDR x -> Bool.False
1851     | N_BIT_ADDR x -> Bool.True
1852     | RELATIVE x -> Bool.False
1853     | ADDR11 x -> Bool.False
1854     | ADDR16 x -> Bool.False)
1855  | Relative ->
1856    (match a with
1857     | DIRECT x -> Bool.False
1858     | INDIRECT x -> Bool.False
1859     | EXT_INDIRECT x -> Bool.False
1860     | REGISTER x -> Bool.False
1861     | ACC_A -> Bool.False
1862     | ACC_B -> Bool.False
1863     | DPTR -> Bool.False
1864     | DATA x -> Bool.False
1865     | DATA16 x -> Bool.False
1866     | ACC_DPTR -> Bool.False
1867     | ACC_PC -> Bool.False
1868     | EXT_INDIRECT_DPTR -> Bool.False
1869     | INDIRECT_DPTR -> Bool.False
1870     | CARRY -> Bool.False
1871     | BIT_ADDR x -> Bool.False
1872     | N_BIT_ADDR x -> Bool.False
1873     | RELATIVE x -> Bool.True
1874     | ADDR11 x -> Bool.False
1875     | ADDR16 x -> Bool.False)
1876  | Addr11 ->
1877    (match a with
1878     | DIRECT x -> Bool.False
1879     | INDIRECT x -> Bool.False
1880     | EXT_INDIRECT x -> Bool.False
1881     | REGISTER x -> Bool.False
1882     | ACC_A -> Bool.False
1883     | ACC_B -> Bool.False
1884     | DPTR -> Bool.False
1885     | DATA x -> Bool.False
1886     | DATA16 x -> Bool.False
1887     | ACC_DPTR -> Bool.False
1888     | ACC_PC -> Bool.False
1889     | EXT_INDIRECT_DPTR -> Bool.False
1890     | INDIRECT_DPTR -> Bool.False
1891     | CARRY -> Bool.False
1892     | BIT_ADDR x -> Bool.False
1893     | N_BIT_ADDR x -> Bool.False
1894     | RELATIVE x -> Bool.False
1895     | ADDR11 x -> Bool.True
1896     | ADDR16 x -> Bool.False)
1897  | Addr16 ->
1898    (match a with
1899     | DIRECT x -> Bool.False
1900     | INDIRECT x -> Bool.False
1901     | EXT_INDIRECT x -> Bool.False
1902     | REGISTER x -> Bool.False
1903     | ACC_A -> Bool.False
1904     | ACC_B -> Bool.False
1905     | DPTR -> Bool.False
1906     | DATA x -> Bool.False
1907     | DATA16 x -> Bool.False
1908     | ACC_DPTR -> Bool.False
1909     | ACC_PC -> Bool.False
1910     | EXT_INDIRECT_DPTR -> Bool.False
1911     | INDIRECT_DPTR -> Bool.False
1912     | CARRY -> Bool.False
1913     | BIT_ADDR x -> Bool.False
1914     | N_BIT_ADDR x -> Bool.False
1915     | RELATIVE x -> Bool.False
1916     | ADDR11 x -> Bool.False
1917     | ADDR16 x -> Bool.True)
1918
1919(** val is_in :
1920    Nat.nat -> addressing_mode_tag Vector.vector -> addressing_mode ->
1921    Bool.bool **)
1922let rec is_in n l a =
1923  match l with
1924  | Vector.VEmpty -> Bool.False
1925  | Vector.VCons (m, he, tl) -> Bool.orb (is_a he a) (is_in m tl a)
1926
1927type subaddressing_mode =
1928  addressing_mode
1929  (* singleton inductive, whose constructor was mk_subaddressing_mode *)
1930
1931(** val subaddressing_mode_rect_Type4 :
1932    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
1933    'a1) -> subaddressing_mode -> 'a1 **)
1934let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_15335 =
1935  let subaddressing_modeel = x_15335 in
1936  h_mk_subaddressing_mode subaddressing_modeel __
1937
1938(** val subaddressing_mode_rect_Type5 :
1939    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
1940    'a1) -> subaddressing_mode -> 'a1 **)
1941let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_15337 =
1942  let subaddressing_modeel = x_15337 in
1943  h_mk_subaddressing_mode subaddressing_modeel __
1944
1945(** val subaddressing_mode_rect_Type3 :
1946    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
1947    'a1) -> subaddressing_mode -> 'a1 **)
1948let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_15339 =
1949  let subaddressing_modeel = x_15339 in
1950  h_mk_subaddressing_mode subaddressing_modeel __
1951
1952(** val subaddressing_mode_rect_Type2 :
1953    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
1954    'a1) -> subaddressing_mode -> 'a1 **)
1955let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_15341 =
1956  let subaddressing_modeel = x_15341 in
1957  h_mk_subaddressing_mode subaddressing_modeel __
1958
1959(** val subaddressing_mode_rect_Type1 :
1960    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
1961    'a1) -> subaddressing_mode -> 'a1 **)
1962let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_15343 =
1963  let subaddressing_modeel = x_15343 in
1964  h_mk_subaddressing_mode subaddressing_modeel __
1965
1966(** val subaddressing_mode_rect_Type0 :
1967    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
1968    'a1) -> subaddressing_mode -> 'a1 **)
1969let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_15345 =
1970  let subaddressing_modeel = x_15345 in
1971  h_mk_subaddressing_mode subaddressing_modeel __
1972
1973(** val subaddressing_modeel :
1974    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
1975    addressing_mode **)
1976let rec subaddressing_modeel n l xxx =
1977  let yyy = xxx in yyy
1978
1979(** val subaddressing_mode_inv_rect_Type4 :
1980    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
1981    (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **)
1982let subaddressing_mode_inv_rect_Type4 x1 x2 hterm h1 =
1983  let hcut = subaddressing_mode_rect_Type4 x1 x2 h1 hterm in hcut __
1984
1985(** val subaddressing_mode_inv_rect_Type3 :
1986    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
1987    (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **)
1988let subaddressing_mode_inv_rect_Type3 x1 x2 hterm h1 =
1989  let hcut = subaddressing_mode_rect_Type3 x1 x2 h1 hterm in hcut __
1990
1991(** val subaddressing_mode_inv_rect_Type2 :
1992    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
1993    (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **)
1994let subaddressing_mode_inv_rect_Type2 x1 x2 hterm h1 =
1995  let hcut = subaddressing_mode_rect_Type2 x1 x2 h1 hterm in hcut __
1996
1997(** val subaddressing_mode_inv_rect_Type1 :
1998    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
1999    (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **)
2000let subaddressing_mode_inv_rect_Type1 x1 x2 hterm h1 =
2001  let hcut = subaddressing_mode_rect_Type1 x1 x2 h1 hterm in hcut __
2002
2003(** val subaddressing_mode_inv_rect_Type0 :
2004    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
2005    (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **)
2006let subaddressing_mode_inv_rect_Type0 x1 x2 hterm h1 =
2007  let hcut = subaddressing_mode_rect_Type0 x1 x2 h1 hterm in hcut __
2008
2009(** val subaddressing_mode_discr :
2010    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
2011    subaddressing_mode -> __ **)
2012let subaddressing_mode_discr a1 a2 x y =
2013  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
2014
2015(** val subaddressing_mode_jmdiscr :
2016    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
2017    subaddressing_mode -> __ **)
2018let subaddressing_mode_jmdiscr a1 a2 x y =
2019  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
2020
2021(** val dpi1__o__subaddressing_modeel__o__inject :
2022    Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
2023    Types.dPair -> addressing_mode Types.sig0 **)
2024let dpi1__o__subaddressing_modeel__o__inject x1 x2 x4 =
2025  subaddressing_modeel x1 x2 x4.Types.dpi1
2026
2027(** val eject__o__subaddressing_modeel__o__inject :
2028    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode
2029    Types.sig0 -> addressing_mode Types.sig0 **)
2030let eject__o__subaddressing_modeel__o__inject x1 x2 x4 =
2031  subaddressing_modeel x1 x2 (Types.pi1 x4)
2032
2033(** val subaddressing_modeel__o__inject :
2034    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
2035    addressing_mode Types.sig0 **)
2036let subaddressing_modeel__o__inject x1 x2 x3 =
2037  subaddressing_modeel x1 x2 x3
2038
2039(** val dpi1__o__subaddressing_modeel :
2040    Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
2041    Types.dPair -> addressing_mode **)
2042let dpi1__o__subaddressing_modeel x0 x1 x3 =
2043  subaddressing_modeel x0 x1 x3.Types.dpi1
2044
2045(** val eject__o__subaddressing_modeel :
2046    Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode
2047    Types.sig0 -> addressing_mode **)
2048let eject__o__subaddressing_modeel x0 x1 x3 =
2049  subaddressing_modeel x0 x1 (Types.pi1 x3)
2050
2051type subaddressing_mode_elim_type = __
2052
2053type 'a preinstruction =
2054| ADD of subaddressing_mode * subaddressing_mode
2055| ADDC of subaddressing_mode * subaddressing_mode
2056| SUBB of subaddressing_mode * subaddressing_mode
2057| INC of subaddressing_mode
2058| DEC of subaddressing_mode
2059| MUL of subaddressing_mode * subaddressing_mode
2060| DIV of subaddressing_mode * subaddressing_mode
2061| DA of subaddressing_mode
2062| JC of 'a
2063| JNC of 'a
2064| JB of subaddressing_mode * 'a
2065| JNB of subaddressing_mode * 'a
2066| JBC of subaddressing_mode * 'a
2067| JZ of 'a
2068| JNZ of 'a
2069| CJNE of ((subaddressing_mode, subaddressing_mode) Types.prod,
2070          (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum * 
2071   'a
2072| DJNZ of subaddressing_mode * 'a
2073| ANL of (((subaddressing_mode, subaddressing_mode) Types.prod,
2074         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2075         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
2076| ORL of (((subaddressing_mode, subaddressing_mode) Types.prod,
2077         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2078         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
2079| XRL of ((subaddressing_mode, subaddressing_mode) Types.prod,
2080         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
2081| CLR of subaddressing_mode
2082| CPL of subaddressing_mode
2083| RL of subaddressing_mode
2084| RLC of subaddressing_mode
2085| RR of subaddressing_mode
2086| RRC of subaddressing_mode
2087| SWAP of subaddressing_mode
2088| MOV of ((((((subaddressing_mode, subaddressing_mode) Types.prod,
2089         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2090         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2091         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2092         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2093         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
2094| MOVX of ((subaddressing_mode, subaddressing_mode) Types.prod,
2095          (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
2096| SETB of subaddressing_mode
2097| PUSH of subaddressing_mode
2098| POP of subaddressing_mode
2099| XCH of subaddressing_mode * subaddressing_mode
2100| XCHD of subaddressing_mode * subaddressing_mode
2101| RET
2102| RETI
2103| NOP
2104
2105(** val preinstruction_rect_Type4 :
2106    (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
2107    -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
2108    subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2109    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2110    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) ->
2111    (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2112    (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2)
2113    -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2114    (((subaddressing_mode, subaddressing_mode) Types.prod,
2115    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 ->
2116    'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode,
2117    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2118    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2119    Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode,
2120    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2121    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2122    Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode,
2123    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2124    Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) ->
2125    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2126    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2127    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2128    (((((((subaddressing_mode, subaddressing_mode) Types.prod,
2129    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2130    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2131    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2132    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2133    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2134    (((subaddressing_mode, subaddressing_mode) Types.prod,
2135    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2136    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2137    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2138    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
2139    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
2140let rec preinstruction_rect_Type4 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function
2141| ADD (x_15445, x_15444) -> h_ADD x_15445 x_15444
2142| ADDC (x_15447, x_15446) -> h_ADDC x_15447 x_15446
2143| SUBB (x_15449, x_15448) -> h_SUBB x_15449 x_15448
2144| INC x_15450 -> h_INC x_15450
2145| DEC x_15451 -> h_DEC x_15451
2146| MUL (x_15453, x_15452) -> h_MUL x_15453 x_15452
2147| DIV (x_15455, x_15454) -> h_DIV x_15455 x_15454
2148| DA x_15456 -> h_DA x_15456
2149| JC x_15457 -> h_JC x_15457
2150| JNC x_15458 -> h_JNC x_15458
2151| JB (x_15460, x_15459) -> h_JB x_15460 x_15459
2152| JNB (x_15462, x_15461) -> h_JNB x_15462 x_15461
2153| JBC (x_15464, x_15463) -> h_JBC x_15464 x_15463
2154| JZ x_15465 -> h_JZ x_15465
2155| JNZ x_15466 -> h_JNZ x_15466
2156| CJNE (x_15468, x_15467) -> h_CJNE x_15468 x_15467
2157| DJNZ (x_15470, x_15469) -> h_DJNZ x_15470 x_15469
2158| ANL x_15471 -> h_ANL x_15471
2159| ORL x_15472 -> h_ORL x_15472
2160| XRL x_15473 -> h_XRL x_15473
2161| CLR x_15474 -> h_CLR x_15474
2162| CPL x_15475 -> h_CPL x_15475
2163| RL x_15476 -> h_RL x_15476
2164| RLC x_15477 -> h_RLC x_15477
2165| RR x_15478 -> h_RR x_15478
2166| RRC x_15479 -> h_RRC x_15479
2167| SWAP x_15480 -> h_SWAP x_15480
2168| MOV x_15481 -> h_MOV x_15481
2169| MOVX x_15482 -> h_MOVX x_15482
2170| SETB x_15483 -> h_SETB x_15483
2171| PUSH x_15484 -> h_PUSH x_15484
2172| POP x_15485 -> h_POP x_15485
2173| XCH (x_15487, x_15486) -> h_XCH x_15487 x_15486
2174| XCHD (x_15489, x_15488) -> h_XCHD x_15489 x_15488
2175| RET -> h_RET
2176| RETI -> h_RETI
2177| NOP -> h_NOP
2178
2179(** val preinstruction_rect_Type5 :
2180    (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
2181    -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
2182    subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2183    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2184    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) ->
2185    (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2186    (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2)
2187    -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2188    (((subaddressing_mode, subaddressing_mode) Types.prod,
2189    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 ->
2190    'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode,
2191    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2192    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2193    Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode,
2194    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2195    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2196    Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode,
2197    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2198    Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) ->
2199    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2200    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2201    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2202    (((((((subaddressing_mode, subaddressing_mode) Types.prod,
2203    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2204    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2205    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2206    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2207    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2208    (((subaddressing_mode, subaddressing_mode) Types.prod,
2209    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2210    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2211    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2212    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
2213    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
2214let rec preinstruction_rect_Type5 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function
2215| ADD (x_15529, x_15528) -> h_ADD x_15529 x_15528
2216| ADDC (x_15531, x_15530) -> h_ADDC x_15531 x_15530
2217| SUBB (x_15533, x_15532) -> h_SUBB x_15533 x_15532
2218| INC x_15534 -> h_INC x_15534
2219| DEC x_15535 -> h_DEC x_15535
2220| MUL (x_15537, x_15536) -> h_MUL x_15537 x_15536
2221| DIV (x_15539, x_15538) -> h_DIV x_15539 x_15538
2222| DA x_15540 -> h_DA x_15540
2223| JC x_15541 -> h_JC x_15541
2224| JNC x_15542 -> h_JNC x_15542
2225| JB (x_15544, x_15543) -> h_JB x_15544 x_15543
2226| JNB (x_15546, x_15545) -> h_JNB x_15546 x_15545
2227| JBC (x_15548, x_15547) -> h_JBC x_15548 x_15547
2228| JZ x_15549 -> h_JZ x_15549
2229| JNZ x_15550 -> h_JNZ x_15550
2230| CJNE (x_15552, x_15551) -> h_CJNE x_15552 x_15551
2231| DJNZ (x_15554, x_15553) -> h_DJNZ x_15554 x_15553
2232| ANL x_15555 -> h_ANL x_15555
2233| ORL x_15556 -> h_ORL x_15556
2234| XRL x_15557 -> h_XRL x_15557
2235| CLR x_15558 -> h_CLR x_15558
2236| CPL x_15559 -> h_CPL x_15559
2237| RL x_15560 -> h_RL x_15560
2238| RLC x_15561 -> h_RLC x_15561
2239| RR x_15562 -> h_RR x_15562
2240| RRC x_15563 -> h_RRC x_15563
2241| SWAP x_15564 -> h_SWAP x_15564
2242| MOV x_15565 -> h_MOV x_15565
2243| MOVX x_15566 -> h_MOVX x_15566
2244| SETB x_15567 -> h_SETB x_15567
2245| PUSH x_15568 -> h_PUSH x_15568
2246| POP x_15569 -> h_POP x_15569
2247| XCH (x_15571, x_15570) -> h_XCH x_15571 x_15570
2248| XCHD (x_15573, x_15572) -> h_XCHD x_15573 x_15572
2249| RET -> h_RET
2250| RETI -> h_RETI
2251| NOP -> h_NOP
2252
2253(** val preinstruction_rect_Type3 :
2254    (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
2255    -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
2256    subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2257    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2258    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) ->
2259    (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2260    (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2)
2261    -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2262    (((subaddressing_mode, subaddressing_mode) Types.prod,
2263    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 ->
2264    'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode,
2265    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2266    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2267    Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode,
2268    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2269    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2270    Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode,
2271    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2272    Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) ->
2273    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2274    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2275    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2276    (((((((subaddressing_mode, subaddressing_mode) Types.prod,
2277    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2278    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2279    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2280    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2281    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2282    (((subaddressing_mode, subaddressing_mode) Types.prod,
2283    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2284    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2285    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2286    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
2287    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
2288let rec preinstruction_rect_Type3 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function
2289| ADD (x_15613, x_15612) -> h_ADD x_15613 x_15612
2290| ADDC (x_15615, x_15614) -> h_ADDC x_15615 x_15614
2291| SUBB (x_15617, x_15616) -> h_SUBB x_15617 x_15616
2292| INC x_15618 -> h_INC x_15618
2293| DEC x_15619 -> h_DEC x_15619
2294| MUL (x_15621, x_15620) -> h_MUL x_15621 x_15620
2295| DIV (x_15623, x_15622) -> h_DIV x_15623 x_15622
2296| DA x_15624 -> h_DA x_15624
2297| JC x_15625 -> h_JC x_15625
2298| JNC x_15626 -> h_JNC x_15626
2299| JB (x_15628, x_15627) -> h_JB x_15628 x_15627
2300| JNB (x_15630, x_15629) -> h_JNB x_15630 x_15629
2301| JBC (x_15632, x_15631) -> h_JBC x_15632 x_15631
2302| JZ x_15633 -> h_JZ x_15633
2303| JNZ x_15634 -> h_JNZ x_15634
2304| CJNE (x_15636, x_15635) -> h_CJNE x_15636 x_15635
2305| DJNZ (x_15638, x_15637) -> h_DJNZ x_15638 x_15637
2306| ANL x_15639 -> h_ANL x_15639
2307| ORL x_15640 -> h_ORL x_15640
2308| XRL x_15641 -> h_XRL x_15641
2309| CLR x_15642 -> h_CLR x_15642
2310| CPL x_15643 -> h_CPL x_15643
2311| RL x_15644 -> h_RL x_15644
2312| RLC x_15645 -> h_RLC x_15645
2313| RR x_15646 -> h_RR x_15646
2314| RRC x_15647 -> h_RRC x_15647
2315| SWAP x_15648 -> h_SWAP x_15648
2316| MOV x_15649 -> h_MOV x_15649
2317| MOVX x_15650 -> h_MOVX x_15650
2318| SETB x_15651 -> h_SETB x_15651
2319| PUSH x_15652 -> h_PUSH x_15652
2320| POP x_15653 -> h_POP x_15653
2321| XCH (x_15655, x_15654) -> h_XCH x_15655 x_15654
2322| XCHD (x_15657, x_15656) -> h_XCHD x_15657 x_15656
2323| RET -> h_RET
2324| RETI -> h_RETI
2325| NOP -> h_NOP
2326
2327(** val preinstruction_rect_Type2 :
2328    (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
2329    -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
2330    subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2331    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2332    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) ->
2333    (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2334    (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2)
2335    -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2336    (((subaddressing_mode, subaddressing_mode) Types.prod,
2337    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 ->
2338    'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode,
2339    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2340    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2341    Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode,
2342    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2343    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2344    Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode,
2345    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2346    Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) ->
2347    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2348    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2349    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2350    (((((((subaddressing_mode, subaddressing_mode) Types.prod,
2351    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2352    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2353    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2354    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2355    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2356    (((subaddressing_mode, subaddressing_mode) Types.prod,
2357    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2358    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2359    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2360    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
2361    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
2362let rec preinstruction_rect_Type2 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function
2363| ADD (x_15697, x_15696) -> h_ADD x_15697 x_15696
2364| ADDC (x_15699, x_15698) -> h_ADDC x_15699 x_15698
2365| SUBB (x_15701, x_15700) -> h_SUBB x_15701 x_15700
2366| INC x_15702 -> h_INC x_15702
2367| DEC x_15703 -> h_DEC x_15703
2368| MUL (x_15705, x_15704) -> h_MUL x_15705 x_15704
2369| DIV (x_15707, x_15706) -> h_DIV x_15707 x_15706
2370| DA x_15708 -> h_DA x_15708
2371| JC x_15709 -> h_JC x_15709
2372| JNC x_15710 -> h_JNC x_15710
2373| JB (x_15712, x_15711) -> h_JB x_15712 x_15711
2374| JNB (x_15714, x_15713) -> h_JNB x_15714 x_15713
2375| JBC (x_15716, x_15715) -> h_JBC x_15716 x_15715
2376| JZ x_15717 -> h_JZ x_15717
2377| JNZ x_15718 -> h_JNZ x_15718
2378| CJNE (x_15720, x_15719) -> h_CJNE x_15720 x_15719
2379| DJNZ (x_15722, x_15721) -> h_DJNZ x_15722 x_15721
2380| ANL x_15723 -> h_ANL x_15723
2381| ORL x_15724 -> h_ORL x_15724
2382| XRL x_15725 -> h_XRL x_15725
2383| CLR x_15726 -> h_CLR x_15726
2384| CPL x_15727 -> h_CPL x_15727
2385| RL x_15728 -> h_RL x_15728
2386| RLC x_15729 -> h_RLC x_15729
2387| RR x_15730 -> h_RR x_15730
2388| RRC x_15731 -> h_RRC x_15731
2389| SWAP x_15732 -> h_SWAP x_15732
2390| MOV x_15733 -> h_MOV x_15733
2391| MOVX x_15734 -> h_MOVX x_15734
2392| SETB x_15735 -> h_SETB x_15735
2393| PUSH x_15736 -> h_PUSH x_15736
2394| POP x_15737 -> h_POP x_15737
2395| XCH (x_15739, x_15738) -> h_XCH x_15739 x_15738
2396| XCHD (x_15741, x_15740) -> h_XCHD x_15741 x_15740
2397| RET -> h_RET
2398| RETI -> h_RETI
2399| NOP -> h_NOP
2400
2401(** val preinstruction_rect_Type1 :
2402    (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
2403    -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
2404    subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2405    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2406    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) ->
2407    (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2408    (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2)
2409    -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2410    (((subaddressing_mode, subaddressing_mode) Types.prod,
2411    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 ->
2412    'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode,
2413    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2414    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2415    Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode,
2416    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2417    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2418    Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode,
2419    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2420    Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) ->
2421    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2422    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2423    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2424    (((((((subaddressing_mode, subaddressing_mode) Types.prod,
2425    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2426    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2427    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2428    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2429    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2430    (((subaddressing_mode, subaddressing_mode) Types.prod,
2431    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2432    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2433    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2434    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
2435    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
2436let rec preinstruction_rect_Type1 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function
2437| ADD (x_15781, x_15780) -> h_ADD x_15781 x_15780
2438| ADDC (x_15783, x_15782) -> h_ADDC x_15783 x_15782
2439| SUBB (x_15785, x_15784) -> h_SUBB x_15785 x_15784
2440| INC x_15786 -> h_INC x_15786
2441| DEC x_15787 -> h_DEC x_15787
2442| MUL (x_15789, x_15788) -> h_MUL x_15789 x_15788
2443| DIV (x_15791, x_15790) -> h_DIV x_15791 x_15790
2444| DA x_15792 -> h_DA x_15792
2445| JC x_15793 -> h_JC x_15793
2446| JNC x_15794 -> h_JNC x_15794
2447| JB (x_15796, x_15795) -> h_JB x_15796 x_15795
2448| JNB (x_15798, x_15797) -> h_JNB x_15798 x_15797
2449| JBC (x_15800, x_15799) -> h_JBC x_15800 x_15799
2450| JZ x_15801 -> h_JZ x_15801
2451| JNZ x_15802 -> h_JNZ x_15802
2452| CJNE (x_15804, x_15803) -> h_CJNE x_15804 x_15803
2453| DJNZ (x_15806, x_15805) -> h_DJNZ x_15806 x_15805
2454| ANL x_15807 -> h_ANL x_15807
2455| ORL x_15808 -> h_ORL x_15808
2456| XRL x_15809 -> h_XRL x_15809
2457| CLR x_15810 -> h_CLR x_15810
2458| CPL x_15811 -> h_CPL x_15811
2459| RL x_15812 -> h_RL x_15812
2460| RLC x_15813 -> h_RLC x_15813
2461| RR x_15814 -> h_RR x_15814
2462| RRC x_15815 -> h_RRC x_15815
2463| SWAP x_15816 -> h_SWAP x_15816
2464| MOV x_15817 -> h_MOV x_15817
2465| MOVX x_15818 -> h_MOVX x_15818
2466| SETB x_15819 -> h_SETB x_15819
2467| PUSH x_15820 -> h_PUSH x_15820
2468| POP x_15821 -> h_POP x_15821
2469| XCH (x_15823, x_15822) -> h_XCH x_15823 x_15822
2470| XCHD (x_15825, x_15824) -> h_XCHD x_15825 x_15824
2471| RET -> h_RET
2472| RETI -> h_RETI
2473| NOP -> h_NOP
2474
2475(** val preinstruction_rect_Type0 :
2476    (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
2477    -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
2478    subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2479    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2480    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) ->
2481    (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2482    (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2)
2483    -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) ->
2484    (((subaddressing_mode, subaddressing_mode) Types.prod,
2485    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 ->
2486    'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode,
2487    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2488    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2489    Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode,
2490    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2491    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2492    Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode,
2493    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2494    Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) ->
2495    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2496    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2497    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2498    (((((((subaddressing_mode, subaddressing_mode) Types.prod,
2499    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2500    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2501    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2502    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2503    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2504    (((subaddressing_mode, subaddressing_mode) Types.prod,
2505    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
2506    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
2507    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
2508    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
2509    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
2510let rec preinstruction_rect_Type0 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function
2511| ADD (x_15865, x_15864) -> h_ADD x_15865 x_15864
2512| ADDC (x_15867, x_15866) -> h_ADDC x_15867 x_15866
2513| SUBB (x_15869, x_15868) -> h_SUBB x_15869 x_15868
2514| INC x_15870 -> h_INC x_15870
2515| DEC x_15871 -> h_DEC x_15871
2516| MUL (x_15873, x_15872) -> h_MUL x_15873 x_15872
2517| DIV (x_15875, x_15874) -> h_DIV x_15875 x_15874
2518| DA x_15876 -> h_DA x_15876
2519| JC x_15877 -> h_JC x_15877
2520| JNC x_15878 -> h_JNC x_15878
2521| JB (x_15880, x_15879) -> h_JB x_15880 x_15879
2522| JNB (x_15882, x_15881) -> h_JNB x_15882 x_15881
2523| JBC (x_15884, x_15883) -> h_JBC x_15884 x_15883
2524| JZ x_15885 -> h_JZ x_15885
2525| JNZ x_15886 -> h_JNZ x_15886
2526| CJNE (x_15888, x_15887) -> h_CJNE x_15888 x_15887
2527| DJNZ (x_15890, x_15889) -> h_DJNZ x_15890 x_15889
2528| ANL x_15891 -> h_ANL x_15891
2529| ORL x_15892 -> h_ORL x_15892
2530| XRL x_15893 -> h_XRL x_15893
2531| CLR x_15894 -> h_CLR x_15894
2532| CPL x_15895 -> h_CPL x_15895
2533| RL x_15896 -> h_RL x_15896
2534| RLC x_15897 -> h_RLC x_15897
2535| RR x_15898 -> h_RR x_15898
2536| RRC x_15899 -> h_RRC x_15899
2537| SWAP x_15900 -> h_SWAP x_15900
2538| MOV x_15901 -> h_MOV x_15901
2539| MOVX x_15902 -> h_MOVX x_15902
2540| SETB x_15903 -> h_SETB x_15903
2541| PUSH x_15904 -> h_PUSH x_15904
2542| POP x_15905 -> h_POP x_15905
2543| XCH (x_15907, x_15906) -> h_XCH x_15907 x_15906
2544| XCHD (x_15909, x_15908) -> h_XCHD x_15909 x_15908
2545| RET -> h_RET
2546| RETI -> h_RETI
2547| NOP -> h_NOP
2548
2549(** val preinstruction_inv_rect_Type4 :
2550    'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
2551    'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2552    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2553    (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
2554    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2555    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2556    (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
2557    'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode
2558    -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1
2559    -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode,
2560    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2561    Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1
2562    -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2563    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2564    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2565    'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2566    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2567    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2568    'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
2569    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2570    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2571    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2572    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2573    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
2574    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2575    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2576    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2577    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2578    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2579    Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode,
2580    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2581    Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2582    -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2583    -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2584    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) ->
2585    (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
2586let preinstruction_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 =
2587  let hcut =
2588    preinstruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
2589      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
2590      h33 h34 h35 h36 h37 hterm
2591  in
2592  hcut __
2593
2594(** val preinstruction_inv_rect_Type3 :
2595    'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
2596    'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2597    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2598    (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
2599    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2600    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2601    (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
2602    'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode
2603    -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1
2604    -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode,
2605    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2606    Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1
2607    -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2608    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2609    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2610    'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2611    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2612    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2613    'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
2614    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2615    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2616    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2617    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2618    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
2619    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2620    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2621    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2622    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2623    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2624    Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode,
2625    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2626    Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2627    -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2628    -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2629    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) ->
2630    (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
2631let preinstruction_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 =
2632  let hcut =
2633    preinstruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
2634      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
2635      h33 h34 h35 h36 h37 hterm
2636  in
2637  hcut __
2638
2639(** val preinstruction_inv_rect_Type2 :
2640    'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
2641    'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2642    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2643    (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
2644    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2645    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2646    (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
2647    'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode
2648    -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1
2649    -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode,
2650    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2651    Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1
2652    -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2653    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2654    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2655    'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2656    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2657    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2658    'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
2659    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2660    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2661    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2662    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2663    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
2664    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2665    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2666    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2667    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2668    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2669    Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode,
2670    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2671    Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2672    -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2673    -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2674    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) ->
2675    (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
2676let preinstruction_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 =
2677  let hcut =
2678    preinstruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
2679      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
2680      h33 h34 h35 h36 h37 hterm
2681  in
2682  hcut __
2683
2684(** val preinstruction_inv_rect_Type1 :
2685    'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
2686    'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2687    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2688    (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
2689    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2690    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2691    (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
2692    'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode
2693    -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1
2694    -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode,
2695    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2696    Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1
2697    -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2698    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2699    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2700    'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2701    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2702    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2703    'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
2704    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2705    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2706    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2707    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2708    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
2709    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2710    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2711    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2712    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2713    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2714    Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode,
2715    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2716    Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2717    -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2718    -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2719    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) ->
2720    (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
2721let preinstruction_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 =
2722  let hcut =
2723    preinstruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
2724      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
2725      h33 h34 h35 h36 h37 hterm
2726  in
2727  hcut __
2728
2729(** val preinstruction_inv_rect_Type0 :
2730    'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
2731    'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2732    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2733    (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
2734    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2735    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2736    (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
2737    'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode
2738    -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1
2739    -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode,
2740    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2741    Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1
2742    -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2743    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2744    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2745    'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
2746    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
2747    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2748    'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
2749    (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
2750    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2751    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2752    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
2753    'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
2754    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2755    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2756    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2757    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2758    Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode)
2759    Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode,
2760    subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
2761    Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2762    -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2)
2763    -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
2764    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) ->
2765    (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
2766let preinstruction_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 =
2767  let hcut =
2768    preinstruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
2769      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
2770      h33 h34 h35 h36 h37 hterm
2771  in
2772  hcut __
2773
2774(** val preinstruction_discr :
2775    'a1 preinstruction -> 'a1 preinstruction -> __ **)
2776let preinstruction_discr x y =
2777  Logic.eq_rect_Type2 x
2778    (match x with
2779     | ADD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2780     | ADDC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2781     | SUBB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2782     | INC a0 -> Obj.magic (fun _ dH -> dH __)
2783     | DEC a0 -> Obj.magic (fun _ dH -> dH __)
2784     | MUL (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2785     | DIV (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2786     | DA a0 -> Obj.magic (fun _ dH -> dH __)
2787     | JC a0 -> Obj.magic (fun _ dH -> dH __)
2788     | JNC a0 -> Obj.magic (fun _ dH -> dH __)
2789     | JB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2790     | JNB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2791     | JBC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2792     | JZ a0 -> Obj.magic (fun _ dH -> dH __)
2793     | JNZ a0 -> Obj.magic (fun _ dH -> dH __)
2794     | CJNE (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2795     | DJNZ (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2796     | ANL a0 -> Obj.magic (fun _ dH -> dH __)
2797     | ORL a0 -> Obj.magic (fun _ dH -> dH __)
2798     | XRL a0 -> Obj.magic (fun _ dH -> dH __)
2799     | CLR a0 -> Obj.magic (fun _ dH -> dH __)
2800     | CPL a0 -> Obj.magic (fun _ dH -> dH __)
2801     | RL a0 -> Obj.magic (fun _ dH -> dH __)
2802     | RLC a0 -> Obj.magic (fun _ dH -> dH __)
2803     | RR a0 -> Obj.magic (fun _ dH -> dH __)
2804     | RRC a0 -> Obj.magic (fun _ dH -> dH __)
2805     | SWAP a0 -> Obj.magic (fun _ dH -> dH __)
2806     | MOV a0 -> Obj.magic (fun _ dH -> dH __)
2807     | MOVX a0 -> Obj.magic (fun _ dH -> dH __)
2808     | SETB a0 -> Obj.magic (fun _ dH -> dH __)
2809     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
2810     | POP a0 -> Obj.magic (fun _ dH -> dH __)
2811     | XCH (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2812     | XCHD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2813     | RET -> Obj.magic (fun _ dH -> dH)
2814     | RETI -> Obj.magic (fun _ dH -> dH)
2815     | NOP -> Obj.magic (fun _ dH -> dH)) y
2816
2817(** val preinstruction_jmdiscr :
2818    'a1 preinstruction -> 'a1 preinstruction -> __ **)
2819let preinstruction_jmdiscr x y =
2820  Logic.eq_rect_Type2 x
2821    (match x with
2822     | ADD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2823     | ADDC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2824     | SUBB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2825     | INC a0 -> Obj.magic (fun _ dH -> dH __)
2826     | DEC a0 -> Obj.magic (fun _ dH -> dH __)
2827     | MUL (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2828     | DIV (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2829     | DA a0 -> Obj.magic (fun _ dH -> dH __)
2830     | JC a0 -> Obj.magic (fun _ dH -> dH __)
2831     | JNC a0 -> Obj.magic (fun _ dH -> dH __)
2832     | JB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2833     | JNB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2834     | JBC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2835     | JZ a0 -> Obj.magic (fun _ dH -> dH __)
2836     | JNZ a0 -> Obj.magic (fun _ dH -> dH __)
2837     | CJNE (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2838     | DJNZ (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2839     | ANL a0 -> Obj.magic (fun _ dH -> dH __)
2840     | ORL a0 -> Obj.magic (fun _ dH -> dH __)
2841     | XRL a0 -> Obj.magic (fun _ dH -> dH __)
2842     | CLR a0 -> Obj.magic (fun _ dH -> dH __)
2843     | CPL a0 -> Obj.magic (fun _ dH -> dH __)
2844     | RL a0 -> Obj.magic (fun _ dH -> dH __)
2845     | RLC a0 -> Obj.magic (fun _ dH -> dH __)
2846     | RR a0 -> Obj.magic (fun _ dH -> dH __)
2847     | RRC a0 -> Obj.magic (fun _ dH -> dH __)
2848     | SWAP a0 -> Obj.magic (fun _ dH -> dH __)
2849     | MOV a0 -> Obj.magic (fun _ dH -> dH __)
2850     | MOVX a0 -> Obj.magic (fun _ dH -> dH __)
2851     | SETB a0 -> Obj.magic (fun _ dH -> dH __)
2852     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
2853     | POP a0 -> Obj.magic (fun _ dH -> dH __)
2854     | XCH (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2855     | XCHD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
2856     | RET -> Obj.magic (fun _ dH -> dH)
2857     | RETI -> Obj.magic (fun _ dH -> dH)
2858     | NOP -> Obj.magic (fun _ dH -> dH)) y
2859
2860(** val eq_preinstruction :
2861    subaddressing_mode preinstruction -> subaddressing_mode preinstruction ->
2862    Bool.bool **)
2863let eq_preinstruction i j =
2864  match i with
2865  | ADD (arg1, arg2) ->
2866    (match j with
2867     | ADD (arg1', arg2') ->
2868       Bool.andb
2869         (eq_addressing_mode
2870           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
2871             Vector.VEmpty)) arg1)
2872           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
2873             Vector.VEmpty)) arg1'))
2874         (eq_addressing_mode
2875           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
2876             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
2877             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
2878             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2)
2879           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
2880             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
2881             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
2882             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2'))
2883     | ADDC (x, x0) -> Bool.False
2884     | SUBB (x, x0) -> Bool.False
2885     | INC x -> Bool.False
2886     | DEC x -> Bool.False
2887     | MUL (x, x0) -> Bool.False
2888     | DIV (x, x0) -> Bool.False
2889     | DA x -> Bool.False
2890     | JC x -> Bool.False
2891     | JNC x -> Bool.False
2892     | JB (x, x0) -> Bool.False
2893     | JNB (x, x0) -> Bool.False
2894     | JBC (x, x0) -> Bool.False
2895     | JZ x -> Bool.False
2896     | JNZ x -> Bool.False
2897     | CJNE (x, x0) -> Bool.False
2898     | DJNZ (x, x0) -> Bool.False
2899     | ANL x -> Bool.False
2900     | ORL x -> Bool.False
2901     | XRL x -> Bool.False
2902     | CLR x -> Bool.False
2903     | CPL x -> Bool.False
2904     | RL x -> Bool.False
2905     | RLC x -> Bool.False
2906     | RR x -> Bool.False
2907     | RRC x -> Bool.False
2908     | SWAP x -> Bool.False
2909     | MOV x -> Bool.False
2910     | MOVX x -> Bool.False
2911     | SETB x -> Bool.False
2912     | PUSH x -> Bool.False
2913     | POP x -> Bool.False
2914     | XCH (x, x0) -> Bool.False
2915     | XCHD (x, x0) -> Bool.False
2916     | RET -> Bool.False
2917     | RETI -> Bool.False
2918     | NOP -> Bool.False)
2919  | ADDC (arg1, arg2) ->
2920    (match j with
2921     | ADD (x, x0) -> Bool.False
2922     | ADDC (arg1', arg2') ->
2923       Bool.andb
2924         (eq_addressing_mode
2925           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
2926             Vector.VEmpty)) arg1)
2927           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
2928             Vector.VEmpty)) arg1'))
2929         (eq_addressing_mode
2930           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
2931             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
2932             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
2933             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2)
2934           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
2935             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
2936             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
2937             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2'))
2938     | SUBB (x, x0) -> Bool.False
2939     | INC x -> Bool.False
2940     | DEC x -> Bool.False
2941     | MUL (x, x0) -> Bool.False
2942     | DIV (x, x0) -> Bool.False
2943     | DA x -> Bool.False
2944     | JC x -> Bool.False
2945     | JNC x -> Bool.False
2946     | JB (x, x0) -> Bool.False
2947     | JNB (x, x0) -> Bool.False
2948     | JBC (x, x0) -> Bool.False
2949     | JZ x -> Bool.False
2950     | JNZ x -> Bool.False
2951     | CJNE (x, x0) -> Bool.False
2952     | DJNZ (x, x0) -> Bool.False
2953     | ANL x -> Bool.False
2954     | ORL x -> Bool.False
2955     | XRL x -> Bool.False
2956     | CLR x -> Bool.False
2957     | CPL x -> Bool.False
2958     | RL x -> Bool.False
2959     | RLC x -> Bool.False
2960     | RR x -> Bool.False
2961     | RRC x -> Bool.False
2962     | SWAP x -> Bool.False
2963     | MOV x -> Bool.False
2964     | MOVX x -> Bool.False
2965     | SETB x -> Bool.False
2966     | PUSH x -> Bool.False
2967     | POP x -> Bool.False
2968     | XCH (x, x0) -> Bool.False
2969     | XCHD (x, x0) -> Bool.False
2970     | RET -> Bool.False
2971     | RETI -> Bool.False
2972     | NOP -> Bool.False)
2973  | SUBB (arg1, arg2) ->
2974    (match j with
2975     | ADD (x, x0) -> Bool.False
2976     | ADDC (x, x0) -> Bool.False
2977     | SUBB (arg1', arg2') ->
2978       Bool.andb
2979         (eq_addressing_mode
2980           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
2981             Vector.VEmpty)) arg1)
2982           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
2983             Vector.VEmpty)) arg1'))
2984         (eq_addressing_mode
2985           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
2986             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
2987             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
2988             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2)
2989           (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
2990             ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S
2991             (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect,
2992             (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2'))
2993     | INC x -> Bool.False
2994     | DEC x -> Bool.False
2995     | MUL (x, x0) -> Bool.False
2996     | DIV (x, x0) -> Bool.False
2997     | DA x -> Bool.False
2998     | JC x -> Bool.False
2999     | JNC x -> Bool.False
3000     | JB (x, x0) -> Bool.False
3001     | JNB (x, x0) -> Bool.False
3002     | JBC (x, x0) -> Bool.False
3003     | JZ x -> Bool.False
3004     | JNZ x -> Bool.False
3005     | CJNE (x, x0) -> Bool.False
3006     | DJNZ (x, x0) -> Bool.False
3007     | ANL x -> Bool.False
3008     | ORL x -> Bool.False
3009     | XRL x -> Bool.False
3010     | CLR x -> Bool.False
3011     | CPL x -> Bool.False
3012     | RL x -> Bool.False
3013     | RLC x -> Bool.False
3014     | RR x -> Bool.False
3015     | RRC x -> Bool.False
3016     | SWAP x -> Bool.False
3017     | MOV x -> Bool.False
3018     | MOVX x -> Bool.False
3019     | SETB x -> Bool.False
3020     | PUSH x -> Bool.False
3021     | POP x -> Bool.False
3022     | XCH (x, x0) -> Bool.False
3023     | XCHD (x, x0) -> Bool.False
3024     | RET -> Bool.False
3025     | RETI -> Bool.False
3026     | NOP -> Bool.False)
3027  | INC arg ->
3028    (match j with
3029     | ADD (x, x0) -> Bool.False
3030     | ADDC (x, x0) -> Bool.False
3031     | SUBB (x, x0) -> Bool.False
3032     | INC arg' ->
3033       eq_addressing_mode
3034         (subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
3035           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Acc_a,
3036           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
3037           (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
3038           ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Dptr,
3039           Vector.VEmpty)))))))))) arg)
3040         (subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
3041           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Acc_a,
3042           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr,
3043           (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons
3044           ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Dptr,
3045           Vector.VEmpty)))))))))) arg')
3046     | DEC x -> Bool.False
3047     | MUL (x, x0) -> Bool.False
3048     | DIV (x, x0) -> Bool.False
3049     | DA x -> Bool.False
3050     | JC x -> Bool.False
3051     | JNC x -> Bool.False
3052     | JB (x, x0) -> Bool.False
3053     | JNB (x, x0) -> Bool.False
3054     | JBC (x, x0) -> Bool.False
3055     | JZ x -> Bool.False
3056     | JNZ x -> Bool.False
3057     | CJNE (x, x0) -> Bool.False
3058     | DJNZ (x, x0) -> Bool.False
3059     | ANL x -> Bool.False
3060     | ORL x -> Bool.False
3061     | XRL x -> Bool.False
3062     | CLR x -> Bool.False
3063     | CPL x -> Bool.False
3064     | RL x -> Bool.False
3065     | RLC x -> Bool.False
3066     | RR x -> Bool.False
3067     | RRC x -> Bool.False
3068     | SWAP x -> Bool.False
3069     | MOV x -> Bool.False
3070     | MOVX x -> Bool.False
3071     | SETB x -> Bool.False
3072     | PUSH x -> Bool.False
3073     | POP x -> Bool.False
3074     | XCH (x, x0) -> Bool.False
3075     | XCHD (x, x0) -> Bool.False
3076     | RET -> Bool.False
3077     | RETI -> Bool.False
3078     | NOP -> Bool.False)
3079  | DEC arg ->
3080    (match j with
3081     | ADD (x, x0) -> Bool.False
3082     | ADDC (x, x0) -> Bool.False
3083     | SUBB (x, x0) -> Bool.False
3084     | INC x -> Bool.False
3085     | DEC arg' ->
3086       eq_addressing_mode
3087         (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
3088           ((Nat.S (Nat.S (Nat.S Nat.O))), Acc_a, (Vector.VCons ((Nat.S
3089           (Nat.S Nat.O)), Registr, (Vector.VCons ((Nat.S Nat.O), Direct,
3090           (Vector.VCons (Nat.O, Indirect, Vector.VEmpty)))))))) arg)
3091         (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
3092           ((Nat.S (Nat.S (Nat.S Nat.O))), Acc_a, (Vector.VCons ((Nat.S
3093           (Nat.S Nat.O)), Registr, (Vector.VCons ((Nat.S Nat.O), Direct,
3094           (Vector.VCons (Nat.O, Indirect, Vector.VEmpty)))))))) arg')
3095     | MUL (x, x0) -> Bool.False
3096     | DIV (x, x0) -> Bool.False
3097     | DA x -> Bool.False
3098     | JC x -> Bool.False
3099     | JNC x -> Bool.False
3100     | JB (x, x0) -> Bool.False
3101     | JNB (x, x0) -> Bool.False
3102     | JBC (x, x0) -> Bool.False
3103     | JZ x -> Bool.False
3104     | JNZ x -> Bool.False
3105     | CJNE (x, x0) -> Bool.False
3106     | DJNZ (x, x0) -> Bool.False
3107     | ANL x -> Bool.False
3108     | ORL x -> Bool.False
3109     | XRL x -> Bool.False
3110     | CLR x -> Bool.False
3111     | CPL x -> Bool.False
3112     | RL x -> Bool.False
3113     | RLC x -> Bool.False
3114     | RR x -> Bool.False
3115     | RRC x -> Bool.False
3116     | SWAP x -> Bool.False
3117     | MOV x -> Bool.False
3118     | MOVX x -> Bool.False
3119     | SETB x -> Bool.False
3120     | PUSH x -> Bool.False
3121     | POP x -> Bool.False
3122     | XCH (x, x0) -> Bool.False
3123     | XCHD (x, x0) -> Bool.False
3124     | RET -> Bool.False
3125     | RETI -> Bool.False
3126     | NOP -> Bool.False)
3127  | MUL (arg1, arg2) ->
3128    (match j with
3129     | ADD (x, x0) -> Bool.False
3130     | ADDC (x, x0) -> Bool.False
3131     | SUBB (x, x0) -> Bool.False
3132     | INC x -> Bool.False
3133     | DEC x -> Bool.False
3134     | MUL (arg1', arg2') ->
3135       Bool.andb
3136         (eq_addressing_mode
3137           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3138             Vector.VEmpty)) arg1)
3139           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3140             Vector.VEmpty)) arg1'))
3141         (eq_addressing_mode
3142           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_b,
3143             Vector.VEmpty)) arg2)
3144           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_b,
3145             Vector.VEmpty)) arg2'))
3146     | DIV (x, x0) -> Bool.False
3147     | DA x -> Bool.False
3148     | JC x -> Bool.False
3149     | JNC x -> Bool.False
3150     | JB (x, x0) -> Bool.False
3151     | JNB (x, x0) -> Bool.False
3152     | JBC (x, x0) -> Bool.False
3153     | JZ x -> Bool.False
3154     | JNZ x -> Bool.False
3155     | CJNE (x, x0) -> Bool.False
3156     | DJNZ (x, x0) -> Bool.False
3157     | ANL x -> Bool.False
3158     | ORL x -> Bool.False
3159     | XRL x -> Bool.False
3160     | CLR x -> Bool.False
3161     | CPL x -> Bool.False
3162     | RL x -> Bool.False
3163     | RLC x -> Bool.False
3164     | RR x -> Bool.False
3165     | RRC x -> Bool.False
3166     | SWAP x -> Bool.False
3167     | MOV x -> Bool.False
3168     | MOVX x -> Bool.False
3169     | SETB x -> Bool.False
3170     | PUSH x -> Bool.False
3171     | POP x -> Bool.False
3172     | XCH (x, x0) -> Bool.False
3173     | XCHD (x, x0) -> Bool.False
3174     | RET -> Bool.False
3175     | RETI -> Bool.False
3176     | NOP -> Bool.False)
3177  | DIV (arg1, arg2) ->
3178    (match j with
3179     | ADD (x, x0) -> Bool.False
3180     | ADDC (x, x0) -> Bool.False
3181     | SUBB (x, x0) -> Bool.False
3182     | INC x -> Bool.False
3183     | DEC x -> Bool.False
3184     | MUL (x, x0) -> Bool.False
3185     | DIV (arg1', arg2') ->
3186       Bool.andb
3187         (eq_addressing_mode
3188           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3189             Vector.VEmpty)) arg1)
3190           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3191             Vector.VEmpty)) arg1'))
3192         (eq_addressing_mode
3193           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_b,
3194             Vector.VEmpty)) arg2)
3195           (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_b,
3196             Vector.VEmpty)) arg2'))
3197     | DA x -> Bool.False
3198     | JC x -> Bool.False
3199     | JNC x -> Bool.False
3200     | JB (x, x0) -> Bool.False
3201     | JNB (x, x0) -> Bool.False
3202     | JBC (x, x0) -> Bool.False
3203     | JZ x -> Bool.False
3204     | JNZ x -> Bool.False
3205     | CJNE (x, x0) -> Bool.False
3206     | DJNZ (x, x0) -> Bool.False
3207     | ANL x -> Bool.False
3208     | ORL x -> Bool.False
3209     | XRL x -> Bool.False
3210     | CLR x -> Bool.False
3211     | CPL x -> Bool.False
3212     | RL x -> Bool.False
3213     | RLC x -> Bool.False
3214     | RR x -> Bool.False
3215     | RRC x -> Bool.False
3216     | SWAP x -> Bool.False
3217     | MOV x -> Bool.False
3218     | MOVX x -> Bool.False
3219     | SETB x -> Bool.False
3220     | PUSH x -> Bool.False
3221     | POP x -> Bool.False
3222     | XCH (x, x0) -> Bool.False
3223     | XCHD (x, x0) -> Bool.False
3224     | RET -> Bool.False
3225     | RETI -> Bool.False
3226     | NOP -> Bool.False)
3227  | DA arg ->
3228    (match j with
3229     | ADD (x, x0) -> Bool.False
3230     | ADDC (x, x0) -> Bool.False
3231     | SUBB (x, x0) -> Bool.False
3232     | INC x -> Bool.False
3233     | DEC x -> Bool.False
3234     | MUL (x, x0) -> Bool.False
3235     | DIV (x, x0) -> Bool.False
3236     | DA arg' ->
3237       eq_addressing_mode
3238         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3239           Vector.VEmpty)) arg)
3240         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a,
3241           Vector.VEmpty)) arg')
3242     | JC x -> Bool.False
3243     | JNC x -> Bool.False
3244     | JB (x, x0) -> Bool.False
3245     | JNB (x, x0) -> Bool.False
3246     | JBC (x, x0) -> Bool.False
3247     | JZ x -> Bool.False
3248     | JNZ x -> Bool.False
3249     | CJNE (x, x0) -> Bool.False
3250     | DJNZ (x, x0) -> Bool.False
3251     | ANL x -> Bool.False
3252     | ORL x -> Bool.False
3253     | XRL x -> Bool.False
3254     | CLR x -> Bool.False
3255     | CPL x -> Bool.False
3256     | RL x -> Bool.False
3257     | RLC x -> Bool.False
3258     | RR x -> Bool.False
3259     | RRC x -> Bool.False
3260     | SWAP x -> Bool.False
3261     | MOV x -> Bool.False
3262     | MOVX x -> Bool.False
3263     | SETB x -> Bool.False
3264     | PUSH x -> Bool.False
3265     | POP x -> Bool.False
3266     | XCH (x, x0) -> Bool.False
3267     | XCHD (x, x0) -> Bool.False
3268     | RET -> Bool.False
3269     | RETI -> Bool.False
3270     | NOP -> Bool.False)
3271  | JC arg ->
3272    (match j with
3273     | ADD (x, x0) -> Bool.False
3274     | ADDC (x, x0) -> Bool.False
3275     | SUBB (x, x0) -> Bool.False
3276     | INC x -> Bool.False
3277     | DEC x -> Bool.False
3278     | MUL (x, x0) -> Bool.False
3279     | DIV (x, x0) -> Bool.False
3280     | DA x -> Bool.False
3281     | JC arg' ->
3282       eq_addressing_mode
3283         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3284           Vector.VEmpty)) arg)
3285         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
3286           Vector.VEmpty)) arg')
3287     | JNC x -> Bool.False
3288     | JB (x, x0) -> Bool.False
3289     | JNB (x, x0) -> Bool.False
3290     | JBC (x, x0) -> Bool.False
3291     | JZ x -> Bool.False
3292     | JNZ x -> Bool.False
3293     | CJNE (x, x0) -> Bool.False
3294     | DJNZ (x, x0) -> Bool.False
3295     | ANL x -> Bool.False
3296     | ORL x -> Bool.False
3297     | XRL x -> Bool.False
3298     | CLR x -> Bool.False
3299     | CPL x -> Bool.False
3300     | RL x -> Bool.False
3301     | RLC x -> Bool.False
3302     | RR x -> Bool.False
3303     | RRC x -> Bool.False
3304     | SWAP x -> Bool.False
3305     | MOV x -> Bool.False
3306     | MOVX x -> Bool.False
3307     | SETB x -> Bool.False
3308     | PUSH x -> Bool.False
3309<