1structure bitstringSyntax :> bitstringSyntax = 2struct 3 4open Abbrev HolKernel wordsSyntax bitstringTheory 5 6val ERR = mk_HOL_ERR "bitstringSyntax" 7 8(* ----------------------------------------------------------------------- *) 9 10val s = HolKernel.syntax_fns1 "bitstring" 11 12val (n2v_tm, mk_n2v, dest_n2v, is_n2v) = s "n2v" 13val (v2n_tm, mk_v2n, dest_v2n, is_v2n) = s "v2n" 14val (s2v_tm, mk_s2v, dest_s2v, is_s2v) = s "s2v" 15val (v2s_tm, mk_v2s, dest_v2s, is_v2s) = s "v2s" 16val (bnot_tm, mk_bnot, dest_bnot, is_bnot) = s "bnot" 17val (w2v_tm, mk_w2v, dest_w2v, is_w2v) = s "w2v" 18 19(* . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . *) 20 21val (v2w_tm, mk_v2w, dest_v2w, is_v2w) = 22 HolKernel.syntax_fns 23 {n = 1, 24 dest = fn tm1 => fn e => fn w => 25 (HolKernel.dest_monop tm1 e w, wordsSyntax.dim_of w), 26 make = fn tm => fn (v, ty) => 27 Term.mk_comb (Term.inst [Type.alpha |-> ty] tm, v)} 28 "bitstring" "v2w" 29 30(* . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . *) 31 32val s = HolKernel.syntax_fns2 "bitstring" 33 34val (zero_extend_tm, mk_zero_extend, dest_zero_extend, is_zero_extend) = 35 s "zero_extend" 36 37val (sign_extend_tm, mk_sign_extend, dest_sign_extend, is_sign_extend) = 38 s "sign_extend" 39 40val (fixwidth_tm, mk_fixwidth, dest_fixwidth, is_fixwidth) = s "fixwidth" 41val (bitify_tm, mk_bitify, dest_bitify, is_bitify) = s "bitify" 42val (boolify_tm, mk_boolify, dest_boolify, is_boolify) = s "boolify" 43val (testbit_tm, mk_testbit, dest_testbit, is_testbit) = s "testbit" 44val (shiftl_tm, mk_shiftl, dest_shiftl, is_shiftl) = s "shiftl" 45val (shiftr_tm, mk_shiftr, dest_shiftr, is_shiftr) = s "shiftr" 46val (rotate_tm, mk_rotate, dest_rotate, is_rotate) = s "rotate" 47val (modify_tm, mk_modify, dest_modify, is_modify) = s "modify" 48val (add_tm, mk_add, dest_add, is_add) = s "add" 49val (bor_tm, mk_bor, dest_bor, is_bor) = s "bor" 50val (band_tm, mk_band, dest_band, is_band) = s "band" 51val (bxor_tm, mk_bxor, dest_bxor, is_bxor) = s "bxor" 52val (replicate_tm, mk_replicate, dest_replicate, is_replicate) = s "replicate" 53 54(* . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . *) 55 56val s = HolKernel.syntax_fns3 "bitstring" 57 58val (field_tm, mk_field, dest_field, is_field) = s "field" 59val (bitwise_tm, mk_bitwise, dest_bitwise, is_bitwise) = s "bitwise" 60 61(* . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . *) 62 63val s = HolKernel.syntax_fns4 "bitstring" 64 65val (field_insert_tm, mk_field_insert, dest_field_insert, is_field_insert) = 66 s "field_insert" 67 68(* ----------------------------------------------------------------------- *) 69 70local 71 fun bitlist_to_num a l = 72 case l of 73 [] => a 74 | (true::r) => bitlist_to_num (Arbnum.plus1 (Arbnum.times2 a)) r 75 | (false::r) => bitlist_to_num (Arbnum.times2 a) r 76in 77 val bitlist_to_num = bitlist_to_num Arbnum.zero 78end 79 80local 81 fun bitlist_to_hex a = 82 fn [] => a 83 | (b1 :: b2 :: b3 :: b4 :: r) => 84 let 85 val c = [b1, b2, b3, b4] 86 in 87 bitlist_to_hex (a ^ Arbnum.toHexString (bitlist_to_num c)) r 88 end 89 | _ => raise ERR "bitlist_to_hex" "length must be multiple of four" 90in 91 val bitlist_to_hex = bitlist_to_hex "" 92end 93 94fun char_of_bool b = if b then #"1" else #"0" 95 96fun bool_of_term t = 97 boolLib.Teq t orelse not (boolLib.Feq t) andalso raise ERR "bool_of_term" "" 98 99val char_of_term = char_of_bool o bool_of_term 100val list_of_term = fst o listSyntax.dest_list 101 102val bitlist_of_term = List.map bool_of_term o list_of_term 103val binstring_of_term = String.implode o List.map char_of_term o list_of_term 104val hexstring_of_term = bitlist_to_hex o bitlist_of_term 105val num_of_term = bitlist_to_num o bitlist_of_term 106fun mk_fixedwidth (tm, n) = mk_v2w (tm, fcpSyntax.mk_int_numeric_type n) 107 108(* ----------------------------------------------------------------------- *) 109 110val bitstring_ty = listSyntax.mk_list_type Type.bool 111 112fun term_of_bool b = if b then boolSyntax.T else boolSyntax.F 113 114val term_of_char = 115 fn #"1" => boolSyntax.T 116 | #"T" => boolSyntax.T 117 | #"0" => boolSyntax.F 118 | #"F" => boolSyntax.F 119 | _ => raise ERR "term_of_char" "" 120 121val bitstring_of_bitlist = listSyntax.lift_list bitstring_ty term_of_bool 122 123val bitstring_of_binstring = 124 listSyntax.lift_list bitstring_ty term_of_char o String.explode 125 126fun fixedwidth_of_bitlist (l, i) = mk_fixedwidth (bitstring_of_bitlist l, i) 127fun fixedwidth_of_binstring (s, i) = mk_fixedwidth (bitstring_of_binstring s, i) 128fun bitvector_of_bitlist l = fixedwidth_of_bitlist (l, List.length l) 129fun bitvector_of_binstring s = fixedwidth_of_binstring (s, String.size s) 130 131local 132 fun boolify a n = 133 if n = Arbnum.zero then a 134 else let 135 val (q, r) = Arbnum.divmod (n, Arbnum.two) 136 in 137 boolify ((r = Arbnum.one) :: a) q 138 end 139 140 val removeWS = 141 String.translate (fn c => if Char.isSpace c then "" else String.str c) 142 143 fun hexSize s = 144 let 145 val n = String.size s * 4 146 in 147 if String.isPrefix "0x" s then n - 8 else n 148 end 149in 150 fun num_to_bitlist n = if n = Arbnum.zero then [false] else boolify [] n 151 152 val bitstring_of_num = bitstring_of_bitlist o num_to_bitlist 153 fun fixedwidth_of_num (i, j) = mk_fixedwidth (bitstring_of_num i, j) 154 val bitvector_of_num = bitvector_of_bitlist o num_to_bitlist 155 156 fun bitstring_of_hexstring s = 157 let 158 val s = removeWS s 159 val l = num_to_bitlist (Arbnum.fromHexString s) 160 val l = List.tabulate (hexSize s - List.length l, K false) @ l 161 in 162 bitstring_of_bitlist l 163 end 164 165 fun bitvector_of_hexstring s = 166 mk_fixedwidth (bitstring_of_hexstring s, hexSize s) 167 168 fun fixedwidth_of_hexstring (s, i) = 169 mk_fixedwidth (bitstring_of_hexstring s, i) 170end 171 172fun padded_fixedwidth_of_num (m, n) = 173 let 174 val u = num_to_bitlist m 175 val u = String.implode (List.map (fn true => #"1" | false => #"0") u) 176 val p = StringCvt.padLeft #"0" n u 177 in 178 fixedwidth_of_binstring (p, n) 179 end 180 181(* ----------------------------------------------------------------------- *) 182 183fun dest_b tm = 184 if boolLib.Teq tm 185 then true 186 else if boolLib.Feq tm 187 then false 188 else raise ERR "dest_b" "" 189 190fun mk_b b = if b then boolSyntax.T else boolSyntax.F 191 192fun mk_bit n = Term.mk_var ("b" ^ Int.toString n, Type.bool) 193 194(* Make term ``[b(n+w); ... ; b(n)]`` *) 195fun mk_bstring w n = 196 listSyntax.mk_list 197 (List.tabulate (w, fn i => mk_bit (w - i - 1 + n)), Type.bool) 198 199(* Make term ``v2w [b(n+w); ... ; b(n)] : w word`` *) 200fun mk_vec w n = mk_v2w (mk_bstring w n, fcpSyntax.mk_int_numeric_type w) 201 202(* Make term ``v2n [b(n+w); ... ; b(n)]`` *) 203fun mk_nvec w n = mk_v2n (mk_bstring w n) 204 205(* ----------------------------------------------------------------------- *) 206 207end 208