83 type serialBufferType =
84 | Eight of BitVector.byte
85 | Nine of BitVector.bit * BitVector.byte
87 val serialBufferType_rect_Type4 :
88 (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
89 serialBufferType -> 'a1
91 val serialBufferType_rect_Type5 :
92 (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
93 serialBufferType -> 'a1
95 val serialBufferType_rect_Type3 :
96 (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
97 serialBufferType -> 'a1
99 val serialBufferType_rect_Type2 :
100 (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
101 serialBufferType -> 'a1
103 val serialBufferType_rect_Type1 :
104 (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
105 serialBufferType -> 'a1
107 val serialBufferType_rect_Type0 :
108 (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
109 serialBufferType -> 'a1
111 val serialBufferType_inv_rect_Type4 :
112 serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
113 BitVector.byte -> __ -> 'a1) -> 'a1
115 val serialBufferType_inv_rect_Type3 :
116 serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
117 BitVector.byte -> __ -> 'a1) -> 'a1
119 val serialBufferType_inv_rect_Type2 :
120 serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
121 BitVector.byte -> __ -> 'a1) -> 'a1
123 val serialBufferType_inv_rect_Type1 :
124 serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
125 BitVector.byte -> __ -> 'a1) -> 'a1
127 val serialBufferType_inv_rect_Type0 :
128 serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
129 BitVector.byte -> __ -> 'a1) -> 'a1
131 val serialBufferType_discr : serialBufferType -> serialBufferType -> __
133 val serialBufferType_jmdiscr : serialBufferType -> serialBufferType -> __
136 | P1 of BitVector.byte
137 | P3 of BitVector.byte
138 | SerialBuffer of serialBufferType
140 val lineType_rect_Type4 :
141 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
142 'a1) -> lineType -> 'a1
144 val lineType_rect_Type5 :
145 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
146 'a1) -> lineType -> 'a1
148 val lineType_rect_Type3 :
149 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
150 'a1) -> lineType -> 'a1
152 val lineType_rect_Type2 :
153 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
154 'a1) -> lineType -> 'a1
156 val lineType_rect_Type1 :
157 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
158 'a1) -> lineType -> 'a1
160 val lineType_rect_Type0 :
161 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
162 'a1) -> lineType -> 'a1
164 val lineType_inv_rect_Type4 :
165 lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
166 -> (serialBufferType -> __ -> 'a1) -> 'a1
168 val lineType_inv_rect_Type3 :
169 lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
170 -> (serialBufferType -> __ -> 'a1) -> 'a1
172 val lineType_inv_rect_Type2 :
173 lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
174 -> (serialBufferType -> __ -> 'a1) -> 'a1
176 val lineType_inv_rect_Type1 :
177 lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
178 -> (serialBufferType -> __ -> 'a1) -> 'a1
180 val lineType_inv_rect_Type0 :
181 lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
182 -> (serialBufferType -> __ -> 'a1) -> 'a1
184 val lineType_discr : lineType -> lineType -> __
186 val lineType_jmdiscr : lineType -> lineType -> __
209 val sFR8051_rect_Type4 :
210 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
211 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
213 val sFR8051_rect_Type5 :
214 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
215 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
217 val sFR8051_rect_Type3 :
218 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
219 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
221 val sFR8051_rect_Type2 :
222 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
223 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
225 val sFR8051_rect_Type1 :
226 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
227 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
229 val sFR8051_rect_Type0 :
230 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
231 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
233 val sFR8051_inv_rect_Type4 :
234 sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
235 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
236 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
237 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
239 val sFR8051_inv_rect_Type3 :
240 sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
241 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
242 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
243 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
245 val sFR8051_inv_rect_Type2 :
246 sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
247 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
248 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
249 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
251 val sFR8051_inv_rect_Type1 :
252 sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
253 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
254 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
255 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
257 val sFR8051_inv_rect_Type0 :
258 sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
259 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
260 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
261 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
263 val sFR8051_discr : sFR8051 -> sFR8051 -> __
265 val sFR8051_jmdiscr : sFR8051 -> sFR8051 -> __
267 val sfr_8051_index : sFR8051 -> Nat.nat
276 val sFR8052_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
278 val sFR8052_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
280 val sFR8052_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
282 val sFR8052_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
284 val sFR8052_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
286 val sFR8052_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
288 val sFR8052_inv_rect_Type4 :
289 sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
292 val sFR8052_inv_rect_Type3 :
293 sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
296 val sFR8052_inv_rect_Type2 :
297 sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
300 val sFR8052_inv_rect_Type1 :
301 sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
304 val sFR8052_inv_rect_Type0 :
305 sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
308 val sFR8052_discr : sFR8052 -> sFR8052 -> __
310 val sFR8052_jmdiscr : sFR8052 -> sFR8052 -> __
312 val sfr_8052_index : sFR8052 -> Nat.nat
314 type 'm preStatus = { low_internal_ram : BitVector.byte
315 BitVectorTrie.bitVectorTrie;
316 high_internal_ram : BitVector.byte
317 BitVectorTrie.bitVectorTrie;
318 external_ram : BitVector.byte
319 BitVectorTrie.bitVectorTrie;
320 program_counter : BitVector.word;
321 special_function_registers_8051 : BitVector.byte
323 special_function_registers_8052 : BitVector.byte
325 p1_latch : BitVector.byte; p3_latch : BitVector.byte;
328 val preStatus_rect_Type4 :
329 'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
330 BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
331 -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
332 Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
335 val preStatus_rect_Type5 :
336 'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
337 BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
338 -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
339 Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
342 val preStatus_rect_Type3 :
343 'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
344 BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
345 -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
346 Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
349 val preStatus_rect_Type2 :
350 'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
351 BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
352 -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
353 Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
356 val preStatus_rect_Type1 :
357 'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
358 BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
359 -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
360 Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
363 val preStatus_rect_Type0 :
364 'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
365 BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
366 -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
367 Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
370 val low_internal_ram :
371 'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie
373 val high_internal_ram :
374 'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie
377 'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie
379 val program_counter : 'a1 -> 'a1 preStatus -> BitVector.word
381 val special_function_registers_8051 :
382 'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector
384 val special_function_registers_8052 :
385 'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector
387 val p1_latch : 'a1 -> 'a1 preStatus -> BitVector.byte
389 val p3_latch : 'a1 -> 'a1 preStatus -> BitVector.byte
391 val clock : 'a1 -> 'a1 preStatus -> time
393 val preStatus_inv_rect_Type4 :
394 'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
395 BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
396 BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
397 Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
398 BitVector.byte -> time -> __ -> 'a2) -> 'a2
400 val preStatus_inv_rect_Type3 :
401 'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
402 BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
403 BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
404 Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
405 BitVector.byte -> time -> __ -> 'a2) -> 'a2
407 val preStatus_inv_rect_Type2 :
408 'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
409 BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
410 BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
411 Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
412 BitVector.byte -> time -> __ -> 'a2) -> 'a2
414 val preStatus_inv_rect_Type1 :
415 'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
416 BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
417 BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
418 Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
419 BitVector.byte -> time -> __ -> 'a2) -> 'a2
421 val preStatus_inv_rect_Type0 :
422 'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
423 BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
424 BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
425 Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
426 BitVector.byte -> time -> __ -> 'a2) -> 'a2
428 val preStatus_jmdiscr : 'a1 -> 'a1 preStatus -> 'a1 preStatus -> __
430 type status = BitVector.byte BitVectorTrie.bitVectorTrie preStatus
432 type pseudoStatus = ASM.pseudo_assembly_program preStatus
434 val set_clock : 'a1 -> 'a1 preStatus -> time -> 'a1 preStatus
436 val set_p1_latch : 'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus
438 val set_p3_latch : 'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus
440 val get_8051_sfr : 'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte
442 val get_8052_sfr : 'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte
445 'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte -> 'a1 preStatus
448 'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte -> 'a1 preStatus
450 val set_program_counter :
451 'a1 -> 'a1 preStatus -> BitVector.word -> 'a1 preStatus
453 val set_code_memory : 'a1 -> 'a1 preStatus -> 'a2 -> 'a2 preStatus
455 val set_low_internal_ram :
456 'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
459 val update_low_internal_ram :
460 'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
463 val set_high_internal_ram :
464 'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
467 val update_high_internal_ram :
468 'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
471 val set_external_ram :
472 'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
475 val update_external_ram :
476 'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
479 val get_psw_flags : 'a1 -> 'a1 preStatus -> Nat.nat -> Bool.bool
481 val get_cy_flag : 'a1 -> 'a1 preStatus -> Bool.bool
483 val get_ac_flag : 'a1 -> 'a1 preStatus -> Bool.bool
485 val get_fo_flag : 'a1 -> 'a1 preStatus -> Bool.bool
487 val get_rs1_flag : 'a1 -> 'a1 preStatus -> Bool.bool
489 val get_rs0_flag : 'a1 -> 'a1 preStatus -> Bool.bool
491 val get_ov_flag : 'a1 -> 'a1 preStatus -> Bool.bool
493 val get_ud_flag : 'a1 -> 'a1 preStatus -> Bool.bool
495 val get_p_flag : 'a1 -> 'a1 preStatus -> Bool.bool
498 'a1 -> 'a1 preStatus -> BitVector.bit -> BitVector.bit Types.option ->
499 BitVector.bit -> 'a1 preStatus
501 val initialise_status : 'a1 -> 'a1 preStatus
503 val sfr_of_Byte : BitVector.byte -> (sFR8051, sFR8052) Types.sum Types.option
505 val get_bit_addressable_sfr :
506 'a1 -> 'a1 preStatus -> BitVector.byte -> Bool.bool -> BitVector.byte
508 val set_bit_addressable_sfr :
509 'a1 -> 'a1 preStatus -> BitVector.byte -> BitVector.byte -> 'a1 preStatus
511 val bit_address_of_register :
512 'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.bitVector
515 'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte
518 'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
521 val read_from_external_ram :
522 'a1 -> 'a1 preStatus -> BitVector.word -> BitVector.byte
524 val read_from_internal_ram :
525 'a1 -> 'a1 preStatus -> BitVector.byte -> BitVector.byte
527 val read_at_stack_pointer : 'a1 -> 'a1 preStatus -> BitVector.byte
529 val write_at_stack_pointer :
530 'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus
533 'a1 -> 'a1 preStatus -> BitVector.word -> ASM.subaddressing_mode -> 'a1
537 'a1 -> 'a1 preStatus -> BitVector.word -> ASM.subaddressing_mode -> 'a1
541 'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.word
544 'a1 -> 'a1 preStatus -> Bool.bool -> ASM.subaddressing_mode ->
548 'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.byte -> 'a1
552 'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> Bool.bool -> Bool.bool
555 'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.bit -> 'a1
558 val construct_datalabels :
559 (ASM.identifier, BitVector.word) Types.prod List.list -> BitVector.word
560 Identifiers.identifier_map