1structure armSyntax :> armSyntax = 2struct 3 4open Abbrev HolKernel arm_seq_monadTheory arm_decoderTheory; 5 6val ERR = Feedback.mk_HOL_ERR "armSyntax"; 7 8fun dest_strip t = 9let val (l,r) = strip_comb t in 10 (fst (dest_const l), r) 11end; 12 13local 14 val arm_state_type = ``:arm_state``; 15 val err = ERR "dest_monad_type" "not an instance of 'a M" 16in 17 fun dest_monad_type ty = 18 let val (tya,tyb) = dom_rng ty in 19 if tya = arm_state_type then 20 case total dest_thy_type tyb of 21 SOME {Tyop = "error_option", Thy = "arm_seq_monad", 22 Args = [tyc, tyd]} => 23 (if tyd = arm_state_type then tyc else raise err) 24 | _ => raise err 25 else 26 raise err 27 end handle HOL_ERR _ => raise err 28end; 29 30fun inst_word_alpha ty tm = 31 Term.inst [Type.alpha |-> 32 (if wordsSyntax.is_word_type (Term.type_of tm) then 33 ty 34 else 35 wordsSyntax.mk_word_type ty)] tm; 36 37fun mk_monad_const s = prim_mk_const{Name = s, Thy = "arm_seq_monad"} 38fun mk_core_const s = prim_mk_const{Name = s, Thy = "arm_coretypes"} 39fun mk_decode_const s = prim_mk_const{Name = s, Thy = "arm_decoder"}; 40 41val error_tm = mk_monad_const "Error" 42val valuestate_tm = mk_monad_const "ValueState" 43 44val constT_tm = mk_monad_const "constT" 45val seqT_tm = mk_monad_const "seqT" 46val parT_tm = mk_monad_const "parT" 47val forT_tm = mk_monad_const "forT" 48val readT_tm = mk_monad_const "readT" 49val writeT_tm = mk_monad_const "writeT" 50 51val read__reg_tm = mk_monad_const "read__reg" 52val write__reg_tm = mk_monad_const "write__reg" 53val read__psr_tm = mk_monad_const "read__psr" 54val write__psr_tm = mk_monad_const "write__psr" 55 56val read_reg_mode_tm = mk_monad_const "read_reg_mode" 57val write_reg_mode_tm = mk_monad_const "write_reg_mode" 58val read_reg_tm = mk_monad_const "read_reg" 59val write_reg_tm = mk_monad_const "write_reg" 60val read_cpsr_tm = mk_monad_const "read_cpsr" 61val write_cpsr_tm = mk_monad_const "write_cpsr" 62val read_spsr_tm = mk_monad_const "read_spsr" 63val write_spsr_tm = mk_monad_const "write_spsr" 64val read_memA_tm = mk_monad_const "read_memA" 65val write_memA_tm = mk_monad_const "write_memA" 66 67val clear_event_register_tm = mk_monad_const "clear_event_register" 68val send_event_tm = mk_monad_const "send_event" 69val wait_for_interrupt_tm = mk_monad_const "wait_for_interrupt" 70val clear_wait_for_interrupt_tm = mk_monad_const "clear_wait_for_interrupt" 71 72val decode_psr_tm = mk_core_const "decode_psr" 73val bytes_tm = mk_core_const "bytes" 74val align_tm = mk_core_const "align" 75val aligned_tm = mk_core_const "aligned" 76val bit_count_tm = mk_core_const "bit_count" 77val Encoding_ARM_tm = mk_core_const "Encoding_ARM" 78val Encoding_Thumb_tm = mk_core_const "Encoding_Thumb" 79val Encoding_Thumb2_tm = mk_core_const "Encoding_Thumb2" 80val Encoding_ThumbEE_tm = mk_core_const "Encoding_ThumbEE" 81val ITAdvance_tm = mk_core_const "ITAdvance" 82val NoInterrupt_tm = mk_core_const "NoInterrupt" 83val HW_Reset_tm = mk_core_const "HW_Reset" 84val HW_Fiq_tm = mk_core_const "HW_Fiq" 85val HW_Irq_tm = mk_core_const "HW_Irq" 86 87val arm_decode_tm = mk_decode_const "arm_decode" 88val thumb_decode_tm = mk_decode_const "thumb_decode" 89val thumbee_decode_tm = mk_decode_const "thumbee_decode" 90val thumb2_decode_tm = mk_decode_const "thumb2_decode"; 91 92fun mk_error s = 93 HolKernel.mk_comb(error_tm, 94 Term.inst [Type.alpha |-> stringSyntax.string_ty] s) 95 handle HOL_ERR _ => raise ERR "mk_error" ""; 96 97fun mk_valuestate (v,s) = 98 HolKernel.list_mk_comb(Term.inst 99 [Type.alpha |-> Term.type_of v, 100 Type.beta |-> Term.type_of s] valuestate_tm, [v,s]) 101 handle HOL_ERR _ => raise ERR "mk_valuestate" ""; 102 103fun mk_constT t = 104 HolKernel.mk_comb(Term.inst[Type.alpha |-> Term.type_of t] constT_tm,t) 105 handle HOL_ERR _ => raise ERR "mk_constT" ""; 106 107fun mk_seqT (f,g) = 108 HolKernel.list_mk_comb(Term.inst 109 [Type.alpha |-> dest_monad_type (Term.type_of f), 110 Type.beta |-> (dest_monad_type o snd o Type.dom_rng o Term.type_of) g] 111 seqT_tm, [f,g]) 112 handle HOL_ERR _ => raise ERR "mk_seqT" ""; 113 114fun mk_parT (f,g) = 115 HolKernel.list_mk_comb(Term.inst 116 [Type.alpha |-> dest_monad_type (Term.type_of f), 117 Type.beta |-> dest_monad_type (Term.type_of g)] parT_tm,[f,g]) 118 handle HOL_ERR _ => raise ERR "mk_parT" ""; 119 120fun mk_forT (l,h,f) = 121 HolKernel.list_mk_comb(Term.inst 122 [Type.alpha |-> (dest_monad_type o snd o Type.dom_rng o Term.type_of) f] 123 forT_tm,[l,h,f]) 124 handle HOL_ERR _ => raise ERR "mk_forT" ""; 125 126fun mk_readT f = 127 HolKernel.mk_comb(Term.inst 128 [Type.alpha |-> snd (dom_rng (Term.type_of f))] readT_tm, f) 129 handle HOL_ERR _ => raise ERR "mk_readT" ""; 130 131fun mk_writeT f = 132 HolKernel.mk_comb(writeT_tm, f) 133 handle HOL_ERR _ => raise ERR "mk_writeT" ""; 134 135fun mk_read__reg (ii,r) = 136 HolKernel.list_mk_comb(read__reg_tm, 137 [Term.inst [Type.alpha |-> ``:iiid``] ii, 138 Term.inst [Type.alpha |-> ``:RName``] r]) 139 handle HOL_ERR _ => raise ERR "mk_read__reg" ""; 140 141fun mk_write__reg (ii,r,v) = 142 HolKernel.list_mk_comb(write__reg_tm, 143 [Term.inst [Type.alpha |-> ``:iiid``] ii, 144 Term.inst [Type.alpha |-> ``:RName``] r, 145 inst_word_alpha ``:32`` v]) 146 handle HOL_ERR _ => raise ERR "mk_write__reg" ""; 147 148fun mk_read__psr (ii,r) = 149 HolKernel.list_mk_comb(read__psr_tm, 150 [Term.inst [Type.alpha |-> ``:iiid``] ii, 151 Term.inst [Type.alpha |-> ``:PSRName``] r]) 152 handle HOL_ERR _ => raise ERR "mk_read__psr" ""; 153 154fun mk_write__psr (ii,r,v) = 155 HolKernel.list_mk_comb(write__psr_tm, 156 [Term.inst [Type.alpha |-> ``:iiid``] ii, 157 Term.inst [Type.alpha |-> ``:PSRName``] r, 158 Term.inst [Type.alpha |-> ``:ARMpsr``] v]) 159 handle HOL_ERR _ => raise ERR "mk_write__psr" ""; 160 161fun mk_read_reg (ii,n) = 162 HolKernel.list_mk_comb(read_reg_tm, 163 [Term.inst [Type.alpha |-> ``:iiid``] ii, 164 inst_word_alpha ``:4`` n]) 165 handle HOL_ERR _ => raise ERR "mk_read_reg" ""; 166 167fun mk_write_reg (ii,n,v) = 168 HolKernel.list_mk_comb(write_reg_tm, 169 [Term.inst [Type.alpha |-> ``:iiid``] ii, 170 inst_word_alpha ``:4`` n, 171 inst_word_alpha ``:32`` v]) 172 handle HOL_ERR _ => raise ERR "mk_write_reg" ""; 173 174fun mk_read_reg_mode (ii,n,m) = 175 HolKernel.list_mk_comb(read_reg_mode_tm, 176 [Term.inst [Type.alpha |-> ``:iiid``] ii, 177 pairSyntax.mk_pair 178 (inst_word_alpha ``:4`` n, inst_word_alpha ``:5`` m)]) 179 handle HOL_ERR _ => raise ERR "mk_read_reg_mode" ""; 180 181fun mk_write_reg_mode (ii,n,m,v) = 182 HolKernel.list_mk_comb(write_reg_mode_tm, 183 [Term.inst [Type.alpha |-> ``:iiid``] ii, 184 pairSyntax.mk_pair 185 (inst_word_alpha ``:4`` n, inst_word_alpha ``:5`` m), 186 inst_word_alpha ``:32`` v]) 187 handle HOL_ERR _ => raise ERR "mk_write_reg_mode" ""; 188 189fun mk_read_cpsr ii = 190 HolKernel.mk_comb(read_cpsr_tm, Term.inst [Type.alpha |-> ``:iiid``] ii) 191 handle HOL_ERR _ => raise ERR "mk_read_cpsr" ""; 192 193fun mk_write_cpsr (ii,v) = 194 HolKernel.list_mk_comb(write_cpsr_tm, 195 [Term.inst [Type.alpha |-> ``:iiid``] ii, 196 Term.inst [Type.alpha |-> ``:ARMpsr``] v]) 197 handle HOL_ERR _ => raise ERR "mk_write_cpsr" ""; 198 199fun mk_read_spsr ii = 200 HolKernel.mk_comb(read_spsr_tm, Term.inst [Type.alpha |-> ``:iiid``] ii) 201 handle HOL_ERR _ => raise ERR "mk_read_spsr" ""; 202 203fun mk_write_spsr (ii,v) = 204 HolKernel.list_mk_comb(write_spsr_tm, 205 [Term.inst [Type.alpha |-> ``:iiid``] ii, 206 Term.inst [Type.alpha |-> ``:ARMpsr``] v]) 207 handle HOL_ERR _ => raise ERR "mk_write_spsr" ""; 208 209fun mk_read_memA (ii,a,s) = 210 HolKernel.list_mk_comb(read_memA_tm, 211 [Term.inst [Type.alpha |-> ``:iiid``] ii, 212 pairSyntax.mk_pair 213 (inst_word_alpha ``:32`` a, 214 Term.inst [Type.alpha |-> ``:num``] s)]) 215 handle HOL_ERR _ => raise ERR "mk_read_memA" ""; 216 217fun mk_write_memA (ii,a,s,v) = 218 HolKernel.list_mk_comb(write_memA_tm, 219 [Term.inst [Type.alpha |-> ``:iiid``] ii, 220 pairSyntax.mk_pair 221 (inst_word_alpha ``:32`` a, 222 Term.inst [Type.alpha |-> ``:num``] s), 223 v]) 224 handle HOL_ERR _ => raise ERR "mk_write_memA" ""; 225 226fun mk_clear_event_register ii = 227 HolKernel.mk_comb(clear_event_register_tm, 228 Term.inst [Type.alpha |-> ``:iiid``] ii) 229 handle HOL_ERR _ => raise ERR "mk_clear_event_register" ""; 230 231fun mk_send_event ii = 232 HolKernel.mk_comb(send_event_tm, Term.inst [Type.alpha |-> ``:iiid``] ii) 233 handle HOL_ERR _ => raise ERR "mk_send_event" ""; 234 235fun mk_wait_for_interrupt ii = 236 HolKernel.mk_comb(wait_for_interrupt_tm, 237 Term.inst [Type.alpha |-> ``:iiid``] ii) 238 handle HOL_ERR _ => raise ERR "mk_wait_for_interrupt" ""; 239 240fun mk_clear_wait_for_interrupt ii = 241 HolKernel.mk_comb(clear_wait_for_interrupt_tm, 242 Term.inst [Type.alpha |-> ``:iiid``] ii) 243 handle HOL_ERR _ => raise ERR "mk_clear_wait_for_interrupt" ""; 244 245fun mk_decode_psr w = 246 HolKernel.mk_comb(decode_psr_tm, inst_word_alpha ``:32`` w) 247 handle HOL_ERR _ => raise ERR "mk_decode_psr" ""; 248 249fun mk_bytes (w,n) = 250 HolKernel.mk_comb(bytes_tm, pairSyntax.mk_pair(inst_word_alpha ``:32`` w, n)) 251 handle HOL_ERR _ => raise ERR "mk_bytes" ""; 252 253fun mk_align (w,n) = 254 HolKernel.mk_comb(Term.inst 255 [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] align_tm, 256 pairSyntax.mk_pair(w, n)) 257 handle HOL_ERR _ => raise ERR "mk_align" ""; 258 259fun mk_aligned (w,n) = 260 HolKernel.mk_comb(Term.inst 261 [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] aligned_tm, 262 pairSyntax.mk_pair(w, n)) 263 handle HOL_ERR _ => raise ERR "mk_aligned" ""; 264 265fun mk_bit_count w = 266 HolKernel.mk_comb(Term.inst 267 [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] bit_count_tm, w) 268 handle HOL_ERR _ => raise ERR "mk_bit_count" ""; 269 270fun mk_ITAdvance w = 271 HolKernel.mk_comb(Term.inst 272 [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] ITAdvance_tm, w) 273 handle HOL_ERR _ => raise ERR "mk_ITAdvance" ""; 274 275fun mk_read_memA_1 (ii,a) = mk_read_memA (ii,a,``1n``); 276 277fun mk_write_memA_1 (ii,a,v) = 278 mk_write_memA (ii,a,``1n``,listSyntax.mk_list([v],``:word8``)); 279 280fun mk_read_memA_2 (ii,a) = mk_read_memA (ii,a,``2n``); 281fun mk_write_memA_2 (ii,a,v) = mk_write_memA (ii,a,``2n``,mk_bytes(v,``2n``)); 282fun mk_read_memA_4 (ii,a) = mk_read_memA (ii,a,``4n``); 283fun mk_write_memA_4 (ii,a,v) = mk_write_memA (ii,a,``4n``,mk_bytes(v,``4n``)); 284 285fun mk_arm_decode(b,w) = 286 HolKernel.list_mk_comb(arm_decode_tm, [b,inst_word_alpha ``:32`` w]) 287 handle HOL_ERR _ => raise ERR "mk_arm_decode" ""; 288 289fun mk_thumb_decode(a,itstate,w) = 290 HolKernel.list_mk_comb(thumb_decode_tm, 291 [a,inst_word_alpha ``:8`` itstate, inst_word_alpha ``:16`` w]) 292 handle HOL_ERR _ => raise ERR "mk_thumb_decode" ""; 293 294fun mk_thumbee_decode(a,itstate,w) = 295 HolKernel.list_mk_comb(thumbee_decode_tm, 296 [a,inst_word_alpha ``:8`` itstate, inst_word_alpha ``:16`` w]) 297 handle HOL_ERR _ => raise ERR "mk_thumbee_decode" ""; 298 299fun mk_thumb2_decode(a,itstate,w1,w2) = 300 HolKernel.list_mk_comb(thumb2_decode_tm, 301 [a,inst_word_alpha ``:8`` itstate, 302 pairSyntax.mk_pair 303 (inst_word_alpha ``:16`` w1, 304 inst_word_alpha ``:16`` w2)]) 305 handle HOL_ERR _ => raise ERR "mk_thumb2_decode" ""; 306 307val dest_error = HolKernel.dest_monop error_tm (ERR "dest_error" "") 308 309val dest_valuestate = 310 HolKernel.dest_binop valuestate_tm (ERR "dest_valuestate" "") 311 312val dest_constT = HolKernel.dest_monop constT_tm (ERR "dest_constT" "") 313val dest_seqT = HolKernel.dest_binop seqT_tm (ERR "dest_seqT" "") 314val dest_parT = HolKernel.dest_binop parT_tm (ERR "dest_parT" "") 315val dest_forT = HolKernel.dest_triop forT_tm (ERR "dest_forT" "") 316val dest_readT = HolKernel.dest_monop readT_tm (ERR "dest_readT" "") 317val dest_writeT = HolKernel.dest_monop writeT_tm (ERR "dest_writeT" "") 318 319val dest_read__reg = 320 HolKernel.dest_binop read__reg_tm (ERR "dest_read__reg" "") 321 322val dest_write__reg = 323 HolKernel.dest_triop write__reg_tm (ERR "dest_write__reg" "") 324 325val dest_read__psr = 326 HolKernel.dest_binop read__psr_tm (ERR "dest_read__psr" "") 327 328val dest_write__psr = 329 HolKernel.dest_triop write__psr_tm (ERR "dest_write__psr" "") 330 331val dest_read_reg_mode = 332 HolKernel.dest_binop read_reg_mode_tm (ERR "dest_read_reg_mode" "") 333 334val dest_write_reg_mode = 335 HolKernel.dest_triop write_reg_mode_tm (ERR "dest_write_reg_mode" "") 336 337val dest_read_reg = dest_binop read_reg_tm (ERR "dest_read_reg" "") 338val dest_write_reg = dest_triop write_reg_tm (ERR "dest_write_reg" "") 339val dest_read_cpsr = dest_monop read_cpsr_tm (ERR "dest_read_cpsr" "") 340val dest_write_cpsr = dest_binop write_cpsr_tm (ERR "dest_write_cpsr" "") 341val dest_read_spsr = dest_monop read_spsr_tm (ERR "dest_read_spsr" "") 342val dest_write_spsr = dest_binop write_spsr_tm (ERR "dest_write_spsr" "") 343val dest_read_memA = dest_binop read_memA_tm (ERR "dest_read_memA" "") 344val dest_write_memA = dest_triop write_memA_tm (ERR "dest_write_memA" "") 345val dest_decode_psr = dest_monop decode_psr_tm (ERR "dest_decode_psr" "") 346val dest_bytes = dest_monop bytes_tm (ERR "dest_bytes" ""); 347val dest_align = dest_monop align_tm (ERR "dest_align" ""); 348val dest_aligned = dest_monop aligned_tm (ERR "dest_align" ""); 349val dest_bit_count = dest_monop bit_count_tm (ERR "dest_bit_count" ""); 350val dest_ITAdvance = dest_monop ITAdvance_tm (ERR "dest_ITAdvance" ""); 351 352val dest_clear_event_register = 353 HolKernel.dest_monop decode_psr_tm (ERR "dest_clear_event_register" ""); 354 355val dest_send_event = 356 HolKernel.dest_monop send_event_tm (ERR "dest_send_event" ""); 357 358val dest_wait_for_interrupt = 359 HolKernel.dest_monop wait_for_interrupt_tm 360 (ERR "dest_wait_for_interrupt" ""); 361 362val dest_clear_wait_for_interrupt = 363 HolKernel.dest_monop clear_wait_for_interrupt_tm 364 (ERR "dest_clear_wait_for_interrupt" ""); 365 366val dest_arm_decode = 367 HolKernel.dest_binop arm_decode_tm (ERR "dest_arm_decode" ""); 368 369val dest_thumb_decode = 370 HolKernel.dest_triop thumb_decode_tm (ERR "dest_thumb_decode" ""); 371 372val dest_thumbee_decode = 373 HolKernel.dest_triop thumbee_decode_tm (ERR "dest_thumbee_decode" ""); 374 375val dest_thumb2_decode = 376 HolKernel.dest_triop thumb2_decode_tm (ERR "dest_thumb2_decode" ""); 377 378val can = Lib.can 379 380val is_error = can dest_error 381val is_valuestate = can dest_valuestate 382 383val is_constT = can dest_constT 384val is_seqT = can dest_seqT 385val is_parT = can dest_parT 386val is_forT = can dest_forT 387val is_readT = can dest_readT 388val is_writeT = can dest_writeT 389 390val is_read__reg = can dest_read__reg 391val is_write__reg = can dest_write__reg 392val is_read__psr = can dest_read__psr 393val is_write__psr = can dest_write__psr 394val is_read_reg_mode = can dest_read_reg_mode 395val is_write_reg_mode = can dest_write_reg_mode 396val is_read_reg = can dest_read_reg 397val is_write_reg = can dest_write_reg 398val is_read_cpsr = can dest_read_cpsr 399val is_write_cpsr = can dest_write_cpsr 400val is_read_spsr = can dest_read_spsr 401val is_write_spsr = can dest_write_spsr 402val is_read_memA = can dest_read_memA 403val is_write_memA = can dest_write_memA 404val is_decode_psr = can dest_decode_psr 405val is_bytes = can dest_bytes 406val is_align = can dest_align 407val is_aligned = can dest_aligned 408val is_bit_count = can dest_bit_count 409val is_ITAdvance = can dest_ITAdvance 410 411val is_clear_event_register = can dest_clear_event_register 412val is_send_event = can dest_send_event 413val is_wait_for_interrupt = can dest_wait_for_interrupt 414val is_clear_wait_for_interrupt = can dest_clear_wait_for_interrupt; 415 416val is_arm_decode = can dest_arm_decode 417val is_thumb_decode = can dest_thumb_decode 418val is_thumbee_decode = can dest_thumbee_decode 419val is_thumb2_decode = can dest_thumb2_decode; 420 421end 422