1structure updateML :> updateML =
2struct
3  nonfix MEM_WRITE MEM_WRITE_WORD MEM_WRITE_HALF MEM_WRITE_BYTE SET_HALF
4         SET_BYTE FORMAT GET_BYTE GET_HALF addr30 mem_items empty_memory
5         mem_write_block mem_write mem_read |: data_size Word Half Byte
6         formats_size UnsignedWord UnsignedHalfWord SignedHalfWord
7         UnsignedByte SignedByte * / div mod + - ^ @ <> > < >= <= := o
8         before;
9
10  open numML fcpML wordsML;
11  type mem = (word30, word32) Redblackmap.dict
12  val mem_updates = ref ([]: word30 list)
13  datatype formats
14       = SignedByte
15       | UnsignedByte
16       | SignedHalfWord
17       | UnsignedHalfWord
18       | UnsignedWord
19  fun formats_size x = ZERO
20
21  datatype data = Byte of word8 | Half of word16 | Word of word32
22  fun data_size (Byte(a)) = ONE
23    | data_size (Half(a)) = ONE
24    | data_size (Word(a)) = ONE
25
26  fun |: a l =
27        fn m => fn b =>
28        if word_ls a b andalso < (- (w2n b) (w2n a)) (listML.LENGTH l)
29          then listML.EL (- (w2n b) (w2n a)) l else m b
30
31  fun fromNum32 n =
32        wordsML.fromNum(numML.fromHexString n, fcpML.ITSELF(numML.fromInt 32))
33
34  fun mem_read (m,a) = Redblackmap.find(m:mem, a)
35                       handle NotFound => fromNum32 "E6000010"
36
37  fun mem_write m a d = (:= (mem_updates, a :: !mem_updates);
38                         Redblackmap.insert(m:mem, a, d))
39
40  fun mem_write_block m a [] = m
41    | mem_write_block m a (d::l) =
42        mem_write_block (mem_write m a d)
43          (word_add a (n2w_itself (ONE,fcpML.ITSELF(numML.fromInt 30)))) l
44
45  fun word_compare(v, w) =
46    let val m = w2n v and n = w2n w in
47      if m = n then
48        EQUAL
49      else
50        if < m n then LESS else GREATER
51    end
52
53  val empty_memory = (Redblackmap.mkDict word_compare):mem
54
55  fun mem_items m = Redblackmap.listItems m
56
57  fun addr30 addr =
58        word_extract_itself (fcpML.ITSELF (numML.fromDecString"30"))
59          (fromString"31") TWO addr
60
61  fun GET_HALF oareg data =
62        if word_index oareg ONE
63          then word_extract_itself
64                 (fcpML.ITSELF (numML.fromDecString"16"))
65                 (fromString"31") (fromString"16") data
66          else word_extract_itself
67                 (fcpML.ITSELF (numML.fromDecString"16"))
68                 (fromString"15") ZERO data
69
70  fun GET_BYTE oareg data =
71        case
72          word_eq oareg
73            (n2w_itself (ZERO,(fcpML.ITSELF (numML.fromDecString"2"))))
74         of true =>
75               word_extract_itself
76                 (fcpML.ITSELF (numML.fromDecString"8")) (fromString"7")
77                 ZERO data
78          | false =>
79               (case
80                  word_eq oareg
81                    (n2w_itself
82                       (ONE,(fcpML.ITSELF (numML.fromDecString"2"))))
83                of true =>
84                      word_extract_itself
85                        (fcpML.ITSELF (numML.fromDecString"8"))
86                        (fromString"15") (fromString"8") data
87                 | false =>
88                      (case
89                         word_eq oareg
90                           (n2w_itself
91                              (TWO,(fcpML.ITSELF (numML.fromDecString"2"))))
92                       of true =>
93                             word_extract_itself
94                               (fcpML.ITSELF (numML.fromDecString"8"))
95                               (fromString"23") (fromString"16") data
96                        | false =>
97                             word_extract_itself
98                               (fcpML.ITSELF (numML.fromDecString"8"))
99                               (fromString"31") (fromString"24") data))
100
101  fun FORMAT fmt oareg data =
102        case fmt
103         of SignedByte =>
104               sw2sw_itself (fcpML.ITSELF (numML.fromDecString"32"))
105                 (GET_BYTE oareg data)
106          | UnsignedByte =>
107               w2w_itself (fcpML.ITSELF (numML.fromDecString"32"))
108                 (GET_BYTE oareg data)
109          | SignedHalfWord =>
110               sw2sw_itself (fcpML.ITSELF (numML.fromDecString"32"))
111                 (GET_HALF oareg data)
112          | UnsignedHalfWord =>
113               w2w_itself (fcpML.ITSELF (numML.fromDecString"32"))
114                 (GET_HALF oareg data)
115          | UnsignedWord =>
116               word_ror data ( *  (fromString"8") (w2n oareg))
117
118  fun SET_BYTE oareg b w =
119        word_modify (fn i => fn x =>
120          < i (fromString"8")
121          andalso
122          (if word_eq oareg
123                (n2w_itself
124                   (ZERO,(fcpML.ITSELF (numML.fromDecString"2"))))
125             then word_index b i else x)
126          orelse
127          ((<= (fromString"8") i andalso < i (fromString"16"))
128           andalso
129           (if word_eq oareg
130                 (n2w_itself
131                    (ONE,(fcpML.ITSELF (numML.fromDecString"2"))))
132              then word_index b (- i (fromString"8")) else x)
133           orelse
134           ((<= (fromString"16") i andalso < i (fromString"24"))
135            andalso
136            (if word_eq oareg
137                  (n2w_itself
138                     (TWO,(fcpML.ITSELF (numML.fromDecString"2"))))
139               then word_index b (- i (fromString"16")) else x)
140            orelse
141            (<= (fromString"24") i andalso < i (fromString"32"))
142            andalso
143            (if word_eq oareg
144                  (n2w_itself
145                     ((
146                      fromString
147                      "3"
148                      ),(fcpML.ITSELF (numML.fromDecString"2"))))
149               then word_index b (- i (fromString"24")) else x)))) w
150
151  fun SET_HALF oareg hw w =
152        word_modify (fn i => fn x =>
153          < i (fromString"16")
154          andalso
155          (if not oareg then word_index hw i else x)
156          orelse
157          (<= (fromString"16") i andalso < i (fromString"32"))
158          andalso
159          (if oareg then word_index hw (- i (fromString"16")) else x)) w
160
161  fun MEM_WRITE_BYTE mem addr word =
162        let val a30 = addr30 addr
163        in
164           mem_write mem a30
165             (SET_BYTE
166                (word_extract_itself
167                   (fcpML.ITSELF (numML.fromDecString"2")) ONE ZERO
168                   addr) word (mem_read (mem,a30)))
169        end
170
171  fun MEM_WRITE_HALF mem addr word =
172        let val a30 = addr30 addr
173        in
174           mem_write mem a30
175             (SET_HALF (word_index addr ONE) word
176                (mem_read (mem,a30)))
177        end
178
179  fun MEM_WRITE_WORD mem addr word = mem_write mem (addr30 addr) word
180
181  fun MEM_WRITE mem addr d =
182        case d
183         of Byte(b) => MEM_WRITE_BYTE mem addr b
184          | Half(hw) => MEM_WRITE_HALF mem addr hw
185          | Word(w) => MEM_WRITE_WORD mem addr w
186
187end
188