-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathword8.ml
252 lines (155 loc) · 8.39 KB
/
word8.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
(*Generated by Lem from word8.lem.*)
(*
Copyright 2016 Sami Mäkelä
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
open Lem_pervasives
open Lem_word
type word8 = W8 of Nat_big_num.num
(* perhaps should truncate here? *)
(*val bs_to_w8 : bitSequence -> word8*)
let bs_to_w8 seq:word8= (W8 (integerFromBitSeq seq))
(*val w8_to_bs : word8 -> bitSequence*)
let w8_to_bs (W8 i):bitSequence= (bitSeqFromInteger (Some( 8)) i)
(*val base : integer*)
let base:Nat_big_num.num= (Nat_big_num.pow_int(Nat_big_num.of_int 2)( 8))
(*val word8BinTest : forall 'a. (integer -> integer -> 'a) -> word8 -> word8 -> 'a*)
let word8BinTest binop (W8 w1) (W8 w2):'a= (binop ( Nat_big_num.modulus w1 base) ( Nat_big_num.modulus w2 base))
(*val word8BBinTest : forall 'a. (bitSequence -> bitSequence -> 'a) -> word8 -> word8 -> 'a*)
let word8BBinTest binop w1 w2:'a= (binop (w8_to_bs w1) (w8_to_bs w2))
(*val word8BinOp : (integer -> integer -> integer) -> word8 -> word8 -> word8*)
let word8BinOp binop (W8 w1) (W8 w2):word8= (W8 ( Nat_big_num.modulus(binop ( Nat_big_num.modulus w1 base) ( Nat_big_num.modulus w2 base)) base))
(*val word8BBinOp : (bitSequence -> bitSequence -> bitSequence) -> word8 -> word8 -> word8*)
let word8BBinOp binop w1 w2:word8= (bs_to_w8 (binop (w8_to_bs w1) (w8_to_bs w2)))
(*val word8NatOp : (integer -> nat -> integer) -> word8 -> nat -> word8*)
let word8NatOp binop (W8 w1) n:word8= (W8 ( Nat_big_num.modulus(binop ( Nat_big_num.modulus w1 base) n) base))
(*val word8BNatOp : (bitSequence -> nat -> bitSequence) -> word8 -> nat -> word8*)
let word8BNatOp binop w1 n:word8= (bs_to_w8 (binop (w8_to_bs w1) n))
(*val word8BUnaryOp : (bitSequence -> bitSequence) -> word8 -> word8*)
let word8BUnaryOp op w:word8= (bs_to_w8 (op (w8_to_bs w)))
(*val word8UnaryOp : (integer -> integer) -> word8 -> word8*)
let word8UnaryOp op (W8 w):word8= (W8 ( Nat_big_num.modulus(op w) base))
(*val word8ToNat : word8 -> nat*)
let word8ToNat w:int= (abs (Nat_big_num.to_int (integerFromBitSeq (w8_to_bs w))))
(*val word8ToInt : word8 -> int*)
let word8ToInt w:int= (Nat_big_num.to_int (integerFromBitSeq (w8_to_bs w)))
(*val word8FromInteger : integer -> word8*)
let word8FromInteger i:word8= (W8 ( Nat_big_num.modulus i base))
(*val word8FromInt : int -> word8*)
let word8FromInt i:word8= (W8 ( Nat_big_num.modulus(Nat_big_num.of_int i) base))
(*val word8FromNat : nat -> word8*)
let word8FromNat i:word8= (word8FromInteger (Nat_big_num.of_int i))
(*val word8FromBoollist : list bool -> word8*)
let word8FromBoollist lst:word8= ((match bitSeqFromBoolList lst with
| None -> bs_to_w8(bitSeqFromInteger None (Nat_big_num.of_int 0))
| Some a -> bs_to_w8 a
))
(*val boolListFromWord8 : word8 -> list bool*)
let boolListFromWord8 w:(bool)list= (boolListFrombitSeq( 8) (w8_to_bs w))
(*val word8FromNumeral : numeral -> word8*)
let word8FromNumeral w:word8= (W8 ( Nat_big_num.modulus(Nat_big_num.of_int w) base))
(*val w8Eq : word8 -> word8 -> bool*)
let w8Eq:word8 ->word8 ->bool= (=)
(*val w8Less : word8 -> word8 -> bool*)
let w8Less bs1 bs2:bool= (word8BinTest Nat_big_num.less bs1 bs2)
(*val w8LessEqual : word8 -> word8 -> bool*)
let w8LessEqual bs1 bs2:bool= (word8BinTest Nat_big_num.less_equal bs1 bs2)
(*val w8Greater : word8 -> word8 -> bool*)
let w8Greater bs1 bs2:bool= (word8BinTest Nat_big_num.greater bs1 bs2)
(*val w8GreaterEqual : word8 -> word8 -> bool*)
let w8GreaterEqual bs1 bs2:bool= (word8BinTest Nat_big_num.greater_equal bs1 bs2)
(*val w8Compare : word8 -> word8 -> ordering*)
let w8Compare bs1 bs2:int= (word8BinTest Nat_big_num.compare bs1 bs2)
let instance_Basic_classes_Ord_Word8_word8_dict:(word8)ord_class= ({
compare_method = w8Compare;
isLess_method = w8Less;
isLessEqual_method = w8LessEqual;
isGreater_method = w8Greater;
isGreaterEqual_method = w8GreaterEqual})
let instance_Basic_classes_SetType_Word8_word8_dict:(word8)setType_class= ({
setElemCompare_method = w8Compare})
(*val word8Negate : word8 -> word8*)
let word8Negate:word8 ->word8= (word8UnaryOp Nat_big_num.negate)
(*val word8Succ : word8 -> word8*)
let word8Succ:word8 ->word8= (word8UnaryOp Nat_big_num.succ)
(*val word8Pred : word8 -> word8*)
let word8Pred:word8 ->word8= (word8UnaryOp Nat_big_num.pred)
(*val word8Lnot : word8 -> word8*)
let word8Lnot:word8 ->word8= (word8UnaryOp integerLnot)
(*val word8Add : word8 -> word8 -> word8*)
let word8Add:word8 ->word8 ->word8= (word8BinOp Nat_big_num.add)
(*val word8Minus : word8 -> word8 -> word8*)
let word8Minus:word8 ->word8 ->word8= (word8BinOp Nat_big_num.sub)
(*val word8Mult : word8 -> word8 -> word8*)
let word8Mult:word8 ->word8 ->word8= (word8BinOp Nat_big_num.mul)
(*val word8IntegerDivision : word8 -> word8 -> word8*)
let word8IntegerDivision:word8 ->word8 ->word8= (word8BinOp Nat_big_num.div)
(*val word8Division : word8 -> word8 -> word8*)
let word8Division:word8 ->word8 ->word8= (word8BinOp Nat_big_num.div)
(*val word8Remainder : word8 -> word8 -> word8*)
let word8Remainder:word8 ->word8 ->word8= (word8BinOp Nat_big_num.modulus)
(*val word8Land : word8 -> word8 -> word8*)
let word8Land:word8 ->word8 ->word8= (word8BinOp Nat_big_num.bitwise_and)
(*val word8Lor : word8 -> word8 -> word8*)
let word8Lor:word8 ->word8 ->word8= (word8BinOp Nat_big_num.bitwise_or)
(*val word8Lxor : word8 -> word8 -> word8*)
let word8Lxor:word8 ->word8 ->word8= (word8BinOp Nat_big_num.bitwise_xor)
(*val word8Min : word8 -> word8 -> word8*)
let word8Min:word8 ->word8 ->word8= (word8BinOp (Nat_big_num.min))
(*val word8Max : word8 -> word8 -> word8*)
let word8Max:word8 ->word8 ->word8= (word8BinOp (Nat_big_num.max))
(*val word8Power : word8 -> nat -> word8*)
let word8Power:word8 ->int ->word8= (word8NatOp Nat_big_num.pow_int)
(*val word8Asr : word8 -> nat -> word8*)
let word8Asr:word8 ->int ->word8= (word8NatOp Nat_big_num.shift_right)
(*val word8Lsr : word8 -> nat -> word8*)
let word8Lsr:word8 ->int ->word8= (word8NatOp Nat_big_num.shift_right)
(*val word8Lsl : word8 -> nat -> word8*)
let word8Lsl:word8 ->int ->word8= (word8NatOp Nat_big_num.shift_left)
let instance_Num_NumNegate_Word8_word8_dict:(word8)numNegate_class= ({
numNegate_method = word8Negate})
let instance_Num_NumAdd_Word8_word8_dict:(word8)numAdd_class= ({
numAdd_method = word8Add})
let instance_Num_NumMinus_Word8_word8_dict:(word8)numMinus_class= ({
numMinus_method = word8Minus})
let instance_Num_NumSucc_Word8_word8_dict:(word8)numSucc_class= ({
succ_method = word8Succ})
let instance_Num_NumPred_Word8_word8_dict:(word8)numPred_class= ({
pred_method = word8Pred})
let instance_Num_NumMult_Word8_word8_dict:(word8)numMult_class= ({
numMult_method = word8Mult})
let instance_Num_NumPow_Word8_word8_dict:(word8)numPow_class= ({
numPow_method = word8Power})
let instance_Num_NumIntegerDivision_Word8_word8_dict:(word8)numIntegerDivision_class= ({
div_method = word8IntegerDivision})
let instance_Num_NumDivision_Word8_word8_dict:(word8)numDivision_class= ({
numDivision_method = word8Division})
let instance_Num_NumRemainder_Word8_word8_dict:(word8)numRemainder_class= ({
mod_method = word8Remainder})
let instance_Basic_classes_OrdMaxMin_Word8_word8_dict:(word8)ordMaxMin_class= ({
max_method = word8Max;
min_method = word8Min})
let instance_Word_WordNot_Word8_word8_dict:(word8)wordNot_class= ({
lnot_method = word8Lnot})
let instance_Word_WordAnd_Word8_word8_dict:(word8)wordAnd_class= ({
land_method = word8Land})
let instance_Word_WordOr_Word8_word8_dict:(word8)wordOr_class= ({
lor_method = word8Lor})
let instance_Word_WordXor_Word8_word8_dict:(word8)wordXor_class= ({
lxor_method = word8Lxor})
let instance_Word_WordLsl_Word8_word8_dict:(word8)wordLsl_class= ({
lsl_method = word8Lsl})
let instance_Word_WordLsr_Word8_word8_dict:(word8)wordLsr_class= ({
lsr_method = word8Lsr})
let instance_Word_WordAsr_Word8_word8_dict:(word8)wordAsr_class= ({
asr_method = word8Asr})
(*val word8UGT : word8 -> word8 -> bool*)
let word8UGT a b:bool= (word8ToNat a > word8ToNat b)