source: extracted/fetch.ml @ 2649

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

...

File size: 83.6 KB
Line 
1open Preamble
2
3open Extranat
4
5open Vector
6
7open Div_and_mod
8
9open Jmeq
10
11open Russell
12
13open List
14
15open Util
16
17open FoldStuff
18
19open Bool
20
21open Relations
22
23open Nat
24
25open BitVector
26
27open Hints_declaration
28
29open Core_notation
30
31open Pts
32
33open Logic
34
35open Types
36
37open BitVectorTrie
38
39open Arithmetic
40
41open String
42
43open LabelledObjects
44
45open Integers
46
47open AST
48
49open CostLabel
50
51open Proper
52
53open PositiveMap
54
55open Deqsets
56
57open ErrorMessages
58
59open PreIdentifiers
60
61open Errors
62
63open Extralib
64
65open Setoids
66
67open Monad
68
69open Option
70
71open Lists
72
73open Positive
74
75open Identifiers
76
77open ASM
78
79(** val inefficient_address_of_word_labels_code_mem :
80    ASM.labelled_instruction List.list -> ASM.identifier0 ->
81    BitVector.bitVector **)
82let inefficient_address_of_word_labels_code_mem code_mem id =
83  Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
84    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
85    Nat.O))))))))))))))))
86    (LabelledObjects.index_of0
87      (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag
88        id) code_mem)
89
90type label_map = Nat.nat Identifiers.identifier_map
91
92(** val create_label_cost_map0 :
93    ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
94    BitVectorTrie.bitVectorTrie) Types.prod Types.sig0 **)
95let create_label_cost_map0 program0 =
96  (Types.pi1
97    (FoldStuff.foldl_strong program0 (fun prefix0 x tl _ labels_costs_ppc ->
98      (let { Types.fst = eta24561; Types.snd = ppc } =
99         Types.pi1 labels_costs_ppc
100       in
101      (fun _ ->
102      (let { Types.fst = labels; Types.snd = costs } = eta24561 in
103      (fun _ ->
104      (let { Types.fst = label; Types.snd = instr } = x in
105      (fun _ ->
106      let labels1 =
107        match label with
108        | Types.None -> labels
109        | Types.Some l -> Identifiers.add PreIdentifiers.ASMTag labels l ppc
110      in
111      let costs1 =
112        match instr with
113        | ASM.Instruction x0 -> costs
114        | ASM.Comment x0 -> costs
115        | ASM.Cost cost ->
116          BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
117            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
118            (Nat.S Nat.O))))))))))))))))
119            (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
120              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
121              (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) cost costs
122        | ASM.Jmp x0 -> costs
123        | ASM.Call x0 -> costs
124        | ASM.Mov (x0, x1) -> costs
125      in
126      { Types.fst = { Types.fst = labels1; Types.snd = costs1 }; Types.snd =
127      (Nat.S ppc) })) __)) __)) __) { Types.fst = { Types.fst =
128      (Identifiers.empty_map PreIdentifiers.ASMTag); Types.snd =
129      (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
130      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
131      Nat.O))))))))))))))))) }; Types.snd = Nat.O })).Types.fst
132
133(** val create_label_cost_map :
134    ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
135    BitVectorTrie.bitVectorTrie) Types.prod **)
136let create_label_cost_map program0 =
137  Types.pi1 (create_label_cost_map0 program0)
138
139(** val address_of_word_labels :
140    ASM.labelled_instruction List.list -> ASM.identifier0 -> BitVector.word **)
141let address_of_word_labels code_mem id =
142  let labels = (create_label_cost_map code_mem).Types.fst in
143  Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
144    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
145    Nat.O))))))))))))))))
146    (Identifiers.lookup_def PreIdentifiers.ASMTag labels id Nat.O)
147
148(** val bitvector_max_nat : Nat.nat -> Nat.nat **)
149let bitvector_max_nat length0 =
150  Util.exponential (Nat.S (Nat.S Nat.O)) length0
151
152(** val code_memory_size : Nat.nat **)
153let code_memory_size =
154  bitvector_max_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
155    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
156    Nat.O))))))))))))))))
157
158(** val next :
159    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
160    (BitVector.word, BitVector.byte) Types.prod **)
161let next pmem pc =
162  { Types.fst =
163    (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
164      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
165      Nat.O)))))))))))))))) pc
166      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
167        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
168        Nat.O)))))))))))))))) (Nat.S Nat.O))); Types.snd =
169    (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
170      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
171      Nat.O)))))))))))))))) pc pmem
172      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
173        Nat.O)))))))))) }
174
175(** val load_code_memory0 :
176    BitVector.byte List.list -> BitVector.byte BitVectorTrie.bitVectorTrie
177    Types.sig0 **)
178let load_code_memory0 program0 =
179  (Types.pi1
180    (FoldStuff.foldl_strong program0 (fun prefix0 v tl _ i_mem ->
181      (let { Types.fst = i; Types.snd = mem1 } = Types.pi1 i_mem in
182      (fun _ -> { Types.fst = (Nat.S i); Types.snd =
183      (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
184        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
185        Nat.O))))))))))))))))
186        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
187          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
188          (Nat.S (Nat.S Nat.O)))))))))))))))) i) v mem1) })) __)
189      { Types.fst = Nat.O; Types.snd = (BitVectorTrie.Stub (Nat.S (Nat.S
190      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
191      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))) })).Types.snd
192
193(** val load_code_memory :
194    BitVector.byte List.list -> BitVector.byte BitVectorTrie.bitVectorTrie **)
195let load_code_memory program0 =
196  Types.pi1 (load_code_memory0 program0)
197
198(** val prod_inv_rect_Type5 :
199    ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
200let prod_inv_rect_Type5 clearme =
201  let { Types.fst = fst0; Types.snd = snd0 } = clearme in
202  (fun auto -> auto fst0 snd0 __)
203
204(** val fetch0 :
205    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
206    BitVector.byte -> ((ASM.instruction, BitVector.word) Types.prod, Nat.nat)
207    Types.prod **)
208let fetch0 pmem pc v =
209  let { Types.fst = b; Types.snd = v0 } =
210    Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
211      v
212  in
213  (match b with
214   | Bool.True ->
215     let { Types.fst = b0; Types.snd = v1 } =
216       Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) v0
217     in
218     (match b0 with
219      | Bool.True ->
220        let { Types.fst = b1; Types.snd = v2 } =
221          Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1
222        in
223        (match b1 with
224         | Bool.True ->
225           let { Types.fst = b2; Types.snd = v3 } =
226             Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
227           in
228           (match b2 with
229            | Bool.True ->
230              let { Types.fst = b3; Types.snd = v4 } =
231                Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
232              in
233              (match b3 with
234               | Bool.True ->
235                 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
236                   (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
237                   { Types.fst = (ASM.REGISTER v4); Types.snd =
238                   ASM.ACC_A }))))))); Types.snd = pc }; Types.snd = (Nat.S
239                   Nat.O) }
240               | Bool.False ->
241                 let { Types.fst = b4; Types.snd = v5 } =
242                   Vector.head (Nat.S (Nat.S Nat.O)) v4
243                 in
244                 (match b4 with
245                  | Bool.True ->
246                    let { Types.fst = b5; Types.snd = v6 } =
247                      Vector.head (Nat.S Nat.O) v5
248                    in
249                    (match b5 with
250                     | Bool.True ->
251                       { Types.fst = { Types.fst = (ASM.RealInstruction
252                         (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl
253                         (Types.Inr { Types.fst = (ASM.INDIRECT
254                         (Vector.from_singl v6)); Types.snd =
255                         ASM.ACC_A }))))))); Types.snd = pc }; Types.snd =
256                         (Nat.S Nat.O) }
257                     | Bool.False ->
258                       let { Types.fst = b6; Types.snd = v7 } =
259                         Vector.head Nat.O v6
260                       in
261                       (match b6 with
262                        | Bool.True ->
263                          prod_inv_rect_Type5 (next pmem pc)
264                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
265                            (ASM.RealInstruction (ASM.MOV (Types.Inl
266                            (Types.Inl (Types.Inl (Types.Inr { Types.fst =
267                            (ASM.DIRECT b10); Types.snd = ASM.ACC_A }))))));
268                            Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) })
269                        | Bool.False ->
270                          { Types.fst = { Types.fst = (ASM.RealInstruction
271                            (ASM.CPL ASM.ACC_A)); Types.snd = pc };
272                            Types.snd = (Nat.S Nat.O) }))
273                  | Bool.False ->
274                    let { Types.fst = b5; Types.snd = v6 } =
275                      Vector.head (Nat.S Nat.O) v5
276                    in
277                    (match b5 with
278                     | Bool.True ->
279                       { Types.fst = { Types.fst = (ASM.RealInstruction
280                         (ASM.MOVX (Types.Inr { Types.fst = (ASM.EXT_INDIRECT
281                         (Vector.from_singl v6)); Types.snd = ASM.ACC_A })));
282                         Types.snd = pc }; Types.snd = (Nat.S (Nat.S
283                         Nat.O)) }
284                     | Bool.False ->
285                       let { Types.fst = b6; Types.snd = v7 } =
286                         Vector.head Nat.O v6
287                       in
288                       (match b6 with
289                        | Bool.True ->
290                          prod_inv_rect_Type5 (next pmem pc)
291                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
292                            (ASM.ACALL (ASM.ADDR11
293                            (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
294                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
295                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
296                              ((Nat.S (Nat.S Nat.O)), Bool.True,
297                              (Vector.VCons ((Nat.S Nat.O), Bool.True,
298                              (Vector.VCons (Nat.O, Bool.True,
299                              Vector.VEmpty)))))) b10))); Types.snd = pc0 };
300                            Types.snd = (Nat.S (Nat.S Nat.O)) })
301                        | Bool.False ->
302                          { Types.fst = { Types.fst = (ASM.RealInstruction
303                            (ASM.MOVX (Types.Inr { Types.fst =
304                            ASM.EXT_INDIRECT_DPTR; Types.snd =
305                            ASM.ACC_A }))); Types.snd = pc }; Types.snd =
306                            (Nat.S (Nat.S Nat.O)) }))))
307            | Bool.False ->
308              let { Types.fst = b3; Types.snd = v4 } =
309                Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
310              in
311              (match b3 with
312               | Bool.True ->
313                 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
314                   (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl
315                   { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER
316                   v4) }))))))); Types.snd = pc }; Types.snd = (Nat.S
317                   Nat.O) }
318               | Bool.False ->
319                 let { Types.fst = b4; Types.snd = v5 } =
320                   Vector.head (Nat.S (Nat.S Nat.O)) v4
321                 in
322                 (match b4 with
323                  | Bool.True ->
324                    let { Types.fst = b5; Types.snd = v6 } =
325                      Vector.head (Nat.S Nat.O) v5
326                    in
327                    (match b5 with
328                     | Bool.True ->
329                       { Types.fst = { Types.fst = (ASM.RealInstruction
330                         (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl
331                         (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
332                         (ASM.INDIRECT (Vector.from_singl v6)) })))))));
333                         Types.snd = pc }; Types.snd = (Nat.S Nat.O) }
334                     | Bool.False ->
335                       let { Types.fst = b6; Types.snd = v7 } =
336                         Vector.head Nat.O v6
337                       in
338                       (match b6 with
339                        | Bool.True ->
340                          prod_inv_rect_Type5 (next pmem pc)
341                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
342                            (ASM.RealInstruction (ASM.MOV (Types.Inl
343                            (Types.Inl (Types.Inl (Types.Inl (Types.Inl
344                            { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT
345                            b10) }))))))); Types.snd = pc0 }; Types.snd =
346                            (Nat.S Nat.O) })
347                        | Bool.False ->
348                          { Types.fst = { Types.fst = (ASM.RealInstruction
349                            (ASM.CLR ASM.ACC_A)); Types.snd = pc };
350                            Types.snd = (Nat.S Nat.O) }))
351                  | Bool.False ->
352                    let { Types.fst = b5; Types.snd = v6 } =
353                      Vector.head (Nat.S Nat.O) v5
354                    in
355                    (match b5 with
356                     | Bool.True ->
357                       { Types.fst = { Types.fst = (ASM.RealInstruction
358                         (ASM.MOVX (Types.Inl { Types.fst = ASM.ACC_A;
359                         Types.snd = (ASM.EXT_INDIRECT
360                         (Vector.from_singl v6)) }))); Types.snd = pc };
361                         Types.snd = (Nat.S (Nat.S Nat.O)) }
362                     | Bool.False ->
363                       let { Types.fst = b6; Types.snd = v7 } =
364                         Vector.head Nat.O v6
365                       in
366                       (match b6 with
367                        | Bool.True ->
368                          prod_inv_rect_Type5 (next pmem pc)
369                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
370                            (ASM.AJMP (ASM.ADDR11
371                            (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
372                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
373                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
374                              ((Nat.S (Nat.S Nat.O)), Bool.True,
375                              (Vector.VCons ((Nat.S Nat.O), Bool.True,
376                              (Vector.VCons (Nat.O, Bool.True,
377                              Vector.VEmpty)))))) b10))); Types.snd = pc0 };
378                            Types.snd = (Nat.S (Nat.S Nat.O)) })
379                        | Bool.False ->
380                          { Types.fst = { Types.fst = (ASM.RealInstruction
381                            (ASM.MOVX (Types.Inl { Types.fst = ASM.ACC_A;
382                            Types.snd = ASM.EXT_INDIRECT_DPTR })));
383                            Types.snd = pc }; Types.snd = (Nat.S (Nat.S
384                            Nat.O)) })))))
385         | Bool.False ->
386           let { Types.fst = b2; Types.snd = v3 } =
387             Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
388           in
389           (match b2 with
390            | Bool.True ->
391              let { Types.fst = b3; Types.snd = v4 } =
392                Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
393              in
394              (match b3 with
395               | Bool.True ->
396                 prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
397                   { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DJNZ
398                   ((ASM.REGISTER v4), (ASM.RELATIVE b10)))); Types.snd =
399                   pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) })
400               | Bool.False ->
401                 let { Types.fst = b4; Types.snd = v5 } =
402                   Vector.head (Nat.S (Nat.S Nat.O)) v4
403                 in
404                 (match b4 with
405                  | Bool.True ->
406                    let { Types.fst = b5; Types.snd = v6 } =
407                      Vector.head (Nat.S Nat.O) v5
408                    in
409                    (match b5 with
410                     | Bool.True ->
411                       { Types.fst = { Types.fst = (ASM.RealInstruction
412                         (ASM.XCHD (ASM.ACC_A, (ASM.INDIRECT
413                         (Vector.from_singl v6))))); Types.snd = pc };
414                         Types.snd = (Nat.S Nat.O) }
415                     | Bool.False ->
416                       let { Types.fst = b6; Types.snd = v7 } =
417                         Vector.head Nat.O v6
418                       in
419                       (match b6 with
420                        | Bool.True ->
421                          prod_inv_rect_Type5 (next pmem pc)
422                            (fun pc0 b10 _ ->
423                            prod_inv_rect_Type5 (next pmem pc0)
424                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
425                              (ASM.RealInstruction (ASM.DJNZ ((ASM.DIRECT
426                              b10), (ASM.RELATIVE b20)))); Types.snd = pc1 };
427                              Types.snd = (Nat.S (Nat.S Nat.O)) }))
428                        | Bool.False ->
429                          { Types.fst = { Types.fst = (ASM.RealInstruction
430                            (ASM.DA ASM.ACC_A)); Types.snd = pc };
431                            Types.snd = (Nat.S Nat.O) }))
432                  | Bool.False ->
433                    let { Types.fst = b5; Types.snd = v6 } =
434                      Vector.head (Nat.S Nat.O) v5
435                    in
436                    (match b5 with
437                     | Bool.True ->
438                       let { Types.fst = b6; Types.snd = v7 } =
439                         Vector.head Nat.O v6
440                       in
441                       (match b6 with
442                        | Bool.True ->
443                          { Types.fst = { Types.fst = (ASM.RealInstruction
444                            (ASM.SETB ASM.CARRY)); Types.snd = pc };
445                            Types.snd = (Nat.S Nat.O) }
446                        | Bool.False ->
447                          prod_inv_rect_Type5 (next pmem pc)
448                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
449                            (ASM.RealInstruction (ASM.SETB (ASM.BIT_ADDR
450                            b10))); Types.snd = pc0 }; Types.snd = (Nat.S
451                            Nat.O) }))
452                     | Bool.False ->
453                       let { Types.fst = b6; Types.snd = v7 } =
454                         Vector.head Nat.O v6
455                       in
456                       (match b6 with
457                        | Bool.True ->
458                          prod_inv_rect_Type5 (next pmem pc)
459                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
460                            (ASM.ACALL (ASM.ADDR11
461                            (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
462                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
463                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
464                              ((Nat.S (Nat.S Nat.O)), Bool.True,
465                              (Vector.VCons ((Nat.S Nat.O), Bool.True,
466                              (Vector.VCons (Nat.O, Bool.False,
467                              Vector.VEmpty)))))) b10))); Types.snd = pc0 };
468                            Types.snd = (Nat.S (Nat.S Nat.O)) })
469                        | Bool.False ->
470                          prod_inv_rect_Type5 (next pmem pc)
471                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
472                            (ASM.RealInstruction (ASM.POP (ASM.DIRECT b10)));
473                            Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S
474                            Nat.O)) })))))
475            | Bool.False ->
476              let { Types.fst = b3; Types.snd = v4 } =
477                Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
478              in
479              (match b3 with
480               | Bool.True ->
481                 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.XCH
482                   (ASM.ACC_A, (ASM.REGISTER v4)))); Types.snd = pc };
483                   Types.snd = (Nat.S Nat.O) }
484               | Bool.False ->
485                 let { Types.fst = b4; Types.snd = v5 } =
486                   Vector.head (Nat.S (Nat.S Nat.O)) v4
487                 in
488                 (match b4 with
489                  | Bool.True ->
490                    let { Types.fst = b5; Types.snd = v6 } =
491                      Vector.head (Nat.S Nat.O) v5
492                    in
493                    (match b5 with
494                     | Bool.True ->
495                       { Types.fst = { Types.fst = (ASM.RealInstruction
496                         (ASM.XCH (ASM.ACC_A, (ASM.INDIRECT
497                         (Vector.from_singl v6))))); Types.snd = pc };
498                         Types.snd = (Nat.S Nat.O) }
499                     | Bool.False ->
500                       let { Types.fst = b6; Types.snd = v7 } =
501                         Vector.head Nat.O v6
502                       in
503                       (match b6 with
504                        | Bool.True ->
505                          prod_inv_rect_Type5 (next pmem pc)
506                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
507                            (ASM.RealInstruction (ASM.XCH (ASM.ACC_A,
508                            (ASM.DIRECT b10)))); Types.snd = pc0 };
509                            Types.snd = (Nat.S Nat.O) })
510                        | Bool.False ->
511                          { Types.fst = { Types.fst = (ASM.RealInstruction
512                            (ASM.SWAP ASM.ACC_A)); Types.snd = pc };
513                            Types.snd = (Nat.S Nat.O) }))
514                  | Bool.False ->
515                    let { Types.fst = b5; Types.snd = v6 } =
516                      Vector.head (Nat.S Nat.O) v5
517                    in
518                    (match b5 with
519                     | Bool.True ->
520                       let { Types.fst = b6; Types.snd = v7 } =
521                         Vector.head Nat.O v6
522                       in
523                       (match b6 with
524                        | Bool.True ->
525                          { Types.fst = { Types.fst = (ASM.RealInstruction
526                            (ASM.CLR ASM.CARRY)); Types.snd = pc };
527                            Types.snd = (Nat.S Nat.O) }
528                        | Bool.False ->
529                          prod_inv_rect_Type5 (next pmem pc)
530                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
531                            (ASM.RealInstruction (ASM.CLR (ASM.BIT_ADDR
532                            b10))); Types.snd = pc0 }; Types.snd = (Nat.S
533                            Nat.O) }))
534                     | Bool.False ->
535                       let { Types.fst = b6; Types.snd = v7 } =
536                         Vector.head Nat.O v6
537                       in
538                       (match b6 with
539                        | Bool.True ->
540                          prod_inv_rect_Type5 (next pmem pc)
541                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
542                            (ASM.AJMP (ASM.ADDR11
543                            (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
544                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
545                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
546                              ((Nat.S (Nat.S Nat.O)), Bool.True,
547                              (Vector.VCons ((Nat.S Nat.O), Bool.True,
548                              (Vector.VCons (Nat.O, Bool.False,
549                              Vector.VEmpty)))))) b10))); Types.snd = pc0 };
550                            Types.snd = (Nat.S (Nat.S Nat.O)) })
551                        | Bool.False ->
552                          prod_inv_rect_Type5 (next pmem pc)
553                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
554                            (ASM.RealInstruction (ASM.PUSH (ASM.DIRECT
555                            b10))); Types.snd = pc0 }; Types.snd = (Nat.S
556                            (Nat.S Nat.O)) })))))))
557      | Bool.False ->
558        let { Types.fst = b1; Types.snd = v2 } =
559          Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1
560        in
561        (match b1 with
562         | Bool.True ->
563           let { Types.fst = b2; Types.snd = v3 } =
564             Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
565           in
566           (match b2 with
567            | Bool.True ->
568              let { Types.fst = b3; Types.snd = v4 } =
569                Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
570              in
571              (match b3 with
572               | Bool.True ->
573                 prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
574                   prod_inv_rect_Type5 (next pmem pc0) (fun pc1 b20 _ ->
575                     { Types.fst = { Types.fst = (ASM.RealInstruction
576                     (ASM.CJNE ((Types.Inr { Types.fst = (ASM.REGISTER v4);
577                     Types.snd = (ASM.DATA b10) }), (ASM.RELATIVE b20))));
578                     Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))
579               | Bool.False ->
580                 let { Types.fst = b4; Types.snd = v5 } =
581                   Vector.head (Nat.S (Nat.S Nat.O)) v4
582                 in
583                 (match b4 with
584                  | Bool.True ->
585                    let { Types.fst = b5; Types.snd = v6 } =
586                      Vector.head (Nat.S Nat.O) v5
587                    in
588                    (match b5 with
589                     | Bool.True ->
590                       prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
591                         prod_inv_rect_Type5 (next pmem pc0)
592                           (fun pc1 b20 _ -> { Types.fst = { Types.fst =
593                           (ASM.RealInstruction (ASM.CJNE ((Types.Inr
594                           { Types.fst = (ASM.INDIRECT
595                           (Vector.from_singl v6)); Types.snd = (ASM.DATA
596                           b10) }), (ASM.RELATIVE b20)))); Types.snd = pc1 };
597                           Types.snd = (Nat.S (Nat.S Nat.O)) }))
598                     | Bool.False ->
599                       let { Types.fst = b6; Types.snd = v7 } =
600                         Vector.head Nat.O v6
601                       in
602                       (match b6 with
603                        | Bool.True ->
604                          prod_inv_rect_Type5 (next pmem pc)
605                            (fun pc0 b10 _ ->
606                            prod_inv_rect_Type5 (next pmem pc0)
607                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
608                              (ASM.RealInstruction (ASM.CJNE ((Types.Inl
609                              { Types.fst = ASM.ACC_A; Types.snd =
610                              (ASM.DIRECT b10) }), (ASM.RELATIVE b20))));
611                              Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S
612                              Nat.O)) }))
613                        | Bool.False ->
614                          prod_inv_rect_Type5 (next pmem pc)
615                            (fun pc0 b10 _ ->
616                            prod_inv_rect_Type5 (next pmem pc0)
617                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
618                              (ASM.RealInstruction (ASM.CJNE ((Types.Inl
619                              { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA
620                              b10) }), (ASM.RELATIVE b20)))); Types.snd =
621                              pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))))
622                  | Bool.False ->
623                    let { Types.fst = b5; Types.snd = v6 } =
624                      Vector.head (Nat.S Nat.O) v5
625                    in
626                    (match b5 with
627                     | Bool.True ->
628                       let { Types.fst = b6; Types.snd = v7 } =
629                         Vector.head Nat.O v6
630                       in
631                       (match b6 with
632                        | Bool.True ->
633                          { Types.fst = { Types.fst = (ASM.RealInstruction
634                            (ASM.CPL ASM.CARRY)); Types.snd = pc };
635                            Types.snd = (Nat.S Nat.O) }
636                        | Bool.False ->
637                          prod_inv_rect_Type5 (next pmem pc)
638                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
639                            (ASM.RealInstruction (ASM.CPL (ASM.BIT_ADDR
640                            b10))); Types.snd = pc0 }; Types.snd = (Nat.S
641                            Nat.O) }))
642                     | Bool.False ->
643                       let { Types.fst = b6; Types.snd = v7 } =
644                         Vector.head Nat.O v6
645                       in
646                       (match b6 with
647                        | Bool.True ->
648                          prod_inv_rect_Type5 (next pmem pc)
649                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
650                            (ASM.ACALL (ASM.ADDR11
651                            (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
652                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
653                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
654                              ((Nat.S (Nat.S Nat.O)), Bool.True,
655                              (Vector.VCons ((Nat.S Nat.O), Bool.False,
656                              (Vector.VCons (Nat.O, Bool.True,
657                              Vector.VEmpty)))))) b10))); Types.snd = pc0 };
658                            Types.snd = (Nat.S (Nat.S Nat.O)) })
659                        | Bool.False ->
660                          prod_inv_rect_Type5 (next pmem pc)
661                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
662                            (ASM.RealInstruction (ASM.ANL (Types.Inr
663                            { Types.fst = ASM.CARRY; Types.snd =
664                            (ASM.N_BIT_ADDR b10) }))); Types.snd = pc0 };
665                            Types.snd = (Nat.S (Nat.S Nat.O)) })))))
666            | Bool.False ->
667              let { Types.fst = b3; Types.snd = v4 } =
668                Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
669              in
670              (match b3 with
671               | Bool.True ->
672                 prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
673                   { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
674                   (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
675                   { Types.fst = (ASM.REGISTER v4); Types.snd = (ASM.DIRECT
676                   b10) }))))))); Types.snd = pc0 }; Types.snd = (Nat.S
677                   (Nat.S Nat.O)) })
678               | Bool.False ->
679                 let { Types.fst = b4; Types.snd = v5 } =
680                   Vector.head (Nat.S (Nat.S Nat.O)) v4
681                 in
682                 (match b4 with
683                  | Bool.True ->
684                    let { Types.fst = b5; Types.snd = v6 } =
685                      Vector.head (Nat.S Nat.O) v5
686                    in
687                    (match b5 with
688                     | Bool.True ->
689                       prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
690                         { Types.fst = { Types.fst = (ASM.RealInstruction
691                         (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl
692                         (Types.Inr { Types.fst = (ASM.INDIRECT
693                         (Vector.from_singl v6)); Types.snd = (ASM.DIRECT
694                         b10) }))))))); Types.snd = pc0 }; Types.snd = (Nat.S
695                         (Nat.S Nat.O)) })
696                     | Bool.False ->
697                       { Types.fst = { Types.fst = (ASM.RealInstruction
698                         (ASM.MUL (ASM.ACC_A, ASM.ACC_B))); Types.snd = pc };
699                         Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
700                  | Bool.False ->
701                    let { Types.fst = b5; Types.snd = v6 } =
702                      Vector.head (Nat.S Nat.O) v5
703                    in
704                    (match b5 with
705                     | Bool.True ->
706                       let { Types.fst = b6; Types.snd = v7 } =
707                         Vector.head Nat.O v6
708                       in
709                       (match b6 with
710                        | Bool.True ->
711                          { Types.fst = { Types.fst = (ASM.RealInstruction
712                            (ASM.INC ASM.DPTR)); Types.snd = pc };
713                            Types.snd = (Nat.S (Nat.S Nat.O)) }
714                        | Bool.False ->
715                          prod_inv_rect_Type5 (next pmem pc)
716                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
717                            (ASM.RealInstruction (ASM.MOV (Types.Inl
718                            (Types.Inr { Types.fst = ASM.CARRY; Types.snd =
719                            (ASM.BIT_ADDR b10) })))); Types.snd = pc0 };
720                            Types.snd = (Nat.S Nat.O) }))
721                     | Bool.False ->
722                       let { Types.fst = b6; Types.snd = v7 } =
723                         Vector.head Nat.O v6
724                       in
725                       (match b6 with
726                        | Bool.True ->
727                          prod_inv_rect_Type5 (next pmem pc)
728                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
729                            (ASM.AJMP (ASM.ADDR11
730                            (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
731                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
732                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
733                              ((Nat.S (Nat.S Nat.O)), Bool.True,
734                              (Vector.VCons ((Nat.S Nat.O), Bool.False,
735                              (Vector.VCons (Nat.O, Bool.True,
736                              Vector.VEmpty)))))) b10))); Types.snd = pc0 };
737                            Types.snd = (Nat.S (Nat.S Nat.O)) })
738                        | Bool.False ->
739                          prod_inv_rect_Type5 (next pmem pc)
740                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
741                            (ASM.RealInstruction (ASM.ORL (Types.Inr
742                            { Types.fst = ASM.CARRY; Types.snd =
743                            (ASM.N_BIT_ADDR b10) }))); Types.snd = pc0 };
744                            Types.snd = (Nat.S (Nat.S Nat.O)) }))))))
745         | Bool.False ->
746           let { Types.fst = b2; Types.snd = v3 } =
747             Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
748           in
749           (match b2 with
750            | Bool.True ->
751              let { Types.fst = b3; Types.snd = v4 } =
752                Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
753              in
754              (match b3 with
755               | Bool.True ->
756                 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.SUBB
757                   (ASM.ACC_A, (ASM.REGISTER v4)))); Types.snd = pc };
758                   Types.snd = (Nat.S Nat.O) }
759               | Bool.False ->
760                 let { Types.fst = b4; Types.snd = v5 } =
761                   Vector.head (Nat.S (Nat.S Nat.O)) v4
762                 in
763                 (match b4 with
764                  | Bool.True ->
765                    let { Types.fst = b5; Types.snd = v6 } =
766                      Vector.head (Nat.S Nat.O) v5
767                    in
768                    (match b5 with
769                     | Bool.True ->
770                       { Types.fst = { Types.fst = (ASM.RealInstruction
771                         (ASM.SUBB (ASM.ACC_A, (ASM.INDIRECT
772                         (Vector.from_singl v6))))); Types.snd = pc };
773                         Types.snd = (Nat.S Nat.O) }
774                     | Bool.False ->
775                       let { Types.fst = b6; Types.snd = v7 } =
776                         Vector.head Nat.O v6
777                       in
778                       (match b6 with
779                        | Bool.True ->
780                          prod_inv_rect_Type5 (next pmem pc)
781                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
782                            (ASM.RealInstruction (ASM.SUBB (ASM.ACC_A,
783                            (ASM.DIRECT b10)))); Types.snd = pc0 };
784                            Types.snd = (Nat.S Nat.O) })
785                        | Bool.False ->
786                          prod_inv_rect_Type5 (next pmem pc)
787                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
788                            (ASM.RealInstruction (ASM.SUBB (ASM.ACC_A,
789                            (ASM.DATA b10)))); Types.snd = pc0 }; Types.snd =
790                            (Nat.S Nat.O) })))
791                  | Bool.False ->
792                    let { Types.fst = b5; Types.snd = v6 } =
793                      Vector.head (Nat.S Nat.O) v5
794                    in
795                    (match b5 with
796                     | Bool.True ->
797                       let { Types.fst = b6; Types.snd = v7 } =
798                         Vector.head Nat.O v6
799                       in
800                       (match b6 with
801                        | Bool.True ->
802                          { Types.fst = { Types.fst = (ASM.MOVC (ASM.ACC_A,
803                            ASM.ACC_DPTR)); Types.snd = pc }; Types.snd =
804                            (Nat.S (Nat.S Nat.O)) }
805                        | Bool.False ->
806                          prod_inv_rect_Type5 (next pmem pc)
807                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
808                            (ASM.RealInstruction (ASM.MOV (Types.Inr
809                            { Types.fst = (ASM.BIT_ADDR b10); Types.snd =
810                            ASM.CARRY }))); Types.snd = pc0 }; Types.snd =
811                            (Nat.S (Nat.S Nat.O)) }))
812                     | Bool.False ->
813                       let { Types.fst = b6; Types.snd = v7 } =
814                         Vector.head Nat.O v6
815                       in
816                       (match b6 with
817                        | Bool.True ->
818                          prod_inv_rect_Type5 (next pmem pc)
819                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
820                            (ASM.ACALL (ASM.ADDR11
821                            (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
822                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
823                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
824                              ((Nat.S (Nat.S Nat.O)), Bool.True,
825                              (Vector.VCons ((Nat.S Nat.O), Bool.False,
826                              (Vector.VCons (Nat.O, Bool.False,
827                              Vector.VEmpty)))))) b10))); Types.snd = pc0 };
828                            Types.snd = (Nat.S (Nat.S Nat.O)) })
829                        | Bool.False ->
830                          prod_inv_rect_Type5 (next pmem pc)
831                            (fun pc0 b10 _ ->
832                            prod_inv_rect_Type5 (next pmem pc0)
833                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
834                              (ASM.RealInstruction (ASM.MOV (Types.Inl
835                              (Types.Inl (Types.Inr { Types.fst = ASM.DPTR;
836                              Types.snd = (ASM.DATA16
837                              (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S
838                                (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
839                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
840                                (Nat.S (Nat.S Nat.O)))))))) b10 b20)) })))));
841                              Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S
842                              Nat.O)) }))))))
843            | Bool.False ->
844              let { Types.fst = b3; Types.snd = v4 } =
845                Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
846              in
847              (match b3 with
848               | Bool.True ->
849                 prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
850                   { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
851                   (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst =
852                   (ASM.DIRECT b10); Types.snd = (ASM.REGISTER v4) }))))));
853                   Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) })
854               | Bool.False ->
855                 let { Types.fst = b4; Types.snd = v5 } =
856                   Vector.head (Nat.S (Nat.S Nat.O)) v4
857                 in
858                 (match b4 with
859                  | Bool.True ->
860                    let { Types.fst = b5; Types.snd = v6 } =
861                      Vector.head (Nat.S Nat.O) v5
862                    in
863                    (match b5 with
864                     | Bool.True ->
865                       prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
866                         { Types.fst = { Types.fst = (ASM.RealInstruction
867                         (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inr
868                         { Types.fst = (ASM.DIRECT b10); Types.snd =
869                         (ASM.INDIRECT (Vector.from_singl v6)) }))))));
870                         Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S
871                         Nat.O)) })
872                     | Bool.False ->
873                       let { Types.fst = b6; Types.snd = v7 } =
874                         Vector.head Nat.O v6
875                       in
876                       (match b6 with
877                        | Bool.True ->
878                          prod_inv_rect_Type5 (next pmem pc)
879                            (fun pc0 b10 _ ->
880                            prod_inv_rect_Type5 (next pmem pc0)
881                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
882                              (ASM.RealInstruction (ASM.MOV (Types.Inl
883                              (Types.Inl (Types.Inl (Types.Inr { Types.fst =
884                              (ASM.DIRECT b10); Types.snd = (ASM.DIRECT
885                              b20) })))))); Types.snd = pc1 }; Types.snd =
886                              (Nat.S (Nat.S Nat.O)) }))
887                        | Bool.False ->
888                          { Types.fst = { Types.fst = (ASM.RealInstruction
889                            (ASM.DIV (ASM.ACC_A, ASM.ACC_B))); Types.snd =
890                            pc }; Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S
891                            Nat.O)))) }))
892                  | Bool.False ->
893                    let { Types.fst = b5; Types.snd = v6 } =
894                      Vector.head (Nat.S Nat.O) v5
895                    in
896                    (match b5 with
897                     | Bool.True ->
898                       let { Types.fst = b6; Types.snd = v7 } =
899                         Vector.head Nat.O v6
900                       in
901                       (match b6 with
902                        | Bool.True ->
903                          { Types.fst = { Types.fst = (ASM.MOVC (ASM.ACC_A,
904                            ASM.ACC_PC)); Types.snd = pc }; Types.snd =
905                            (Nat.S (Nat.S Nat.O)) }
906                        | Bool.False ->
907                          prod_inv_rect_Type5 (next pmem pc)
908                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
909                            (ASM.RealInstruction (ASM.ANL (Types.Inr
910                            { Types.fst = ASM.CARRY; Types.snd =
911                            (ASM.BIT_ADDR b10) }))); Types.snd = pc0 };
912                            Types.snd = (Nat.S (Nat.S Nat.O)) }))
913                     | Bool.False ->
914                       let { Types.fst = b6; Types.snd = v7 } =
915                         Vector.head Nat.O v6
916                       in
917                       (match b6 with
918                        | Bool.True ->
919                          prod_inv_rect_Type5 (next pmem pc)
920                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
921                            (ASM.AJMP (ASM.ADDR11
922                            (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
923                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
924                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
925                              ((Nat.S (Nat.S Nat.O)), Bool.True,
926                              (Vector.VCons ((Nat.S Nat.O), Bool.False,
927                              (Vector.VCons (Nat.O, Bool.False,
928                              Vector.VEmpty)))))) b10))); Types.snd = pc0 };
929                            Types.snd = (Nat.S (Nat.S Nat.O)) })
930                        | Bool.False ->
931                          prod_inv_rect_Type5 (next pmem pc)
932                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
933                            (ASM.SJMP (ASM.RELATIVE b10)); Types.snd = pc0 };
934                            Types.snd = (Nat.S (Nat.S Nat.O)) }))))))))
935   | Bool.False ->
936     let { Types.fst = b0; Types.snd = v1 } =
937       Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) v0
938     in
939     (match b0 with
940      | Bool.True ->
941        let { Types.fst = b1; Types.snd = v2 } =
942          Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1
943        in
944        (match b1 with
945         | Bool.True ->
946           let { Types.fst = b2; Types.snd = v3 } =
947             Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
948           in
949           (match b2 with
950            | Bool.True ->
951              let { Types.fst = b3; Types.snd = v4 } =
952                Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
953              in
954              (match b3 with
955               | Bool.True ->
956                 prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
957                   { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
958                   (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
959                   { Types.fst = (ASM.REGISTER v4); Types.snd = (ASM.DATA
960                   b10) }))))))); Types.snd = pc0 }; Types.snd = (Nat.S
961                   Nat.O) })
962               | Bool.False ->
963                 let { Types.fst = b4; Types.snd = v5 } =
964                   Vector.head (Nat.S (Nat.S Nat.O)) v4
965                 in
966                 (match b4 with
967                  | Bool.True ->
968                    let { Types.fst = b5; Types.snd = v6 } =
969                      Vector.head (Nat.S Nat.O) v5
970                    in
971                    (match b5 with
972                     | Bool.True ->
973                       prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
974                         { Types.fst = { Types.fst = (ASM.RealInstruction
975                         (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl
976                         (Types.Inr { Types.fst = (ASM.INDIRECT
977                         (Vector.from_singl v6)); Types.snd = (ASM.DATA
978                         b10) }))))))); Types.snd = pc0 }; Types.snd = (Nat.S
979                         Nat.O) })
980                     | Bool.False ->
981                       let { Types.fst = b6; Types.snd = v7 } =
982                         Vector.head Nat.O v6
983                       in
984                       (match b6 with
985                        | Bool.True ->
986                          prod_inv_rect_Type5 (next pmem pc)
987                            (fun pc0 b10 _ ->
988                            prod_inv_rect_Type5 (next pmem pc0)
989                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
990                              (ASM.RealInstruction (ASM.MOV (Types.Inl
991                              (Types.Inl (Types.Inl (Types.Inr { Types.fst =
992                              (ASM.DIRECT b10); Types.snd = (ASM.DATA
993                              b20) })))))); Types.snd = pc1 }; Types.snd =
994                              (Nat.S (Nat.S (Nat.S Nat.O))) }))
995                        | Bool.False ->
996                          prod_inv_rect_Type5 (next pmem pc)
997                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
998                            (ASM.RealInstruction (ASM.MOV (Types.Inl
999                            (Types.Inl (Types.Inl (Types.Inl (Types.Inl
1000                            { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA
1001                            b10) }))))))); Types.snd = pc0 }; Types.snd =
1002                            (Nat.S Nat.O) })))
1003                  | Bool.False ->
1004                    let { Types.fst = b5; Types.snd = v6 } =
1005                      Vector.head (Nat.S Nat.O) v5
1006                    in
1007                    (match b5 with
1008                     | Bool.True ->
1009                       let { Types.fst = b6; Types.snd = v7 } =
1010                         Vector.head Nat.O v6
1011                       in
1012                       (match b6 with
1013                        | Bool.True ->
1014                          { Types.fst = { Types.fst = (ASM.JMP
1015                            ASM.INDIRECT_DPTR); Types.snd = pc }; Types.snd =
1016                            (Nat.S (Nat.S Nat.O)) }
1017                        | Bool.False ->
1018                          prod_inv_rect_Type5 (next pmem pc)
1019                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1020                            (ASM.RealInstruction (ASM.ORL (Types.Inr
1021                            { Types.fst = ASM.CARRY; Types.snd =
1022                            (ASM.BIT_ADDR b10) }))); Types.snd = pc0 };
1023                            Types.snd = (Nat.S (Nat.S Nat.O)) }))
1024                     | Bool.False ->
1025                       let { Types.fst = b6; Types.snd = v7 } =
1026                         Vector.head Nat.O v6
1027                       in
1028                       (match b6 with
1029                        | Bool.True ->
1030                          prod_inv_rect_Type5 (next pmem pc)
1031                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1032                            (ASM.ACALL (ASM.ADDR11
1033                            (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
1034                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1035                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1036                              ((Nat.S (Nat.S Nat.O)), Bool.False,
1037                              (Vector.VCons ((Nat.S Nat.O), Bool.True,
1038                              (Vector.VCons (Nat.O, Bool.True,
1039                              Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1040                            Types.snd = (Nat.S (Nat.S Nat.O)) })
1041                        | Bool.False ->
1042                          prod_inv_rect_Type5 (next pmem pc)
1043                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1044                            (ASM.RealInstruction (ASM.JNZ (ASM.RELATIVE
1045                            b10))); Types.snd = pc0 }; Types.snd = (Nat.S
1046                            (Nat.S Nat.O)) })))))
1047            | Bool.False ->
1048              let { Types.fst = b3; Types.snd = v4 } =
1049                Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1050              in
1051              (match b3 with
1052               | Bool.True ->
1053                 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.XRL
1054                   (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1055                   (ASM.REGISTER v4) }))); Types.snd = pc }; Types.snd =
1056                   (Nat.S Nat.O) }
1057               | Bool.False ->
1058                 let { Types.fst = b4; Types.snd = v5 } =
1059                   Vector.head (Nat.S (Nat.S Nat.O)) v4
1060                 in
1061                 (match b4 with
1062                  | Bool.True ->
1063                    let { Types.fst = b5; Types.snd = v6 } =
1064                      Vector.head (Nat.S Nat.O) v5
1065                    in
1066                    (match b5 with
1067                     | Bool.True ->
1068                       { Types.fst = { Types.fst = (ASM.RealInstruction
1069                         (ASM.XRL (Types.Inl { Types.fst = ASM.ACC_A;
1070                         Types.snd = (ASM.INDIRECT
1071                         (Vector.from_singl v6)) }))); Types.snd = pc };
1072                         Types.snd = (Nat.S Nat.O) }
1073                     | Bool.False ->
1074                       let { Types.fst = b6; Types.snd = v7 } =
1075                         Vector.head Nat.O v6
1076                       in
1077                       (match b6 with
1078                        | Bool.True ->
1079                          prod_inv_rect_Type5 (next pmem pc)
1080                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1081                            (ASM.RealInstruction (ASM.XRL (Types.Inl
1082                            { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT
1083                            b10) }))); Types.snd = pc0 }; Types.snd = (Nat.S
1084                            Nat.O) })
1085                        | Bool.False ->
1086                          prod_inv_rect_Type5 (next pmem pc)
1087                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1088                            (ASM.RealInstruction (ASM.XRL (Types.Inl
1089                            { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA
1090                            b10) }))); Types.snd = pc0 }; Types.snd = (Nat.S
1091                            Nat.O) })))
1092                  | Bool.False ->
1093                    let { Types.fst = b5; Types.snd = v6 } =
1094                      Vector.head (Nat.S Nat.O) v5
1095                    in
1096                    (match b5 with
1097                     | Bool.True ->
1098                       let { Types.fst = b6; Types.snd = v7 } =
1099                         Vector.head Nat.O v6
1100                       in
1101                       (match b6 with
1102                        | Bool.True ->
1103                          prod_inv_rect_Type5 (next pmem pc)
1104                            (fun pc0 b10 _ ->
1105                            prod_inv_rect_Type5 (next pmem pc0)
1106                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1107                              (ASM.RealInstruction (ASM.XRL (Types.Inr
1108                              { Types.fst = (ASM.DIRECT b10); Types.snd =
1109                              (ASM.DATA b20) }))); Types.snd = pc1 };
1110                              Types.snd = (Nat.S (Nat.S Nat.O)) }))
1111                        | Bool.False ->
1112                          prod_inv_rect_Type5 (next pmem pc)
1113                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1114                            (ASM.RealInstruction (ASM.XRL (Types.Inr
1115                            { Types.fst = (ASM.DIRECT b10); Types.snd =
1116                            ASM.ACC_A }))); Types.snd = pc0 }; Types.snd =
1117                            (Nat.S Nat.O) }))
1118                     | Bool.False ->
1119                       let { Types.fst = b6; Types.snd = v7 } =
1120                         Vector.head Nat.O v6
1121                       in
1122                       (match b6 with
1123                        | Bool.True ->
1124                          prod_inv_rect_Type5 (next pmem pc)
1125                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1126                            (ASM.AJMP (ASM.ADDR11
1127                            (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
1128                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1129                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1130                              ((Nat.S (Nat.S Nat.O)), Bool.False,
1131                              (Vector.VCons ((Nat.S Nat.O), Bool.True,
1132                              (Vector.VCons (Nat.O, Bool.True,
1133                              Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1134                            Types.snd = (Nat.S (Nat.S Nat.O)) })
1135                        | Bool.False ->
1136                          prod_inv_rect_Type5 (next pmem pc)
1137                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1138                            (ASM.RealInstruction (ASM.JZ (ASM.RELATIVE
1139                            b10))); Types.snd = pc0 }; Types.snd = (Nat.S
1140                            (Nat.S Nat.O)) }))))))
1141         | Bool.False ->
1142           let { Types.fst = b2; Types.snd = v3 } =
1143             Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
1144           in
1145           (match b2 with
1146            | Bool.True ->
1147              let { Types.fst = b3; Types.snd = v4 } =
1148                Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1149              in
1150              (match b3 with
1151               | Bool.True ->
1152                 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ANL
1153                   (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1154                   (ASM.REGISTER v4) })))); Types.snd = pc }; Types.snd =
1155                   (Nat.S Nat.O) }
1156               | Bool.False ->
1157                 let { Types.fst = b4; Types.snd = v5 } =
1158                   Vector.head (Nat.S (Nat.S Nat.O)) v4
1159                 in
1160                 (match b4 with
1161                  | Bool.True ->
1162                    let { Types.fst = b5; Types.snd = v6 } =
1163                      Vector.head (Nat.S Nat.O) v5
1164                    in
1165                    (match b5 with
1166                     | Bool.True ->
1167                       { Types.fst = { Types.fst = (ASM.RealInstruction
1168                         (ASM.ANL (Types.Inl (Types.Inl { Types.fst =
1169                         ASM.ACC_A; Types.snd = (ASM.INDIRECT
1170                         (Vector.from_singl v6)) })))); Types.snd = pc };
1171                         Types.snd = (Nat.S Nat.O) }
1172                     | Bool.False ->
1173                       let { Types.fst = b6; Types.snd = v7 } =
1174                         Vector.head Nat.O v6
1175                       in
1176                       (match b6 with
1177                        | Bool.True ->
1178                          prod_inv_rect_Type5 (next pmem pc)
1179                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1180                            (ASM.RealInstruction (ASM.ANL (Types.Inl
1181                            (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1182                            (ASM.DIRECT b10) })))); Types.snd = pc0 };
1183                            Types.snd = (Nat.S Nat.O) })
1184                        | Bool.False ->
1185                          prod_inv_rect_Type5 (next pmem pc)
1186                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1187                            (ASM.RealInstruction (ASM.ANL (Types.Inl
1188                            (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1189                            (ASM.DATA b10) })))); Types.snd = pc0 };
1190                            Types.snd = (Nat.S Nat.O) })))
1191                  | Bool.False ->
1192                    let { Types.fst = b5; Types.snd = v6 } =
1193                      Vector.head (Nat.S Nat.O) v5
1194                    in
1195                    (match b5 with
1196                     | Bool.True ->
1197                       let { Types.fst = b6; Types.snd = v7 } =
1198                         Vector.head Nat.O v6
1199                       in
1200                       (match b6 with
1201                        | Bool.True ->
1202                          prod_inv_rect_Type5 (next pmem pc)
1203                            (fun pc0 b10 _ ->
1204                            prod_inv_rect_Type5 (next pmem pc0)
1205                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1206                              (ASM.RealInstruction (ASM.ANL (Types.Inl
1207                              (Types.Inr { Types.fst = (ASM.DIRECT b10);
1208                              Types.snd = (ASM.DATA b20) })))); Types.snd =
1209                              pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))
1210                        | Bool.False ->
1211                          prod_inv_rect_Type5 (next pmem pc)
1212                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1213                            (ASM.RealInstruction (ASM.ANL (Types.Inl
1214                            (Types.Inr { Types.fst = (ASM.DIRECT b10);
1215                            Types.snd = ASM.ACC_A })))); Types.snd = pc0 };
1216                            Types.snd = (Nat.S Nat.O) }))
1217                     | Bool.False ->
1218                       let { Types.fst = b6; Types.snd = v7 } =
1219                         Vector.head Nat.O v6
1220                       in
1221                       (match b6 with
1222                        | Bool.True ->
1223                          prod_inv_rect_Type5 (next pmem pc)
1224                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1225                            (ASM.ACALL (ASM.ADDR11
1226                            (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
1227                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1228                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1229                              ((Nat.S (Nat.S Nat.O)), Bool.False,
1230                              (Vector.VCons ((Nat.S Nat.O), Bool.True,
1231                              (Vector.VCons (Nat.O, Bool.False,
1232                              Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1233                            Types.snd = (Nat.S (Nat.S Nat.O)) })
1234                        | Bool.False ->
1235                          prod_inv_rect_Type5 (next pmem pc)
1236                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1237                            (ASM.RealInstruction (ASM.JNC (ASM.RELATIVE
1238                            b10))); Types.snd = pc0 }; Types.snd = (Nat.S
1239                            (Nat.S Nat.O)) })))))
1240            | Bool.False ->
1241              let { Types.fst = b3; Types.snd = v4 } =
1242                Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1243              in
1244              (match b3 with
1245               | Bool.True ->
1246                 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ORL
1247                   (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1248                   (ASM.REGISTER v4) })))); Types.snd = pc }; Types.snd =
1249                   (Nat.S Nat.O) }
1250               | Bool.False ->
1251                 let { Types.fst = b4; Types.snd = v5 } =
1252                   Vector.head (Nat.S (Nat.S Nat.O)) v4
1253                 in
1254                 (match b4 with
1255                  | Bool.True ->
1256                    let { Types.fst = b5; Types.snd = v6 } =
1257                      Vector.head (Nat.S Nat.O) v5
1258                    in
1259                    (match b5 with
1260                     | Bool.True ->
1261                       { Types.fst = { Types.fst = (ASM.RealInstruction
1262                         (ASM.ORL (Types.Inl (Types.Inl { Types.fst =
1263                         ASM.ACC_A; Types.snd = (ASM.INDIRECT
1264                         (Vector.from_singl v6)) })))); Types.snd = pc };
1265                         Types.snd = (Nat.S Nat.O) }
1266                     | Bool.False ->
1267                       let { Types.fst = b6; Types.snd = v7 } =
1268                         Vector.head Nat.O v6
1269                       in
1270                       (match b6 with
1271                        | Bool.True ->
1272                          prod_inv_rect_Type5 (next pmem pc)
1273                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1274                            (ASM.RealInstruction (ASM.ORL (Types.Inl
1275                            (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1276                            (ASM.DIRECT b10) })))); Types.snd = pc0 };
1277                            Types.snd = (Nat.S Nat.O) })
1278                        | Bool.False ->
1279                          prod_inv_rect_Type5 (next pmem pc)
1280                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1281                            (ASM.RealInstruction (ASM.ORL (Types.Inl
1282                            (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1283                            (ASM.DATA b10) })))); Types.snd = pc0 };
1284                            Types.snd = (Nat.S Nat.O) })))
1285                  | Bool.False ->
1286                    let { Types.fst = b5; Types.snd = v6 } =
1287                      Vector.head (Nat.S Nat.O) v5
1288                    in
1289                    (match b5 with
1290                     | Bool.True ->
1291                       let { Types.fst = b6; Types.snd = v7 } =
1292                         Vector.head Nat.O v6
1293                       in
1294                       (match b6 with
1295                        | Bool.True ->
1296                          prod_inv_rect_Type5 (next pmem pc)
1297                            (fun pc0 b10 _ ->
1298                            prod_inv_rect_Type5 (next pmem pc0)
1299                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1300                              (ASM.RealInstruction (ASM.ORL (Types.Inl
1301                              (Types.Inr { Types.fst = (ASM.DIRECT b10);
1302                              Types.snd = (ASM.DATA b20) })))); Types.snd =
1303                              pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))
1304                        | Bool.False ->
1305                          prod_inv_rect_Type5 (next pmem pc)
1306                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1307                            (ASM.RealInstruction (ASM.ORL (Types.Inl
1308                            (Types.Inr { Types.fst = (ASM.DIRECT b10);
1309                            Types.snd = ASM.ACC_A })))); Types.snd = pc0 };
1310                            Types.snd = (Nat.S Nat.O) }))
1311                     | Bool.False ->
1312                       let { Types.fst = b6; Types.snd = v7 } =
1313                         Vector.head Nat.O v6
1314                       in
1315                       (match b6 with
1316                        | Bool.True ->
1317                          prod_inv_rect_Type5 (next pmem pc)
1318                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1319                            (ASM.AJMP (ASM.ADDR11
1320                            (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
1321                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1322                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1323                              ((Nat.S (Nat.S Nat.O)), Bool.False,
1324                              (Vector.VCons ((Nat.S Nat.O), Bool.True,
1325                              (Vector.VCons (Nat.O, Bool.False,
1326                              Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1327                            Types.snd = (Nat.S (Nat.S Nat.O)) })
1328                        | Bool.False ->
1329                          prod_inv_rect_Type5 (next pmem pc)
1330                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1331                            (ASM.RealInstruction (ASM.JC (ASM.RELATIVE
1332                            b10))); Types.snd = pc0 }; Types.snd = (Nat.S
1333                            (Nat.S Nat.O)) })))))))
1334      | Bool.False ->
1335        let { Types.fst = b1; Types.snd = v2 } =
1336          Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1
1337        in
1338        (match b1 with
1339         | Bool.True ->
1340           let { Types.fst = b2; Types.snd = v3 } =
1341             Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
1342           in
1343           (match b2 with
1344            | Bool.True ->
1345              let { Types.fst = b3; Types.snd = v4 } =
1346                Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1347              in
1348              (match b3 with
1349               | Bool.True ->
1350                 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ADDC
1351                   (ASM.ACC_A, (ASM.REGISTER v4)))); Types.snd = pc };
1352                   Types.snd = (Nat.S Nat.O) }
1353               | Bool.False ->
1354                 let { Types.fst = b4; Types.snd = v5 } =
1355                   Vector.head (Nat.S (Nat.S Nat.O)) v4
1356                 in
1357                 (match b4 with
1358                  | Bool.True ->
1359                    let { Types.fst = b5; Types.snd = v6 } =
1360                      Vector.head (Nat.S Nat.O) v5
1361                    in
1362                    (match b5 with
1363                     | Bool.True ->
1364                       { Types.fst = { Types.fst = (ASM.RealInstruction
1365                         (ASM.ADDC (ASM.ACC_A, (ASM.INDIRECT
1366                         (Vector.from_singl v6))))); Types.snd = pc };
1367                         Types.snd = (Nat.S Nat.O) }
1368                     | Bool.False ->
1369                       let { Types.fst = b6; Types.snd = v7 } =
1370                         Vector.head Nat.O v6
1371                       in
1372                       (match b6 with
1373                        | Bool.True ->
1374                          prod_inv_rect_Type5 (next pmem pc)
1375                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1376                            (ASM.RealInstruction (ASM.ADDC (ASM.ACC_A,
1377                            (ASM.DIRECT b10)))); Types.snd = pc0 };
1378                            Types.snd = (Nat.S Nat.O) })
1379                        | Bool.False ->
1380                          prod_inv_rect_Type5 (next pmem pc)
1381                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1382                            (ASM.RealInstruction (ASM.ADDC (ASM.ACC_A,
1383                            (ASM.DATA b10)))); Types.snd = pc0 }; Types.snd =
1384                            (Nat.S Nat.O) })))
1385                  | Bool.False ->
1386                    let { Types.fst = b5; Types.snd = v6 } =
1387                      Vector.head (Nat.S Nat.O) v5
1388                    in
1389                    (match b5 with
1390                     | Bool.True ->
1391                       let { Types.fst = b6; Types.snd = v7 } =
1392                         Vector.head Nat.O v6
1393                       in
1394                       (match b6 with
1395                        | Bool.True ->
1396                          { Types.fst = { Types.fst = (ASM.RealInstruction
1397                            (ASM.RLC ASM.ACC_A)); Types.snd = pc };
1398                            Types.snd = (Nat.S Nat.O) }
1399                        | Bool.False ->
1400                          { Types.fst = { Types.fst = (ASM.RealInstruction
1401                            ASM.RETI); Types.snd = pc }; Types.snd = (Nat.S
1402                            (Nat.S Nat.O)) })
1403                     | Bool.False ->
1404                       let { Types.fst = b6; Types.snd = v7 } =
1405                         Vector.head Nat.O v6
1406                       in
1407                       (match b6 with
1408                        | Bool.True ->
1409                          prod_inv_rect_Type5 (next pmem pc)
1410                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1411                            (ASM.ACALL (ASM.ADDR11
1412                            (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
1413                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1414                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1415                              ((Nat.S (Nat.S Nat.O)), Bool.False,
1416                              (Vector.VCons ((Nat.S Nat.O), Bool.False,
1417                              (Vector.VCons (Nat.O, Bool.True,
1418                              Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1419                            Types.snd = (Nat.S (Nat.S Nat.O)) })
1420                        | Bool.False ->
1421                          prod_inv_rect_Type5 (next pmem pc)
1422                            (fun pc0 b10 _ ->
1423                            prod_inv_rect_Type5 (next pmem pc0)
1424                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1425                              (ASM.RealInstruction (ASM.JNB ((ASM.BIT_ADDR
1426                              b10), (ASM.RELATIVE b20)))); Types.snd = pc1 };
1427                              Types.snd = (Nat.S (Nat.S Nat.O)) }))))))
1428            | Bool.False ->
1429              let { Types.fst = b3; Types.snd = v4 } =
1430                Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1431              in
1432              (match b3 with
1433               | Bool.True ->
1434                 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ADD
1435                   (ASM.ACC_A, (ASM.REGISTER v4)))); Types.snd = pc };
1436                   Types.snd = (Nat.S Nat.O) }
1437               | Bool.False ->
1438                 let { Types.fst = b4; Types.snd = v5 } =
1439                   Vector.head (Nat.S (Nat.S Nat.O)) v4
1440                 in
1441                 (match b4 with
1442                  | Bool.True ->
1443                    let { Types.fst = b5; Types.snd = v6 } =
1444                      Vector.head (Nat.S Nat.O) v5
1445                    in
1446                    (match b5 with
1447                     | Bool.True ->
1448                       { Types.fst = { Types.fst = (ASM.RealInstruction
1449                         (ASM.ADD (ASM.ACC_A, (ASM.INDIRECT
1450                         (Vector.from_singl v6))))); Types.snd = pc };
1451                         Types.snd = (Nat.S Nat.O) }
1452                     | Bool.False ->
1453                       let { Types.fst = b6; Types.snd = v7 } =
1454                         Vector.head Nat.O v6
1455                       in
1456                       (match b6 with
1457                        | Bool.True ->
1458                          prod_inv_rect_Type5 (next pmem pc)
1459                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1460                            (ASM.RealInstruction (ASM.ADD (ASM.ACC_A,
1461                            (ASM.DIRECT b10)))); Types.snd = pc0 };
1462                            Types.snd = (Nat.S Nat.O) })
1463                        | Bool.False ->
1464                          prod_inv_rect_Type5 (next pmem pc)
1465                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1466                            (ASM.RealInstruction (ASM.ADD (ASM.ACC_A,
1467                            (ASM.DATA b10)))); Types.snd = pc0 }; Types.snd =
1468                            (Nat.S Nat.O) })))
1469                  | Bool.False ->
1470                    let { Types.fst = b5; Types.snd = v6 } =
1471                      Vector.head (Nat.S Nat.O) v5
1472                    in
1473                    (match b5 with
1474                     | Bool.True ->
1475                       let { Types.fst = b6; Types.snd = v7 } =
1476                         Vector.head Nat.O v6
1477                       in
1478                       (match b6 with
1479                        | Bool.True ->
1480                          { Types.fst = { Types.fst = (ASM.RealInstruction
1481                            (ASM.RL ASM.ACC_A)); Types.snd = pc };
1482                            Types.snd = (Nat.S Nat.O) }
1483                        | Bool.False ->
1484                          { Types.fst = { Types.fst = (ASM.RealInstruction
1485                            ASM.RET); Types.snd = pc }; Types.snd = (Nat.S
1486                            (Nat.S Nat.O)) })
1487                     | Bool.False ->
1488                       let { Types.fst = b6; Types.snd = v7 } =
1489                         Vector.head Nat.O v6
1490                       in
1491                       (match b6 with
1492                        | Bool.True ->
1493                          prod_inv_rect_Type5 (next pmem pc)
1494                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1495                            (ASM.AJMP (ASM.ADDR11
1496                            (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
1497                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1498                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1499                              ((Nat.S (Nat.S Nat.O)), Bool.False,
1500                              (Vector.VCons ((Nat.S Nat.O), Bool.False,
1501                              (Vector.VCons (Nat.O, Bool.True,
1502                              Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1503                            Types.snd = (Nat.S (Nat.S Nat.O)) })
1504                        | Bool.False ->
1505                          prod_inv_rect_Type5 (next pmem pc)
1506                            (fun pc0 b10 _ ->
1507                            prod_inv_rect_Type5 (next pmem pc0)
1508                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1509                              (ASM.RealInstruction (ASM.JB ((ASM.BIT_ADDR
1510                              b10), (ASM.RELATIVE b20)))); Types.snd = pc1 };
1511                              Types.snd = (Nat.S (Nat.S Nat.O)) })))))))
1512         | Bool.False ->
1513           let { Types.fst = b2; Types.snd = v3 } =
1514             Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
1515           in
1516           (match b2 with
1517            | Bool.True ->
1518              let { Types.fst = b3; Types.snd = v4 } =
1519                Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1520              in
1521              (match b3 with
1522               | Bool.True ->
1523                 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DEC
1524                   (ASM.REGISTER v4))); Types.snd = pc }; Types.snd = (Nat.S
1525                   Nat.O) }
1526               | Bool.False ->
1527                 let { Types.fst = b4; Types.snd = v5 } =
1528                   Vector.head (Nat.S (Nat.S Nat.O)) v4
1529                 in
1530                 (match b4 with
1531                  | Bool.True ->
1532                    let { Types.fst = b5; Types.snd = v6 } =
1533                      Vector.head (Nat.S Nat.O) v5
1534                    in
1535                    (match b5 with
1536                     | Bool.True ->
1537                       { Types.fst = { Types.fst = (ASM.RealInstruction
1538                         (ASM.DEC (ASM.INDIRECT (Vector.from_singl v6))));
1539                         Types.snd = pc }; Types.snd = (Nat.S Nat.O) }
1540                     | Bool.False ->
1541                       let { Types.fst = b6; Types.snd = v7 } =
1542                         Vector.head Nat.O v6
1543                       in
1544                       (match b6 with
1545                        | Bool.True ->
1546                          prod_inv_rect_Type5 (next pmem pc)
1547                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1548                            (ASM.RealInstruction (ASM.DEC (ASM.DIRECT b10)));
1549                            Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) })
1550                        | Bool.False ->
1551                          { Types.fst = { Types.fst = (ASM.RealInstruction
1552                            (ASM.DEC ASM.ACC_A)); Types.snd = pc };
1553                            Types.snd = (Nat.S Nat.O) }))
1554                  | Bool.False ->
1555                    let { Types.fst = b5; Types.snd = v6 } =
1556                      Vector.head (Nat.S Nat.O) v5
1557                    in
1558                    (match b5 with
1559                     | Bool.True ->
1560                       let { Types.fst = b6; Types.snd = v7 } =
1561                         Vector.head Nat.O v6
1562                       in
1563                       (match b6 with
1564                        | Bool.True ->
1565                          { Types.fst = { Types.fst = (ASM.RealInstruction
1566                            (ASM.RRC ASM.ACC_A)); Types.snd = pc };
1567                            Types.snd = (Nat.S Nat.O) }
1568                        | Bool.False ->
1569                          prod_inv_rect_Type5 (next pmem pc)
1570                            (fun pc0 b10 _ ->
1571                            prod_inv_rect_Type5 (next pmem pc0)
1572                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1573                              (ASM.LCALL (ASM.ADDR16
1574                              (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S
1575                                (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
1576                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1577                                (Nat.S (Nat.S Nat.O)))))))) b10 b20)));
1578                              Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S
1579                              Nat.O)) })))
1580                     | Bool.False ->
1581                       let { Types.fst = b6; Types.snd = v7 } =
1582                         Vector.head Nat.O v6
1583                       in
1584                       (match b6 with
1585                        | Bool.True ->
1586                          prod_inv_rect_Type5 (next pmem pc)
1587                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1588                            (ASM.ACALL (ASM.ADDR11
1589                            (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
1590                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1591                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1592                              ((Nat.S (Nat.S Nat.O)), Bool.False,
1593                              (Vector.VCons ((Nat.S Nat.O), Bool.False,
1594                              (Vector.VCons (Nat.O, Bool.False,
1595                              Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1596                            Types.snd = (Nat.S (Nat.S Nat.O)) })
1597                        | Bool.False ->
1598                          prod_inv_rect_Type5 (next pmem pc)
1599                            (fun pc0 b10 _ ->
1600                            prod_inv_rect_Type5 (next pmem pc0)
1601                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1602                              (ASM.RealInstruction (ASM.JBC ((ASM.BIT_ADDR
1603                              b10), (ASM.RELATIVE b20)))); Types.snd = pc1 };
1604                              Types.snd = (Nat.S (Nat.S Nat.O)) }))))))
1605            | Bool.False ->
1606              let { Types.fst = b3; Types.snd = v4 } =
1607                Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1608              in
1609              (match b3 with
1610               | Bool.True ->
1611                 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.INC
1612                   (ASM.REGISTER v4))); Types.snd = pc }; Types.snd = (Nat.S
1613                   Nat.O) }
1614               | Bool.False ->
1615                 let { Types.fst = b4; Types.snd = v5 } =
1616                   Vector.head (Nat.S (Nat.S Nat.O)) v4
1617                 in
1618                 (match b4 with
1619                  | Bool.True ->
1620                    let { Types.fst = b5; Types.snd = v6 } =
1621                      Vector.head (Nat.S Nat.O) v5
1622                    in
1623                    (match b5 with
1624                     | Bool.True ->
1625                       { Types.fst = { Types.fst = (ASM.RealInstruction
1626                         (ASM.INC (ASM.INDIRECT (Vector.from_singl v6))));
1627                         Types.snd = pc }; Types.snd = (Nat.S Nat.O) }
1628                     | Bool.False ->
1629                       let { Types.fst = b6; Types.snd = v7 } =
1630                         Vector.head Nat.O v6
1631                       in
1632                       (match b6 with
1633                        | Bool.True ->
1634                          prod_inv_rect_Type5 (next pmem pc)
1635                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1636                            (ASM.RealInstruction (ASM.INC (ASM.DIRECT b10)));
1637                            Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) })
1638                        | Bool.False ->
1639                          { Types.fst = { Types.fst = (ASM.RealInstruction
1640                            (ASM.INC ASM.ACC_A)); Types.snd = pc };
1641                            Types.snd = (Nat.S Nat.O) }))
1642                  | Bool.False ->
1643                    let { Types.fst = b5; Types.snd = v6 } =
1644                      Vector.head (Nat.S Nat.O) v5
1645                    in
1646                    (match b5 with
1647                     | Bool.True ->
1648                       let { Types.fst = b6; Types.snd = v7 } =
1649                         Vector.head Nat.O v6
1650                       in
1651                       (match b6 with
1652                        | Bool.True ->
1653                          { Types.fst = { Types.fst = (ASM.RealInstruction
1654                            (ASM.RR ASM.ACC_A)); Types.snd = pc };
1655                            Types.snd = (Nat.S Nat.O) }
1656                        | Bool.False ->
1657                          prod_inv_rect_Type5 (next pmem pc)
1658                            (fun pc0 b10 _ ->
1659                            prod_inv_rect_Type5 (next pmem pc0)
1660                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1661                              (ASM.LJMP (ASM.ADDR16
1662                              (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S
1663                                (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
1664                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1665                                (Nat.S (Nat.S Nat.O)))))))) b10 b20)));
1666                              Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S
1667                              Nat.O)) })))
1668                     | Bool.False ->
1669                       let { Types.fst = b6; Types.snd = v7 } =
1670                         Vector.head Nat.O v6
1671                       in
1672                       (match b6 with
1673                        | Bool.True ->
1674                          prod_inv_rect_Type5 (next pmem pc)
1675                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1676                            (ASM.AJMP (ASM.ADDR11
1677                            (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
1678                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1679                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1680                              ((Nat.S (Nat.S Nat.O)), Bool.False,
1681                              (Vector.VCons ((Nat.S Nat.O), Bool.False,
1682                              (Vector.VCons (Nat.O, Bool.False,
1683                              Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1684                            Types.snd = (Nat.S (Nat.S Nat.O)) })
1685                        | Bool.False ->
1686                          { Types.fst = { Types.fst = (ASM.RealInstruction
1687                            ASM.NOP); Types.snd = pc }; Types.snd = (Nat.S
1688                            Nat.O) }))))))))
1689
1690(** val fetch :
1691    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
1692    ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod **)
1693let fetch pmem pc =
1694  let { Types.fst = word0; Types.snd = byte0 } = next pmem pc in
1695  fetch0 pmem word0 byte0
1696
Note: See TracBrowser for help on using the repository browser.