8 (function p -> (function p1 -> (function p2 -> (function m ->
16 let memory_impl_rect =
17 (function p -> (function p1 -> (function p2 -> (function m ->
25 type aux_mem_type = unit (* TOO POLYMORPHIC TYPE *)
28 type aux_chk_type = unit (* TOO POLYMORPHIC TYPE *)
31 let out_of_bound_memory =
34 MEM_FUNC -> Obj.magic (Matita_freescale_memory_func.mf_out_of_bound_memory)
35 | MEM_TREE -> Obj.magic (Matita_freescale_memory_trees.mt_out_of_bound_memory)
36 | MEM_BITS -> Obj.magic (Matita_freescale_memory_bits.mb_out_of_bound_memory))
43 MEM_FUNC -> Obj.magic (Matita_freescale_memory_func.mf_zero_memory)
44 | MEM_TREE -> Obj.magic (Matita_freescale_memory_trees.mt_zero_memory)
45 | MEM_BITS -> Obj.magic (Matita_freescale_memory_bits.mb_zero_memory))
52 MEM_FUNC -> Obj.magic ((function m -> (function addr -> (m addr))))
53 | MEM_TREE -> Obj.magic ((function m -> (function addr -> (Matita_freescale_memory_trees.mt_visit m addr))))
54 | MEM_BITS -> Obj.magic ((function m -> (function addr -> (Matita_freescale_memory_struct.byte8_of_bits (Matita_freescale_memory_trees.mt_visit m addr))))))
59 (function t -> (function c -> (function addr -> (
61 MEM_FUNC -> Obj.magic (Matita_freescale_memory_func.mf_chk_get)
62 | MEM_TREE -> Obj.magic (Matita_freescale_memory_trees.mt_chk_get)
63 | MEM_BITS -> Obj.magic (Matita_freescale_memory_bits.mb_chk_get))
68 (function t -> (function m -> (function c -> (function addr -> (
70 MEM_FUNC -> Obj.magic (Matita_freescale_memory_func.mf_mem_read)
71 | MEM_TREE -> Obj.magic (Matita_freescale_memory_trees.mt_mem_read)
72 | MEM_BITS -> Obj.magic (Matita_freescale_memory_bits.mb_mem_read))
79 MEM_FUNC -> Obj.magic ((function m -> (function c -> (function addr -> (function o -> (Matita_freescale_extra.opt_map (Matita_freescale_memory_func.mf_mem_read m c addr) (function b -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T o (Matita_freescale_memory_struct.bits_of_byte8 b)))))))))))
80 | MEM_TREE -> Obj.magic ((function m -> (function c -> (function addr -> (function o -> (Matita_freescale_extra.opt_map (Matita_freescale_memory_trees.mt_mem_read m c addr) (function b -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T o (Matita_freescale_memory_struct.bits_of_byte8 b)))))))))))
81 | MEM_BITS -> Obj.magic ((function m -> (function c -> (function addr -> (function o -> (Matita_freescale_memory_bits.mb_mem_read_bit m c addr o)))))))
86 (function t -> (function m -> (function c -> (function addr -> (function v -> (
88 MEM_FUNC -> Obj.magic (Matita_freescale_memory_func.mf_mem_update)
89 | MEM_TREE -> Obj.magic (Matita_freescale_memory_trees.mt_mem_update)
90 | MEM_BITS -> Obj.magic (Matita_freescale_memory_bits.mb_mem_update))
91 m (chk_get t c addr) addr v))))))
97 MEM_FUNC -> Obj.magic ((function m -> (function c -> (function addr -> (function o -> (function v -> (Matita_freescale_extra.opt_map (Matita_freescale_memory_func.mf_mem_read m c addr) (function b -> (Matita_freescale_memory_func.mf_mem_update m (chk_get MEM_FUNC c addr) addr (Matita_freescale_memory_struct.byte8_of_bits (Matita_freescale_memory_struct.setn_array8T o (Matita_freescale_memory_struct.bits_of_byte8 b) v)))))))))))
98 | MEM_TREE -> Obj.magic ((function m -> (function c -> (function addr -> (function o -> (function v -> (Matita_freescale_extra.opt_map (Matita_freescale_memory_trees.mt_mem_read m c addr) (function b -> (Matita_freescale_memory_trees.mt_mem_update m (chk_get MEM_TREE c addr) addr (Matita_freescale_memory_struct.byte8_of_bits (Matita_freescale_memory_struct.setn_array8T o (Matita_freescale_memory_struct.bits_of_byte8 b) v)))))))))))
99 | MEM_BITS -> Obj.magic ((function m -> (function c -> (function addr -> (function o -> (function v -> (Matita_freescale_memory_bits.mb_mem_update_bit m c addr o v))))))))
103 let load_from_source_at =
104 (function t -> (function m -> (function l -> (function addr -> (
106 MEM_FUNC -> Obj.magic (Matita_freescale_memory_func.mf_load_from_source_at)
107 | MEM_TREE -> Obj.magic (Matita_freescale_memory_trees.mt_load_from_source_at)
108 | MEM_BITS -> Obj.magic (Matita_freescale_memory_bits.mb_load_from_source_at))
112 let check_update_ranged =
115 MEM_FUNC -> Obj.magic ((function c -> (function inf -> (function sup -> (function v -> (Matita_freescale_memory_func.mf_check_update_ranged c inf sup v))))))
116 | MEM_TREE -> Obj.magic ((function c -> (function inf -> (function sup -> (function v -> (Matita_freescale_memory_trees.mt_update_ranged c inf sup v))))))
117 | MEM_BITS -> Obj.magic ((function c -> (function inf -> (function sup -> (function v -> (Matita_freescale_memory_trees.mt_update_ranged c inf sup (Matita_freescale_memory_struct.Array_8T(v,v,v,v,v,v,v,v)))))))))
121 let check_update_bit =
124 MEM_FUNC -> Obj.magic ((function c -> (function addr -> (function o -> (function v -> c)))))
125 | MEM_TREE -> Obj.magic ((function c -> (function addr -> (function o -> (function v -> c)))))
126 | MEM_BITS -> Obj.magic ((function c -> (function addr -> (function o -> (function v -> (Matita_freescale_memory_bits.mb_chk_update_bit c addr o v)))))))