]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_memory_func.ml
made executable again
[helm.git] / helm / software / 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