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