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