source: extracted/fetch.ml @ 3080

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

New extraction.

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