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

   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)))))
   3 ;;
   4
   5 let mb_zero_memory =
   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)))))
   7 ;;
   8
   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))
  15 )))))
  16 ;;
  17
  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))))))
  20 ;;
  21
  22 let mb_mem_read_bit =
  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))
  28 ))))
  29 ;;
  30
  31 let mb_chk_get =
  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))))))
  33 ;;
  34
  35 let mb_mem_update =
  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))
  41  in (let newbit1 =
  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))
  46  in (let newbit2 =
  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))
  51  in (let newbit3 =
  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))
  56  in (let newbit4 =
  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))
  61  in (let newbit5 =
  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))
  66  in (let newbit6 =
  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))
  71  in (let newbit7 =
  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)))))))))))))))))))))))))))))))))))
  77 ;;
  78
  79 let mb_mem_read =
  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))
  85  in (let newbit1 =
  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))
  90  in (let newbit2 =
  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))
  95  in (let newbit3 =
  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))
 100  in (let newbit4 =
 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))
 105  in (let newbit5 =
 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))
 110  in (let newbit6 =
 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))
 115  in (let newbit7 =
 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))))))))))))))))))))))))))))))))))
 121 ;;
 122
 123 let mb_load_from_source_at =
 124 let rec mb_load_from_source_at =
 125 (function old_mem -> (function source -> (function addr ->
 126 (match source with
 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)))
 132 )
 133 ))) in mb_load_from_source_at
 134 ;;
 135