source: driver/extracted/assembly.ml @ 3106

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

New extraction.
File size: 182.2 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Extralib
30
31open BitVectorTrie
32
33open String
34
35open Integers
36
37open AST
38
39open LabelledObjects
40
41open Proper
42
43open PositiveMap
44
45open Deqsets
46
47open ErrorMessages
48
49open PreIdentifiers
50
51open Errors
52
53open Lists
54
55open Positive
56
57open Identifiers
58
59open CostLabel
60
61open ASM
62
63open Exp
64
65open Setoids
66
67open Monad
68
69open Option
70
71open Extranat
72
73open Vector
74
75open FoldStuff
76
77open BitVector
78
79open Arithmetic
80
81open Fetch
82
83open Status
84
85type jump_length =
86| Short_jump
87| Absolute_jump
88| Long_jump
89
90(** val jump_length_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
91let rec jump_length_rect_Type4 h_short_jump h_absolute_jump h_long_jump = function
92| Short_jump -> h_short_jump
93| Absolute_jump -> h_absolute_jump
94| Long_jump -> h_long_jump
95
96(** val jump_length_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
97let rec jump_length_rect_Type5 h_short_jump h_absolute_jump h_long_jump = function
98| Short_jump -> h_short_jump
99| Absolute_jump -> h_absolute_jump
100| Long_jump -> h_long_jump
101
102(** val jump_length_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
103let rec jump_length_rect_Type3 h_short_jump h_absolute_jump h_long_jump = function
104| Short_jump -> h_short_jump
105| Absolute_jump -> h_absolute_jump
106| Long_jump -> h_long_jump
107
108(** val jump_length_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
109let rec jump_length_rect_Type2 h_short_jump h_absolute_jump h_long_jump = function
110| Short_jump -> h_short_jump
111| Absolute_jump -> h_absolute_jump
112| Long_jump -> h_long_jump
113
114(** val jump_length_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
115let rec jump_length_rect_Type1 h_short_jump h_absolute_jump h_long_jump = function
116| Short_jump -> h_short_jump
117| Absolute_jump -> h_absolute_jump
118| Long_jump -> h_long_jump
119
120(** val jump_length_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
121let rec jump_length_rect_Type0 h_short_jump h_absolute_jump h_long_jump = function
122| Short_jump -> h_short_jump
123| Absolute_jump -> h_absolute_jump
124| Long_jump -> h_long_jump
125
126(** val jump_length_inv_rect_Type4 :
127    jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
128let jump_length_inv_rect_Type4 hterm h1 h2 h3 =
129  let hcut = jump_length_rect_Type4 h1 h2 h3 hterm in hcut __
130
131(** val jump_length_inv_rect_Type3 :
132    jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
133let jump_length_inv_rect_Type3 hterm h1 h2 h3 =
134  let hcut = jump_length_rect_Type3 h1 h2 h3 hterm in hcut __
135
136(** val jump_length_inv_rect_Type2 :
137    jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
138let jump_length_inv_rect_Type2 hterm h1 h2 h3 =
139  let hcut = jump_length_rect_Type2 h1 h2 h3 hterm in hcut __
140
141(** val jump_length_inv_rect_Type1 :
142    jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
143let jump_length_inv_rect_Type1 hterm h1 h2 h3 =
144  let hcut = jump_length_rect_Type1 h1 h2 h3 hterm in hcut __
145
146(** val jump_length_inv_rect_Type0 :
147    jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
148let jump_length_inv_rect_Type0 hterm h1 h2 h3 =
149  let hcut = jump_length_rect_Type0 h1 h2 h3 hterm in hcut __
150
151(** val jump_length_discr : jump_length -> jump_length -> __ **)
152let jump_length_discr x y =
153  Logic.eq_rect_Type2 x
154    (match x with
155     | Short_jump -> Obj.magic (fun _ dH -> dH)
156     | Absolute_jump -> Obj.magic (fun _ dH -> dH)
157     | Long_jump -> Obj.magic (fun _ dH -> dH)) y
158
159(** val jump_length_jmdiscr : jump_length -> jump_length -> __ **)
160let jump_length_jmdiscr x y =
161  Logic.eq_rect_Type2 x
162    (match x with
163     | Short_jump -> Obj.magic (fun _ dH -> dH)
164     | Absolute_jump -> Obj.magic (fun _ dH -> dH)
165     | Long_jump -> Obj.magic (fun _ dH -> dH)) y
166
167(** val short_jump_cond :
168    BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector)
169    Types.prod **)
170let short_jump_cond pc_plus_jmp_length addr =
171  let { Types.fst = result; Types.snd = flags } =
172    Arithmetic.sub_16_with_carry addr pc_plus_jmp_length Bool.False
173  in
174  let { Types.fst = upper; Types.snd = lower } =
175    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
176      (Nat.S Nat.O))))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
177      Nat.O))))))) result
178  in
179  (match Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags with
180   | Bool.True ->
181     { Types.fst =
182       (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
183         (Nat.S (Nat.S Nat.O))))))))) upper (Vector.VCons ((Nat.S (Nat.S
184         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), Bool.True,
185         (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
186         Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
187         (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
188         (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S
189         (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S
190         (Nat.S (Nat.S Nat.O))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
191         Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True,
192         (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))))));
193       Types.snd = (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
194       (Nat.S Nat.O))))))), Bool.True, lower)) }
195   | Bool.False ->
196     { Types.fst =
197       (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
198         (Nat.S (Nat.S Nat.O))))))))) upper
199         (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
200           (Nat.S (Nat.S Nat.O))))))))))); Types.snd = (Vector.VCons ((Nat.S
201       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False,
202       lower)) })
203
204(** val absolute_jump_cond :
205    BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector)
206    Types.prod **)
207let absolute_jump_cond pc_plus_jmp_length addr =
208  let { Types.fst = fst_5_addr; Types.snd = rest_addr } =
209    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S
210      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
211      Nat.O))))))))))) addr
212  in
213  let { Types.fst = fst_5_pc; Types.snd = rest_pc } =
214    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S
215      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
216      Nat.O))))))))))) pc_plus_jmp_length
217  in
218  { Types.fst =
219  (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) fst_5_addr
220    fst_5_pc); Types.snd = rest_addr }
221
222(** val assembly_preinstruction :
223    ('a1 -> BitVector.byte) -> 'a1 ASM.preinstruction -> Bool.bool
224    Vector.vector List.list **)
225let assembly_preinstruction addr_of = function
226| ASM.ADD (addr1, addr2) ->
227  (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
228           ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S
229           (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O),
230           ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
231           Vector.VEmpty)))))))) addr2 with
232   | ASM.DIRECT b1 ->
233     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
234       (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
235       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
236       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
237       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
238       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
239       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
240       Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
241       Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
242   | ASM.INDIRECT i1 ->
243     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
244       (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
245       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
246       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
247       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
248       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
249       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
250       Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
251       Vector.VEmpty)))))))))))))))), List.Nil))
252   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
253   | ASM.REGISTER r ->
254     (fun _ -> List.Cons
255       ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
256          (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
257          Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
258          Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
259          Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
260          (Nat.O, Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
261   | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
262   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
263   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
264   | ASM.DATA b1 ->
265     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
266       (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
267       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
268       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
269       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
270       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
271       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
272       Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
273       Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
274   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
275   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
276   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
277   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
278   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
279   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
280   | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
281   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
282   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
283   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
284   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
285| ASM.ADDC (addr1, addr2) ->
286  (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
287           ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S
288           (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O),
289           ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
290           Vector.VEmpty)))))))) addr2 with
291   | ASM.DIRECT b1 ->
292     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
293       (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
294       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
295       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
296       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
297       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
298       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
299       Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
300       Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
301   | ASM.INDIRECT i1 ->
302     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
303       (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
304       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
305       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
306       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
307       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
308       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
309       Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
310       Vector.VEmpty)))))))))))))))), List.Nil))
311   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
312   | ASM.REGISTER r ->
313     (fun _ -> List.Cons
314       ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
315          (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
316          Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
317          Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
318          Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
319          (Nat.O, Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
320   | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
321   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
322   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
323   | ASM.DATA b1 ->
324     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
325       (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
326       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
327       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
328       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
329       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
330       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
331       Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
332       Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
333   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
334   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
335   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
336   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
337   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
338   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
339   | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
340   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
341   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
342   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
343   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
344| ASM.SUBB (addr1, addr2) ->
345  (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
346           ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S
347           (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O),
348           ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
349           Vector.VEmpty)))))))) addr2 with
350   | ASM.DIRECT b1 ->
351     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
352       (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
353       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
354       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
355       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
356       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
357       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
358       Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
359       Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
360   | ASM.INDIRECT i1 ->
361     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
362       (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
363       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
364       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
365       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
366       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
367       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
368       Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
369       Vector.VEmpty)))))))))))))))), List.Nil))
370   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
371   | ASM.REGISTER r ->
372     (fun _ -> List.Cons
373       ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
374          (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
375          Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
376          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
377          (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
378          Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
379   | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
380   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
381   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
382   | ASM.DATA b1 ->
383     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
384       (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
385       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
386       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
387       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
388       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
389       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
390       Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
391       Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
392   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
393   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
394   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
395   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
396   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
397   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
398   | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
399   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
400   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
401   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
402   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
403| ASM.INC addr ->
404  (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
405           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Acc_a,
406           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr,
407           (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons
408           ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Dptr,
409           Vector.VEmpty)))))))))) addr with
410   | ASM.DIRECT b1 ->
411     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
412       (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
413       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
414       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
415       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
416       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
417       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
418       Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
419       Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
420   | ASM.INDIRECT i1 ->
421     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
422       (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
423       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
424       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
425       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
426       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
427       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
428       Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
429       Vector.VEmpty)))))))))))))))), List.Nil))
430   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
431   | ASM.REGISTER r ->
432     (fun _ -> List.Cons
433       ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
434          (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
435          Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
436          Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
437          Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
438          (Nat.O, Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
439   | ASM.ACC_A ->
440     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
441       (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
442       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
443       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
444       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
445       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
446       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
447       Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
448       Vector.VEmpty)))))))))))))))), List.Nil))
449   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
450   | ASM.DPTR ->
451     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
452       (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
453       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
454       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
455       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
456       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
457       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
458       ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
459       Vector.VEmpty)))))))))))))))), List.Nil))
460   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
461   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
462   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
463   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
464   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
465   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
466   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
467   | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
468   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
469   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
470   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
471   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
472| ASM.DEC addr ->
473  (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
474           ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S
475           (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O),
476           ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect,
477           Vector.VEmpty)))))))) addr with
478   | ASM.DIRECT b1 ->
479     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
480       (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
481       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
482       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
483       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
484       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
485       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
486       Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
487       Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
488   | ASM.INDIRECT i1 ->
489     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
490       (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
491       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
492       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
493       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
494       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
495       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
496       Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
497       Vector.VEmpty)))))))))))))))), List.Nil))
498   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
499   | ASM.REGISTER r ->
500     (fun _ -> List.Cons
501       ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
502          (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
503          Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
504          Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
505          Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
506          (Nat.O, Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
507   | ASM.ACC_A ->
508     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
509       (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
510       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
511       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
512       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
513       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
514       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
515       Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
516       Vector.VEmpty)))))))))))))))), List.Nil))
517   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
518   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
519   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
520   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
521   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
522   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
523   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
524   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
525   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
526   | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
527   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
528   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
529   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
530   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
531| ASM.MUL (addr1, addr2) ->
532  List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
533    Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
534    (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
535    (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
536    (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
537    Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
538    (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
539    Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
540| ASM.DIV (addr1, addr2) ->
541  List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
542    Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
543    (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
544    (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
545    (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
546    Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
547    (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
548    Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
549| ASM.DA addr ->
550  List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
551    Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
552    (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
553    (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
554    (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
555    Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
556    (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
557    Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
558| ASM.JC addr ->
559  let b1 = addr_of addr in
560  List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
561  Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
562  (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
563  (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
564  Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
565  Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
566  ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
567  Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil)))
568| ASM.JNC addr ->
569  let b1 = addr_of addr in
570  List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
571  Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
572  (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
573  (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
574  Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
575  Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
576  ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
577  Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil)))
578| ASM.JB (addr1, addr2) ->
579  let b2 = addr_of addr2 in
580  (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Bit_addr,
581           Vector.VEmpty)) addr1 with
582   | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
583   | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
584   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
585   | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
586   | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
587   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
588   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
589   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
590   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
591   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
592   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
593   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
594   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
595   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
596   | ASM.BIT_ADDR b1 ->
597     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
598       (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
599       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
600       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
601       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
602       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
603       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
604       ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
605       Vector.VEmpty)))))))))))))))), (List.Cons (b1, (List.Cons (b2,
606       List.Nil))))))
607   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
608   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
609   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
610   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
611| ASM.JNB (addr1, addr2) ->
612  let b2 = addr_of addr2 in
613  (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Bit_addr,
614           Vector.VEmpty)) addr1 with
615   | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
616   | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
617   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
618   | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
619   | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
620   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
621   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
622   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
623   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
624   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
625   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
626   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
627   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
628   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
629   | ASM.BIT_ADDR b1 ->
630     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
631       (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
632       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
633       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
634       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
635       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
636       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
637       ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
638       Vector.VEmpty)))))))))))))))), (List.Cons (b1, (List.Cons (b2,
639       List.Nil))))))
640   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
641   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
642   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
643   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
644| ASM.JBC (addr1, addr2) ->
645  let b2 = addr_of addr2 in
646  (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Bit_addr,
647           Vector.VEmpty)) addr1 with
648   | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
649   | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
650   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
651   | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
652   | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
653   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
654   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
655   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
656   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
657   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
658   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
659   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
660   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
661   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
662   | ASM.BIT_ADDR b1 ->
663     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
664       (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
665       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
666       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
667       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
668       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
669       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
670       ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
671       Vector.VEmpty)))))))))))))))), (List.Cons (b1, (List.Cons (b2,
672       List.Nil))))))
673   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
674   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
675   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
676   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
677| ASM.JZ addr ->
678  let b1 = addr_of addr in
679  List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
680  Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
681  (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
682  (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
683  Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
684  Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
685  ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
686  Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil)))
687| ASM.JNZ addr ->
688  let b1 = addr_of addr in
689  List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
690  Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
691  (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
692  (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
693  Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
694  Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
695  ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
696  Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil)))
697| ASM.CJNE (addrs, addr3) ->
698  let b3 = addr_of addr3 in
699  (match addrs with
700   | Types.Inl addrs0 ->
701     let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
702     (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
703              Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Data,
704              Vector.VEmpty)))) addr2 with
705      | ASM.DIRECT b1 ->
706        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
707          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
708          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
709          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
710          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
711          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
712          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
713          (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
714          Bool.True, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
715          (List.Cons (b3, List.Nil))))))
716      | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
717      | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
718      | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
719      | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
720      | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
721      | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
722      | ASM.DATA b1 ->
723        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
724          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
725          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
726          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
727          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
728          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
729          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
730          (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
731          Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
732          (List.Cons (b3, List.Nil))))))
733      | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
734      | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
735      | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
736      | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
737      | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
738      | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
739      | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
740      | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
741      | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
742      | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
743      | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
744   | Types.Inr addrs0 ->
745     let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
746     let b2 =
747       (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Data,
748                Vector.VEmpty)) addr2 with
749        | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
750        | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
751        | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
752        | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
753        | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
754        | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
755        | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
756        | ASM.DATA b2 -> (fun _ -> b2)
757        | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
758        | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
759        | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
760        | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
761        | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
762        | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
763        | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
764        | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
765        | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
766        | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
767        | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
768     in
769     (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
770              Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Indirect,
771              Vector.VEmpty)))) addr1 with
772      | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
773      | ASM.INDIRECT i1 ->
774        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
775          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
776          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
777          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
778          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
779          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
780          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
781          (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
782          Vector.VEmpty)))))))))))))))), (List.Cons (b2, (List.Cons (b3,
783          List.Nil))))))
784      | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
785      | ASM.REGISTER r ->
786        (fun _ -> List.Cons
787          ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
788             (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
789             (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
790             (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
791             Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True,
792             (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))) r),
793          (List.Cons (b2, (List.Cons (b3, List.Nil))))))
794      | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
795      | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
796      | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
797      | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
798      | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
799      | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
800      | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
801      | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
802      | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
803      | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
804      | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
805      | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
806      | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
807      | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
808      | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
809| ASM.DJNZ (addr1, addr2) ->
810  let b2 = addr_of addr2 in
811  (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
812           ASM.Registr, (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty))))
813           addr1 with
814   | ASM.DIRECT b1 ->
815     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
816       (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
817       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
818       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
819       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
820       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
821       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
822       Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
823       Vector.VEmpty)))))))))))))))), (List.Cons (b1, (List.Cons (b2,
824       List.Nil))))))
825   | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
826   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
827   | ASM.REGISTER r ->
828     (fun _ -> List.Cons
829       ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
830          (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
831          Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
832          Bool.True, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
833          (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
834          Bool.True, Vector.VEmpty)))))))))) r), (List.Cons (b2, List.Nil))))
835   | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
836   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
837   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
838   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
839   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
840   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
841   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
842   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
843   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
844   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
845   | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
846   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
847   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
848   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
849   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
850| ASM.ANL addrs ->
851  (match addrs with
852   | Types.Inl addrs0 ->
853     (match addrs0 with
854      | Types.Inl addrs1 ->
855        let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in
856        (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
857                 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr,
858                 (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct,
859                 (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons
860                 (Nat.O, ASM.Data, Vector.VEmpty)))))))) addr2 with
861         | ASM.DIRECT b1 ->
862           (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
863             (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
864             ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
865             Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
866             Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
867             (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
868             Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
869             Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
870             (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
871             (List.Cons (b1, List.Nil))))
872         | ASM.INDIRECT i1 ->
873           (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
874             (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
875             ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
876             Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
877             Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
878             (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
879             Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
880             Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True,
881             (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))),
882             List.Nil))
883         | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
884         | ASM.REGISTER r ->
885           (fun _ -> List.Cons
886             ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
887                (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
888                (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S
889                (Nat.S (Nat.S Nat.O))), Bool.True, (Vector.VCons ((Nat.S
890                (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O),
891                Bool.True, (Vector.VCons (Nat.O, Bool.True,
892                Vector.VEmpty)))))))))) r), List.Nil))
893         | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
894         | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
895         | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
896         | ASM.DATA b1 ->
897           (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
898             (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
899             ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
900             Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
901             Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
902             (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
903             Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
904             Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
905             (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
906             (List.Cons (b1, List.Nil))))
907         | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
908         | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
909         | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
910         | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
911         | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
912         | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
913         | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
914         | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
915         | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
916         | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
917         | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
918      | Types.Inr addrs1 ->
919        let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in
920        let b1 =
921          (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
922                   ASM.Direct, Vector.VEmpty)) addr1 with
923           | ASM.DIRECT b1 -> (fun _ -> b1)
924           | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
925           | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
926           | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
927           | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
928           | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
929           | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
930           | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
931           | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
932           | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
933           | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
934           | ASM.EXT_INDIRECT_DPTR ->
935             (fun _ -> assert false (* absurd case *))
936           | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
937           | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
938           | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
939           | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
940           | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
941           | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
942           | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
943        in
944        (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
945                 Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data,
946                 Vector.VEmpty)))) addr2 with
947         | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
948         | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
949         | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
950         | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
951         | ASM.ACC_A ->
952           (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
953             (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
954             ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
955             Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
956             Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
957             (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
958             Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
959             Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
960             (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
961             (List.Cons (b1, List.Nil))))
962         | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
963         | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
964         | ASM.DATA b2 ->
965           (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
966             (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
967             ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
968             Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
969             Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
970             (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
971             Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
972             Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
973             (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
974             (List.Cons (b1, (List.Cons (b2, List.Nil))))))
975         | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
976         | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
977         | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
978         | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
979         | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
980         | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
981         | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
982         | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
983         | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
984         | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
985         | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
986   | Types.Inr addrs0 ->
987     let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
988     (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
989              Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.N_bit_addr,
990              Vector.VEmpty)))) addr2 with
991      | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
992      | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
993      | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
994      | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
995      | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
996      | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
997      | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
998      | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
999      | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1000      | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1001      | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1002      | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1003      | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1004      | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1005      | ASM.BIT_ADDR b1 ->
1006        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1007          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
1008          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1009          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1010          Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1011          Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1012          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1013          (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
1014          Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1015          List.Nil))))
1016      | ASM.N_BIT_ADDR b1 ->
1017        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1018          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
1019          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1020          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1021          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1022          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1023          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1024          (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
1025          Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1026          List.Nil))))
1027      | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1028      | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1029      | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1030| ASM.ORL addrs ->
1031  (match addrs with
1032   | Types.Inl addrs0 ->
1033     (match addrs0 with
1034      | Types.Inl addrs1 ->
1035        let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in
1036        (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
1037                 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr,
1038                 (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Data,
1039                 (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons
1040                 (Nat.O, ASM.Indirect, Vector.VEmpty)))))))) addr2 with
1041         | ASM.DIRECT b1 ->
1042           (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1043             (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1044             ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1045             Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1046             Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1047             (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1048             (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1049             Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
1050             (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
1051             (List.Cons (b1, List.Nil))))
1052         | ASM.INDIRECT i1 ->
1053           (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1054             (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1055             ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1056             Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1057             Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1058             (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1059             (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1060             Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True,
1061             (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))),
1062             List.Nil))
1063         | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1064         | ASM.REGISTER r ->
1065           (fun _ -> List.Cons
1066             ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1067                (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
1068                (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S
1069                (Nat.S (Nat.S Nat.O))), Bool.True, (Vector.VCons ((Nat.S
1070                (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O),
1071                Bool.False, (Vector.VCons (Nat.O, Bool.True,
1072                Vector.VEmpty)))))))))) r), List.Nil))
1073         | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1074         | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1075         | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1076         | ASM.DATA b1 ->
1077           (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1078             (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1079             ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1080             Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1081             Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1082             (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1083             (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1084             Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
1085             (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
1086             (List.Cons (b1, List.Nil))))
1087         | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1088         | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1089         | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1090         | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1091         | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1092         | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1093         | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1094         | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1095         | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1096         | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1097         | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1098      | Types.Inr addrs1 ->
1099        let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in
1100        let b1 =
1101          (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1102                   ASM.Direct, Vector.VEmpty)) addr1 with
1103           | ASM.DIRECT b1 -> (fun _ -> b1)
1104           | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1105           | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1106           | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1107           | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1108           | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1109           | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1110           | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1111           | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1112           | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1113           | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1114           | ASM.EXT_INDIRECT_DPTR ->
1115             (fun _ -> assert false (* absurd case *))
1116           | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1117           | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1118           | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1119           | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1120           | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1121           | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1122           | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1123        in
1124        (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
1125                 Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data,
1126                 Vector.VEmpty)))) addr2 with
1127         | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1128         | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1129         | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1130         | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1131         | ASM.ACC_A ->
1132           (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1133             (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1134             ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1135             Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1136             Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1137             (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1138             (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1139             Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
1140             (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
1141             (List.Cons (b1, List.Nil))))
1142         | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1143         | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1144         | ASM.DATA b2 ->
1145           (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1146             (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1147             ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1148             Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1149             Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1150             (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1151             (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1152             Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
1153             (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
1154             (List.Cons (b1, (List.Cons (b2, List.Nil))))))
1155         | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1156         | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1157         | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1158         | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1159         | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1160         | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1161         | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1162         | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1163         | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1164         | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1165         | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1166   | Types.Inr addrs0 ->
1167     let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
1168     (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
1169              Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.N_bit_addr,
1170              Vector.VEmpty)))) addr2 with
1171      | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1172      | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1173      | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1174      | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1175      | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1176      | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1177      | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1178      | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1179      | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1180      | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1181      | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1182      | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1183      | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1184      | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1185      | ASM.BIT_ADDR b1 ->
1186        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1187          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1188          ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1189          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1190          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1191          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1192          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1193          (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
1194          Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1195          List.Nil))))
1196      | ASM.N_BIT_ADDR b1 ->
1197        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1198          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
1199          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1200          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1201          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1202          Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1203          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1204          (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
1205          Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1206          List.Nil))))
1207      | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1208      | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1209      | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1210| ASM.XRL addrs ->
1211  (match addrs with
1212   | Types.Inl addrs0 ->
1213     let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
1214     (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
1215              (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Data,
1216              (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr,
1217              (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O,
1218              ASM.Indirect, Vector.VEmpty)))))))) addr2 with
1219      | ASM.DIRECT b1 ->
1220        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1221          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1222          ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1223          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1224          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1225          Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1226          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1227          (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
1228          Bool.True, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1229          List.Nil))))
1230      | ASM.INDIRECT i1 ->
1231        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1232          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1233          ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1234          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1235          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1236          Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1237          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1238          (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
1239          Vector.VEmpty)))))))))))))))), List.Nil))
1240      | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1241      | ASM.REGISTER r ->
1242        (fun _ -> List.Cons
1243          ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1244             (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
1245             (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S
1246             (Nat.S (Nat.S Nat.O))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1247             Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
1248             (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))) r),
1249          List.Nil))
1250      | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1251      | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1252      | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1253      | ASM.DATA b1 ->
1254        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1255          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1256          ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1257          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1258          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1259          Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1260          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1261          (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
1262          Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1263          List.Nil))))
1264      | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1265      | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1266      | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1267      | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1268      | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1269      | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1270      | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1271      | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1272      | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1273      | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1274      | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1275   | Types.Inr addrs0 ->
1276     let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
1277     let b1 =
1278       (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1279                ASM.Direct, Vector.VEmpty)) addr1 with
1280        | ASM.DIRECT b1 -> (fun _ -> b1)
1281        | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1282        | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1283        | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1284        | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1285        | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1286        | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1287        | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1288        | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1289        | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1290        | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1291        | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1292        | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1293        | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1294        | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1295        | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1296        | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1297        | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1298        | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1299     in
1300     (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
1301              Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data,
1302              Vector.VEmpty)))) addr2 with
1303      | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1304      | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1305      | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1306      | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1307      | ASM.ACC_A ->
1308        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1309          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1310          ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1311          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1312          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1313          Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1314          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1315          (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
1316          Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1317          List.Nil))))
1318      | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1319      | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1320      | ASM.DATA b2 ->
1321        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1322          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1323          ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1324          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1325          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1326          Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1327          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1328          (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
1329          Bool.True, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1330          (List.Cons (b2, List.Nil))))))
1331      | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1332      | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1333      | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1334      | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1335      | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1336      | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1337      | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1338      | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1339      | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1340      | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1341      | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1342| ASM.CLR addr ->
1343  (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
1344           (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O),
1345           ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))))))
1346           addr with
1347   | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1348   | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1349   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1350   | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1351   | ASM.ACC_A ->
1352     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1353       (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1354       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
1355       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1356       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1357       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1358       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
1359       Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
1360       Vector.VEmpty)))))))))))))))), List.Nil))
1361   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1362   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1363   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1364   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1365   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1366   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1367   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1368   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1369   | ASM.CARRY ->
1370     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1371       (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1372       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
1373       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
1374       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1375       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1376       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
1377       ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1378       Vector.VEmpty)))))))))))))))), List.Nil))
1379   | ASM.BIT_ADDR b1 ->
1380     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1381       (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1382       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
1383       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
1384       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1385       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1386       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
1387       ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.False,
1388       Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
1389   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1390   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1391   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1392   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1393| ASM.CPL addr ->
1394  (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
1395           (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O),
1396           ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))))))
1397           addr with
1398   | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1399   | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1400   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1401   | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1402   | ASM.ACC_A ->
1403     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1404       (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1405       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
1406       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1407       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1408       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1409       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
1410       Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
1411       Vector.VEmpty)))))))))))))))), List.Nil))
1412   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1413   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1414   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1415   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1416   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1417   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1418   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1419   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1420   | ASM.CARRY ->
1421     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1422       (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1423       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
1424       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1425       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1426       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1427       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
1428       ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1429       Vector.VEmpty)))))))))))))))), List.Nil))
1430   | ASM.BIT_ADDR b1 ->
1431     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1432       (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1433       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
1434       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1435       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1436       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1437       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
1438       ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.False,
1439       Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
1440   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1441   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1442   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1443   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1444| ASM.RL addr ->
1445  List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1446    Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1447    (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1448    (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1449    (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1450    Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1451    (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1452    Vector.VEmpty)))))))))))))))), List.Nil)
1453| ASM.RLC addr ->
1454  List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1455    Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1456    (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1457    (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1458    (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1459    Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1460    (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1461    Vector.VEmpty)))))))))))))))), List.Nil)
1462| ASM.RR addr ->
1463  List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1464    Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1465    (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1466    (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1467    (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1468    Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1469    (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1470    Vector.VEmpty)))))))))))))))), List.Nil)
1471| ASM.RRC addr ->
1472  List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1473    Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1474    (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1475    (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1476    (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1477    Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1478    (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1479    Vector.VEmpty)))))))))))))))), List.Nil)
1480| ASM.SWAP addr ->
1481  List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1482    Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1483    (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1484    (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1485    (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1486    Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1487    (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
1488    Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
1489| ASM.MOV addrs ->
1490  (match addrs with
1491   | Types.Inl addrs0 ->
1492     (match addrs0 with
1493      | Types.Inl addrs1 ->
1494        (match addrs1 with
1495         | Types.Inl addrs2 ->
1496           (match addrs2 with
1497            | Types.Inl addrs3 ->
1498              (match addrs3 with
1499               | Types.Inl addrs4 ->
1500                 let { Types.fst = addr1; Types.snd = addr2 } = addrs4 in
1501                 (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S
1502                          Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1503                          Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S
1504                          Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O),
1505                          ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
1506                          Vector.VEmpty)))))))) addr2 with
1507                  | ASM.DIRECT b1 ->
1508                    (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1509                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True,
1510                      (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1511                      (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S
1512                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1513                      (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1514                      Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1515                      Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1516                      Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O),
1517                      Bool.False, (Vector.VCons (Nat.O, Bool.True,
1518                      Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1519                      List.Nil))))
1520                  | ASM.INDIRECT i1 ->
1521                    (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1522                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True,
1523                      (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1524                      (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S
1525                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1526                      (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1527                      Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1528                      Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1529                      Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O),
1530                      Bool.True, (Vector.VCons (Nat.O, i1,
1531                      Vector.VEmpty)))))))))))))))), List.Nil))
1532                  | ASM.EXT_INDIRECT x ->
1533                    (fun _ -> assert false (* absurd case *))
1534                  | ASM.REGISTER r ->
1535                    (fun _ -> List.Cons
1536                      ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1537                         Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
1538                         (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1539                         Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1540                         (Nat.S Nat.O))), Bool.True, (Vector.VCons ((Nat.S
1541                         (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
1542                         Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
1543                         Vector.VEmpty)))))))))) r), List.Nil))
1544                  | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1545                  | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1546                  | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1547                  | ASM.DATA b1 ->
1548                    (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1549                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False,
1550                      (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1551                      (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S
1552                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1553                      (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1554                      Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1555                      Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1556                      Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O),
1557                      Bool.False, (Vector.VCons (Nat.O, Bool.False,
1558                      Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1559                      List.Nil))))
1560                  | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1561                  | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1562                  | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1563                  | ASM.EXT_INDIRECT_DPTR ->
1564                    (fun _ -> assert false (* absurd case *))
1565                  | ASM.INDIRECT_DPTR ->
1566                    (fun _ -> assert false (* absurd case *))
1567                  | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1568                  | ASM.BIT_ADDR x ->
1569                    (fun _ -> assert false (* absurd case *))
1570                  | ASM.N_BIT_ADDR x ->
1571                    (fun _ -> assert false (* absurd case *))
1572                  | ASM.RELATIVE x ->
1573                    (fun _ -> assert false (* absurd case *))
1574                  | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1575                  | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *)))
1576                   __
1577               | Types.Inr addrs4 ->
1578                 let { Types.fst = addr1; Types.snd = addr2 } = addrs4 in
1579                 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons
1580                          ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O,
1581                          ASM.Indirect, Vector.VEmpty)))) addr1 with
1582                  | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1583                  | ASM.INDIRECT i1 ->
1584                    (fun _ ->
1585                      (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O))
1586                               (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1587                               ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O),
1588                               ASM.Direct, (Vector.VCons (Nat.O, ASM.Data,
1589                               Vector.VEmpty)))))) addr2 with
1590                       | ASM.DIRECT b1 ->
1591                         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S
1592                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
1593                           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1594                           (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1595                           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1596                           Nat.O))))), Bool.True, (Vector.VCons ((Nat.S
1597                           (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1598                           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1599                           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1600                           Bool.True, (Vector.VCons ((Nat.S Nat.O),
1601                           Bool.True, (Vector.VCons (Nat.O, i1,
1602                           Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1603                           List.Nil))))
1604                       | ASM.INDIRECT x0 ->
1605                         (fun _ -> assert false (* absurd case *))
1606                       | ASM.EXT_INDIRECT x0 ->
1607                         (fun _ -> assert false (* absurd case *))
1608                       | ASM.REGISTER x0 ->
1609                         (fun _ -> assert false (* absurd case *))
1610                       | ASM.ACC_A ->
1611                         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S
1612                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
1613                           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1614                           (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1615                           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1616                           Nat.O))))), Bool.True, (Vector.VCons ((Nat.S
1617                           (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1618                           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1619                           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1620                           Bool.True, (Vector.VCons ((Nat.S Nat.O),
1621                           Bool.True, (Vector.VCons (Nat.O, i1,
1622                           Vector.VEmpty)))))))))))))))), List.Nil))
1623                       | ASM.ACC_B ->
1624                         (fun _ -> assert false (* absurd case *))
1625                       | ASM.DPTR ->
1626                         (fun _ -> assert false (* absurd case *))
1627                       | ASM.DATA b1 ->
1628                         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S
1629                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
1630                           Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1631                           (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1632                           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1633                           Nat.O))))), Bool.True, (Vector.VCons ((Nat.S
1634                           (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1635                           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1636                           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1637                           Bool.True, (Vector.VCons ((Nat.S Nat.O),
1638                           Bool.True, (Vector.VCons (Nat.O, i1,
1639                           Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1640                           List.Nil))))
1641                       | ASM.DATA16 x0 ->
1642                         (fun _ -> assert false (* absurd case *))
1643                       | ASM.ACC_DPTR ->
1644                         (fun _ -> assert false (* absurd case *))
1645                       | ASM.ACC_PC ->
1646                         (fun _ -> assert false (* absurd case *))
1647                       | ASM.EXT_INDIRECT_DPTR ->
1648                         (fun _ -> assert false (* absurd case *))
1649                       | ASM.INDIRECT_DPTR ->
1650                         (fun _ -> assert false (* absurd case *))
1651                       | ASM.CARRY ->
1652                         (fun _ -> assert false (* absurd case *))
1653                       | ASM.BIT_ADDR x0 ->
1654                         (fun _ -> assert false (* absurd case *))
1655                       | ASM.N_BIT_ADDR x0 ->
1656                         (fun _ -> assert false (* absurd case *))
1657                       | ASM.RELATIVE x0 ->
1658                         (fun _ -> assert false (* absurd case *))
1659                       | ASM.ADDR11 x0 ->
1660                         (fun _ -> assert false (* absurd case *))
1661                       | ASM.ADDR16 x0 ->
1662                         (fun _ -> assert false (* absurd case *))) __)
1663                  | ASM.EXT_INDIRECT x ->
1664                    (fun _ -> assert false (* absurd case *))
1665                  | ASM.REGISTER r ->
1666                    (fun _ ->
1667                      (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O))
1668                               (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1669                               ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O),
1670                               ASM.Direct, (Vector.VCons (Nat.O, ASM.Data,
1671                               Vector.VEmpty)))))) addr2 with
1672                       | ASM.DIRECT b1 ->
1673                         (fun _ -> List.Cons
1674                           ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1675                              Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
1676                              (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1677                              Nat.O)))), Bool.True, (Vector.VCons ((Nat.S
1678                              (Nat.S (Nat.S Nat.O))), Bool.False,
1679                              (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1680                              Bool.True, (Vector.VCons ((Nat.S Nat.O),
1681                              Bool.False, (Vector.VCons (Nat.O, Bool.True,
1682                              Vector.VEmpty)))))))))) r), (List.Cons (b1,
1683                           List.Nil))))
1684                       | ASM.INDIRECT x0 ->
1685                         (fun _ -> assert false (* absurd case *))
1686                       | ASM.EXT_INDIRECT x0 ->
1687                         (fun _ -> assert false (* absurd case *))
1688                       | ASM.REGISTER x0 ->
1689                         (fun _ -> assert false (* absurd case *))
1690                       | ASM.ACC_A ->
1691                         (fun _ -> List.Cons
1692                           ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1693                              Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
1694                              (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1695                              Nat.O)))), Bool.True, (Vector.VCons ((Nat.S
1696                              (Nat.S (Nat.S Nat.O))), Bool.True,
1697                              (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1698                              Bool.True, (Vector.VCons ((Nat.S Nat.O),
1699                              Bool.True, (Vector.VCons (Nat.O, Bool.True,
1700                              Vector.VEmpty)))))))))) r), List.Nil))
1701                       | ASM.ACC_B ->
1702                         (fun _ -> assert false (* absurd case *))
1703                       | ASM.DPTR ->
1704                         (fun _ -> assert false (* absurd case *))
1705                       | ASM.DATA b1 ->
1706                         (fun _ -> List.Cons
1707                           ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1708                              Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
1709                              (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1710                              Nat.O)))), Bool.False, (Vector.VCons ((Nat.S
1711                              (Nat.S (Nat.S Nat.O))), Bool.True,
1712                              (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1713                              Bool.True, (Vector.VCons ((Nat.S Nat.O),
1714                              Bool.True, (Vector.VCons (Nat.O, Bool.True,
1715                              Vector.VEmpty)))))))))) r), (List.Cons (b1,
1716                           List.Nil))))
1717                       | ASM.DATA16 x0 ->
1718                         (fun _ -> assert false (* absurd case *))
1719                       | ASM.ACC_DPTR ->
1720                         (fun _ -> assert false (* absurd case *))
1721                       | ASM.ACC_PC ->
1722                         (fun _ -> assert false (* absurd case *))
1723                       | ASM.EXT_INDIRECT_DPTR ->
1724                         (fun _ -> assert false (* absurd case *))
1725                       | ASM.INDIRECT_DPTR ->
1726                         (fun _ -> assert false (* absurd case *))
1727                       | ASM.CARRY ->
1728                         (fun _ -> assert false (* absurd case *))
1729                       | ASM.BIT_ADDR x0 ->
1730                         (fun _ -> assert false (* absurd case *))
1731                       | ASM.N_BIT_ADDR x0 ->
1732                         (fun _ -> assert false (* absurd case *))
1733                       | ASM.RELATIVE x0 ->
1734                         (fun _ -> assert false (* absurd case *))
1735                       | ASM.ADDR11 x0 ->
1736                         (fun _ -> assert false (* absurd case *))
1737                       | ASM.ADDR16 x0 ->
1738                         (fun _ -> assert false (* absurd case *))) __)
1739                  | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1740                  | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1741                  | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1742                  | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1743                  | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1744                  | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1745                  | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1746                  | ASM.EXT_INDIRECT_DPTR ->
1747                    (fun _ -> assert false (* absurd case *))
1748                  | ASM.INDIRECT_DPTR ->
1749                    (fun _ -> assert false (* absurd case *))
1750                  | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1751                  | ASM.BIT_ADDR x ->
1752                    (fun _ -> assert false (* absurd case *))
1753                  | ASM.N_BIT_ADDR x ->
1754                    (fun _ -> assert false (* absurd case *))
1755                  | ASM.RELATIVE x ->
1756                    (fun _ -> assert false (* absurd case *))
1757                  | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1758                  | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *)))
1759                   __)
1760            | Types.Inr addrs3 ->
1761              let { Types.fst = addr1; Types.snd = addr2 } = addrs3 in
1762              let b1 =
1763                (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1764                         ASM.Direct, Vector.VEmpty)) addr1 with
1765                 | ASM.DIRECT b1 -> (fun _ -> b1)
1766                 | ASM.INDIRECT x ->
1767                   (fun _ -> assert false (* absurd case *))
1768                 | ASM.EXT_INDIRECT x ->
1769                   (fun _ -> assert false (* absurd case *))
1770                 | ASM.REGISTER x ->
1771                   (fun _ -> assert false (* absurd case *))
1772                 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1773                 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1774                 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1775                 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1776                 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1777                 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1778                 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1779                 | ASM.EXT_INDIRECT_DPTR ->
1780                   (fun _ -> assert false (* absurd case *))
1781                 | ASM.INDIRECT_DPTR ->
1782                   (fun _ -> assert false (* absurd case *))
1783                 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1784                 | ASM.BIT_ADDR x ->
1785                   (fun _ -> assert false (* absurd case *))
1786                 | ASM.N_BIT_ADDR x ->
1787                   (fun _ -> assert false (* absurd case *))
1788                 | ASM.RELATIVE x ->
1789                   (fun _ -> assert false (* absurd case *))
1790                 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1791                 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *)))
1792                  __
1793              in
1794              (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S
1795                       Nat.O)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1796                       Nat.O)))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1797                       (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S
1798                       (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
1799                       Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
1800                       Vector.VEmpty)))))))))) addr2 with
1801               | ASM.DIRECT b2 ->
1802                 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1803                   (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True,
1804                   (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1805                   Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1806                   (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons
1807                   ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1808                   (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1809                   (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1810                   (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
1811                   (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
1812                   (List.Cons (b1, (List.Cons (b2, List.Nil))))))
1813               | ASM.INDIRECT i1 ->
1814                 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1815                   (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True,
1816                   (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1817                   Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1818                   (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons
1819                   ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1820                   (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1821                   (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1822                   (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
1823                   (Nat.O, i1, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1824                   List.Nil))))
1825               | ASM.EXT_INDIRECT x ->
1826                 (fun _ -> assert false (* absurd case *))
1827               | ASM.REGISTER r ->
1828                 (fun _ -> List.Cons
1829                   ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1830                      Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
1831                      ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1832                      (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1833                      Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1834                      Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False,
1835                      (Vector.VCons (Nat.O, Bool.True,
1836                      Vector.VEmpty)))))))))) r), (List.Cons (b1,
1837                   List.Nil))))
1838               | ASM.ACC_A ->
1839                 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1840                   (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True,
1841                   (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1842                   Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1843                   (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons
1844                   ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1845                   (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1846                   (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1847                   (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
1848                   (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
1849                   (List.Cons (b1, List.Nil))))
1850               | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1851               | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1852               | ASM.DATA b2 ->
1853                 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1854                   (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False,
1855                   (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1856                   Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1857                   (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons
1858                   ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1859                   (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1860                   (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1861                   (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
1862                   (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
1863                   (List.Cons (b1, (List.Cons (b2, List.Nil))))))
1864               | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1865               | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1866               | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1867               | ASM.EXT_INDIRECT_DPTR ->
1868                 (fun _ -> assert false (* absurd case *))
1869               | ASM.INDIRECT_DPTR ->
1870                 (fun _ -> assert false (* absurd case *))
1871               | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1872               | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1873               | ASM.N_BIT_ADDR x ->
1874                 (fun _ -> assert false (* absurd case *))
1875               | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1876               | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1877               | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *)))
1878                __)
1879         | Types.Inr addrs2 ->
1880           let { Types.fst = addr1; Types.snd = addr2 } = addrs2 in
1881           (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1882                    ASM.Data16, Vector.VEmpty)) addr2 with
1883            | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1884            | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1885            | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1886            | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1887            | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1888            | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1889            | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1890            | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1891            | ASM.DATA16 w ->
1892              (fun _ ->
1893                let b1_b2 =
1894                  Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1895                    (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
1896                    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) w
1897                in
1898                let b1 = b1_b2.Types.fst in
1899                let b2 = b1_b2.Types.snd in
1900                List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1901                (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
1902                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1903                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1904                Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1905                Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1906                Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1907                Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False,
1908                (Vector.VCons (Nat.O, Bool.False,
1909                Vector.VEmpty)))))))))))))))), (List.Cons (b1, (List.Cons
1910                (b2, List.Nil))))))
1911            | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1912            | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1913            | ASM.EXT_INDIRECT_DPTR ->
1914              (fun _ -> assert false (* absurd case *))
1915            | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1916            | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1917            | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1918            | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1919            | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1920            | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1921            | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1922      | Types.Inr addrs1 ->
1923        let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in
1924        (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1925                 ASM.Bit_addr, Vector.VEmpty)) addr2 with
1926         | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1927         | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1928         | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1929         | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1930         | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1931         | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1932         | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1933         | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1934         | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1935         | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1936         | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1937         | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1938         | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1939         | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1940         | ASM.BIT_ADDR b1 ->
1941           (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1942             (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons
1943             ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1944             Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1945             Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1946             (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1947             (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1948             Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
1949             (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
1950             (List.Cons (b1, List.Nil))))
1951         | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1952         | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1953         | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1954         | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1955   | Types.Inr addrs0 ->
1956     let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
1957     (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1958              ASM.Bit_addr, Vector.VEmpty)) addr1 with
1959      | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1960      | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1961      | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1962      | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1963      | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1964      | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1965      | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1966      | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1967      | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1968      | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1969      | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1970      | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1971      | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1972      | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1973      | ASM.BIT_ADDR b1 ->
1974        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1975          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
1976          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1977          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1978          Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1979          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1980          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1981          (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
1982          Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1983          List.Nil))))
1984      | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1985      | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1986      | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1987      | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1988| ASM.MOVX addrs ->
1989  (match addrs with
1990   | Types.Inl addrs0 ->
1991     let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
1992     (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
1993              Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1994              ASM.Ext_indirect_dptr, Vector.VEmpty)))) addr2 with
1995      | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1996      | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1997      | ASM.EXT_INDIRECT i1 ->
1998        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1999          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
2000          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
2001          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2002          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
2003          Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2004          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2005          (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
2006          Vector.VEmpty)))))))))))))))), List.Nil))
2007      | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2008      | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2009      | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2010      | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2011      | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2012      | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2013      | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2014      | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2015      | ASM.EXT_INDIRECT_DPTR ->
2016        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2017          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
2018          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
2019          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2020          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
2021          Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2022          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2023          (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
2024          Bool.False, Vector.VEmpty)))))))))))))))), List.Nil))
2025      | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2026      | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2027      | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2028      | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2029      | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2030      | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2031      | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2032   | Types.Inr addrs0 ->
2033     let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
2034     (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
2035              Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
2036              ASM.Ext_indirect_dptr, Vector.VEmpty)))) addr1 with
2037      | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2038      | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2039      | ASM.EXT_INDIRECT i1 ->
2040        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2041          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
2042          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
2043          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2044          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
2045          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2046          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2047          (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
2048          Vector.VEmpty)))))))))))))))), List.Nil))
2049      | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2050      | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2051      | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2052      | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2053      | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2054      | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2055      | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2056      | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2057      | ASM.EXT_INDIRECT_DPTR ->
2058        (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2059          (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
2060          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
2061          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2062          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
2063          Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2064          Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2065          (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
2066          Bool.False, Vector.VEmpty)))))))))))))))), List.Nil))
2067      | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2068      | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2069      | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2070      | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2071      | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2072      | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2073      | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
2074| ASM.SETB addr ->
2075  (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
2076           ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))))
2077           addr with
2078   | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2079   | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2080   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2081   | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2082   | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2083   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2084   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2085   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2086   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2087   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2088   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2089   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2090   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2091   | ASM.CARRY ->
2092     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2093       (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2094       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
2095       ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2096       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
2097       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2098       (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
2099       ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
2100       Vector