1structure wordsSyntax :> wordsSyntax = 2struct 3 4open HolKernel Parse boolLib bossLib 5open bitSyntax fcpSyntax fcpLib wordsTheory 6 7val ERR = mk_HOL_ERR "wordsSyntax" 8 9fun syntax_fns n d m = HolKernel.syntax_fns {n = n, dest = d, make = m} "words" 10 11(*---------------------------------------------------------------------------*) 12(* Word types *) 13(*---------------------------------------------------------------------------*) 14 15fun mk_word_type ty = fcpSyntax.mk_cart_type (Type.bool, ty) 16 17val mk_int_word_type = mk_word_type o fcpSyntax.mk_int_numeric_type 18 19fun dest_word_type ty = 20 let 21 val (a, b) = fcpSyntax.dest_cart_type ty 22 val _ = a = Type.bool orelse 23 raise ERR "dest_word_type" "not an instance of :bool['a]" 24 in 25 b 26 end 27 28val is_word_type = Lib.can dest_word_type 29val dim_of = dest_word_type o Term.type_of 30val size_of = fcpLib.index_to_num o dim_of 31 32(*---------------------------------------------------------------------------*) 33(* Terms, Constructors, Destructors and Discriminators *) 34(*---------------------------------------------------------------------------*) 35 36val fcp_index_tm = fcpSyntax.fcp_index_tm 37 38fun mk_index (w, n) = 39 Lib.with_exn HolKernel.list_mk_comb 40 (Term.inst [Type.alpha |-> Type.bool, Type.beta |-> dim_of w] fcp_index_tm, 41 [w, n]) 42 (ERR "mk_index" "") 43 44val dest_index = fcpSyntax.dest_fcp_index 45val is_index = Lib.can dest_index 46 47val dimindex_tm = fcpSyntax.dimindex_tm 48val mk_dimindex = fcpSyntax.mk_dimindex 49val dest_dimindex = fcpSyntax.dest_dimindex 50val is_dimindex = Lib.can dest_dimindex 51 52(* - - - - - - - - - - - - - - - - - - - - - - *) 53 54val s = syntax_fns 0 55 (fn tm1 => fn e => fn tm2 => 56 if Term.same_const tm1 tm2 then dim_of tm2 else raise e) 57 (fn tm => fn ty => Term.inst [Type.alpha |-> ty] tm) 58 59val (word_T_tm, mk_word_T, dest_word_T, is_word_T) = s "word_T" 60val (word_L_tm, mk_word_L, dest_word_L, is_word_L) = s "word_L" 61val (word_H_tm, mk_word_H, dest_word_H, is_word_H) = s "word_H" 62val (word_L2_tm, mk_word_L2, dest_word_L2, is_word_L2) = s "word_L2" 63 64(* - - - - - - - - - - - - - - - - - - - - - - *) 65 66val s = syntax_fns 1 67 (fn tm1 => fn e => boolSyntax.dest_itself o HolKernel.dest_monop tm1 e) 68 (fn tm => fn ty => 69 Term.mk_comb (Term.inst [Type.alpha |-> ty] tm, boolSyntax.mk_itself ty)) 70 71val (dimword_tm, mk_dimword, dest_dimword, is_dimword) = s "dimword" 72val (uint_max_tm, mk_uint_max, dest_uint_max, is_uint_max) = s "UINT_MAX" 73val (int_min_tm, mk_int_min, dest_int_min, is_int_min) = s "INT_MIN" 74val (int_max_tm, mk_int_max, dest_int_max, is_int_max) = s "INT_MAX" 75 76(* - - - - - - - - - - - - - - - - - - - - - - *) 77 78val s = HolKernel.syntax_fns1 "words" 79 80val (w2n_tm, mk_w2n, dest_w2n, is_w2n) = s "w2n" 81val (word_abs_tm, mk_word_abs, dest_word_abs, is_word_abs) = s "word_abs" 82val (word_len_tm, mk_word_len, dest_word_len, is_word_len) = s "word_len" 83val (word_log2_tm, mk_word_log2, dest_word_log2, is_word_log2) = s "word_log2" 84val (word_msb_tm, mk_word_msb, dest_word_msb, is_word_msb) = s "word_msb" 85val (word_lsb_tm, mk_word_lsb, dest_word_lsb, is_word_lsb) = s "word_lsb" 86val (bit_count_tm, mk_bit_count, dest_bit_count, is_bit_count) = s "bit_count" 87val (reduce_or_tm, mk_reduce_or, dest_reduce_or, is_reduce_or) = s "reduce_or" 88 89val (reduce_and_tm, mk_reduce_and, dest_reduce_and, is_reduce_and) = 90 s "reduce_and" 91 92val (reduce_nand_tm, mk_reduce_nand, dest_reduce_nand, is_reduce_nand) = 93 s "reduce_nand" 94 95val (reduce_nor_tm, mk_reduce_nor, dest_reduce_nor, is_reduce_nor) = 96 s "reduce_nor" 97 98val (reduce_xnor_tm, mk_reduce_xnor, dest_reduce_xnor, is_reduce_xnor) = 99 s "reduce_xnor" 100 101val (reduce_xor_tm, mk_reduce_xor, dest_reduce_xor, is_reduce_xor) = 102 s "reduce_xor" 103 104val (word_1comp_tm, mk_word_1comp, dest_word_1comp, is_word_1comp) = 105 s "word_1comp" 106 107val (word_2comp_tm, mk_word_2comp, dest_word_2comp, is_word_2comp) = 108 s "word_2comp" 109 110val (word_reverse_tm, mk_word_reverse, dest_word_reverse, is_word_reverse) = 111 s "word_reverse" 112 113val (word_to_bin_list_tm, mk_word_to_bin_list, 114 dest_word_to_bin_list, is_word_to_bin_list) = s "word_to_bin_list" 115 116val (word_to_oct_list_tm, mk_word_to_oct_list, 117 dest_word_to_oct_list, is_word_to_oct_list) = s "word_to_oct_list" 118 119val (word_to_dec_list_tm, mk_word_to_dec_list, 120 dest_word_to_dec_list, is_word_to_dec_list) = s "word_to_dec_list" 121 122val (word_to_hex_list_tm, mk_word_to_hex_list, 123 dest_word_to_hex_list, is_word_to_hex_list) = s "word_to_hex_list" 124 125val (word_to_bin_string_tm, mk_word_to_bin_string, 126 dest_word_to_bin_string, is_word_to_bin_string) = s "word_to_bin_string" 127 128val (word_to_oct_string_tm, mk_word_to_oct_string, 129 dest_word_to_oct_string, is_word_to_oct_string) = s "word_to_oct_string" 130 131val (word_to_dec_string_tm, mk_word_to_dec_string, 132 dest_word_to_dec_string, is_word_to_dec_string) = s "word_to_dec_string" 133 134val (word_to_hex_string_tm, mk_word_to_hex_string, 135 dest_word_to_hex_string, is_word_to_hex_string) = s "word_to_hex_string" 136 137(* - - - - - - - - - - - - - - - - - - - - - - *) 138 139val s = syntax_fns 1 140 (fn tm => fn e => pairSyntax.dest_pair o HolKernel.dest_monop tm e) 141 (fn tm => fn (x, w) => 142 Term.mk_comb (Term.inst [Type.alpha |-> dim_of w] tm, 143 pairSyntax.mk_pair (x, w))) 144 145val (word_rrx_tm, mk_word_rrx, dest_word_rrx, is_word_rrx) = s "word_rrx" 146 147(* - - - - - - - - - - - - - - - - - - - - - - *) 148 149val s = syntax_fns 1 150 (fn tm => fn e => fn x => 151 let 152 val (a, y) = pairSyntax.dest_pair (HolKernel.dest_monop tm e x) 153 val (b, c) = pairSyntax.dest_pair y 154 in 155 (a, b, c) 156 end) 157 (fn tm => fn (a, b, c) => 158 Term.mk_comb (Term.inst [Type.alpha |-> dim_of a] tm, 159 pairSyntax.list_mk_pair [a, b, c])) 160 161val (add_with_carry_tm, mk_add_with_carry, 162 dest_add_with_carry, is_add_with_carry) = s "add_with_carry" 163 164(* - - - - - - - - - - - - - - - - - - - - - - *) 165 166val s = syntax_fns 1 167 (fn tm1 => fn e => fn w => (HolKernel.dest_monop tm1 e w, dim_of w)) 168 (fn tm => fn (w, ty) => Term.mk_comb (Term.inst [Type.alpha |-> ty] tm, w)) 169 170val (n2w_tm, mk_n2w, dest_n2w, is_n2w) = s "n2w" 171 172val (saturate_n2w_tm, mk_saturate_n2w, dest_saturate_n2w, is_saturate_n2w) = 173 s "saturate_n2w" 174 175val (word_from_bin_list_tm, mk_word_from_bin_list, 176 dest_word_from_bin_list, is_word_from_bin_list) = s "word_from_bin_list" 177 178val (word_from_oct_list_tm, mk_word_from_oct_list, 179 dest_word_from_oct_list, is_word_from_oct_list) = s "word_from_oct_list" 180 181val (word_from_dec_list_tm, mk_word_from_dec_list, 182 dest_word_from_dec_list, is_word_from_dec_list) = s "word_from_dec_list" 183 184val (word_from_hex_list_tm, mk_word_from_hex_list, 185 dest_word_from_hex_list, is_word_from_hex_list) = s "word_from_hex_list" 186 187val (word_from_bin_string_tm, mk_word_from_bin_string, 188 dest_word_from_bin_string, is_word_from_bin_string) = 189 s "word_from_bin_string" 190 191val (word_from_oct_string_tm, mk_word_from_oct_string, 192 dest_word_from_oct_string, is_word_from_oct_string) = 193 s "word_from_oct_string" 194 195val (word_from_dec_string_tm, mk_word_from_dec_string, 196 dest_word_from_dec_string, is_word_from_dec_string) = 197 s "word_from_dec_string" 198 199val (word_from_hex_string_tm, mk_word_from_hex_string, 200 dest_word_from_hex_string, is_word_from_hex_string) = s 201 "word_from_hex_string" 202 203(* - - - - - - - - - - - - - - - - - - - - - - *) 204 205val s = syntax_fns 1 206 (fn tm1 => fn e => fn w => (HolKernel.dest_monop tm1 e w, dim_of w)) 207 (fn tm => fn (w, ty) => 208 Term.mk_comb 209 (Term.inst [Type.alpha |-> dim_of w, Type.beta |-> ty] tm, w)) 210 211val (w2w_tm, mk_w2w, dest_w2w, is_w2w) = s "w2w" 212val (sw2sw_tm, mk_sw2sw, dest_sw2sw, is_sw2sw) = s "sw2sw" 213 214val (saturate_w2w_tm, mk_saturate_w2w, dest_saturate_w2w, is_saturate_w2w) = 215 s "saturate_w2w" 216 217(* - - - - - - - - - - - - - - - - - - - - - - *) 218 219val s = syntax_fns 1 220 (fn tm1 => fn e => fn w => (HolKernel.dest_monop tm1 e w, dim_of w)) 221 (fn tm => fn (l, ty) => 222 let 223 val d = dest_word_type (listSyntax.dest_list_type (Term.type_of l)) 224 in 225 Term.mk_comb (Term.inst [Type.alpha |-> d, Type.beta |-> ty] tm, l) 226 end) 227 228val (concat_word_list_tm, mk_concat_word_list, 229 dest_concat_word_list, is_concat_word_list) = s "concat_word_list" 230 231(* - - - - - - - - - - - - - - - - - - - - - - *) 232 233val s = HolKernel.syntax_fns2 "words" 234 235val (w2l_tm, mk_w2l, dest_w2l, is_w2l) = s "w2l" 236val (nzcv_tm, mk_nzcv, dest_nzcv, is_nzcv) = s "nzcv" 237val (word_lt_tm, mk_word_lt, dest_word_lt, is_word_lt) = s "word_lt" 238val (word_le_tm, mk_word_le, dest_word_le, is_word_le) = s "word_le" 239val (word_gt_tm, mk_word_gt, dest_word_gt, is_word_gt) = s "word_gt" 240val (word_ge_tm, mk_word_ge, dest_word_ge, is_word_ge) = s "word_ge" 241val (word_lo_tm, mk_word_lo, dest_word_lo, is_word_lo) = s "word_lo" 242val (word_ls_tm, mk_word_ls, dest_word_ls, is_word_ls) = s "word_ls" 243val (word_hi_tm, mk_word_hi, dest_word_hi, is_word_hi) = s "word_hi" 244val (word_hs_tm, mk_word_hs, dest_word_hs, is_word_hs) = s "word_hs" 245val (word_or_tm, mk_word_or, dest_word_or, is_word_or) = s "word_or" 246val (word_and_tm, mk_word_and, dest_word_and, is_word_and) = s "word_and" 247val (word_xor_tm, mk_word_xor, dest_word_xor, is_word_xor) = s "word_xor" 248val (word_nor_tm, mk_word_nor, dest_word_nor, is_word_nor) = s "word_nor" 249val (word_nand_tm, mk_word_nand, dest_word_nand, is_word_nand) = s "word_nand" 250val (word_xnor_tm, mk_word_xnor, dest_word_xnor, is_word_xnor) = s "word_xnor" 251val (word_add_tm, mk_word_add, dest_word_add, is_word_add) = s "word_add" 252val (word_sub_tm, mk_word_sub, dest_word_sub, is_word_sub) = s "word_sub" 253val (word_mul_tm, mk_word_mul, dest_word_mul, is_word_mul) = s "word_mul" 254val (word_div_tm, mk_word_div, dest_word_div, is_word_div) = s "word_div" 255val (word_mod_tm, mk_word_mod, dest_word_mod, is_word_mod) = s "word_mod" 256val (word_quot_tm, mk_word_quot, dest_word_quot, is_word_quot) = s "word_quot" 257val (word_rem_tm, mk_word_rem, dest_word_rem, is_word_rem) = s "word_rem" 258val (word_smin_tm, mk_word_smin, dest_word_smin, is_word_smin) = s "word_smin" 259val (word_smax_tm, mk_word_smax, dest_word_smax, is_word_smax) = s "word_smax" 260val (word_min_tm, mk_word_min, dest_word_min, is_word_min) = s "word_min" 261val (word_max_tm, mk_word_max, dest_word_max, is_word_max) = s "word_max" 262val (word_lsl_tm, mk_word_lsl, dest_word_lsl, is_word_lsl) = s "word_lsl" 263val (word_lsr_tm, mk_word_lsr, dest_word_lsr, is_word_lsr) = s "word_lsr" 264val (word_asr_tm, mk_word_asr, dest_word_asr, is_word_asr) = s "word_asr" 265val (word_ror_tm, mk_word_ror, dest_word_ror, is_word_ror) = s "word_ror" 266val (word_rol_tm, mk_word_rol, dest_word_rol, is_word_rol) = s "word_rol" 267val (word_bit_tm, mk_word_bit, dest_word_bit, is_word_bit) = s "word_bit" 268 269val (word_lsl_bv_tm, mk_word_lsl_bv, dest_word_lsl_bv, is_word_lsl_bv) = 270 s "word_lsl_bv" 271 272val (word_lsr_bv_tm, mk_word_lsr_bv, dest_word_lsr_bv, is_word_lsr_bv) = 273 s "word_lsr_bv" 274 275val (word_asr_bv_tm, mk_word_asr_bv, dest_word_asr_bv, is_word_asr_bv) = 276 s "word_asr_bv" 277 278val (word_ror_bv_tm, mk_word_ror_bv, dest_word_ror_bv, is_word_ror_bv) = 279 s "word_ror_bv" 280 281val (word_rol_bv_tm, mk_word_rol_bv, dest_word_rol_bv, is_word_rol_bv) = 282 s "word_rol_bv" 283 284val (word_compare_tm, mk_word_compare, dest_word_compare, is_word_compare) = 285 s "word_compare" 286 287val (saturate_add_tm, mk_saturate_add, dest_saturate_add, is_saturate_add) = 288 s "saturate_add" 289 290val (saturate_sub_tm, mk_saturate_sub, dest_saturate_sub, is_saturate_sub) = 291 s "saturate_sub" 292 293val (saturate_mul_tm, mk_saturate_mul, dest_saturate_mul, is_saturate_mul) = 294 s "saturate_mul" 295 296val (word_modify_tm, mk_word_modify, dest_word_modify, is_word_modify) = 297 s "word_modify" 298 299val (word_reduce_tm, mk_word_reduce, dest_word_reduce, is_word_reduce) = 300 s "word_reduce" 301 302val (bit_count_upto_tm, mk_bit_count_upto, 303 dest_bit_count_upto, is_bit_count_upto) = s "bit_count_upto" 304 305val (word_sign_extend_tm, mk_word_sign_extend, 306 dest_word_sign_extend, is_word_sign_extend) = s "word_sign_extend" 307 308val (word_join_tm, mk_word_join, dest_word_join, is_word_join) = s "word_join" 309 310(* - - - - - - - - - - - - - - - - - - - - - - *) 311 312val s = syntax_fns 2 313 (fn tm1 => fn e => fn w => 314 let val (n, l) = HolKernel.dest_binop tm1 e w in (n, l, dim_of w) end) 315 (fn tm => fn (n, l, ty) => 316 Term.list_mk_comb (Term.inst [Type.alpha |-> ty] tm, [n, l])) 317 318val (l2w_tm, mk_l2w, dest_l2w, is_l2w) = s "l2w" 319 320(* - - - - - - - - - - - - - - - - - - - - - - *) 321 322val s = syntax_fns 2 HolKernel.dest_binop 323 (fn tm => fn (w1, w2) => 324 let 325 val d1 = dim_of w1 326 val d2 = dim_of w2 327 val d3 = fcpLib.index_type 328 (Arbnum.+ (fcpLib.index_to_num d1, fcpLib.index_to_num d2)) 329 handle HOL_ERR _ => Type.gamma 330 in 331 Term.list_mk_comb 332 (Term.inst [Type.alpha |-> d1, Type.beta |-> d2, 333 Type.gamma |-> d3] tm, [w1, w2]) 334 end) 335 336val (word_concat_tm, mk_word_concat, dest_word_concat, is_word_concat) = 337 s "word_concat" 338 339(* - - - - - - - - - - - - - - - - - - - - - - *) 340 341val s = syntax_fns 2 HolKernel.dest_binop 342 (fn tm => fn (n, w) => 343 let 344 val d1 = dim_of w 345 val d2 = fcpLib.index_type 346 (Arbnum.* (fcpLib.index_to_num d1, 347 numSyntax.dest_numeral n)) 348 handle HOL_ERR _ => Type.beta 349 in 350 Term.list_mk_comb 351 (Term.inst [Type.alpha |-> d1, Type.beta |-> d2] tm, [n, w]) 352 end) 353 354val (word_replicate_tm, mk_word_replicate, 355 dest_word_replicate, is_word_replicate) = s "word_replicate" 356 357fun mk_word_replicate_ty (n, w, ty) = 358 Term.list_mk_comb 359 (Term.inst [Type.alpha |-> dim_of w, Type.beta |-> ty] word_replicate_tm, 360 [n, w]) 361 362(* - - - - - - - - - - - - - - - - - - - - - - *) 363 364val (bit_set_tm, mk_bit_set, dest_bit_set, is_bit_set) = 365 syntax_fns 3 HolKernel.dest_binop HolKernel.mk_binop "BIT_SET" 366 367(* - - - - - - - - - - - - - - - - - - - - - - *) 368 369val s = HolKernel.syntax_fns3 "words" 370 371val (word_bits_tm, mk_word_bits, dest_word_bits, is_word_bits) = s "word_bits" 372 373val (word_slice_tm, mk_word_slice, dest_word_slice, is_word_slice) = 374 s "word_slice" 375 376val (w2s_tm, mk_w2s, dest_w2s, is_w2s) = s "w2s" 377 378(* - - - - - - - - - - - - - - - - - - - - - - *) 379 380val s = syntax_fns 3 381 (fn tm1 => fn e => fn w => 382 let 383 val (n1, n2, s) = HolKernel.dest_triop tm1 e w 384 in 385 (n1, n2, w, dim_of w) 386 end) 387 (fn tm => fn (n1, n2, n3, ty) => 388 Term.list_mk_comb (Term.inst [Type.alpha |-> ty] tm, [n1, n2, n3])) 389 390val (s2w_tm, mk_s2w, dest_s2w, is_s2w) = s "s2w" 391 392(* - - - - - - - - - - - - - - - - - - - - - - *) 393 394val s = syntax_fns 3 395 (fn tm1 => fn e => fn w => 396 let 397 val (n1, n2, w1) = HolKernel.dest_triop tm1 e w 398 in 399 (n1, n2, w1, dim_of w) 400 end) 401 (fn tm => fn (n1, n2, w, ty) => 402 Term.list_mk_comb 403 (Term.inst [Type.alpha |-> dim_of w, Type.beta |-> ty] tm, 404 [n1, n2, w])) 405 406val (word_extract_tm, mk_word_extract, dest_word_extract, is_word_extract) = 407 s "word_extract" 408 409(* - - - - - - - - - - - - - - - - - - - - - - *) 410 411val s = HolKernel.syntax_fns4 "words" 412 413val (bit_field_insert_tm, mk_bit_field_insert, 414 dest_bit_field_insert, is_bit_field_insert) = s "bit_field_insert" 415 416(*---------------------------------------------------------------------------*) 417 418fun mk_word (v, n) = mk_n2w (numSyntax.mk_numeral v, fcpLib.index_type n) 419fun mk_wordi (v, i) = mk_word (v, Arbnum.fromInt i) 420fun mk_wordii (v, i) = mk_wordi (Arbnum.fromInt v, i) 421 422val dest_word_literal = numSyntax.dest_numeral o fst o dest_n2w 423 424val is_word_literal = Lib.can dest_word_literal 425 426val uint_of_word = numSyntax.int_of_term o fst o dest_n2w 427 428fun mod_2exp (m, n) = 429 if n = Arbnum.zero orelse m = Arbnum.zero 430 then Arbnum.zero 431 else let 432 val v = Arbnum.times2 (mod_2exp (Arbnum.div2 m, Arbnum.less1 n)) 433 in 434 if Arbnum.mod2 m = Arbnum.zero then v else Arbnum.plus1 v 435 end 436 437fun dest_mod_word_literal tm = 438 let 439 val (tm1, ty) = dest_n2w tm 440 val sz = fcpLib.index_to_num ty 441 in 442 (mod_2exp (numSyntax.dest_numeral tm1, sz), sz) 443 end handle HOL_ERR _ => raise ERR "dest_mod_word_literal" "" 444 445end 446