]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_model.ml
projects / helm.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
branch for universe
[helm.git] / matita / contribs / assembly / freescale / freescale_ocaml / matita_freescale_model.ml
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 (file)
index 0000000..2c3359b
--- /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))))
+)
+)))
+))))))
+;;
+
Unnamed repository; edit this file 'description' to name the repository.