X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_freescale_model.ml;fp=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_freescale_model.ml;h=2c3359bcedaa9508ffbfecdec66eee07a3fb1e92;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_model.ml b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_model.ml new file mode 100644 index 000000000..2c3359bce --- /dev/null +++ b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_model.ml @@ -0,0 +1,347 @@ +type hC05_mcu_model = +MC68HC05J5A +;; + +let hC05_mcu_model_rec = +(function p -> (function h -> +(match h with + MC68HC05J5A -> p) +)) +;; + +let hC05_mcu_model_rect = +(function p -> (function h -> +(match h with + MC68HC05J5A -> p) +)) +;; + +type hC08_mcu_model = +MC68HC08AB16A +;; + +let hC08_mcu_model_rec = +(function p -> (function h -> +(match h with + MC68HC08AB16A -> p) +)) +;; + +let hC08_mcu_model_rect = +(function p -> (function h -> +(match h with + MC68HC08AB16A -> p) +)) +;; + +type hCS08_mcu_model = +MC9S08AW60 + | MC9S08GB60 + | MC9S08GT60 + | MC9S08GB32 + | MC9S08GT32 + | MC9S08GT16 + | MC9S08GB60A + | MC9S08GT60A + | MC9S08GB32A + | MC9S08GT32A + | MC9S08GT16A + | MC9S08GT8A + | MC9S08LC60 + | MC9S08LC36 + | MC9S08QD4 + | MC9S08QD2 + | MC9S08QG8 + | MC9S08QG4 + | MC9S08RC60 + | MC9S08RD60 + | MC9S08RE60 + | MC9S08RG60 + | MC9S08RC32 + | MC9S08RD32 + | MC9S08RE32 + | MC9S08RG32 + | MC9S08RC16 + | MC9S08RD16 + | MC9S08RE16 + | MC9S08RC8 + | MC9S08RD8 + | MC9S08RE8 +;; + +let hCS08_mcu_model_rec = +(function p -> (function p1 -> (function p2 -> (function p3 -> (function p4 -> (function p5 -> (function p6 -> (function p7 -> (function p8 -> (function p9 -> (function p10 -> (function p11 -> (function p12 -> (function p13 -> (function p14 -> (function p15 -> (function p16 -> (function p17 -> (function p18 -> (function p19 -> (function p20 -> (function p21 -> (function p22 -> (function p23 -> (function p24 -> (function p25 -> (function p26 -> (function p27 -> (function p28 -> (function p29 -> (function p30 -> (function p31 -> (function h -> +(match h with + MC9S08AW60 -> p + | MC9S08GB60 -> p1 + | MC9S08GT60 -> p2 + | MC9S08GB32 -> p3 + | MC9S08GT32 -> p4 + | MC9S08GT16 -> p5 + | MC9S08GB60A -> p6 + | MC9S08GT60A -> p7 + | MC9S08GB32A -> p8 + | MC9S08GT32A -> p9 + | MC9S08GT16A -> p10 + | MC9S08GT8A -> p11 + | MC9S08LC60 -> p12 + | MC9S08LC36 -> p13 + | MC9S08QD4 -> p14 + | MC9S08QD2 -> p15 + | MC9S08QG8 -> p16 + | MC9S08QG4 -> p17 + | MC9S08RC60 -> p18 + | MC9S08RD60 -> p19 + | MC9S08RE60 -> p20 + | MC9S08RG60 -> p21 + | MC9S08RC32 -> p22 + | MC9S08RD32 -> p23 + | MC9S08RE32 -> p24 + | MC9S08RG32 -> p25 + | MC9S08RC16 -> p26 + | MC9S08RD16 -> p27 + | MC9S08RE16 -> p28 + | MC9S08RC8 -> p29 + | MC9S08RD8 -> p30 + | MC9S08RE8 -> p31) +))))))))))))))))))))))))))))))))) +;; + +let hCS08_mcu_model_rect = +(function p -> (function p1 -> (function p2 -> (function p3 -> (function p4 -> (function p5 -> (function p6 -> (function p7 -> (function p8 -> (function p9 -> (function p10 -> (function p11 -> (function p12 -> (function p13 -> (function p14 -> (function p15 -> (function p16 -> (function p17 -> (function p18 -> (function p19 -> (function p20 -> (function p21 -> (function p22 -> (function p23 -> (function p24 -> (function p25 -> (function p26 -> (function p27 -> (function p28 -> (function p29 -> (function p30 -> (function p31 -> (function h -> +(match h with + MC9S08AW60 -> p + | MC9S08GB60 -> p1 + | MC9S08GT60 -> p2 + | MC9S08GB32 -> p3 + | MC9S08GT32 -> p4 + | MC9S08GT16 -> p5 + | MC9S08GB60A -> p6 + | MC9S08GT60A -> p7 + | MC9S08GB32A -> p8 + | MC9S08GT32A -> p9 + | MC9S08GT16A -> p10 + | MC9S08GT8A -> p11 + | MC9S08LC60 -> p12 + | MC9S08LC36 -> p13 + | MC9S08QD4 -> p14 + | MC9S08QD2 -> p15 + | MC9S08QG8 -> p16 + | MC9S08QG4 -> p17 + | MC9S08RC60 -> p18 + | MC9S08RD60 -> p19 + | MC9S08RE60 -> p20 + | MC9S08RG60 -> p21 + | MC9S08RC32 -> p22 + | MC9S08RD32 -> p23 + | MC9S08RE32 -> p24 + | MC9S08RG32 -> p25 + | MC9S08RC16 -> p26 + | MC9S08RD16 -> p27 + | MC9S08RE16 -> p28 + | MC9S08RC8 -> p29 + | MC9S08RD8 -> p30 + | MC9S08RE8 -> p31) +))))))))))))))))))))))))))))))))) +;; + +type rS08_mcu_model = +MC9RS08KA1 + | MC9RS08KA2 +;; + +let rS08_mcu_model_rec = +(function p -> (function p1 -> (function r -> +(match r with + MC9RS08KA1 -> p + | MC9RS08KA2 -> p1) +))) +;; + +let rS08_mcu_model_rect = +(function p -> (function p1 -> (function r -> +(match r with + MC9RS08KA1 -> p + | MC9RS08KA2 -> p1) +))) +;; + +type any_mcu_model = +FamilyHC05 of hC05_mcu_model + | FamilyHC08 of hC08_mcu_model + | FamilyHCS08 of hCS08_mcu_model + | FamilyRS08 of rS08_mcu_model +;; + +let any_mcu_model_rec = +(function f -> (function f1 -> (function f2 -> (function f3 -> (function a -> +(match a with + FamilyHC05(h) -> (f h) + | FamilyHC08(h) -> (f1 h) + | FamilyHCS08(h) -> (f2 h) + | FamilyRS08(r) -> (f3 r)) +))))) +;; + +let any_mcu_model_rect = +(function f -> (function f1 -> (function f2 -> (function f3 -> (function a -> +(match a with + FamilyHC05(h) -> (f h) + | FamilyHC08(h) -> (f1 h) + | FamilyHCS08(h) -> (f2 h) + | FamilyRS08(r) -> (f3 r)) +))))) +;; + +let memory_type_of_FamilyHC05 = +(function m -> +(match m with + MC68HC05J5A -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil)))))))) +) +;; + +let memory_type_of_FamilyHC08 = +(function m -> +(match m with + MC68HC08AB16A -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.XE)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XD)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XE)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X2)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil)))))))))))) +) +;; + +let memory_type_of_FamilyHCS08 = +(function m -> +(match m with + MC9S08AW60 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X7)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))))) + | MC9S08GB60 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X7)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XC)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))))) + | MC9S08GT60 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X7)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XC)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))))) + | MC9S08GB32 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08GT32 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08GT16 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08GB60A -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X7)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XC)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))))) + | MC9S08GT60A -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X7)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XC)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))))) + | MC9S08GB32A -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08GT32A -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08GT16A -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08GT8A -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08LC60 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X7)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))))) + | MC9S08LC36 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))))) + | MC9S08QD4 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08QD2 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08QG8 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08QG4 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08RC60 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X5)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X7)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XC)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))))) + | MC9S08RD60 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X5)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X7)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XC)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))))) + | MC9S08RE60 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X5)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X7)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XC)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))))) + | MC9S08RG60 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X5)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X7)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XC)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))))) + | MC9S08RC32 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X5)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08RD32 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X5)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08RE32 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X5)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08RG32 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X5)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08RC16 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08RD16 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08RE16 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08RC8 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08RD8 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))) + | MC9S08RE8 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil)))))) +) +;; + +let memory_type_of_FamilyRS08 = +(function m -> +(match m with + MC9RS08KA1 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XC)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil))))))))))))) + | MC9RS08KA2 -> (Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_WRITE)),(Matita_list_list.Cons((Matita_freescale_extra.TripleT((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))),(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))),Matita_freescale_memory_struct.MEM_READ_ONLY)),(Matita_list_list.Nil)))))))))))))) +) +;; + +let memory_type_of_mcu_version = +(function mcu -> +(match mcu with + FamilyHC05(m) -> (memory_type_of_FamilyHC05 m) + | FamilyHC08(m) -> (memory_type_of_FamilyHC08 m) + | FamilyHCS08(m) -> (memory_type_of_FamilyHCS08 m) + | FamilyRS08(m) -> (memory_type_of_FamilyRS08 m)) +) +;; + +let build_memory_type_of_mcu_version = +(function mcu -> (function t -> (let rec aux = +(function param -> (function result -> +(match param with + Matita_list_list.Nil -> result + | Matita_list_list.Cons(hd,tl) -> (aux tl (Matita_freescale_memory_abs.check_update_ranged t result (Matita_freescale_extra.fst3T hd) (Matita_freescale_extra.snd3T hd) (Matita_freescale_extra.thd3T hd)))) +)) in aux (memory_type_of_mcu_version mcu) (Matita_freescale_memory_abs.out_of_bound_memory t)))) +;; + +let memory_of_mcu_version = +(function mcu -> (function t -> +(match mcu with + FamilyHC05(m) -> +(match m with + MC68HC05J5A -> (Matita_freescale_memory_abs.zero_memory t)) + + | FamilyHC08(m) -> +(match m with + MC68HC08AB16A -> (Matita_freescale_memory_abs.zero_memory t)) + + | FamilyHCS08(_) -> (Matita_freescale_memory_abs.zero_memory t) + | FamilyRS08(_) -> (Matita_freescale_memory_abs.zero_memory t)) +)) +;; + +let mcu_of_model = +(function m -> +(match m with + FamilyHC05(_) -> Matita_freescale_opcode.HC05 + | FamilyHC08(_) -> Matita_freescale_opcode.HC08 + | FamilyHCS08(_) -> Matita_freescale_opcode.HCS08 + | FamilyRS08(_) -> Matita_freescale_opcode.RS08) +) +;; + +let start_of_mcu_version = +(function mcu -> (function t -> (let pc_reset_h = (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XE)))) in (let pc_reset_l = (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))) in (let pc_RS08_reset = (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XD)))) in (let sp_reset = (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))) in +(match mcu with + FamilyHC05(m) -> Obj.magic ((function mem -> (function chk -> (function ndby1 -> (function ndby2 -> (function irqfl -> (function ndbo1 -> (function ndbo2 -> (function ndbo3 -> (function ndbo4 -> (function ndbo5 -> (let build = (function spm -> (function spf -> (function pcm -> (let fetched_pc = (Matita_freescale_word16.Mk_word16((Matita_freescale_memory_abs.mem_read_abs t mem (Matita_freescale_word16.and_w16 pc_reset_h pcm)),(Matita_freescale_memory_abs.mem_read_abs t mem (Matita_freescale_word16.and_w16 pc_reset_l pcm)))) in (Matita_freescale_status.Mk_any_status(Obj.magic((Matita_freescale_status.Mk_alu_HC05(ndby1,ndby2,(Matita_freescale_word16.or_w16 (Matita_freescale_word16.and_w16 sp_reset spm) spf),spm,spf,(Matita_freescale_word16.and_w16 fetched_pc pcm),pcm,ndbo1,Matita_datatypes_bool.True,ndbo2,ndbo3,ndbo4,irqfl))),mem,chk,(Matita_datatypes_constructors.None))))))) in +(match m with + MC68HC05J5A -> (build (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF)))) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X0)))) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))))) +)))))))))))) + | FamilyHC08(m) -> Obj.magic ((function mem -> (function chk -> (function ndby1 -> (function ndby2 -> (function irqfl -> (function ndbo1 -> (function ndbo2 -> (function ndbo3 -> (function ndbo4 -> (function ndbo5 -> (let build = (let fetched_pc = (Matita_freescale_word16.Mk_word16((Matita_freescale_memory_abs.mem_read_abs t mem pc_reset_h),(Matita_freescale_memory_abs.mem_read_abs t mem pc_reset_l))) in (Matita_freescale_status.Mk_any_status(Obj.magic((Matita_freescale_status.Mk_alu_HC08(ndby1,ndby2,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),sp_reset,fetched_pc,ndbo1,ndbo2,Matita_datatypes_bool.True,ndbo3,ndbo4,ndbo5,irqfl))),mem,chk,(Matita_datatypes_constructors.None)))) in build)))))))))))) + | FamilyHCS08(m) -> Obj.magic ((function mem -> (function chk -> (function ndby1 -> (function ndby2 -> (function irqfl -> (function ndbo1 -> (function ndbo2 -> (function ndbo3 -> (function ndbo4 -> (function ndbo5 -> (let build = (let fetched_pc = (Matita_freescale_word16.Mk_word16((Matita_freescale_memory_abs.mem_read_abs t mem pc_reset_h),(Matita_freescale_memory_abs.mem_read_abs t mem pc_reset_l))) in (Matita_freescale_status.Mk_any_status(Obj.magic((Matita_freescale_status.Mk_alu_HC08(ndby1,ndby2,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),sp_reset,fetched_pc,ndbo1,ndbo2,Matita_datatypes_bool.True,ndbo3,ndbo4,ndbo5,irqfl))),mem,chk,(Matita_datatypes_constructors.None)))) in build)))))))))))) + | FamilyRS08(m) -> Obj.magic ((function mem -> (function chk -> (function ndby1 -> (function ndby2 -> (function irqfl -> (function ndbo1 -> (function ndbo2 -> (function ndbo3 -> (function ndbo4 -> (function ndbo5 -> (let build = (function pcm -> (Matita_freescale_status.Mk_any_status(Obj.magic((Matita_freescale_status.Mk_alu_RS08((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_word16.and_w16 pc_RS08_reset pcm),pcm,(Matita_freescale_word16.and_w16 pc_RS08_reset pcm),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)),Matita_datatypes_bool.False,Matita_datatypes_bool.False))),mem,chk,(Matita_datatypes_constructors.None)))) in (build (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))))))))))))))))) +)))))) +;; + +let reset_of_mcu = +(function m -> (function t -> (let pc_reset_h = (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XE)))) in (let pc_reset_l = (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))) in (let pc_RS08_reset = (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XD)))) in (let sp_reset = (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)))) in +(match m with + Matita_freescale_opcode.HC05 -> Obj.magic ((function s -> +(match s with + Matita_freescale_status.Mk_any_status(alu,mem,chk,clk) -> +(match Obj.magic(alu) with + Matita_freescale_status.Mk_alu_HC05(acclow,indxlow,_,spm,spf,_,pcm,hfl,_,nfl,zfl,cfl,irqfl) -> (let fetched_pc = (Matita_freescale_word16.Mk_word16((Matita_freescale_memory_abs.mem_read_abs t mem (Matita_freescale_word16.and_w16 pc_reset_h pcm)),(Matita_freescale_memory_abs.mem_read_abs t mem (Matita_freescale_word16.and_w16 pc_reset_l pcm)))) in (Matita_freescale_status.Mk_any_status(Obj.magic((Matita_freescale_status.Mk_alu_HC05(acclow,indxlow,(Matita_freescale_word16.or_w16 (Matita_freescale_word16.and_w16 sp_reset spm) spf),spm,spf,(Matita_freescale_word16.and_w16 fetched_pc pcm),pcm,hfl,Matita_datatypes_bool.True,nfl,zfl,cfl,irqfl))),mem,chk,(Matita_datatypes_constructors.None))))) +) +)) + | Matita_freescale_opcode.HC08 -> Obj.magic ((function s -> +(match s with + Matita_freescale_status.Mk_any_status(alu,mem,chk,clk) -> +(match Obj.magic(alu) with + Matita_freescale_status.Mk_alu_HC08(acclow,indxlow,_,_,_,vfl,hfl,_,nfl,zfl,cfl,irqfl) -> (let fetched_pc = (Matita_freescale_word16.Mk_word16((Matita_freescale_memory_abs.mem_read_abs t mem pc_reset_h),(Matita_freescale_memory_abs.mem_read_abs t mem pc_reset_l))) in (Matita_freescale_status.Mk_any_status(Obj.magic((Matita_freescale_status.Mk_alu_HC08(acclow,indxlow,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),sp_reset,fetched_pc,vfl,hfl,Matita_datatypes_bool.True,nfl,zfl,cfl,irqfl))),mem,chk,(Matita_datatypes_constructors.None))))) +) +)) + | Matita_freescale_opcode.HCS08 -> Obj.magic ((function s -> +(match s with + Matita_freescale_status.Mk_any_status(alu,mem,chk,clk) -> +(match Obj.magic(alu) with + Matita_freescale_status.Mk_alu_HC08(acclow,indxlow,_,_,_,vfl,hfl,_,nfl,zfl,cfl,irqfl) -> (let fetched_pc = (Matita_freescale_word16.Mk_word16((Matita_freescale_memory_abs.mem_read_abs t mem pc_reset_h),(Matita_freescale_memory_abs.mem_read_abs t mem pc_reset_l))) in (Matita_freescale_status.Mk_any_status(Obj.magic((Matita_freescale_status.Mk_alu_HC08(acclow,indxlow,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),sp_reset,fetched_pc,vfl,hfl,Matita_datatypes_bool.True,nfl,zfl,cfl,irqfl))),mem,chk,(Matita_datatypes_constructors.None))))) +) +)) + | Matita_freescale_opcode.RS08 -> Obj.magic ((function s -> +(match s with + Matita_freescale_status.Mk_any_status(alu,mem,chk,clk) -> +(match Obj.magic(alu) with + Matita_freescale_status.Mk_alu_RS08(_,_,pcm,_,_,_,_,_) -> (Matita_freescale_status.Mk_any_status(Obj.magic((Matita_freescale_status.Mk_alu_RS08((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_word16.and_w16 pc_RS08_reset pcm),pcm,(Matita_freescale_word16.and_w16 pc_RS08_reset pcm),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)),Matita_datatypes_bool.False,Matita_datatypes_bool.False))),mem,chk,(Matita_datatypes_constructors.None)))) +) +))) +)))))) +;; +