git.iko.soy/Idris-dev
on master help sign in
Make export modifiers consistent.
1f6965bMatus Tejiscak
libs/base/Data/Bits.idr+57−92
compare with master
unifiedsplit
@@ -3,6 +3,7 @@ module Data.Bits
3import Data.Fin
3import Data.Fin
4
4
5%default total
5%default total
6+%access export
6
7
7public export
8public export
8nextPow2 : Nat -> Nat
9nextPow2 : Nat -> Nat
@@ -28,7 +29,7 @@ bitsUsed : Nat -> Nat
28bitsUsed n = 8 * (2 `power` n)
29bitsUsed n = 8 * (2 `power` n)
29
30
30%assert_total
31%assert_total
31−natToBits' : [static] {n : Nat} -> machineTy n -> Nat -> machineTy n
32+natToBits' : %static {n : Nat} -> machineTy n -> Nat -> machineTy n
32natToBits' a Z = a
33natToBits' a Z = a
33natToBits' {n=n} a x with (n)
34natToBits' {n=n} a x with (n)
34 -- it seems I have to manually recover the value of n here, instead of being able to reference it
35 -- it seems I have to manually recover the value of n here, instead of being able to reference it
@@ -37,14 +38,14 @@ natToBits' {n=n} a x with (n)
37 natToBits' a (S x') | S (S Z) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x'
38 natToBits' a (S x') | S (S Z) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x'
38 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'
39 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'
39
40
40−natToBits : [static] {n : Nat} -> Nat -> machineTy n
41+natToBits : %static {n : Nat} -> Nat -> machineTy n
41natToBits {n=n} x with (n)
42natToBits {n=n} x with (n)
42 | Z = natToBits' {n=0} (prim__truncInt_B8 0) x
43 | Z = natToBits' {n=0} (prim__truncInt_B8 0) x
43 | S Z = natToBits' {n=1} (prim__truncInt_B16 0) x
44 | S Z = natToBits' {n=1} (prim__truncInt_B16 0) x
44 | S (S Z) = natToBits' {n=2} (prim__truncInt_B32 0) x
45 | S (S Z) = natToBits' {n=2} (prim__truncInt_B32 0) x
45 | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x
46 | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x
46
47
47−getPad : [static] {n : Nat} -> Nat -> machineTy n
48+getPad : %static {n : Nat} -> Nat -> machineTy n
48getPad n = natToBits (minus (bitsUsed (nextBytes n)) n)
49getPad n = natToBits (minus (bitsUsed (nextBytes n)) n)
49
50
50public export
51public export
@@ -92,81 +93,69 @@ pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
92 where
93 where
93 pad = getPad {n=3} n
94 pad = getPad {n=3} n
94
95
95−-- TODO: This (and all the other functions along these lings) is public export
96+-- TODO: This (and all the other functions along these lings) is -- because it is used by things. Do they really need to be
96−-- because it is used by public export things. Do they really need to be
97-- public export, or is export good enough?
97-- public export, or is export good enough?
98−public export
99−shiftLeft' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
98+shiftLeft' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
100shiftLeft' {n=n} x c with (nextBytes n)
99shiftLeft' {n=n} x c with (nextBytes n)
101 | Z = pad8' n prim__shlB8 x c
100 | Z = pad8' n prim__shlB8 x c
102 | S Z = pad16' n prim__shlB16 x c
101 | S Z = pad16' n prim__shlB16 x c
103 | S (S Z) = pad32' n prim__shlB32 x c
102 | S (S Z) = pad32' n prim__shlB32 x c
104 | S (S (S _)) = pad64' n prim__shlB64 x c
103 | S (S (S _)) = pad64' n prim__shlB64 x c
105
104
106−public export
107−shiftLeft : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
105+shiftLeft : %static {n : Nat} -> Bits n -> Bits n -> Bits n
108shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
106shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
109
107
110−public export
111−shiftRightLogical' : [static] {n : Nat} -> machineTy n -> machineTy n -> machineTy n
108+shiftRightLogical' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
112shiftRightLogical' {n=n} x c with (n)
109shiftRightLogical' {n=n} x c with (n)
113 | Z = prim__lshrB8 x c
110 | Z = prim__lshrB8 x c
114 | S Z = prim__lshrB16 x c
111 | S Z = prim__lshrB16 x c
115 | S (S Z) = prim__lshrB32 x c
112 | S (S Z) = prim__lshrB32 x c
116 | S (S (S _)) = prim__lshrB64 x c
113 | S (S (S _)) = prim__lshrB64 x c
117
114
118−public export
119−shiftRightLogical : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
115+shiftRightLogical : %static {n : Nat} -> Bits n -> Bits n -> Bits n
120shiftRightLogical {n} (MkBits x) (MkBits y)
116shiftRightLogical {n} (MkBits x) (MkBits y)
121 = MkBits {n} (shiftRightLogical' {n=nextBytes n} x y)
117 = MkBits {n} (shiftRightLogical' {n=nextBytes n} x y)
122
118
123−public export
124−shiftRightArithmetic' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
119+shiftRightArithmetic' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
125shiftRightArithmetic' {n=n} x c with (nextBytes n)
120shiftRightArithmetic' {n=n} x c with (nextBytes n)
126 | Z = pad8' n prim__ashrB8 x c
121 | Z = pad8' n prim__ashrB8 x c
127 | S Z = pad16' n prim__ashrB16 x c
122 | S Z = pad16' n prim__ashrB16 x c
128 | S (S Z) = pad32' n prim__ashrB32 x c
123 | S (S Z) = pad32' n prim__ashrB32 x c
129 | S (S (S _)) = pad64' n prim__ashrB64 x c
124 | S (S (S _)) = pad64' n prim__ashrB64 x c
130
125
131−public export
132−shiftRightArithmetic : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
126+shiftRightArithmetic : %static {n : Nat} -> Bits n -> Bits n -> Bits n
133shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
127shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
134
128
135−public export
136−and' : [static] {n : Nat} -> machineTy n -> machineTy n -> machineTy n
129+and' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
137and' {n=n} x y with (n)
130and' {n=n} x y with (n)
138 | Z = prim__andB8 x y
131 | Z = prim__andB8 x y
139 | S Z = prim__andB16 x y
132 | S Z = prim__andB16 x y
140 | S (S Z) = prim__andB32 x y
133 | S (S Z) = prim__andB32 x y
141 | S (S (S _)) = prim__andB64 x y
134 | S (S (S _)) = prim__andB64 x y
142
135
143−public export
144−and : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
136+and : %static {n : Nat} -> Bits n -> Bits n -> Bits n
145and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)
137and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)
146
138
147−or' : [static] {n : Nat} -> machineTy n -> machineTy n -> machineTy n
139+or' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
148or' {n=n} x y with (n)
140or' {n=n} x y with (n)
149 | Z = prim__orB8 x y
141 | Z = prim__orB8 x y
150 | S Z = prim__orB16 x y
142 | S Z = prim__orB16 x y
151 | S (S Z) = prim__orB32 x y
143 | S (S Z) = prim__orB32 x y
152 | S (S (S _)) = prim__orB64 x y
144 | S (S (S _)) = prim__orB64 x y
153
145
154−public export
155−or : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
146+or : %static {n : Nat} -> Bits n -> Bits n -> Bits n
156or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)
147or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)
157
148
158−xor' : [static] {n : Nat} -> machineTy n -> machineTy n -> machineTy n
149+xor' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
159xor' {n=n} x y with (n)
150xor' {n=n} x y with (n)
160 | Z = prim__xorB8 x y
151 | Z = prim__xorB8 x y
161 | S Z = prim__xorB16 x y
152 | S Z = prim__xorB16 x y
162 | S (S Z) = prim__xorB32 x y
153 | S (S Z) = prim__xorB32 x y
163 | S (S (S _)) = prim__xorB64 x y
154 | S (S (S _)) = prim__xorB64 x y
164
155
165−public export
166−xor : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
156+xor : %static {n : Nat} -> Bits n -> Bits n -> Bits n
167xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)
157xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)
168
158
169−public export
170plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
159plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
171plus' {n=n} x y with (nextBytes n)
160plus' {n=n} x y with (nextBytes n)
172 | Z = pad8 n prim__addB8 x y
161 | Z = pad8 n prim__addB8 x y
@@ -174,11 +163,9 @@ plus' {n=n} x y with (nextBytes n)
174 | S (S Z) = pad32 n prim__addB32 x y
163 | S (S Z) = pad32 n prim__addB32 x y
175 | S (S (S _)) = pad64 n prim__addB64 x y
164 | S (S (S _)) = pad64 n prim__addB64 x y
176
165
177−public export
178−plus : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
166+plus : %static {n : Nat} -> Bits n -> Bits n -> Bits n
179plus (MkBits x) (MkBits y) = MkBits (plus' x y)
167plus (MkBits x) (MkBits y) = MkBits (plus' x y)
180
168
181−public export
182minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
169minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
183minus' {n=n} x y with (nextBytes n)
170minus' {n=n} x y with (nextBytes n)
184 | Z = pad8 n prim__subB8 x y
171 | Z = pad8 n prim__subB8 x y
@@ -186,11 +173,9 @@ minus' {n=n} x y with (nextBytes n)
186 | S (S Z) = pad32 n prim__subB32 x y
173 | S (S Z) = pad32 n prim__subB32 x y
187 | S (S (S _)) = pad64 n prim__subB64 x y
174 | S (S (S _)) = pad64 n prim__subB64 x y
188
175
189−public export
190−minus : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
176+minus : %static {n : Nat} -> Bits n -> Bits n -> Bits n
191minus (MkBits x) (MkBits y) = MkBits (minus' x y)
177minus (MkBits x) (MkBits y) = MkBits (minus' x y)
192
178
193−public export
194times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
179times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
195times' {n=n} x y with (nextBytes n)
180times' {n=n} x y with (nextBytes n)
196 | Z = pad8 n prim__mulB8 x y
181 | Z = pad8 n prim__mulB8 x y
@@ -198,12 +183,10 @@ times' {n=n} x y with (nextBytes n)
198 | S (S Z) = pad32 n prim__mulB32 x y
183 | S (S Z) = pad32 n prim__mulB32 x y
199 | S (S (S _)) = pad64 n prim__mulB64 x y
184 | S (S (S _)) = pad64 n prim__mulB64 x y
200
185
201−public export
202−times : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
186+times : %static {n : Nat} -> Bits n -> Bits n -> Bits n
203times (MkBits x) (MkBits y) = MkBits (times' x y)
187times (MkBits x) (MkBits y) = MkBits (times' x y)
204
188
205partial
189partial
206−public export
207sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
190sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
208sdiv' {n=n} x y with (nextBytes n)
191sdiv' {n=n} x y with (nextBytes n)
209 | Z = prim__sdivB8 x y
192 | Z = prim__sdivB8 x y
@@ -211,88 +194,85 @@ sdiv' {n=n} x y with (nextBytes n)
211 | S (S Z) = prim__sdivB32 x y
194 | S (S Z) = prim__sdivB32 x y
212 | S (S (S _)) = prim__sdivB64 x y
195 | S (S (S _)) = prim__sdivB64 x y
213
196
214−public export partial
197+partial
215−sdiv : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
198+sdiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n
216sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
199sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
217
200
218partial
201partial
219−public export
220−udiv' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
202+udiv' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
221udiv' {n=n} x y with (nextBytes n)
203udiv' {n=n} x y with (nextBytes n)
222 | Z = prim__udivB8 x y
204 | Z = prim__udivB8 x y
223 | S Z = prim__udivB16 x y
205 | S Z = prim__udivB16 x y
224 | S (S Z) = prim__udivB32 x y
206 | S (S Z) = prim__udivB32 x y
225 | S (S (S _)) = prim__udivB64 x y
207 | S (S (S _)) = prim__udivB64 x y
226
208
227−public export partial
209+partial
228−udiv : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
210+udiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n
229udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
211udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
230
212
231−public export partial
213+partial
232−srem' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
214+srem' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
233srem' {n=n} x y with (nextBytes n)
215srem' {n=n} x y with (nextBytes n)
234 | Z = prim__sremB8 x y
216 | Z = prim__sremB8 x y
235 | S Z = prim__sremB16 x y
217 | S Z = prim__sremB16 x y
236 | S (S Z) = prim__sremB32 x y
218 | S (S Z) = prim__sremB32 x y
237 | S (S (S _)) = prim__sremB64 x y
219 | S (S (S _)) = prim__sremB64 x y
238
220
239−public export partial
221+partial
240−srem : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
222+srem : %static {n : Nat} -> Bits n -> Bits n -> Bits n
241srem (MkBits x) (MkBits y) = MkBits (srem' x y)
223srem (MkBits x) (MkBits y) = MkBits (srem' x y)
242
224
243−public export partial
225+partial
244−urem' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
226+urem' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
245urem' {n=n} x y with (nextBytes n)
227urem' {n=n} x y with (nextBytes n)
246 | Z = prim__uremB8 x y
228 | Z = prim__uremB8 x y
247 | S Z = prim__uremB16 x y
229 | S Z = prim__uremB16 x y
248 | S (S Z) = prim__uremB32 x y
230 | S (S Z) = prim__uremB32 x y
249 | S (S (S _)) = prim__uremB64 x y
231 | S (S (S _)) = prim__uremB64 x y
250
232
251−public export partial
233+partial
252−urem : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
234+urem : %static {n : Nat} -> Bits n -> Bits n -> Bits n
253urem (MkBits x) (MkBits y) = MkBits (urem' x y)
235urem (MkBits x) (MkBits y) = MkBits (urem' x y)
254
236
255-- TODO: Proofy comparisons via postulates
237-- TODO: Proofy comparisons via postulates
256−lt : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
238+lt : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
257lt {n=n} x y with (nextBytes n)
239lt {n=n} x y with (nextBytes n)
258 | Z = prim__ltB8 x y
240 | Z = prim__ltB8 x y
259 | S Z = prim__ltB16 x y
241 | S Z = prim__ltB16 x y
260 | S (S Z) = prim__ltB32 x y
242 | S (S Z) = prim__ltB32 x y
261 | S (S (S _)) = prim__ltB64 x y
243 | S (S (S _)) = prim__ltB64 x y
262
244
263−lte : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
245+lte : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
264lte {n=n} x y with (nextBytes n)
246lte {n=n} x y with (nextBytes n)
265 | Z = prim__lteB8 x y
247 | Z = prim__lteB8 x y
266 | S Z = prim__lteB16 x y
248 | S Z = prim__lteB16 x y
267 | S (S Z) = prim__lteB32 x y
249 | S (S Z) = prim__lteB32 x y
268 | S (S (S _)) = prim__lteB64 x y
250 | S (S (S _)) = prim__lteB64 x y
269
251
270−eq : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
252+eq : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
271eq {n=n} x y with (nextBytes n)
253eq {n=n} x y with (nextBytes n)
272 | Z = prim__eqB8 x y
254 | Z = prim__eqB8 x y
273 | S Z = prim__eqB16 x y
255 | S Z = prim__eqB16 x y
274 | S (S Z) = prim__eqB32 x y
256 | S (S Z) = prim__eqB32 x y
275 | S (S (S _)) = prim__eqB64 x y
257 | S (S (S _)) = prim__eqB64 x y
276
258
277−gte : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
259+gte : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
278gte {n=n} x y with (nextBytes n)
260gte {n=n} x y with (nextBytes n)
279 | Z = prim__gteB8 x y
261 | Z = prim__gteB8 x y
280 | S Z = prim__gteB16 x y
262 | S Z = prim__gteB16 x y
281 | S (S Z) = prim__gteB32 x y
263 | S (S Z) = prim__gteB32 x y
282 | S (S (S _)) = prim__gteB64 x y
264 | S (S (S _)) = prim__gteB64 x y
283
265
284−gt : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
266+gt : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
285gt {n=n} x y with (nextBytes n)
267gt {n=n} x y with (nextBytes n)
286 | Z = prim__gtB8 x y
268 | Z = prim__gtB8 x y
287 | S Z = prim__gtB16 x y
269 | S Z = prim__gtB16 x y
288 | S (S Z) = prim__gtB32 x y
270 | S (S Z) = prim__gtB32 x y
289 | S (S (S _)) = prim__gtB64 x y
271 | S (S (S _)) = prim__gtB64 x y
290
272
291−public export
292implementation Eq (Bits n) where
273implementation Eq (Bits n) where
293 (MkBits x) == (MkBits y) = boolOp eq x y
274 (MkBits x) == (MkBits y) = boolOp eq x y
294
275
295−public export
296implementation Ord (Bits n) where
276implementation Ord (Bits n) where
297 (MkBits x) < (MkBits y) = boolOp lt x y
277 (MkBits x) < (MkBits y) = boolOp lt x y
298 (MkBits x) <= (MkBits y) = boolOp lte x y
278 (MkBits x) <= (MkBits y) = boolOp lte x y
@@ -305,8 +285,7 @@ implementation Ord (Bits n) where
305 then EQ
285 then EQ
306 else GT
286 else GT
307
287
308−public export
309−complement' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)
288+complement' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)
310complement' {n=n} x with (nextBytes n)
289complement' {n=n} x with (nextBytes n)
311 | Z = let pad = getPad {n=0} n in
290 | Z = let pad = getPad {n=0} n in
312 prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
291 prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
@@ -317,13 +296,12 @@ complement' {n=n} x with (nextBytes n)
317 | S (S (S _)) = let pad = getPad {n=3} n in
296 | S (S (S _)) = let pad = getPad {n=3} n in
318 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
297 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
319
298
320−public export
321−complement : [static] {n : Nat} -> Bits n -> Bits n
299+complement : %static {n : Nat} -> Bits n -> Bits n
322complement (MkBits x) = MkBits (complement' x)
300complement (MkBits x) = MkBits (complement' x)
323
301
324-- TODO: Prove
302-- TODO: Prove
325%assert_total -- can't verify coverage of with block
303%assert_total -- can't verify coverage of with block
326−zext' : [static] {n : Nat} -> [static] {m : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
304+zext' : %static {n : Nat} -> %static {m : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
327zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
305zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
328 | (Z, Z) = believe_me x
306 | (Z, Z) = believe_me x
329 | (Z, S Z) = believe_me (prim__zextB8_B16 (believe_me x))
307 | (Z, S Z) = believe_me (prim__zextB8_B16 (believe_me x))
@@ -336,14 +314,11 @@ zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
336 | (S (S Z), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))
314 | (S (S Z), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))
337 | (S (S (S _)), S (S (S _))) = believe_me x
315 | (S (S (S _)), S (S (S _))) = believe_me x
338
316
339−public export
340−zeroExtend : [static] {n : Nat} -> [static] {m : Nat} -> Bits n -> Bits (n+m)
317+zeroExtend : %static {n : Nat} -> %static {m : Nat} -> Bits n -> Bits (n+m)
341zeroExtend (MkBits x) = MkBits (zext' x)
318zeroExtend (MkBits x) = MkBits (zext' x)
342
319
343−public export
344%assert_total
320%assert_total
345−intToBits' : [static] {n : Nat} -> Integer -> machineTy (nextBytes n)
321+intToBits' : %static {n : Nat} -> Integer -> machineTy (nextBytes n)
346−intToBits' : Integer -> machineTy (nextBytes n)
347intToBits' {n=n} x with (nextBytes n)
322intToBits' {n=n} x with (nextBytes n)
348 | Z = let pad = getPad {n=0} n in
323 | Z = let pad = getPad {n=0} n in
349 prim__lshrB8 (prim__shlB8 (prim__truncBigInt_B8 x) pad) pad
324 prim__lshrB8 (prim__shlB8 (prim__truncBigInt_B8 x) pad) pad
@@ -354,27 +329,24 @@ intToBits' {n=n} x with (nextBytes n)
354 | S (S (S _)) = let pad = getPad {n=3} n in
329 | S (S (S _)) = let pad = getPad {n=3} n in
355 prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad
330 prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad
356
331
357−public export
358−intToBits : [static] {n : Nat} -> Integer -> Bits n
332+intToBits : %static {n : Nat} -> Integer -> Bits n
359intToBits n = MkBits (intToBits' n)
333intToBits n = MkBits (intToBits' n)
360
334
361implementation Cast Integer (Bits n) where
335implementation Cast Integer (Bits n) where
362 cast = intToBits
336 cast = intToBits
363
337
364−public export
365−bitsToInt' : [static] {n : Nat} -> machineTy (nextBytes n) -> Integer
338+bitsToInt' : %static {n : Nat} -> machineTy (nextBytes n) -> Integer
366bitsToInt' {n=n} x with (nextBytes n)
339bitsToInt' {n=n} x with (nextBytes n)
367 | Z = prim__zextB8_BigInt x
340 | Z = prim__zextB8_BigInt x
368 | S Z = prim__zextB16_BigInt x
341 | S Z = prim__zextB16_BigInt x
369 | S (S Z) = prim__zextB32_BigInt x
342 | S (S Z) = prim__zextB32_BigInt x
370 | S (S (S _)) = prim__zextB64_BigInt x
343 | S (S (S _)) = prim__zextB64_BigInt x
371
344
372−public export
373−bitsToInt : [static] {n : Nat} -> Bits n -> Integer
345+bitsToInt : %static {n : Nat} -> Bits n -> Integer
374bitsToInt (MkBits x) = bitsToInt' x
346bitsToInt (MkBits x) = bitsToInt' x
375
347
376-- Zero out the high bits of a truncated bitstring
348-- Zero out the high bits of a truncated bitstring
377−zeroUnused : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)
349+zeroUnused : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)
378zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
350zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
379
351
380--implementation Cast Nat (Bits n) where
352--implementation Cast Nat (Bits n) where
@@ -382,7 +354,7 @@ zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
382
354
383-- TODO: Prove
355-- TODO: Prove
384%assert_total -- can't verify coverage of with block
356%assert_total -- can't verify coverage of with block
385−sext' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
357+sext' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
386sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
358sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
387 | (Z, Z) = let pad = getPad {n=0} n in
359 | (Z, Z) = let pad = getPad {n=0} n in
388 believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)
360 believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)
@@ -411,14 +383,12 @@ sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
411 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
383 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
412 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)
384 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)
413
385
414−--public export
415−--signExtend : Bits n -> Bits (n+m)
386+----signExtend : Bits n -> Bits (n+m)
416--signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
387--signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
417
388
418-- TODO: Prove
389-- TODO: Prove
419−public export
420%assert_total -- can't verify coverage of with block
390%assert_total -- can't verify coverage of with block
421−trunc' : [static] {m : Nat} -> [static] {n : Nat} -> machineTy (nextBytes (m+n)) -> machineTy (nextBytes n)
391+trunc' : %static {m : Nat} -> %static {n : Nat} -> machineTy (nextBytes (m+n)) -> machineTy (nextBytes n)
422trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))
392trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))
423 | (Z, Z) = believe_me x
393 | (Z, Z) = believe_me x
424 | (Z, S Z) = believe_me (prim__truncB16_B8 (believe_me x))
394 | (Z, S Z) = believe_me (prim__truncB16_B8 (believe_me x))
@@ -431,31 +401,26 @@ trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))
431 | (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))
401 | (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))
432 | (S (S (S _)), S (S (S _))) = believe_me x
402 | (S (S (S _)), S (S (S _))) = believe_me x
433
403
434−public export
435−truncate : [static] {m : Nat} -> [static] {n : Nat} -> Bits (m+n) -> Bits n
404+truncate : %static {m : Nat} -> %static {n : Nat} -> Bits (m+n) -> Bits n
436truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
405truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
437
406
438−public export
439−bitAt : [static] {n : Nat} -> Fin n -> Bits n
407+bitAt : %static {n : Nat} -> Fin n -> Bits n
440bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
408bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
441
409
442−public export
443−getBit : [static] {n : Nat} -> Fin n -> Bits n -> Bool
410+getBit : %static {n : Nat} -> Fin n -> Bits n -> Bool
444getBit n x = (x `and` (bitAt n)) /= intToBits 0
411getBit n x = (x `and` (bitAt n)) /= intToBits 0
445
412
446−public export
447−setBit : [static] {n : Nat} -> Fin n -> Bits n -> Bits n
413+setBit : %static {n : Nat} -> Fin n -> Bits n -> Bits n
448setBit n x = x `or` (bitAt n)
414setBit n x = x `or` (bitAt n)
449
415
450−public export
451−unsetBit : [static] {n : Nat} -> Fin n -> Bits n -> Bits n
416+unsetBit : %static {n : Nat} -> Fin n -> Bits n -> Bits n
452unsetBit n x = x `and` complement (bitAt n)
417unsetBit n x = x `and` complement (bitAt n)
453
418
454−bitsToStr : [static] {n : Nat} -> Bits n -> String
419+bitsToStr : %static {n : Nat} -> Bits n -> String
455bitsToStr x = pack (helper last x)
420bitsToStr x = pack (helper last x)
456 where
421 where
457 %assert_total
422 %assert_total
458− helper : [static] {n : Nat} -> Fin (S n) -> Bits n -> List Char
423+ helper : %static {n : Nat} -> Fin (S n) -> Bits n -> List Char
459 helper FZ _ = []
424 helper FZ _ = []
460 helper (FS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b
425 helper (FS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b
461
426