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

   1 let mt_out_of_bound_memory =
   2 (let lev4 = (Matita_freescale_memory_struct.Array_16T(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,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 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 mt_zero_memory =
   6 (let lev4 = (Matita_freescale_memory_struct.Array_16T((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.X0)),(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.X0)),(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.X0)),(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.X0)),(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.X0)),(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.X0)),(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.X0)),(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.X0)))) 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 mt_visit =
  10 (function data -> (function addr ->
  11 (match addr with
  12    Matita_freescale_word16.Mk_word16(wh,wl) -> (Matita_freescale_memory_struct.getn_array16T (Matita_freescale_byte8.b8l wl) (Matita_freescale_memory_struct.getn_array16T (Matita_freescale_byte8.b8h wl) (Matita_freescale_memory_struct.getn_array16T (Matita_freescale_byte8.b8l wh) (Matita_freescale_memory_struct.getn_array16T (Matita_freescale_byte8.b8h wh) data)))))
  13 ))
  14 ;;
  15
  16 let mt_update =
  17 (function data -> (function addr -> (function v ->
  18 (match addr with
  19    Matita_freescale_word16.Mk_word16(wh,wl) -> (let lev2 = (Matita_freescale_memory_struct.getn_array16T (Matita_freescale_byte8.b8h wh) data) in (let lev3 = (Matita_freescale_memory_struct.getn_array16T (Matita_freescale_byte8.b8l wh) lev2) in (let lev4 = (Matita_freescale_memory_struct.getn_array16T (Matita_freescale_byte8.b8h wl) lev3) in (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8h wh) data (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8l wh) lev2 (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8h wl) lev3 (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8l wl) lev4 v))))))))
  20 )))
  21 ;;
  22
  23 let mt_update_ranged =
  24 (function data -> (function i -> (function s -> (function v ->
  25 (match (Matita_freescale_word16.le_w16 i s) with
  26    Matita_datatypes_bool.True ->
  27 (match i with
  28    Matita_freescale_word16.Mk_word16(ih,il) ->
  29 (match s with
  30    Matita_freescale_word16.Mk_word16(sh,sl) -> (let ilev2 = (Matita_freescale_memory_struct.getn_array16T (Matita_freescale_byte8.b8h ih) data) in (let ilev3 = (Matita_freescale_memory_struct.getn_array16T (Matita_freescale_byte8.b8l ih) ilev2) in (let ilev4 = (Matita_freescale_memory_struct.getn_array16T (Matita_freescale_byte8.b8h il) ilev3) in (let slev2 = (Matita_freescale_memory_struct.getn_array16T (Matita_freescale_byte8.b8h sh) data) in (let slev3 = (Matita_freescale_memory_struct.getn_array16T (Matita_freescale_byte8.b8l sh) slev2) in (let slev4 = (Matita_freescale_memory_struct.getn_array16T (Matita_freescale_byte8.b8h sl) slev3) in (let vlev4 = (Matita_freescale_memory_struct.Array_16T(v,v,v,v,v,v,v,v,v,v,v,v,v,v,v,v)) in (let vlev3 = (Matita_freescale_memory_struct.Array_16T(vlev4,vlev4,vlev4,vlev4,vlev4,vlev4,vlev4,vlev4,vlev4,vlev4,vlev4,vlev4,vlev4,vlev4,vlev4,vlev4)) in (let vlev2 = (Matita_freescale_memory_struct.Array_16T(vlev3,vlev3,vlev3,vlev3,vlev3,vlev3,vlev3,vlev3,vlev3,vlev3,vlev3,vlev3,vlev3,vlev3,vlev3,vlev3)) in
  31 (match (Matita_freescale_exadecim.eq_ex (Matita_freescale_byte8.b8h ih) (Matita_freescale_byte8.b8h sh)) with
  32    Matita_datatypes_bool.True ->
  33 (match (Matita_freescale_exadecim.eq_ex (Matita_freescale_byte8.b8l ih) (Matita_freescale_byte8.b8l sh)) with
  34    Matita_datatypes_bool.True ->
  35 (match (Matita_freescale_exadecim.eq_ex (Matita_freescale_byte8.b8h il) (Matita_freescale_byte8.b8h sl)) with
  36    Matita_datatypes_bool.True -> (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8h ih) data (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8l ih) ilev2 (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8h il) ilev3 (Matita_freescale_memory_struct.setmn_array16T (Matita_freescale_byte8.b8l il) (Matita_freescale_byte8.b8l sl) ilev4 v))))
  37  | Matita_datatypes_bool.False -> (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8h ih) data (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8l ih) ilev2 (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8h sl) (Matita_freescale_memory_struct.setmn_array16T_succ_pred (Matita_freescale_byte8.b8h il) (Matita_freescale_byte8.b8h sl) (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8h il) ilev3 (Matita_freescale_memory_struct.setmn_array16T (Matita_freescale_byte8.b8l il) Matita_freescale_exadecim.XF ilev4 v)) vlev4) (Matita_freescale_memory_struct.setmn_array16T Matita_freescale_exadecim.X0 (Matita_freescale_byte8.b8l sl) slev4 v)))))
  38
  39  | Matita_datatypes_bool.False -> (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8h ih) data (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8l sh) (Matita_freescale_memory_struct.setmn_array16T_succ_pred (Matita_freescale_byte8.b8l ih) (Matita_freescale_byte8.b8l sh) (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8l ih) ilev2 (Matita_freescale_memory_struct.setmn_array16T_succ (Matita_freescale_byte8.b8h il) (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8h il) ilev3 (Matita_freescale_memory_struct.setmn_array16T (Matita_freescale_byte8.b8l il) Matita_freescale_exadecim.XF ilev4 v)) vlev4)) vlev3) (Matita_freescale_memory_struct.setmn_array16T_pred (Matita_freescale_byte8.b8h sl) (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8h sl) slev3 (Matita_freescale_memory_struct.setmn_array16T Matita_freescale_exadecim.X0 (Matita_freescale_byte8.b8l sl) slev4 v)) vlev4))))
  40
  41  | Matita_datatypes_bool.False -> (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8h sh) (Matita_freescale_memory_struct.setmn_array16T_succ_pred (Matita_freescale_byte8.b8h ih) (Matita_freescale_byte8.b8h sh) (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8h ih) data (Matita_freescale_memory_struct.setmn_array16T_succ (Matita_freescale_byte8.b8l ih) (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8l ih) ilev2 (Matita_freescale_memory_struct.setmn_array16T_succ (Matita_freescale_byte8.b8h il) (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8h il) ilev3 (Matita_freescale_memory_struct.setmn_array16T (Matita_freescale_byte8.b8l il) Matita_freescale_exadecim.XF ilev4 v)) vlev4)) vlev3)) vlev2) (Matita_freescale_memory_struct.setmn_array16T_pred (Matita_freescale_byte8.b8l sh) (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8l sh) slev2 (Matita_freescale_memory_struct.setmn_array16T_pred (Matita_freescale_byte8.b8h sl) (Matita_freescale_memory_struct.setn_array16T (Matita_freescale_byte8.b8h sl) slev3 (Matita_freescale_memory_struct.setmn_array16T Matita_freescale_exadecim.X0 (Matita_freescale_byte8.b8l sl) slev4 v)) vlev4)) vlev3)))
  42 ))))))))))
  43 )
  44
  45  | Matita_datatypes_bool.False -> data)
  46 ))))
  47 ;;
  48
  49 let mt_chk_get =
  50 (function chk -> (function addr ->
  51 (match (mt_visit chk addr) with
  52    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))
  53  | 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))
  54  | 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)))
  55 ))
  56 ;;
  57
  58 let mt_mem_update =
  59 (function mem -> (function chk -> (function addr -> (function v ->
  60 (match (Matita_freescale_memory_struct.getn_array8T Matita_freescale_aux_bases.O0 chk) with
  61    Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some(mem))
  62  | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((mt_update mem addr v)))
  63  | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
  64 ))))
  65 ;;
  66
  67 let mt_mem_read =
  68 (function mem -> (function chk -> (function addr ->
  69 (match (mt_visit chk addr) with
  70    Matita_freescale_memory_struct.MEM_READ_ONLY -> (Matita_datatypes_constructors.Some((mt_visit mem addr)))
  71  | Matita_freescale_memory_struct.MEM_READ_WRITE -> (Matita_datatypes_constructors.Some((mt_visit mem addr)))
  72  | Matita_freescale_memory_struct.MEM_OUT_OF_BOUND -> (Matita_datatypes_constructors.None))
  73 )))
  74 ;;
  75
  76 let mt_load_from_source_at =
  77 let rec mt_load_from_source_at =
  78 (function old_mem -> (function source -> (function addr ->
  79 (match source with
  80    Matita_list_list.Nil -> old_mem
  81  | Matita_list_list.Cons(hd,tl) ->
  82 (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
  83    Matita_datatypes_bool.True -> (mt_load_from_source_at (mt_update old_mem addr 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))))))
  84  | Matita_datatypes_bool.False -> (mt_update old_mem addr hd))
  85 )
  86 ))) in mt_load_from_source_at
  87 ;;
  88