source: extracted/fetch.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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