matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_memory_abs.ml

   1 type memory_impl =
   2 MEM_FUNC
   3  | MEM_TREE
   4  | MEM_BITS
   5 ;;
   6
   7 let memory_impl_rec =
   8 (function p -> (function p1 -> (function p2 -> (function m ->
   9 (match m with
  10    MEM_FUNC -> p
  11  | MEM_TREE -> p1
  12  | MEM_BITS -> p2)
  13 ))))
  14 ;;
  15
  16 let memory_impl_rect =
  17 (function p -> (function p1 -> (function p2 -> (function m ->
  18 (match m with
  19    MEM_FUNC -> p
  20  | MEM_TREE -> p1
  21  | MEM_BITS -> p2)
  22 ))))
  23 ;;
  24
  25 type aux_mem_type = unit (* TOO POLYMORPHIC TYPE *)
  26 ;;
  27
  28 type aux_chk_type = unit (* TOO POLYMORPHIC TYPE *)
  29 ;;
  30
  31 let out_of_bound_memory =
  32 (function t ->
  33 (match t with
  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))
  37 )
  38 ;;
  39
  40 let zero_memory =
  41 (function t ->
  42 (match t with
  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))
  46 )
  47 ;;
  48
  49 let mem_read_abs =
  50 (function t ->
  51 (match t with
  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))))))
  55 )
  56 ;;
  57
  58 let chk_get =
  59 (function t -> (function c -> (function addr -> (
  60 (match t with
  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))
  64  c addr))))
  65 ;;
  66
  67 let mem_read =
  68 (function t -> (function m -> (function c -> (function addr -> (
  69 (match t with
  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))
  73  m c addr)))))
  74 ;;
  75
  76 let mem_read_bit =
  77 (function t ->
  78 (match t with
  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)))))))
  82 )
  83 ;;
  84
  85 let mem_update =
  86 (function t -> (function m -> (function c -> (function addr -> (function v -> (
  87 (match t with
  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))))))
  92 ;;
  93
  94 let mem_update_bit =
  95 (function t ->
  96 (match t with
  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))))))))
 100 )
 101 ;;
 102
 103 let load_from_source_at =
 104 (function t -> (function m -> (function l -> (function addr -> (
 105 (match t with
 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))
 109  m l addr)))))
 110 ;;
 111
 112 let check_update_ranged =
 113 (function t ->
 114 (match t with
 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)))))))))
 118 )
 119 ;;
 120
 121 let check_update_bit =
 122 (function t ->
 123 (match t with
 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)))))))
 127 )
 128 ;;
 129