1signature bitstringSyntax = 2sig 3 4 include Abbrev 5 6 val bitstring_ty : hol_type 7 8 val num_to_bitlist : Arbnum.num -> bool list 9 val bitlist_to_num : bool list -> Arbnum.num 10 11 val bool_of_term : term -> bool 12 val term_of_bool : bool -> term 13 14 val bitlist_of_term : term -> bool list 15 val binstring_of_term : term -> string 16 val hexstring_of_term : term -> string 17 val num_of_term : term -> Arbnum.num 18 19 val bitstring_of_bitlist : bool list -> term 20 val bitstring_of_binstring : string -> term 21 val bitstring_of_hexstring : string -> term 22 val bitstring_of_num : Arbnum.num -> term 23 24 val bitvector_of_bitlist : bool list -> term 25 val bitvector_of_binstring : string -> term 26 val bitvector_of_hexstring : string -> term 27 val bitvector_of_num : Arbnum.num -> term 28 29 val fixedwidth_of_bitlist : bool list * int -> term 30 val fixedwidth_of_binstring : string * int -> term 31 val fixedwidth_of_hexstring : string * int -> term 32 val fixedwidth_of_num : Arbnum.num * int -> term 33 34 val padded_fixedwidth_of_num : Arbnum.num * int -> term 35 36 val dest_b : term -> bool 37 38 val mk_b : bool -> term 39 val mk_bit : int -> term 40 val mk_bstring : int -> int -> term 41 val mk_nvec : int -> int -> term 42 val mk_vec : int -> int -> term 43 val mk_fixedwidth : term * int -> term 44 45 val add_tm : term 46 val band_tm : term 47 val bitify_tm : term 48 val bitwise_tm : term 49 val bnot_tm : term 50 val boolify_tm : term 51 val bor_tm : term 52 val bxor_tm : term 53 val field_insert_tm : term 54 val field_tm : term 55 val fixwidth_tm : term 56 val modify_tm : term 57 val n2v_tm : term 58 val replicate_tm : term 59 val rotate_tm : term 60 val s2v_tm : term 61 val shiftl_tm : term 62 val shiftr_tm : term 63 val sign_extend_tm : term 64 val testbit_tm : term 65 val v2n_tm : term 66 val v2s_tm : term 67 val v2w_tm : term 68 val w2v_tm : term 69 val zero_extend_tm : term 70 71 val dest_add : term -> term * term 72 val dest_band : term -> term * term 73 val dest_bitify : term -> term * term 74 val dest_bitwise : term -> term * term * term 75 val dest_bnot : term -> term 76 val dest_boolify : term -> term * term 77 val dest_bor : term -> term * term 78 val dest_bxor : term -> term * term 79 val dest_field : term -> term * term * term 80 val dest_field_insert : term -> term * term * term * term 81 val dest_fixwidth : term -> term * term 82 val dest_modify : term -> term * term 83 val dest_n2v : term -> term 84 val dest_replicate : term -> term * term 85 val dest_rotate : term -> term * term 86 val dest_s2v : term -> term 87 val dest_shiftl : term -> term * term 88 val dest_shiftr : term -> term * term 89 val dest_sign_extend : term -> term * term 90 val dest_testbit : term -> term * term 91 val dest_v2n : term -> term 92 val dest_v2s : term -> term 93 val dest_v2w : term -> term * hol_type 94 val dest_w2v : term -> term 95 val dest_zero_extend : term -> term * term 96 97 val is_add : term -> bool 98 val is_band : term -> bool 99 val is_bitify : term -> bool 100 val is_bitwise : term -> bool 101 val is_bnot : term -> bool 102 val is_boolify : term -> bool 103 val is_bor : term -> bool 104 val is_bxor : term -> bool 105 val is_field : term -> bool 106 val is_field_insert : term -> bool 107 val is_fixwidth : term -> bool 108 val is_modify : term -> bool 109 val is_n2v : term -> bool 110 val is_replicate : term -> bool 111 val is_rotate : term -> bool 112 val is_s2v : term -> bool 113 val is_shiftl : term -> bool 114 val is_shiftr : term -> bool 115 val is_sign_extend : term -> bool 116 val is_testbit : term -> bool 117 val is_v2n : term -> bool 118 val is_v2s : term -> bool 119 val is_v2w : term -> bool 120 val is_w2v : term -> bool 121 val is_zero_extend : term -> bool 122 123 val mk_add : term * term -> term 124 val mk_band : term * term -> term 125 val mk_bitify : term * term -> term 126 val mk_bitwise : term * term * term -> term 127 val mk_bnot : term -> term 128 val mk_boolify : term * term -> term 129 val mk_bor : term * term -> term 130 val mk_bxor : term * term -> term 131 val mk_field : term * term * term -> term 132 val mk_field_insert : term * term * term * term -> term 133 val mk_fixwidth : term * term -> term 134 val mk_modify : term * term -> term 135 val mk_n2v : term -> term 136 val mk_replicate : term * term -> term 137 val mk_rotate : term * term -> term 138 val mk_s2v : term -> term 139 val mk_shiftl : term * term -> term 140 val mk_shiftr : term * term -> term 141 val mk_sign_extend : term * term -> term 142 val mk_testbit : term * term -> term 143 val mk_v2n : term -> term 144 val mk_v2s : term -> term 145 val mk_v2w : term * hol_type -> term 146 val mk_w2v : term -> term 147 val mk_zero_extend : term * term -> term 148 149end 150