source: driver/extracted/fetch.ml @ 3106

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

New extraction.

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