source: extracted/fetch.ml @ 2999

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

code_memory added to labelled_object_code to avoid recomputing it every time.
This gives a major speed up in the semantics of the extracted code.

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