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