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

   1 let mf_check_update_ranged =
   2 (function f -> (function i -> (function s -> (function v -> (function x ->
   3 (match (Matita_freescale_word16.in_range x i s) with
   4    Matita_datatypes_bool.True -> v
   5  | Matita_datatypes_bool.False -> (f x))
   6 )))))
   7 ;;
   8
   9 let mf_out_of_bound_memory =
  10 (function _ -> Matita_freescale_memory_struct.MEM_OUT_OF_BOUND)
  11 ;;
  12
  13 let mf_chk_get =
  14 (function c -> (function a ->
  15 (match (c a) with
  16    Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_freescale_memory_struct.Array_8T(Matita_freescale_memory_struct.MEM_READ_ONLY,Matita_freescale_memory_struct.MEM_READ_ONLY,Matita_freescale_memory_struct.MEM_READ_ONLY,Matita_freescale_memory_struct.MEM_READ_ONLY,Matita_freescale_memory_struct.MEM_READ_ONLY,Matita_freescale_memory_struct.MEM_READ_ONLY,Matita_freescale_memory_struct.MEM_READ_ONLY,Matita_freescale_memory_struct.MEM_READ_ONLY))
  17  | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_freescale_memory_struct.Array_8T(Matita_freescale_memory_struct.MEM_READ_WRITE,Matita_freescale_memory_struct.MEM_READ_WRITE,Matita_freescale_memory_struct.MEM_READ_WRITE,Matita_freescale_memory_struct.MEM_READ_WRITE,Matita_freescale_memory_struct.MEM_READ_WRITE,Matita_freescale_memory_struct.MEM_READ_WRITE,Matita_freescale_memory_struct.MEM_READ_WRITE,Matita_freescale_memory_struct.MEM_READ_WRITE))
  18  | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (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)))
  19 ))
  20 ;;
  21
  22 let mf_mem_update =
  23 (function f -> (function c -> (function a -> (function v ->
  24 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O0 c) with
  25    Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some(f))
  26  | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((function x ->
  27 (match (Matita_freescale_word16.eq_w16 x a) with
  28    Matita_datatypes_bool.True -> v
  29  | Matita_datatypes_bool.False -> (f x))
  30 )))
  31  | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
  32 ))))
  33 ;;
  34
  35 let mf_zero_memory =
  36 (function _ -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))
  37 ;;
  38
  39 let mf_mem_read =
  40 (function f -> (function c -> (function a ->
  41 (match (c a) with
  42    Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((f a)))
  43  | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((f a)))
  44  | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
  45 )))
  46 ;;
  47
  48 let mf_load_from_source_at =
  49 let rec mf_load_from_source_at =
  50 (function old_mem -> (function source -> (function addr ->
  51 (match source with
  52    Matita_list_list.Nil -> old_mem
  53  | Matita_list_list.Cons(hd,tl) -> (function x ->
  54 (match (Matita_freescale_word16.lt_w16 x addr) with
  55    Matita_datatypes_bool.True -> (old_mem x)
  56  | Matita_datatypes_bool.False ->
  57 (match (Matita_freescale_word16.eq_w16 x addr) with
  58    Matita_datatypes_bool.True -> hd
  59  | Matita_datatypes_bool.False -> (mf_load_from_source_at old_mem 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))))) x))
  60 )
  61 ))
  62 ))) in mf_load_from_source_at
  63 ;;
  64