source: extracted/fetch.ml @ 2951

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

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