1signature wordsSyntax = 2sig 3 4 include Abbrev 5 type num = Arbnum.num 6 7 val mk_word_type : hol_type -> hol_type 8 val dest_word_type : hol_type -> hol_type 9 val is_word_type : hol_type -> bool 10 val dim_of : term -> hol_type 11 val size_of : term -> num 12 13 val mk_int_word_type : int -> hol_type 14 15 val mk_word : num * num -> term 16 val mk_wordi : num * int -> term 17 val mk_wordii : int * int -> term 18 19 val dest_mod_word_literal : term -> Arbnum.num * Arbnum.num 20 val dest_word_literal : term -> Arbnum.num 21 val is_word_literal : term -> bool 22 val uint_of_word : term -> int 23 24 val add_with_carry_tm : term 25 val bit_count_tm : term 26 val bit_count_upto_tm : term 27 val bit_field_insert_tm : term 28 val bit_set_tm : term 29 val concat_word_list_tm : term 30 val dimindex_tm : term 31 val dimword_tm : term 32 val fcp_index_tm : term 33 val int_max_tm : term 34 val int_min_tm : term 35 val l2w_tm : term 36 val n2w_tm : term 37 val nzcv_tm : term 38 val reduce_and_tm : term 39 val reduce_nand_tm : term 40 val reduce_nor_tm : term 41 val reduce_or_tm : term 42 val reduce_xnor_tm : term 43 val reduce_xor_tm : term 44 val s2w_tm : term 45 val saturate_add_tm : term 46 val saturate_mul_tm : term 47 val saturate_n2w_tm : term 48 val saturate_sub_tm : term 49 val saturate_w2w_tm : term 50 val sw2sw_tm : term 51 val uint_max_tm : term 52 val w2l_tm : term 53 val w2n_tm : term 54 val w2s_tm : term 55 val w2w_tm : term 56 val word_1comp_tm : term 57 val word_2comp_tm : term 58 val word_H_tm : term 59 val word_L2_tm : term 60 val word_L_tm : term 61 val word_T_tm : term 62 val word_abs_tm : term 63 val word_add_tm : term 64 val word_and_tm : term 65 val word_asr_bv_tm : term 66 val word_asr_tm : term 67 val word_bit_tm : term 68 val word_bits_tm : term 69 val word_compare_tm : term 70 val word_concat_tm : term 71 val word_div_tm : term 72 val word_extract_tm : term 73 val word_from_bin_list_tm : term 74 val word_from_bin_string_tm : term 75 val word_from_dec_list_tm : term 76 val word_from_dec_string_tm : term 77 val word_from_hex_list_tm : term 78 val word_from_hex_string_tm : term 79 val word_from_oct_list_tm : term 80 val word_from_oct_string_tm : term 81 val word_ge_tm : term 82 val word_gt_tm : term 83 val word_hi_tm : term 84 val word_hs_tm : term 85 val word_join_tm : term 86 val word_le_tm : term 87 val word_len_tm : term 88 val word_lo_tm : term 89 val word_log2_tm : term 90 val word_ls_tm : term 91 val word_lsb_tm : term 92 val word_lsl_bv_tm : term 93 val word_lsl_tm : term 94 val word_lsr_bv_tm : term 95 val word_lsr_tm : term 96 val word_lt_tm : term 97 val word_max_tm : term 98 val word_min_tm : term 99 val word_mod_tm : term 100 val word_modify_tm : term 101 val word_msb_tm : term 102 val word_mul_tm : term 103 val word_nand_tm : term 104 val word_nor_tm : term 105 val word_or_tm : term 106 val word_quot_tm : term 107 val word_reduce_tm : term 108 val word_rem_tm : term 109 val word_replicate_tm : term 110 val word_reverse_tm : term 111 val word_rol_bv_tm : term 112 val word_rol_tm : term 113 val word_ror_bv_tm : term 114 val word_ror_tm : term 115 val word_rrx_tm : term 116 val word_sign_extend_tm : term 117 val word_slice_tm : term 118 val word_smax_tm : term 119 val word_smin_tm : term 120 val word_sub_tm : term 121 val word_to_bin_list_tm : term 122 val word_to_bin_string_tm : term 123 val word_to_dec_list_tm : term 124 val word_to_dec_string_tm : term 125 val word_to_hex_list_tm : term 126 val word_to_hex_string_tm : term 127 val word_to_oct_list_tm : term 128 val word_to_oct_string_tm : term 129 val word_xnor_tm : term 130 val word_xor_tm : term 131 132 val dest_add_with_carry : term -> term * term * term 133 val dest_bit_count : term -> term 134 val dest_bit_count_upto : term -> term * term 135 val dest_bit_field_insert : term -> term * term * term * term 136 val dest_bit_set : term -> term * term 137 val dest_concat_word_list : term -> term * hol_type 138 val dest_dimindex : term -> hol_type 139 val dest_dimword : term -> hol_type 140 val dest_index : term -> term * term 141 val dest_int_max : term -> hol_type 142 val dest_int_min : term -> hol_type 143 val dest_l2w : term -> term * term * hol_type 144 val dest_n2w : term -> term * hol_type 145 val dest_nzcv : term -> term * term 146 val dest_reduce_and : term -> term 147 val dest_reduce_nand : term -> term 148 val dest_reduce_nor : term -> term 149 val dest_reduce_or : term -> term 150 val dest_reduce_xnor : term -> term 151 val dest_reduce_xor : term -> term 152 val dest_s2w : term -> term * term * term * hol_type 153 val dest_saturate_add : term -> term * term 154 val dest_saturate_mul : term -> term * term 155 val dest_saturate_n2w : term -> term * hol_type 156 val dest_saturate_sub : term -> term * term 157 val dest_saturate_w2w : term -> term * hol_type 158 val dest_sw2sw : term -> term * hol_type 159 val dest_uint_max : term -> hol_type 160 val dest_w2l : term -> term * term 161 val dest_w2n : term -> term 162 val dest_w2s : term -> term * term * term 163 val dest_w2w : term -> term * hol_type 164 val dest_word_1comp : term -> term 165 val dest_word_2comp : term -> term 166 val dest_word_H : term -> hol_type 167 val dest_word_L : term -> hol_type 168 val dest_word_L2 : term -> hol_type 169 val dest_word_T : term -> hol_type 170 val dest_word_abs : term -> term 171 val dest_word_add : term -> term * term 172 val dest_word_and : term -> term * term 173 val dest_word_asr : term -> term * term 174 val dest_word_asr_bv : term -> term * term 175 val dest_word_bit : term -> term * term 176 val dest_word_bits : term -> term * term * term 177 val dest_word_compare : term -> term * term 178 val dest_word_concat : term -> term * term 179 val dest_word_div : term -> term * term 180 val dest_word_extract : term -> term * term * term * hol_type 181 val dest_word_from_bin_list : term -> term * hol_type 182 val dest_word_from_bin_string : term -> term * hol_type 183 val dest_word_from_dec_list : term -> term * hol_type 184 val dest_word_from_dec_string : term -> term * hol_type 185 val dest_word_from_hex_list : term -> term * hol_type 186 val dest_word_from_hex_string : term -> term * hol_type 187 val dest_word_from_oct_list : term -> term * hol_type 188 val dest_word_from_oct_string : term -> term * hol_type 189 val dest_word_ge : term -> term * term 190 val dest_word_gt : term -> term * term 191 val dest_word_hi : term -> term * term 192 val dest_word_hs : term -> term * term 193 val dest_word_join : term -> term * term 194 val dest_word_le : term -> term * term 195 val dest_word_len : term -> term 196 val dest_word_lo : term -> term * term 197 val dest_word_log2 : term -> term 198 val dest_word_ls : term -> term * term 199 val dest_word_lsb : term -> term 200 val dest_word_lsl : term -> term * term 201 val dest_word_lsl_bv : term -> term * term 202 val dest_word_lsr : term -> term * term 203 val dest_word_lsr_bv : term -> term * term 204 val dest_word_lt : term -> term * term 205 val dest_word_max : term -> term * term 206 val dest_word_min : term -> term * term 207 val dest_word_mod : term -> term * term 208 val dest_word_modify : term -> term * term 209 val dest_word_msb : term -> term 210 val dest_word_mul : term -> term * term 211 val dest_word_nand : term -> term * term 212 val dest_word_nor : term -> term * term 213 val dest_word_or : term -> term * term 214 val dest_word_quot : term -> term * term 215 val dest_word_reduce : term -> term * term 216 val dest_word_rem : term -> term * term 217 val dest_word_replicate : term -> term * term 218 val dest_word_reverse : term -> term 219 val dest_word_rol : term -> term * term 220 val dest_word_rol_bv : term -> term * term 221 val dest_word_ror : term -> term * term 222 val dest_word_ror_bv : term -> term * term 223 val dest_word_rrx : term -> term * term 224 val dest_word_sign_extend : term -> term * term 225 val dest_word_slice : term -> term * term * term 226 val dest_word_smax : term -> term * term 227 val dest_word_smin : term -> term * term 228 val dest_word_sub : term -> term * term 229 val dest_word_to_bin_list : term -> term 230 val dest_word_to_bin_string : term -> term 231 val dest_word_to_dec_list : term -> term 232 val dest_word_to_dec_string : term -> term 233 val dest_word_to_hex_list : term -> term 234 val dest_word_to_hex_string : term -> term 235 val dest_word_to_oct_list : term -> term 236 val dest_word_to_oct_string : term -> term 237 val dest_word_xnor : term -> term * term 238 val dest_word_xor : term -> term * term 239 240 val is_add_with_carry : term -> bool 241 val is_bit_count : term -> bool 242 val is_bit_count_upto : term -> bool 243 val is_bit_field_insert : term -> bool 244 val is_bit_set : term -> bool 245 val is_concat_word_list : term -> bool 246 val is_dimindex : term -> bool 247 val is_dimword : term -> bool 248 val is_index : term -> bool 249 val is_int_max : term -> bool 250 val is_int_min : term -> bool 251 val is_l2w : term -> bool 252 val is_n2w : term -> bool 253 val is_nzcv : term -> bool 254 val is_reduce_and : term -> bool 255 val is_reduce_nand : term -> bool 256 val is_reduce_nor : term -> bool 257 val is_reduce_or : term -> bool 258 val is_reduce_xnor : term -> bool 259 val is_reduce_xor : term -> bool 260 val is_s2w : term -> bool 261 val is_saturate_add : term -> bool 262 val is_saturate_mul : term -> bool 263 val is_saturate_n2w : term -> bool 264 val is_saturate_sub : term -> bool 265 val is_saturate_w2w : term -> bool 266 val is_sw2sw : term -> bool 267 val is_uint_max : term -> bool 268 val is_w2l : term -> bool 269 val is_w2n : term -> bool 270 val is_w2s : term -> bool 271 val is_w2w : term -> bool 272 val is_word_1comp : term -> bool 273 val is_word_2comp : term -> bool 274 val is_word_H : term -> bool 275 val is_word_L : term -> bool 276 val is_word_L2 : term -> bool 277 val is_word_T : term -> bool 278 val is_word_abs : term -> bool 279 val is_word_add : term -> bool 280 val is_word_and : term -> bool 281 val is_word_asr : term -> bool 282 val is_word_asr_bv : term -> bool 283 val is_word_bit : term -> bool 284 val is_word_bits : term -> bool 285 val is_word_compare : term -> bool 286 val is_word_concat : term -> bool 287 val is_word_div : term -> bool 288 val is_word_extract : term -> bool 289 val is_word_from_bin_list : term -> bool 290 val is_word_from_bin_string : term -> bool 291 val is_word_from_dec_list : term -> bool 292 val is_word_from_dec_string : term -> bool 293 val is_word_from_hex_list : term -> bool 294 val is_word_from_hex_string : term -> bool 295 val is_word_from_oct_list : term -> bool 296 val is_word_from_oct_string : term -> bool 297 val is_word_ge : term -> bool 298 val is_word_gt : term -> bool 299 val is_word_hi : term -> bool 300 val is_word_hs : term -> bool 301 val is_word_join : term -> bool 302 val is_word_le : term -> bool 303 val is_word_len : term -> bool 304 val is_word_lo : term -> bool 305 val is_word_log2 : term -> bool 306 val is_word_ls : term -> bool 307 val is_word_lsb : term -> bool 308 val is_word_lsl : term -> bool 309 val is_word_lsl_bv : term -> bool 310 val is_word_lsr : term -> bool 311 val is_word_lsr_bv : term -> bool 312 val is_word_lt : term -> bool 313 val is_word_max : term -> bool 314 val is_word_min : term -> bool 315 val is_word_mod : term -> bool 316 val is_word_modify : term -> bool 317 val is_word_msb : term -> bool 318 val is_word_mul : term -> bool 319 val is_word_nand : term -> bool 320 val is_word_nor : term -> bool 321 val is_word_or : term -> bool 322 val is_word_quot : term -> bool 323 val is_word_reduce : term -> bool 324 val is_word_rem : term -> bool 325 val is_word_replicate : term -> bool 326 val is_word_reverse : term -> bool 327 val is_word_rol : term -> bool 328 val is_word_rol_bv : term -> bool 329 val is_word_ror : term -> bool 330 val is_word_ror_bv : term -> bool 331 val is_word_rrx : term -> bool 332 val is_word_sign_extend : term -> bool 333 val is_word_slice : term -> bool 334 val is_word_smax : term -> bool 335 val is_word_smin : term -> bool 336 val is_word_sub : term -> bool 337 val is_word_to_bin_list : term -> bool 338 val is_word_to_bin_string : term -> bool 339 val is_word_to_dec_list : term -> bool 340 val is_word_to_dec_string : term -> bool 341 val is_word_to_hex_list : term -> bool 342 val is_word_to_hex_string : term -> bool 343 val is_word_to_oct_list : term -> bool 344 val is_word_to_oct_string : term -> bool 345 val is_word_xnor : term -> bool 346 val is_word_xor : term -> bool 347 348 val mk_add_with_carry : term * term * term -> term 349 val mk_bit_count_upto : term * term -> term 350 val mk_bit_count : term -> term 351 val mk_bit_field_insert : term * term * term * term -> term 352 val mk_bit_set : term * term -> term 353 val mk_concat_word_list : term * hol_type -> term 354 val mk_dimindex : hol_type -> term 355 val mk_dimword : hol_type -> term 356 val mk_index : term * term -> term 357 val mk_int_max : hol_type -> term 358 val mk_int_min : hol_type -> term 359 val mk_l2w : term * term * hol_type -> term 360 val mk_n2w : term * hol_type -> term 361 val mk_nzcv : term * term -> term 362 val mk_reduce_and : term -> term 363 val mk_reduce_nand : term -> term 364 val mk_reduce_nor : term -> term 365 val mk_reduce_or : term -> term 366 val mk_reduce_xnor : term -> term 367 val mk_reduce_xor : term -> term 368 val mk_s2w : term * term * term * hol_type -> term 369 val mk_saturate_add : term * term -> term 370 val mk_saturate_mul : term * term -> term 371 val mk_saturate_n2w : term * hol_type -> term 372 val mk_saturate_sub : term * term -> term 373 val mk_saturate_w2w : term * hol_type -> term 374 val mk_sw2sw : term * hol_type -> term 375 val mk_uint_max : hol_type -> term 376 val mk_w2l : term * term -> term 377 val mk_w2n : term -> term 378 val mk_w2s : term * term * term -> term 379 val mk_w2w : term * hol_type -> term 380 val mk_word_1comp : term -> term 381 val mk_word_2comp : term -> term 382 val mk_word_H : hol_type -> term 383 val mk_word_L : hol_type -> term 384 val mk_word_L2 : hol_type -> term 385 val mk_word_T : hol_type -> term 386 val mk_word_abs : term -> term 387 val mk_word_add : term * term -> term 388 val mk_word_and : term * term -> term 389 val mk_word_asr : term * term -> term 390 val mk_word_asr_bv : term * term -> term 391 val mk_word_bit : term * term -> term 392 val mk_word_bits : term * term * term -> term 393 val mk_word_compare : term * term -> term 394 val mk_word_concat : term * term -> term 395 val mk_word_div : term * term -> term 396 val mk_word_extract : term * term * term * hol_type -> term 397 val mk_word_from_bin_list : term * hol_type -> term 398 val mk_word_from_bin_string : term * hol_type -> term 399 val mk_word_from_dec_list : term * hol_type -> term 400 val mk_word_from_dec_string : term * hol_type -> term 401 val mk_word_from_hex_list : term * hol_type -> term 402 val mk_word_from_hex_string : term * hol_type -> term 403 val mk_word_from_oct_list : term * hol_type -> term 404 val mk_word_from_oct_string : term * hol_type -> term 405 val mk_word_ge : term * term -> term 406 val mk_word_gt : term * term -> term 407 val mk_word_hi : term * term -> term 408 val mk_word_hs : term * term -> term 409 val mk_word_join : term * term -> term 410 val mk_word_le : term * term -> term 411 val mk_word_len : term -> term 412 val mk_word_lo : term * term -> term 413 val mk_word_log2 : term -> term 414 val mk_word_ls : term * term -> term 415 val mk_word_lsb : term -> term 416 val mk_word_lsl : term * term -> term 417 val mk_word_lsl_bv : term * term -> term 418 val mk_word_lsr : term * term -> term 419 val mk_word_lsr_bv : term * term -> term 420 val mk_word_lt : term * term -> term 421 val mk_word_max : term * term -> term 422 val mk_word_min : term * term -> term 423 val mk_word_mod : term * term -> term 424 val mk_word_modify : term * term -> term 425 val mk_word_msb : term -> term 426 val mk_word_mul : term * term -> term 427 val mk_word_nand : term * term -> term 428 val mk_word_nor : term * term -> term 429 val mk_word_or : term * term -> term 430 val mk_word_quot : term * term -> term 431 val mk_word_reduce : term * term -> term 432 val mk_word_rem : term * term -> term 433 val mk_word_replicate : term * term -> term 434 val mk_word_replicate_ty : term * term * hol_type -> term 435 val mk_word_reverse : term -> term 436 val mk_word_rol : term * term -> term 437 val mk_word_rol_bv : term * term -> term 438 val mk_word_ror : term * term -> term 439 val mk_word_ror_bv : term * term -> term 440 val mk_word_rrx : term * term -> term 441 val mk_word_sign_extend : term * term -> term 442 val mk_word_slice : term * term * term -> term 443 val mk_word_smax : term * term -> term 444 val mk_word_smin : term * term -> term 445 val mk_word_sub : term * term -> term 446 val mk_word_to_bin_list : term -> term 447 val mk_word_to_bin_string : term -> term 448 val mk_word_to_dec_list : term -> term 449 val mk_word_to_dec_string : term -> term 450 val mk_word_to_hex_list : term -> term 451 val mk_word_to_hex_string : term -> term 452 val mk_word_to_oct_list : term -> term 453 val mk_word_to_oct_string : term -> term 454 val mk_word_xnor : term * term -> term 455 val mk_word_xor : term * term -> term 456 457end 458