2 Mk_alu_HC05 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool
6 (function f -> (function a ->
8 Mk_alu_HC05(b,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7) -> (f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7))
13 (function f -> (function a ->
15 Mk_alu_HC05(b,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7) -> (f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7))
19 let acc_low_reg_HC05 =
22 Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> acc_low_reg_HC05)
26 let indX_low_reg_HC05 =
29 Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> indX_low_reg_HC05)
36 Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> sp_reg_HC05)
43 Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> sp_mask_HC05)
50 Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> sp_fix_HC05)
57 Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> pc_reg_HC05)
64 Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> pc_mask_HC05)
71 Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> h_flag_HC05)
78 Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> i_flag_HC05)
85 Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> n_flag_HC05)
92 Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> z_flag_HC05)
99 Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> c_flag_HC05)
106 Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> irq_flag_HC05)
111 Mk_alu_HC08 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool
115 (function f -> (function a ->
117 Mk_alu_HC08(b,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9) -> (f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9))
122 (function f -> (function a ->
124 Mk_alu_HC08(b,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9) -> (f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9))
128 let acc_low_reg_HC08 =
131 Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> acc_low_reg_HC08)
135 let indX_low_reg_HC08 =
138 Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> indX_low_reg_HC08)
142 let indX_high_reg_HC08 =
145 Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> indX_high_reg_HC08)
152 Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> sp_reg_HC08)
159 Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> pc_reg_HC08)
166 Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> v_flag_HC08)
173 Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> h_flag_HC08)
180 Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> i_flag_HC08)
187 Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> n_flag_HC08)
194 Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> z_flag_HC08)
201 Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> c_flag_HC08)
208 Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> irq_flag_HC08)
213 Mk_alu_RS08 of Matita_freescale_byte8.byte8 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool
217 (function f -> (function a ->
219 Mk_alu_RS08(b,w,w1,w2,b1,b2,b3,b4) -> (f b w w1 w2 b1 b2 b3 b4))
224 (function f -> (function a ->
226 Mk_alu_RS08(b,w,w1,w2,b1,b2,b3,b4) -> (f b w w1 w2 b1 b2 b3 b4))
230 let acc_low_reg_RS08 =
233 Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> acc_low_reg_RS08)
240 Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> pc_reg_RS08)
247 Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> pc_mask_RS08)
254 Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> spc_reg_RS08)
261 Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> x_map_RS08)
268 Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> ps_map_RS08)
275 Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> z_flag_RS08)
282 Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> c_flag_RS08)
287 Mk_any_status of unit (* TOO POLYMORPHIC TYPE *) * Matita_freescale_memory_abs.aux_mem_type * Matita_freescale_memory_abs.aux_chk_type * ((Matita_freescale_byte8.byte8,Matita_freescale_opcode.any_opcode,Matita_freescale_opcode.instr_mode,Matita_freescale_byte8.byte8,Matita_freescale_word16.word16) Matita_freescale_extra.prod5T) Matita_datatypes_constructors.option
291 (function m -> (function m1 -> (function f -> (function a ->
293 Mk_any_status(x,a1,a2,o) -> (f x a1 a2 o))
297 let any_status_rect =
298 (function m -> (function m1 -> (function f -> (function a ->
300 Mk_any_status(x,a1,a2,o) -> (f x a1 a2 o))
305 (function mcu -> (function t -> (function w ->
307 Mk_any_status(alu,mem_desc,chk_desc,clk_desc) -> alu)
312 (function mcu -> (function t -> (function w ->
314 Mk_any_status(alu,mem_desc,chk_desc,clk_desc) -> mem_desc)
319 (function mcu -> (function t -> (function w ->
321 Mk_any_status(alu,mem_desc,chk_desc,clk_desc) -> chk_desc)
326 (function mcu -> (function t -> (function w ->
328 Mk_any_status(alu,mem_desc,chk_desc,clk_desc) -> clk_desc)
332 type ('x) aux_get_typing = (unit (* TOO POLYMORPHIC TYPE *) -> 'x)
335 let get_acc_8_low_reg =
336 (function m -> (function t -> (function s -> (
338 Matita_freescale_opcode.HC05 -> Obj.magic (acc_low_reg_HC05)
339 | Matita_freescale_opcode.HC08 -> Obj.magic (acc_low_reg_HC08)
340 | Matita_freescale_opcode.HCS08 -> Obj.magic (acc_low_reg_HC08)
341 | Matita_freescale_opcode.RS08 -> Obj.magic (acc_low_reg_RS08))
345 let get_indX_8_low_reg =
346 (function m -> (function t -> (function s -> (
348 Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((indX_low_reg_HC05 alu)))))
349 | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((indX_low_reg_HC08 alu)))))
350 | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((indX_low_reg_HC08 alu)))))
351 | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
355 let get_indX_8_high_reg =
356 (function m -> (function t -> (function s -> (
358 Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
359 | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((indX_high_reg_HC08 alu)))))
360 | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((indX_high_reg_HC08 alu)))))
361 | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
365 let get_indX_16_reg =
366 (function m -> (function t -> (function s -> (
368 Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
369 | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((Matita_freescale_word16.Mk_word16((indX_high_reg_HC08 alu),(indX_low_reg_HC08 alu)))))))
370 | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((Matita_freescale_word16.Mk_word16((indX_high_reg_HC08 alu),(indX_low_reg_HC08 alu)))))))
371 | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
376 (function m -> (function t -> (function s -> (
378 Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((sp_reg_HC05 alu)))))
379 | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((sp_reg_HC08 alu)))))
380 | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((sp_reg_HC08 alu)))))
381 | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
386 (function m -> (function t -> (function s -> (
388 Matita_freescale_opcode.HC05 -> Obj.magic (pc_reg_HC05)
389 | Matita_freescale_opcode.HC08 -> Obj.magic (pc_reg_HC08)
390 | Matita_freescale_opcode.HCS08 -> Obj.magic (pc_reg_HC08)
391 | Matita_freescale_opcode.RS08 -> Obj.magic (pc_reg_RS08))
396 (function m -> (function t -> (function s -> (
398 Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
399 | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
400 | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
401 | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((spc_reg_RS08 alu))))))
406 (function m -> (function t -> (function s -> (
408 Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
409 | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
410 | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
411 | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((x_map_RS08 alu))))))
416 (function m -> (function t -> (function s -> (
418 Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
419 | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
420 | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
421 | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((ps_map_RS08 alu))))))
426 (function m -> (function t -> (function s -> (
428 Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
429 | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((v_flag_HC08 alu)))))
430 | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((v_flag_HC08 alu)))))
431 | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
436 (function m -> (function t -> (function s -> (
438 Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((h_flag_HC05 alu)))))
439 | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((h_flag_HC08 alu)))))
440 | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((h_flag_HC08 alu)))))
441 | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
446 (function m -> (function t -> (function s -> (
448 Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((i_flag_HC05 alu)))))
449 | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((i_flag_HC08 alu)))))
450 | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((i_flag_HC08 alu)))))
451 | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
456 (function m -> (function t -> (function s -> (
458 Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((n_flag_HC05 alu)))))
459 | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((n_flag_HC08 alu)))))
460 | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((n_flag_HC08 alu)))))
461 | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
466 (function m -> (function t -> (function s -> (
468 Matita_freescale_opcode.HC05 -> Obj.magic (z_flag_HC05)
469 | Matita_freescale_opcode.HC08 -> Obj.magic (z_flag_HC08)
470 | Matita_freescale_opcode.HCS08 -> Obj.magic (z_flag_HC08)
471 | Matita_freescale_opcode.RS08 -> Obj.magic (z_flag_RS08))
476 (function m -> (function t -> (function s -> (
478 Matita_freescale_opcode.HC05 -> Obj.magic (c_flag_HC05)
479 | Matita_freescale_opcode.HC08 -> Obj.magic (c_flag_HC08)
480 | Matita_freescale_opcode.HCS08 -> Obj.magic (c_flag_HC08)
481 | Matita_freescale_opcode.RS08 -> Obj.magic (c_flag_RS08))
486 (function m -> (function t -> (function s -> (
488 Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((irq_flag_HC05 alu)))))
489 | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((irq_flag_HC08 alu)))))
490 | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((irq_flag_HC08 alu)))))
491 | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
496 (function m -> (function t -> (function s -> (alu m t s))))
500 (function m -> (function t -> (function s -> (mem_desc m t s))))
504 (function m -> (function t -> (function s -> (chk_desc m t s))))
508 (function m -> (function t -> (function s -> (clk_desc m t s))))
511 type ('x) aux_set_typing = (unit (* TOO POLYMORPHIC TYPE *) -> ('x -> unit (* TOO POLYMORPHIC TYPE *)))
514 type ('x) aux_set_typing_opt = ((unit (* TOO POLYMORPHIC TYPE *) -> ('x -> unit (* TOO POLYMORPHIC TYPE *)))) Matita_datatypes_constructors.option
518 (function m -> (function t -> (function s -> (function alu' ->
520 Mk_any_status(_,mem,chk,clk) -> (Mk_any_status(alu',mem,chk,clk)))
525 (function m -> (function t -> (function s -> (function mem' ->
527 Mk_any_status(alu,_,chk,clk) -> (Mk_any_status(alu,mem',chk,clk)))
532 (function m -> (function t -> (function s -> (function chk' ->
534 Mk_any_status(alu,mem,_,clk) -> (Mk_any_status(alu,mem,chk',clk)))
539 (function m -> (function t -> (function s -> (function clk' ->
541 Mk_any_status(alu,mem,chk,_) -> (Mk_any_status(alu,mem,chk,clk')))
545 let set_acc_8_low_reg_HC05 =
546 (function alu -> (function acclow' ->
548 Mk_alu_HC05(_,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow',indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl)))
552 let set_acc_8_low_reg_HC08 =
553 (function alu -> (function acclow' ->
555 Mk_alu_HC08(_,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow',indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
559 let set_acc_8_low_reg_RS08 =
560 (function alu -> (function acclow' ->
562 Mk_alu_RS08(_,pc,pcm,spc,xm,psm,zfl,cfl) -> (Mk_alu_RS08(acclow',pc,pcm,spc,xm,psm,zfl,cfl)))
566 let set_acc_8_low_reg =
567 (function m -> (function t -> (function s -> (function acclow' -> (set_alu m t s (
569 Matita_freescale_opcode.HC05 -> Obj.magic (set_acc_8_low_reg_HC05)
570 | Matita_freescale_opcode.HC08 -> Obj.magic (set_acc_8_low_reg_HC08)
571 | Matita_freescale_opcode.HCS08 -> Obj.magic (set_acc_8_low_reg_HC08)
572 | Matita_freescale_opcode.RS08 -> Obj.magic (set_acc_8_low_reg_RS08))
573 (alu m t s) acclow'))))))
576 let set_indX_8_low_reg_HC05 =
577 (function alu -> (function indxlow' ->
579 Mk_alu_HC05(acclow,_,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow',sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl)))
583 let set_indX_8_low_reg_HC08 =
584 (function alu -> (function indxlow' ->
586 Mk_alu_HC08(acclow,_,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow',indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
590 let set_indX_8_low_reg =
591 (function m -> (function t -> (function s -> (function indxlow' -> (Matita_freescale_extra.opt_map
593 Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_8_low_reg_HC05)))
594 | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_8_low_reg_HC08)))
595 | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_8_low_reg_HC08)))
596 | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
597 (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) indxlow'))))))))))
600 let setweak_indX_8_low_reg =
601 (function m -> (function t -> (function s -> (function indxlow' ->
602 (match (set_indX_8_low_reg m t s indxlow') with
603 Matita_datatypes_constructors.None -> s
604 | Matita_datatypes_constructors.Some(s') -> s')
608 let set_indX_8_high_reg_HC08 =
609 (function alu -> (function indxhigh' ->
611 Mk_alu_HC08(acclow,indxlow,_,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh',sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
615 let set_indX_8_high_reg =
616 (function m -> (function t -> (function s -> (function indxhigh' -> (Matita_freescale_extra.opt_map
618 Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
619 | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_8_high_reg_HC08)))
620 | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_8_high_reg_HC08)))
621 | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
622 (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) indxhigh'))))))))))
625 let setweak_indX_8_high_reg =
626 (function m -> (function t -> (function s -> (function indxhigh' ->
627 (match (set_indX_8_high_reg m t s indxhigh') with
628 Matita_datatypes_constructors.None -> s
629 | Matita_datatypes_constructors.Some(s') -> s')
633 let set_indX_16_reg_HC08 =
634 (function alu -> (function indx16 ->
636 Mk_alu_HC08(acclow,_,_,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,(Matita_freescale_word16.w16l indx16),(Matita_freescale_word16.w16h indx16),sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
640 let set_indX_16_reg =
641 (function m -> (function t -> (function s -> (function indx16 -> (Matita_freescale_extra.opt_map
643 Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
644 | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_16_reg_HC08)))
645 | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_16_reg_HC08)))
646 | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
647 (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) indx16))))))))))
650 let setweak_indX_16_reg =
651 (function m -> (function t -> (function s -> (function indx16 ->
652 (match (set_indX_16_reg m t s indx16) with
653 Matita_datatypes_constructors.None -> s
654 | Matita_datatypes_constructors.Some(s') -> s')
658 let set_sp_reg_HC05 =
659 (function alu -> (function sp' ->
661 Mk_alu_HC05(acclow,indxlow,_,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,(Matita_freescale_word16.or_w16 (Matita_freescale_word16.and_w16 sp' spm) spf),spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl)))
665 let set_sp_reg_HC08 =
666 (function alu -> (function sp' ->
668 Mk_alu_HC08(acclow,indxlow,indxhigh,_,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp',pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
673 (function m -> (function t -> (function s -> (function sp' -> (Matita_freescale_extra.opt_map
675 Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_sp_reg_HC05)))
676 | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_sp_reg_HC08)))
677 | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_sp_reg_HC08)))
678 | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
679 (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) sp'))))))))))
683 (function m -> (function t -> (function s -> (function sp' ->
684 (match (set_sp_reg m t s sp') with
685 Matita_datatypes_constructors.None -> s
686 | Matita_datatypes_constructors.Some(s') -> s')
690 let set_pc_reg_HC05 =
691 (function alu -> (function pc' ->
693 Mk_alu_HC05(acclow,indxlow,sp,spm,spf,_,pcm,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,(Matita_freescale_word16.and_w16 pc' pcm),pcm,hfl,ifl,nfl,zfl,cfl,irqfl)))
697 let set_pc_reg_HC08 =
698 (function alu -> (function pc' ->
700 Mk_alu_HC08(acclow,indxlow,indxhigh,sp,_,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc',vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
704 let set_pc_reg_RS08 =
705 (function alu -> (function pc' ->
707 Mk_alu_RS08(acclow,_,pcm,spc,xm,psm,zfl,cfl) -> (Mk_alu_RS08(acclow,(Matita_freescale_word16.and_w16 pc' pcm),pcm,spc,xm,psm,zfl,cfl)))
712 (function m -> (function t -> (function s -> (function pc' -> (set_alu m t s (
714 Matita_freescale_opcode.HC05 -> Obj.magic (set_pc_reg_HC05)
715 | Matita_freescale_opcode.HC08 -> Obj.magic (set_pc_reg_HC08)
716 | Matita_freescale_opcode.HCS08 -> Obj.magic (set_pc_reg_HC08)
717 | Matita_freescale_opcode.RS08 -> Obj.magic (set_pc_reg_RS08))
718 (alu m t s) pc'))))))
721 let set_spc_reg_RS08 =
722 (function alu -> (function spc' ->
724 Mk_alu_RS08(acclow,pc,pcm,_,xm,psm,zfl,cfl) -> (Mk_alu_RS08(acclow,pc,pcm,(Matita_freescale_word16.and_w16 spc' pcm),xm,psm,zfl,cfl)))
729 (function m -> (function t -> (function s -> (function spc' -> (Matita_freescale_extra.opt_map
731 Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
732 | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.None))
733 | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.None))
734 | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_spc_reg_RS08))))
735 (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) spc'))))))))))
738 let setweak_spc_reg =
739 (function m -> (function t -> (function s -> (function spc' ->
740 (match (set_spc_reg m t s spc') with
741 Matita_datatypes_constructors.None -> s
742 | Matita_datatypes_constructors.Some(s') -> s')
747 (function alu -> (function xm' ->
749 Mk_alu_RS08(acclow,pc,pcm,spc,_,psm,zfl,cfl) -> (Mk_alu_RS08(acclow,pc,pcm,spc,xm',psm,zfl,cfl)))
754 (function m -> (function t -> (function s -> (function xm' -> (Matita_freescale_extra.opt_map
756 Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
757 | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.None))
758 | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.None))
759 | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_x_map_RS08))))
760 (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) xm'))))))))))
764 (function m -> (function t -> (function s -> (function xm' ->
765 (match (set_x_map m t s xm') with
766 Matita_datatypes_constructors.None -> s
767 | Matita_datatypes_constructors.Some(s') -> s')
771 let set_ps_map_RS08 =
772 (function alu -> (function psm' ->
774 Mk_alu_RS08(acclow,pc,pcm,spc,xm,_,zfl,cfl) -> (Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm',zfl,cfl)))
779 (function m -> (function t -> (function s -> (function psm' -> (Matita_freescale_extra.opt_map
781 Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
782 | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.None))
783 | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.None))
784 | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_ps_map_RS08))))
785 (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) psm'))))))))))
789 (function m -> (function t -> (function s -> (function psm' ->
790 (match (set_ps_map m t s psm') with
791 Matita_datatypes_constructors.None -> s
792 | Matita_datatypes_constructors.Some(s') -> s')
796 let set_v_flag_HC08 =
797 (function alu -> (function vfl' ->
799 Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,_,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl',hfl,ifl,nfl,zfl,cfl,irqfl)))
804 (function m -> (function t -> (function s -> (function vfl' -> (Matita_freescale_extra.opt_map
806 Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
807 | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_v_flag_HC08)))
808 | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_v_flag_HC08)))
809 | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
810 (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) vfl'))))))))))
814 (function m -> (function t -> (function s -> (function vfl' ->
815 (match (set_v_flag m t s vfl') with
816 Matita_datatypes_constructors.None -> s
817 | Matita_datatypes_constructors.Some(s') -> s')
821 let set_h_flag_HC05 =
822 (function alu -> (function hfl' ->
824 Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,_,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl',ifl,nfl,zfl,cfl,irqfl)))
828 let set_h_flag_HC08 =
829 (function alu -> (function hfl' ->
831 Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,_,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl',ifl,nfl,zfl,cfl,irqfl)))
836 (function m -> (function t -> (function s -> (function hfl' -> (Matita_freescale_extra.opt_map
838 Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_h_flag_HC05)))
839 | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_h_flag_HC08)))
840 | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_h_flag_HC08)))
841 | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
842 (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) hfl'))))))))))
846 (function m -> (function t -> (function s -> (function hfl' ->
847 (match (set_h_flag m t s hfl') with
848 Matita_datatypes_constructors.None -> s
849 | Matita_datatypes_constructors.Some(s') -> s')
853 let set_i_flag_HC05 =
854 (function alu -> (function ifl' ->
856 Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,_,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl',nfl,zfl,cfl,irqfl)))
860 let set_i_flag_HC08 =
861 (function alu -> (function ifl' ->
863 Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,_,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl',nfl,zfl,cfl,irqfl)))
868 (function m -> (function t -> (function s -> (function ifl' -> (Matita_freescale_extra.opt_map
870 Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_i_flag_HC05)))
871 | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_i_flag_HC08)))
872 | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_i_flag_HC08)))
873 | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
874 (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) ifl'))))))))))
878 (function m -> (function t -> (function s -> (function ifl' ->
879 (match (set_i_flag m t s ifl') with
880 Matita_datatypes_constructors.None -> s
881 | Matita_datatypes_constructors.Some(s') -> s')
885 let set_n_flag_HC05 =
886 (function alu -> (function nfl' ->
888 Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,_,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl',zfl,cfl,irqfl)))
892 let set_n_flag_HC08 =
893 (function alu -> (function nfl' ->
895 Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,_,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl',zfl,cfl,irqfl)))
900 (function m -> (function t -> (function s -> (function nfl' -> (Matita_freescale_extra.opt_map
902 Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_n_flag_HC05)))
903 | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_n_flag_HC08)))
904 | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_n_flag_HC08)))
905 | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
906 (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) nfl'))))))))))
910 (function m -> (function t -> (function s -> (function nfl' ->
911 (match (set_n_flag m t s nfl') with
912 Matita_datatypes_constructors.None -> s
913 | Matita_datatypes_constructors.Some(s') -> s')
917 let set_z_flag_HC05 =
918 (function alu -> (function zfl' ->
920 Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,_,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl',cfl,irqfl)))
924 let set_z_flag_HC08 =
925 (function alu -> (function zfl' ->
927 Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,_,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl',cfl,irqfl)))
931 let set_z_flag_RS08 =
932 (function alu -> (function zfl' ->
934 Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,_,cfl) -> (Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl',cfl)))
939 (function m -> (function t -> (function s -> (function zfl' -> (set_alu m t s (
941 Matita_freescale_opcode.HC05 -> Obj.magic (set_z_flag_HC05)
942 | Matita_freescale_opcode.HC08 -> Obj.magic (set_z_flag_HC08)
943 | Matita_freescale_opcode.HCS08 -> Obj.magic (set_z_flag_HC08)
944 | Matita_freescale_opcode.RS08 -> Obj.magic (set_z_flag_RS08))
945 (alu m t s) zfl'))))))
948 let set_c_flag_HC05 =
949 (function alu -> (function cfl' ->
951 Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,_,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl',irqfl)))
955 let set_c_flag_HC08 =
956 (function alu -> (function cfl' ->
958 Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,_,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl',irqfl)))
962 let set_c_flag_RS08 =
963 (function alu -> (function cfl' ->
965 Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl,_) -> (Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl,cfl')))
970 (function m -> (function t -> (function s -> (function cfl' -> (set_alu m t s (
972 Matita_freescale_opcode.HC05 -> Obj.magic (set_c_flag_HC05)
973 | Matita_freescale_opcode.HC08 -> Obj.magic (set_c_flag_HC08)
974 | Matita_freescale_opcode.HCS08 -> Obj.magic (set_c_flag_HC08)
975 | Matita_freescale_opcode.RS08 -> Obj.magic (set_c_flag_RS08))
976 (alu m t s) cfl'))))))
979 let set_irq_flag_HC05 =
980 (function alu -> (function irqfl' ->
982 Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,_) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl')))
986 let set_irq_flag_HC08 =
987 (function alu -> (function irqfl' ->
989 Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,_) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl')))
994 (function m -> (function t -> (function s -> (function irqfl' -> (Matita_freescale_extra.opt_map
996 Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_irq_flag_HC05)))
997 | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_irq_flag_HC08)))
998 | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_irq_flag_HC08)))
999 | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
1000 (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) irqfl'))))))))))
1003 let setweak_irq_flag =
1004 (function m -> (function t -> (function s -> (function irqfl' ->
1005 (match (set_irq_flag m t s irqfl') with
1006 Matita_datatypes_constructors.None -> s
1007 | Matita_datatypes_constructors.Some(s') -> s')
1012 (function alu1 -> (function alu2 ->
1014 Mk_alu_HC05(acclow1,indxlow1,sp1,spm1,spf1,pc1,pcm1,hfl1,ifl1,nfl1,zfl1,cfl1,irqfl1) ->
1016 Mk_alu_HC05(acclow2,indxlow2,sp2,spm2,spf2,pc2,pcm2,hfl2,ifl2,nfl2,zfl2,cfl2,irqfl2) -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_byte8.eq_b8 acclow1 acclow2) (Matita_freescale_byte8.eq_b8 indxlow1 indxlow2)) (Matita_freescale_word16.eq_w16 sp1 sp2)) (Matita_freescale_word16.eq_w16 spm1 spm2)) (Matita_freescale_word16.eq_w16 spf1 spf2)) (Matita_freescale_word16.eq_w16 pc1 pc2)) (Matita_freescale_word16.eq_w16 pcm1 pcm2)) (Matita_freescale_extra.eq_bool hfl1 hfl2)) (Matita_freescale_extra.eq_bool ifl1 ifl2)) (Matita_freescale_extra.eq_bool nfl1 nfl2)) (Matita_freescale_extra.eq_bool zfl1 zfl2)) (Matita_freescale_extra.eq_bool cfl1 cfl2)) (Matita_freescale_extra.eq_bool irqfl1 irqfl2)))
1022 (function alu1 -> (function alu2 ->
1024 Mk_alu_HC08(acclow1,indxlow1,indxhigh1,sp1,pc1,vfl1,hfl1,ifl1,nfl1,zfl1,cfl1,irqfl1) ->
1026 Mk_alu_HC08(acclow2,indxlow2,indxhigh2,sp2,pc2,vfl2,hfl2,ifl2,nfl2,zfl2,cfl2,irqfl2) -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_byte8.eq_b8 acclow1 acclow2) (Matita_freescale_byte8.eq_b8 indxlow1 indxlow2)) (Matita_freescale_byte8.eq_b8 indxhigh1 indxhigh2)) (Matita_freescale_word16.eq_w16 sp1 sp2)) (Matita_freescale_word16.eq_w16 pc1 pc2)) (Matita_freescale_extra.eq_bool vfl1 vfl2)) (Matita_freescale_extra.eq_bool hfl1 hfl2)) (Matita_freescale_extra.eq_bool ifl1 ifl2)) (Matita_freescale_extra.eq_bool nfl1 nfl2)) (Matita_freescale_extra.eq_bool zfl1 zfl2)) (Matita_freescale_extra.eq_bool cfl1 cfl2)) (Matita_freescale_extra.eq_bool irqfl1 irqfl2)))
1032 (function alu1 -> (function alu2 ->
1034 Mk_alu_RS08(acclow1,pc1,pcm1,spc1,xm1,psm1,zfl1,cfl1) ->
1036 Mk_alu_RS08(acclow2,pc2,pcm2,spc2,xm2,psm2,zfl2,cfl2) -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_byte8.eq_b8 acclow1 acclow2) (Matita_freescale_word16.eq_w16 pc1 pc2)) (Matita_freescale_word16.eq_w16 pcm1 pcm2)) (Matita_freescale_word16.eq_w16 spc1 spc2)) (Matita_freescale_byte8.eq_b8 xm1 xm2)) (Matita_freescale_byte8.eq_b8 psm1 psm2)) (Matita_freescale_extra.eq_bool zfl1 zfl2)) (Matita_freescale_extra.eq_bool cfl1 cfl2)))
1042 (function b1 -> (function b2 ->
1044 Matita_datatypes_constructors.None ->
1046 Matita_datatypes_constructors.None -> Matita_datatypes_bool.True
1047 | Matita_datatypes_constructors.Some(_) -> Matita_datatypes_bool.False)
1049 | Matita_datatypes_constructors.Some(b1') ->
1051 Matita_datatypes_constructors.None -> Matita_datatypes_bool.False
1052 | Matita_datatypes_constructors.Some(b2') -> (Matita_freescale_byte8.eq_b8 b1' b2'))
1057 let forall_memory_ranged =
1058 let rec forall_memory_ranged =
1059 (function t -> (function chk1 -> (function chk2 -> (function mem1 -> (function mem2 -> (function inf -> (function n ->
1061 Matita_nat_nat.O -> (eq_b8_opt (Matita_freescale_memory_abs.mem_read t mem1 chk1 inf) (Matita_freescale_memory_abs.mem_read t mem2 chk2 inf))
1062 | Matita_nat_nat.S(n') -> (Matita_freescale_extra.and_bool (eq_b8_opt (Matita_freescale_memory_abs.mem_read t mem1 chk1 (Matita_freescale_word16.plus_w16nc inf (Matita_freescale_word16.word16_of_nat n))) (Matita_freescale_memory_abs.mem_read t mem2 chk2 (Matita_freescale_word16.plus_w16nc inf (Matita_freescale_word16.word16_of_nat n)))) (forall_memory_ranged t chk1 chk2 mem1 mem2 inf n')))
1063 ))))))) in forall_memory_ranged
1067 (function m -> (function c1 -> (function c2 ->
1069 Matita_datatypes_constructors.None ->
1071 Matita_datatypes_constructors.None -> Matita_datatypes_bool.True
1072 | Matita_datatypes_constructors.Some(_) -> Matita_datatypes_bool.False)
1074 | Matita_datatypes_constructors.Some(c1') ->
1076 Matita_datatypes_constructors.None -> Matita_datatypes_bool.False
1077 | Matita_datatypes_constructors.Some(c2') -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_byte8.eq_b8 (Matita_freescale_extra.fst5T c1') (Matita_freescale_extra.fst5T c2')) (Matita_freescale_opcode.eqop m (Matita_freescale_extra.snd5T c1') (Matita_freescale_extra.snd5T c2'))) (Matita_freescale_opcode.eqim (Matita_freescale_extra.thd5T c1') (Matita_freescale_extra.thd5T c2'))) (Matita_freescale_byte8.eq_b8 (Matita_freescale_extra.frth5T c1') (Matita_freescale_extra.frth5T c2'))) (Matita_freescale_word16.eq_w16 (Matita_freescale_extra.ffth5T c1') (Matita_freescale_extra.ffth5T c2'))))
1083 (function m -> (function t -> (function s1 -> (function s2 -> (function inf -> (function n ->
1085 Mk_any_status(alu1,mem1,chk1,clk1) ->
1087 Mk_any_status(alu2,mem2,chk2,clk2) -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (
1089 Matita_freescale_opcode.HC05 -> Obj.magic (eq_alu_HC05)
1090 | Matita_freescale_opcode.HC08 -> Obj.magic (eq_alu_HC08)
1091 | Matita_freescale_opcode.HCS08 -> Obj.magic (eq_alu_HC08)
1092 | Matita_freescale_opcode.RS08 -> Obj.magic (eq_alu_RS08))
1093 alu1 alu2) (forall_memory_ranged t chk1 chk2 mem1 mem2 inf n)) (eq_clk m clk1 clk2)))