source: extracted/fetch.ml @ 3065

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

Efficiency of semantics of assembled improved: ticks_of was re-computing the
address_of_word_labels map again and again.

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