1 let mb_out_of_bound_memory =
2 (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)))))
6 (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)))))
9 let mb_mem_update_bit =
10 (function mem -> (function chk -> (function addr -> (function sub -> (function v ->
11 (match (Matita_freescale_memory_struct.getn_array8T sub (Matita_freescale_memory_trees.mt_visit chk addr)) with
12 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some(mem))
13 | 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))))
14 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
18 let mb_chk_update_bit =
19 (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))))))
23 (function mem -> (function chk -> (function addr -> (function sub ->
24 (match (Matita_freescale_memory_struct.getn_array8T sub (Matita_freescale_memory_trees.mt_visit chk addr)) with
25 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))))
26 | 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))))
27 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
32 (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))))))
36 (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 =
37 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O0 chk) with
38 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O0 old_value)))
39 | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O0 new_value)))
40 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
42 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O1 chk) with
43 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O1 old_value)))
44 | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O1 new_value)))
45 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
47 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O2 chk) with
48 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O2 old_value)))
49 | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O2 new_value)))
50 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
52 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O3 chk) with
53 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O3 old_value)))
54 | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O3 new_value)))
55 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
57 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O4 chk) with
58 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O4 old_value)))
59 | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O4 new_value)))
60 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
62 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O5 chk) with
63 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O5 old_value)))
64 | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O5 new_value)))
65 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
67 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O6 chk) with
68 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O6 old_value)))
69 | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O6 new_value)))
70 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
72 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O7 chk) with
73 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O7 old_value)))
74 | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O7 new_value)))
75 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
76 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)))))))))))))))))))))))))))))))))))
80 (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 =
81 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O0 bit_types) with
82 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O0 value)))
83 | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O0 value)))
84 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
86 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O1 bit_types) with
87 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O1 value)))
88 | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O1 value)))
89 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
91 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O2 bit_types) with
92 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O2 value)))
93 | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O2 value)))
94 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
96 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O3 bit_types) with
97 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O3 value)))
98 | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O3 value)))
99 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
101 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O4 bit_types) with
102 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O4 value)))
103 | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O4 value)))
104 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
106 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O5 bit_types) with
107 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O5 value)))
108 | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O5 value)))
109 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
111 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O6 bit_types) with
112 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O6 value)))
113 | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O6 value)))
114 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
116 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O7 bit_types) with
117 Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O7 value)))
118 | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O7 value)))
119 | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
120 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))))))))))))))))))))))))))))))))))
123 let mb_load_from_source_at =
124 let rec mb_load_from_source_at =
125 (function old_mem -> (function source -> (function addr ->
127 Matita_list_list.Nil -> old_mem
128 | Matita_list_list.Cons(hd,tl) ->
129 (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
130 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))))))
131 | Matita_datatypes_bool.False -> (Matita_freescale_memory_trees.mt_update old_mem addr (Matita_freescale_memory_struct.bits_of_byte8 hd)))
133 ))) in mb_load_from_source_at