branch for universe

[helm.git] / matita / contribs / assembly / freescale / freescale_ocaml / matita_freescale_memory_bits.ml

diff --git a/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_memory_bits.ml b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_memory_bits.ml
new file mode 100644 (file)
index 0000000..85f7acb
--- /dev/null
+++ b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_memory_bits.ml
@@ -0,0 +1,135 @@
+let mb_out_of_bound_memory =
+(let base = (Matita_freescale_memory_struct.Array_8T(Matita_freescale_memory_struct.MEM_OUT_OF_BOUND,Matita_freescale_memory_struct.MEM_OUT_OF_BOUND,Matita_freescale_memory_struct.MEM_OUT_OF_BOUND,Matita_freescale_memory_struct.MEM_OUT_OF_BOUND,Matita_freescale_memory_struct.MEM_OUT_OF_BOUND,Matita_freescale_memory_struct.MEM_OUT_OF_BOUND,Matita_freescale_memory_struct.MEM_OUT_OF_BOUND,Matita_freescale_memory_struct.MEM_OUT_OF_BOUND)) in (let lev4 = (Matita_freescale_memory_struct.Array_16T(base,base,base,base,base,base,base,base,base,base,base,base,base,base,base,base)) in (let lev3 = (Matita_freescale_memory_struct.Array_16T(lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4)) in (let lev2 = (Matita_freescale_memory_struct.Array_16T(lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3)) in (let lev1 = (Matita_freescale_memory_struct.Array_16T(lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2)) in lev1)))))
+;;
+
+let mb_zero_memory =
+(let base = (Matita_freescale_memory_struct.Array_8T(Matita_datatypes_bool.False,Matita_datatypes_bool.False,Matita_datatypes_bool.False,Matita_datatypes_bool.False,Matita_datatypes_bool.False,Matita_datatypes_bool.False,Matita_datatypes_bool.False,Matita_datatypes_bool.False)) in (let lev4 = (Matita_freescale_memory_struct.Array_16T(base,base,base,base,base,base,base,base,base,base,base,base,base,base,base,base)) in (let lev3 = (Matita_freescale_memory_struct.Array_16T(lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4,lev4)) in (let lev2 = (Matita_freescale_memory_struct.Array_16T(lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3,lev3)) in (let lev1 = (Matita_freescale_memory_struct.Array_16T(lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2,lev2)) in lev1)))))
+;;
+
+let mb_mem_update_bit =
+(function mem -> (function chk -> (function addr -> (function sub -> (function v -> 
+(match (Matita_freescale_memory_struct.getn_array8T sub (Matita_freescale_memory_trees.mt_visit chk addr)) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some(mem))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_trees.mt_update mem addr (Matita_freescale_memory_struct.setn_array8T sub (Matita_freescale_memory_trees.mt_visit mem addr) v))))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+)))))
+;;
+
+let mb_chk_update_bit =
+(function chk -> (function addr -> (function sub -> (function v -> (Matita_freescale_memory_trees.mt_update chk addr (Matita_freescale_memory_struct.setn_array8T sub (Matita_freescale_memory_trees.mt_visit chk addr) v))))))
+;;
+
+let mb_mem_read_bit =
+(function mem -> (function chk -> (function addr -> (function sub -> 
+(match (Matita_freescale_memory_struct.getn_array8T sub (Matita_freescale_memory_trees.mt_visit chk addr)) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T sub (Matita_freescale_memory_trees.mt_visit mem addr))))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T sub (Matita_freescale_memory_trees.mt_visit mem addr))))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+))))
+;;
+
+let mb_chk_get =
+(function chk -> (function addr -> (let c = (Matita_freescale_memory_trees.mt_visit chk addr) in (Matita_freescale_memory_struct.Array_8T((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O7 c),(Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O6 c),(Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O5 c),(Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O4 c),(Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O3 c),(Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O2 c),(Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O1 c),(Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O0 c))))))
+;;
+
+let mb_mem_update =
+(function mem -> (function chk -> (function addr -> (function v -> (let old_value = (Matita_freescale_memory_trees.mt_visit mem addr) in (let new_value = (Matita_freescale_memory_struct.bits_of_byte8 v) in (let newbit0 = 
+(match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O0 chk) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O0 old_value)))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O0 new_value)))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+ in (let newbit1 = 
+(match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O1 chk) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O1 old_value)))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O1 new_value)))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+ in (let newbit2 = 
+(match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O2 chk) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O2 old_value)))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O2 new_value)))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+ in (let newbit3 = 
+(match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O3 chk) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O3 old_value)))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O3 new_value)))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+ in (let newbit4 = 
+(match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O4 chk) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O4 old_value)))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O4 new_value)))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+ in (let newbit5 = 
+(match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O5 chk) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O5 old_value)))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O5 new_value)))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+ in (let newbit6 = 
+(match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O6 chk) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O6 old_value)))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O6 new_value)))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+ in (let newbit7 = 
+(match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O7 chk) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O7 old_value)))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O7 new_value)))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+ in (Matita_freescale_extra.opt_map newbit0 (function nb0 -> (Matita_freescale_extra.opt_map newbit1 (function nb1 -> (Matita_freescale_extra.opt_map newbit2 (function nb2 -> (Matita_freescale_extra.opt_map newbit3 (function nb3 -> (Matita_freescale_extra.opt_map newbit4 (function nb4 -> (Matita_freescale_extra.opt_map newbit5 (function nb5 -> (Matita_freescale_extra.opt_map newbit6 (function nb6 -> (Matita_freescale_extra.opt_map newbit7 (function nb7 -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_trees.mt_update mem addr (Matita_freescale_memory_struct.Array_8T(nb7,nb6,nb5,nb4,nb3,nb2,nb1,nb0)))))))))))))))))))))))))))))))))))
+;;
+
+let mb_mem_read =
+(function mem -> (function chk -> (function addr -> (let bit_types = (Matita_freescale_memory_trees.mt_visit chk addr) in (let value = (Matita_freescale_memory_trees.mt_visit mem addr) in (let newbit0 = 
+(match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O0 bit_types) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O0 value)))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O0 value)))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+ in (let newbit1 = 
+(match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O1 bit_types) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O1 value)))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O1 value)))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+ in (let newbit2 = 
+(match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O2 bit_types) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O2 value)))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O2 value)))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+ in (let newbit3 = 
+(match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O3 bit_types) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O3 value)))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O3 value)))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+ in (let newbit4 = 
+(match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O4 bit_types) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O4 value)))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O4 value)))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+ in (let newbit5 = 
+(match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O5 bit_types) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O5 value)))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O5 value)))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+ in (let newbit6 = 
+(match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O6 bit_types) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O6 value)))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O6 value)))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+ in (let newbit7 = 
+(match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O7 bit_types) with 
+   Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O7 value)))
+ | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O7 value)))
+ | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
+ in (Matita_freescale_extra.opt_map newbit0 (function nb0 -> (Matita_freescale_extra.opt_map newbit1 (function nb1 -> (Matita_freescale_extra.opt_map newbit2 (function nb2 -> (Matita_freescale_extra.opt_map newbit3 (function nb3 -> (Matita_freescale_extra.opt_map newbit4 (function nb4 -> (Matita_freescale_extra.opt_map newbit5 (function nb5 -> (Matita_freescale_extra.opt_map newbit6 (function nb6 -> (Matita_freescale_extra.opt_map newbit7 (function nb7 -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.byte8_of_bits (Matita_freescale_memory_struct.Array_8T(nb7,nb6,nb5,nb4,nb3,nb2,nb1,nb0))))))))))))))))))))))))))))))))))
+;;
+
+let mb_load_from_source_at =
+let rec mb_load_from_source_at = 
+(function old_mem -> (function source -> (function addr -> 
+(match source with 
+   Matita_list_list.Nil -> old_mem
+ | Matita_list_list.Cons(hd,tl) -> 
+(match (Matita_freescale_word16.lt_w16 addr (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))))) with 
+   Matita_datatypes_bool.True -> (mb_load_from_source_at (Matita_freescale_memory_trees.mt_update old_mem addr (Matita_freescale_memory_struct.bits_of_byte8 hd)) tl (Matita_freescale_word16.plus_w16nc addr (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.X1))))))
+ | Matita_datatypes_bool.False -> (Matita_freescale_memory_trees.mt_update old_mem addr (Matita_freescale_memory_struct.bits_of_byte8 hd)))
+)
+))) in mb_load_from_source_at
+;;
+