git.iko.soy/Idris-dev
on master help sign in
Move bitstring stuff to Data to reduce potential for name clashes
a9d6518Benjamin Saunders
lib/Data/Bits.idr+432−18
compare with master
unifiedsplit
@@ -1,25 +1,439 @@
1module Data.Bits
1module Data.Bits
2
2
3−%access public
4−%default partial
3+%default total
5
4
6−infixl 5 .|.
5+divCeil : Nat -> Nat -> Nat
7−infixl 7 .&.
6+divCeil x y = case x `mod` y of
7+ O => x `div` y
8+ S _ => S (x `div` y)
8
9
10+nextPow2 : Nat -> Nat
11+nextPow2 O = O
12+nextPow2 x = if x == (2 `power` l2x)
13+ then l2x
14+ else S l2x
9−class Num a => Bits a where
15+ where
10− (.|.) : a -> a -> a
16+ l2x = log2 x
11− (.&.) : a -> a -> a
12
17
13− xor : a -> a -> a
18+nextBytes : Nat -> Nat
14− complement : a -> a
19+nextBytes bits = (nextPow2 (bits `divCeil` 8))
15− shiftL : a -> Int -> a
16− shiftR : a -> Int -> a
17
20
18−instance Bits Int where
21+machineTy : Nat -> Type
19− (.|.) = prim__orInt
22+machineTy O = Bits8
20− (.&.) = prim__andInt
23+machineTy (S O) = Bits16
24+machineTy (S (S O)) = Bits32
25+machineTy (S (S (S _))) = Bits64
21
26
22− xor = prim__xorInt
27+bitsUsed : Nat -> Nat
23− complement = prim__complInt
28+bitsUsed n = 8 * (2 `power` n)
24− shiftL = prim__shLInt
29+
25− shiftR = prim__shRInt
30+%assert_total
31+natToBits' : machineTy n -> Nat -> machineTy n
32+natToBits' a O = a
33+natToBits' {n=n} a x with n
34+ natToBits' a (S x') | O = natToBits' (prim__addB8 a (prim__intToB8 1)) x'
35+ natToBits' a (S x') | S O = natToBits' (prim__addB16 a (prim__intToB16 1)) x'
36+ natToBits' a (S x') | S (S O) = natToBits' (prim__addB32 a (prim__intToB32 1)) x'
37+ natToBits' a (S x') | S (S (S _)) = natToBits' (prim__addB64 a (prim__intToB64 1)) x'
38+
39+natToBits : Nat -> machineTy n
40+natToBits {n=n} x with n
41+ | O = natToBits' (prim__intToB8 0) x
42+ | S O = natToBits' (prim__intToB16 0) x
43+ | S (S O) = natToBits' (prim__intToB32 0) x
44+ | S (S (S _)) = natToBits' (prim__intToB64 0) x
45+
46+getPad : Nat -> machineTy n
47+getPad n = natToBits ((bitsUsed (nextBytes n)) - n)
48+
49+public
50+data Bits : Nat -> Type where
51+ MkBits : machineTy (nextBytes n) -> Bits n
52+
53+pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
54+pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
55+ where
56+ pad = getPad {n=0} n
57+
58+pad16 : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
59+pad16 n f x y = prim__lshrB16 (f (prim__shlB16 x pad) (prim__shlB16 y pad)) pad
60+ where
61+ pad = getPad {n=1} n
62+
63+pad32 : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
64+pad32 n f x y = prim__lshrB32 (f (prim__shlB32 x pad) (prim__shlB32 y pad)) pad
65+ where
66+ pad = getPad {n=2} n
67+
68+pad64 : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
69+pad64 n f x y = prim__lshrB64 (f (prim__shlB64 x pad) (prim__shlB64 y pad)) pad
70+ where
71+ pad = getPad {n=3} n
72+
73+-- These versions only pad the first operand
74+pad8' : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
75+pad8' n f x y = prim__lshrB8 (f (prim__shlB8 x pad) y) pad
76+ where
77+ pad = getPad {n=0} n
78+
79+pad16' : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
80+pad16' n f x y = prim__lshrB16 (f (prim__shlB16 x pad) y) pad
81+ where
82+ pad = getPad {n=1} n
83+
84+pad32' : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
85+pad32' n f x y = prim__lshrB32 (f (prim__shlB32 x pad) y) pad
86+ where
87+ pad = getPad {n=2} n
88+
89+pad64' : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
90+pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
91+ where
92+ pad = getPad {n=3} n
93+
94+shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
95+shiftLeft' {n=n} x c with (nextBytes n)
96+ | O = pad8' n prim__shlB8 x c
97+ | S O = pad16' n prim__shlB16 x c
98+ | S (S O) = pad32' n prim__shlB32 x c
99+ | S (S (S _)) = pad64' n prim__shlB64 x c
100+
101+public
102+shiftLeft : Bits n -> Bits n -> Bits n
103+shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
104+
105+shiftRightLogical' : machineTy n -> machineTy n -> machineTy n
106+shiftRightLogical' {n=n} x c with n
107+ | O = prim__lshrB8 x c
108+ | S O = prim__lshrB16 x c
109+ | S (S O) = prim__lshrB32 x c
110+ | S (S (S _)) = prim__lshrB64 x c
111+
112+public
113+shiftRightLogical : Bits n -> Bits n -> Bits n
114+shiftRightLogical (MkBits x) (MkBits y) = MkBits (shiftRightLogical' x y)
115+
116+shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
117+shiftRightArithmetic' {n=n} x c with (nextBytes n)
118+ | O = pad8' n prim__ashrB8 x c
119+ | S O = pad16' n prim__ashrB16 x c
120+ | S (S O) = pad32' n prim__ashrB32 x c
121+ | S (S (S _)) = pad64' n prim__ashrB64 x c
122+
123+public
124+shiftRightArithmetic : Bits n -> Bits n -> Bits n
125+shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
126+
127+and' : machineTy n -> machineTy n -> machineTy n
128+and' {n=n} x y with n
129+ | O = prim__andB8 x y
130+ | S O = prim__andB16 x y
131+ | S (S O) = prim__andB32 x y
132+ | S (S (S _)) = prim__andB64 x y
133+
134+public
135+and : Bits n -> Bits n -> Bits n
136+and (MkBits x) (MkBits y) = MkBits (and' x y)
137+
138+or' : machineTy n -> machineTy n -> machineTy n
139+or' {n=n} x y with n
140+ | O = prim__orB8 x y
141+ | S O = prim__orB16 x y
142+ | S (S O) = prim__orB32 x y
143+ | S (S (S _)) = prim__orB64 x y
144+
145+public
146+or : Bits n -> Bits n -> Bits n
147+or (MkBits x) (MkBits y) = MkBits (or' x y)
148+
149+xor' : machineTy n -> machineTy n -> machineTy n
150+xor' {n=n} x y with n
151+ | O = prim__xorB8 x y
152+ | S O = prim__xorB16 x y
153+ | S (S O) = prim__xorB32 x y
154+ | S (S (S _)) = prim__xorB64 x y
155+
156+public
157+xor : Bits n -> Bits n -> Bits n
158+xor (MkBits x) (MkBits y) = MkBits (xor' x y)
159+
160+plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
161+plus' {n=n} x y with (nextBytes n)
162+ | O = pad8 n prim__addB8 x y
163+ | S O = pad16 n prim__addB16 x y
164+ | S (S O) = pad32 n prim__addB32 x y
165+ | S (S (S _)) = pad64 n prim__addB64 x y
166+
167+public
168+plus : Bits n -> Bits n -> Bits n
169+plus (MkBits x) (MkBits y) = MkBits (plus' x y)
170+
171+minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
172+minus' {n=n} x y with (nextBytes n)
173+ | O = pad8 n prim__subB8 x y
174+ | S O = pad16 n prim__subB16 x y
175+ | S (S O) = pad32 n prim__subB32 x y
176+ | S (S (S _)) = pad64 n prim__subB64 x y
177+
178+public
179+minus : Bits n -> Bits n -> Bits n
180+minus (MkBits x) (MkBits y) = MkBits (minus' x y)
181+
182+times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
183+times' {n=n} x y with (nextBytes n)
184+ | O = pad8 n prim__mulB8 x y
185+ | S O = pad16 n prim__mulB16 x y
186+ | S (S O) = pad32 n prim__mulB32 x y
187+ | S (S (S _)) = pad64 n prim__mulB64 x y
188+
189+public
190+times : Bits n -> Bits n -> Bits n
191+times (MkBits x) (MkBits y) = MkBits (times' x y)
192+
193+partial
194+sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
195+sdiv' {n=n} x y with (nextBytes n)
196+ | O = prim__sdivB8 x y
197+ | S O = prim__sdivB16 x y
198+ | S (S O) = prim__sdivB32 x y
199+ | S (S (S _)) = prim__sdivB64 x y
200+
201+public partial
202+sdiv : Bits n -> Bits n -> Bits n
203+sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
204+
205+partial
206+udiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
207+udiv' {n=n} x y with (nextBytes n)
208+ | O = prim__udivB8 x y
209+ | S O = prim__udivB16 x y
210+ | S (S O) = prim__udivB32 x y
211+ | S (S (S _)) = prim__udivB64 x y
212+
213+public partial
214+udiv : Bits n -> Bits n -> Bits n
215+udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
216+
217+partial
218+srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
219+srem' {n=n} x y with (nextBytes n)
220+ | O = prim__sremB8 x y
221+ | S O = prim__sremB16 x y
222+ | S (S O) = prim__sremB32 x y
223+ | S (S (S _)) = prim__sremB64 x y
224+
225+public partial
226+srem : Bits n -> Bits n -> Bits n
227+srem (MkBits x) (MkBits y) = MkBits (srem' x y)
228+
229+partial
230+urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
231+urem' {n=n} x y with (nextBytes n)
232+ | O = prim__uremB8 x y
233+ | S O = prim__uremB16 x y
234+ | S (S O) = prim__uremB32 x y
235+ | S (S (S _)) = prim__uremB64 x y
236+
237+public partial
238+urem : Bits n -> Bits n -> Bits n
239+urem (MkBits x) (MkBits y) = MkBits (urem' x y)
240+
241+-- TODO: Proofy comparisons via postulates
242+lt : machineTy n -> machineTy n -> Int
243+lt {n=n} x y with n
244+ | O = prim__ltB8 x y
245+ | S O = prim__ltB16 x y
246+ | S (S O) = prim__ltB32 x y
247+ | S (S (S _)) = prim__ltB64 x y
248+
249+lte : machineTy n -> machineTy n -> Int
250+lte {n=n} x y with n
251+ | O = prim__lteB8 x y
252+ | S O = prim__lteB16 x y
253+ | S (S O) = prim__lteB32 x y
254+ | S (S (S _)) = prim__lteB64 x y
255+
256+eq : machineTy n -> machineTy n -> Int
257+eq {n=n} x y with n
258+ | O = prim__eqB8 x y
259+ | S O = prim__eqB16 x y
260+ | S (S O) = prim__eqB32 x y
261+ | S (S (S _)) = prim__eqB64 x y
262+
263+gte : machineTy n -> machineTy n -> Int
264+gte {n=n} x y with n
265+ | O = prim__gteB8 x y
266+ | S O = prim__gteB16 x y
267+ | S (S O) = prim__gteB32 x y
268+ | S (S (S _)) = prim__gteB64 x y
269+
270+gt : machineTy n -> machineTy n -> Int
271+gt {n=n} x y with n
272+ | O = prim__gtB8 x y
273+ | S O = prim__gtB16 x y
274+ | S (S O) = prim__gtB32 x y
275+ | S (S (S _)) = prim__gtB64 x y
276+
277+instance Eq (Bits n) where
278+ (MkBits x) == (MkBits y) = boolOp eq x y
279+
280+instance Ord (Bits n) where
281+ (MkBits x) < (MkBits y) = boolOp lt x y
282+ (MkBits x) <= (MkBits y) = boolOp lte x y
283+ (MkBits x) >= (MkBits y) = boolOp gte x y
284+ (MkBits x) > (MkBits y) = boolOp gt x y
285+ compare (MkBits x) (MkBits y) =
286+ if boolOp lt x y
287+ then LT
288+ else if boolOp eq x y
289+ then EQ
290+ else GT
291+
292+complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)
293+complement' {n=n} x with (nextBytes n)
294+ | O = let pad = getPad {n=0} n in
295+ prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
296+ | S O = let pad = getPad {n=1} n in
297+ prim__complB16 (x `prim__shlB16` pad) `prim__lshrB16` pad
298+ | S (S O) = let pad = getPad {n=2} n in
299+ prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad
300+ | S (S (S _)) = let pad = getPad {n=3} n in
301+ prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
302+
303+public
304+complement : Bits n -> Bits n
305+complement (MkBits x) = MkBits (complement' x)
306+
307+-- TODO: Prove
308+zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
309+zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
310+ | (O, O) = believe_me x
311+ | (O, S O) = believe_me (prim__zextB8_16 (believe_me x))
312+ | (O, S (S O)) = believe_me (prim__zextB8_32 (believe_me x))
313+ | (O, S (S (S _))) = believe_me (prim__zextB8_64 (believe_me x))
314+ | (S O, S O) = believe_me x
315+ | (S O, S (S O)) = believe_me (prim__zextB16_32 (believe_me x))
316+ | (S O, S (S (S _))) = believe_me (prim__zextB16_64 (believe_me x))
317+ | (S (S O), S (S O)) = believe_me x
318+ | (S (S O), S (S (S _))) = believe_me (prim__zextB32_64 (believe_me x))
319+ | (S (S (S _)), S (S (S _))) = believe_me x
320+
321+public
322+zeroExtend : Bits n -> Bits (n+m)
323+zeroExtend (MkBits x) = MkBits (zext' x)
324+
325+%assert_total
326+intToBits' : Int -> machineTy (nextBytes n)
327+intToBits' {n=n} x with (nextBytes n)
328+ | O = let pad = getPad {n=0} n in
329+ prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
330+ | S O = let pad = getPad {n=1} n in
331+ prim__lshrB16 (prim__shlB16 (prim__intToB16 x) pad) pad
332+ | S (S O) = let pad = getPad {n=2} n in
333+ prim__lshrB32 (prim__shlB32 (prim__intToB32 x) pad) pad
334+ | S (S (S _)) = let pad = getPad {n=3} n in
335+ prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
336+
337+public
338+intToBits : Int -> Bits n
339+intToBits n = MkBits (intToBits' n)
340+
341+instance Cast Int (Bits n) where
342+ cast = intToBits
343+
344+bitsToInt' : machineTy n -> Int
345+bitsToInt' {n=n} x with n
346+ | O = prim__B32ToInt (prim__zextB8_32 x)
347+ | S O = prim__B32ToInt (prim__zextB16_32 x)
348+ | S (S O) = prim__B32ToInt x
349+ | S (S (S _)) = prim__B32ToInt (prim__truncB64_32 x)
350+
351+public
352+bitsToInt : Bits n -> Int
353+bitsToInt (MkBits x) = bitsToInt' x
354+
355+-- Zero out the high bits of a truncated bitstring
356+zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)
357+zeroUnused x = x `and'` complement' (intToBits' 0)
358+
359+instance Cast Nat (Bits n) where
360+ cast x = MkBits (zeroUnused (natToBits n))
361+
362+-- TODO: Prove
363+sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
364+sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
365+ | (O, O) = let pad = getPad {n=0} n in
366+ believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)
367+ | (O, S O) = let pad = getPad {n=0} n in
368+ believe_me (prim__ashrB16 (prim__sextB8_16 (prim__shlB8 (believe_me x) pad))
369+ (prim__zextB8_16 pad))
370+ | (O, S (S O)) = let pad = getPad {n=0} n in
371+ believe_me (prim__ashrB32 (prim__sextB8_32 (prim__shlB8 (believe_me x) pad))
372+ (prim__zextB8_32 pad))
373+ | (O, S (S (S _))) = let pad = getPad {n=0} n in
374+ believe_me (prim__ashrB64 (prim__sextB8_64 (prim__shlB8 (believe_me x) pad))
375+ (prim__zextB8_64 pad))
376+ | (S O, S O) = let pad = getPad {n=1} n in
377+ believe_me (prim__ashrB16 (prim__shlB16 (believe_me x) pad) pad)
378+ | (S O, S (S O)) = let pad = getPad {n=1} n in
379+ believe_me (prim__ashrB32 (prim__sextB16_32 (prim__shlB16 (believe_me x) pad))
380+ (prim__zextB16_32 pad))
381+ | (S O, S (S (S _))) = let pad = getPad {n=1} n in
382+ believe_me (prim__ashrB64 (prim__sextB16_64 (prim__shlB16 (believe_me x) pad))
383+ (prim__zextB16_64 pad))
384+ | (S (S O), S (S O)) = let pad = getPad {n=2} n in
385+ believe_me (prim__ashrB32 (prim__shlB32 (believe_me x) pad) pad)
386+ | (S (S O), S (S (S _))) = let pad = getPad {n=2} n in
387+ believe_me (prim__ashrB64 (prim__sextB32_64 (prim__shlB32 (believe_me x) pad))
388+ (prim__zextB32_64 pad))
389+ | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
390+ believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)
391+
392+public
393+signExtend : Bits n -> Bits (n+m)
394+signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
395+
396+-- TODO: Prove
397+trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)
398+trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
399+ | (O, O) = believe_me x
400+ | (O, S O) = believe_me (prim__truncB16_8 (believe_me x))
401+ | (O, S (S O)) = believe_me (prim__truncB32_8 (believe_me x))
402+ | (O, S (S (S _))) = believe_me (prim__truncB64_8 (believe_me x))
403+ | (S O, S O) = believe_me x
404+ | (S O, S (S O)) = believe_me (prim__truncB32_16 (believe_me x))
405+ | (S O, S (S (S _))) = believe_me (prim__truncB64_16 (believe_me x))
406+ | (S (S O), S (S O)) = believe_me x
407+ | (S (S O), S (S (S _))) = believe_me (prim__truncB64_32 (believe_me x))
408+ | (S (S (S _)), S (S (S _))) = believe_me x
409+
410+public
411+truncate : Bits (n+m) -> Bits n
412+truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
413+
414+public
415+bitAt : Fin n -> Bits n
416+bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
417+
418+public
419+getBit : Fin n -> Bits n -> Bool
420+getBit n x = (x `and` (bitAt n)) /= intToBits 0
421+
422+public
423+setBit : Fin n -> Bits n -> Bits n
424+setBit n x = x `or` (bitAt n)
425+
426+public
427+unsetBit : Fin n -> Bits n -> Bits n
428+unsetBit n x = x `and` complement (bitAt n)
429+
430+bitsToStr : Bits n -> String
431+bitsToStr x = pack (helper last x)
432+ where
433+ %assert_total
434+ helper : Fin (S n) -> Bits n -> List Char
435+ helper fO _ = []
436+ helper (fS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b
437+
438+instance Show (Bits n) where
439+ show = bitsToStr
lib/Prelude/Modular.idr → lib/Data/Mod2.idrrenamed+6−4
@@ -1,6 +1,6 @@
1−module Prelude.Modular
1+module Data.Mod2
2
2
3−import Prelude.Bits
3+import Data.Bits
4
4
5%default total
5%default total
6
6
@@ -51,8 +51,6 @@ instance Cast (Mod2 n) (Bits n) where
51instance Cast (Bits n) (Mod2 n) where
51instance Cast (Bits n) (Mod2 n) where
52 cast x = MkMod2 x
52 cast x = MkMod2 x
53
53
54−-- TODO: Other bases
55−public
56modToStr : Mod2 n -> String
54modToStr : Mod2 n -> String
57modToStr x = pack (reverse (helper x))
55modToStr x = pack (reverse (helper x))
58 where
56 where
@@ -60,3 +58,7 @@ modToStr x = pack (reverse (helper x))
60 helper : Mod2 n -> List Char
58 helper : Mod2 n -> List Char
61 helper x = strIndex "0123456789" (bitsToInt (cast (x `rem` 10)))
59 helper x = strIndex "0123456789" (bitsToInt (cast (x `rem` 10)))
62 :: (if x < 10 then [] else helper (x `div` 10))
60 :: (if x < 10 then [] else helper (x `div` 10))
61+
62+
63+instance Show (Mod2 n) where
64+ show = modToStr
lib/Prelude.idr−7
@@ -6,7 +6,6 @@ import IO
6import Prelude.Cast
6import Prelude.Cast
7import Prelude.Nat
7import Prelude.Nat
8import Prelude.Fin
8import Prelude.Fin
9−import Prelude.Modular
10import Prelude.List
9import Prelude.List
11import Prelude.Maybe
10import Prelude.Maybe
12import Prelude.Monad
11import Prelude.Monad
@@ -32,12 +31,6 @@ instance Show Nat where
32instance Show Int where
31instance Show Int where
33 show = prim__intToStr
32 show = prim__intToStr
34
33
35−instance Show (Bits n) where
36− show = bitsToStr
37−
38−instance Show (Mod2 n) where
39− show = modToStr
40−
41instance Show Integer where
34instance Show Integer where
42 show = prim__bigIntToStr
35 show = prim__bigIntToStr
43
36
lib/Prelude/Bits.idrdeleted−439
@@ -1,439 +0,0 @@
1−module Prelude.Bits
2−
3−import Prelude.Strings
4−
5−%default total
6−
7−divCeil : Nat -> Nat -> Nat
8−divCeil x y = case x `mod` y of
9− O => x `div` y
10− S _ => S (x `div` y)
11−
12−nextPow2 : Nat -> Nat
13−nextPow2 O = O
14−nextPow2 x = if x == (2 `power` l2x)
15− then l2x
16− else S l2x
17− where
18− l2x = log2 x
19−
20−nextBytes : Nat -> Nat
21−nextBytes bits = (nextPow2 (bits `divCeil` 8))
22−
23−machineTy : Nat -> Type
24−machineTy O = Bits8
25−machineTy (S O) = Bits16
26−machineTy (S (S O)) = Bits32
27−machineTy (S (S (S _))) = Bits64
28−
29−bitsUsed : Nat -> Nat
30−bitsUsed n = 8 * (2 `power` n)
31−
32−%assert_total
33−natToBits' : machineTy n -> Nat -> machineTy n
34−natToBits' a O = a
35−natToBits' {n=n} a x with n
36− natToBits' a (S x') | O = natToBits' (prim__addB8 a (prim__intToB8 1)) x'
37− natToBits' a (S x') | S O = natToBits' (prim__addB16 a (prim__intToB16 1)) x'
38− natToBits' a (S x') | S (S O) = natToBits' (prim__addB32 a (prim__intToB32 1)) x'
39− natToBits' a (S x') | S (S (S _)) = natToBits' (prim__addB64 a (prim__intToB64 1)) x'
40−
41−natToBits : Nat -> machineTy n
42−natToBits {n=n} x with n
43− | O = natToBits' (prim__intToB8 0) x
44− | S O = natToBits' (prim__intToB16 0) x
45− | S (S O) = natToBits' (prim__intToB32 0) x
46− | S (S (S _)) = natToBits' (prim__intToB64 0) x
47−
48−getPad : Nat -> machineTy n
49−getPad n = natToBits ((bitsUsed (nextBytes n)) - n)
50−
51−public
52−data Bits : Nat -> Type where
53− MkBits : machineTy (nextBytes n) -> Bits n
54−
55−pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
56−pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
57− where
58− pad = getPad {n=0} n
59−
60−pad16 : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
61−pad16 n f x y = prim__lshrB16 (f (prim__shlB16 x pad) (prim__shlB16 y pad)) pad
62− where
63− pad = getPad {n=1} n
64−
65−pad32 : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
66−pad32 n f x y = prim__lshrB32 (f (prim__shlB32 x pad) (prim__shlB32 y pad)) pad
67− where
68− pad = getPad {n=2} n
69−
70−pad64 : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
71−pad64 n f x y = prim__lshrB64 (f (prim__shlB64 x pad) (prim__shlB64 y pad)) pad
72− where
73− pad = getPad {n=3} n
74−
75−-- These versions only pad the first operand
76−pad8' : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
77−pad8' n f x y = prim__lshrB8 (f (prim__shlB8 x pad) y) pad
78− where
79− pad = getPad {n=0} n
80−
81−pad16' : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
82−pad16' n f x y = prim__lshrB16 (f (prim__shlB16 x pad) y) pad
83− where
84− pad = getPad {n=1} n
85−
86−pad32' : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
87−pad32' n f x y = prim__lshrB32 (f (prim__shlB32 x pad) y) pad
88− where
89− pad = getPad {n=2} n
90−
91−pad64' : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
92−pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
93− where
94− pad = getPad {n=3} n
95−
96−shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
97−shiftLeft' {n=n} x c with (nextBytes n)
98− | O = pad8' n prim__shlB8 x c
99− | S O = pad16' n prim__shlB16 x c
100− | S (S O) = pad32' n prim__shlB32 x c
101− | S (S (S _)) = pad64' n prim__shlB64 x c
102−
103−public
104−shiftLeft : Bits n -> Bits n -> Bits n
105−shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
106−
107−shiftRightLogical' : machineTy n -> machineTy n -> machineTy n
108−shiftRightLogical' {n=n} x c with n
109− | O = prim__lshrB8 x c
110− | S O = prim__lshrB16 x c
111− | S (S O) = prim__lshrB32 x c
112− | S (S (S _)) = prim__lshrB64 x c
113−
114−public
115−shiftRightLogical : Bits n -> Bits n -> Bits n
116−shiftRightLogical (MkBits x) (MkBits y) = MkBits (shiftRightLogical' x y)
117−
118−shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
119−shiftRightArithmetic' {n=n} x c with (nextBytes n)
120− | O = pad8' n prim__ashrB8 x c
121− | S O = pad16' n prim__ashrB16 x c
122− | S (S O) = pad32' n prim__ashrB32 x c
123− | S (S (S _)) = pad64' n prim__ashrB64 x c
124−
125−public
126−shiftRightArithmetic : Bits n -> Bits n -> Bits n
127−shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
128−
129−and' : machineTy n -> machineTy n -> machineTy n
130−and' {n=n} x y with n
131− | O = prim__andB8 x y
132− | S O = prim__andB16 x y
133− | S (S O) = prim__andB32 x y
134− | S (S (S _)) = prim__andB64 x y
135−
136−public
137−and : Bits n -> Bits n -> Bits n
138−and (MkBits x) (MkBits y) = MkBits (and' x y)
139−
140−or' : machineTy n -> machineTy n -> machineTy n
141−or' {n=n} x y with n
142− | O = prim__orB8 x y
143− | S O = prim__orB16 x y
144− | S (S O) = prim__orB32 x y
145− | S (S (S _)) = prim__orB64 x y
146−
147−public
148−or : Bits n -> Bits n -> Bits n
149−or (MkBits x) (MkBits y) = MkBits (or' x y)
150−
151−xor' : machineTy n -> machineTy n -> machineTy n
152−xor' {n=n} x y with n
153− | O = prim__xorB8 x y
154− | S O = prim__xorB16 x y
155− | S (S O) = prim__xorB32 x y
156− | S (S (S _)) = prim__xorB64 x y
157−
158−public
159−xor : Bits n -> Bits n -> Bits n
160−xor (MkBits x) (MkBits y) = MkBits (xor' x y)
161−
162−plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
163−plus' {n=n} x y with (nextBytes n)
164− | O = pad8 n prim__addB8 x y
165− | S O = pad16 n prim__addB16 x y
166− | S (S O) = pad32 n prim__addB32 x y
167− | S (S (S _)) = pad64 n prim__addB64 x y
168−
169−public
170−plus : Bits n -> Bits n -> Bits n
171−plus (MkBits x) (MkBits y) = MkBits (plus' x y)
172−
173−minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
174−minus' {n=n} x y with (nextBytes n)
175− | O = pad8 n prim__subB8 x y
176− | S O = pad16 n prim__subB16 x y
177− | S (S O) = pad32 n prim__subB32 x y
178− | S (S (S _)) = pad64 n prim__subB64 x y
179−
180−public
181−minus : Bits n -> Bits n -> Bits n
182−minus (MkBits x) (MkBits y) = MkBits (minus' x y)
183−
184−times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
185−times' {n=n} x y with (nextBytes n)
186− | O = pad8 n prim__mulB8 x y
187− | S O = pad16 n prim__mulB16 x y
188− | S (S O) = pad32 n prim__mulB32 x y
189− | S (S (S _)) = pad64 n prim__mulB64 x y
190−
191−public
192−times : Bits n -> Bits n -> Bits n
193−times (MkBits x) (MkBits y) = MkBits (times' x y)
194−
195−partial
196−sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
197−sdiv' {n=n} x y with (nextBytes n)
198− | O = prim__sdivB8 x y
199− | S O = prim__sdivB16 x y
200− | S (S O) = prim__sdivB32 x y
201− | S (S (S _)) = prim__sdivB64 x y
202−
203−public partial
204−sdiv : Bits n -> Bits n -> Bits n
205−sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
206−
207−partial
208−udiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
209−udiv' {n=n} x y with (nextBytes n)
210− | O = prim__udivB8 x y
211− | S O = prim__udivB16 x y
212− | S (S O) = prim__udivB32 x y
213− | S (S (S _)) = prim__udivB64 x y
214−
215−public partial
216−udiv : Bits n -> Bits n -> Bits n
217−udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
218−
219−partial
220−srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
221−srem' {n=n} x y with (nextBytes n)
222− | O = prim__sremB8 x y
223− | S O = prim__sremB16 x y
224− | S (S O) = prim__sremB32 x y
225− | S (S (S _)) = prim__sremB64 x y
226−
227−public partial
228−srem : Bits n -> Bits n -> Bits n
229−srem (MkBits x) (MkBits y) = MkBits (srem' x y)
230−
231−partial
232−urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
233−urem' {n=n} x y with (nextBytes n)
234− | O = prim__uremB8 x y
235− | S O = prim__uremB16 x y
236− | S (S O) = prim__uremB32 x y
237− | S (S (S _)) = prim__uremB64 x y
238−
239−public partial
240−urem : Bits n -> Bits n -> Bits n
241−urem (MkBits x) (MkBits y) = MkBits (urem' x y)
242−
243−-- TODO: Proofy comparisons via postulates
244−lt : machineTy n -> machineTy n -> Int
245−lt {n=n} x y with n
246− | O = prim__ltB8 x y
247− | S O = prim__ltB16 x y
248− | S (S O) = prim__ltB32 x y
249− | S (S (S _)) = prim__ltB64 x y
250−
251−lte : machineTy n -> machineTy n -> Int
252−lte {n=n} x y with n
253− | O = prim__lteB8 x y
254− | S O = prim__lteB16 x y
255− | S (S O) = prim__lteB32 x y
256− | S (S (S _)) = prim__lteB64 x y
257−
258−eq : machineTy n -> machineTy n -> Int
259−eq {n=n} x y with n
260− | O = prim__eqB8 x y
261− | S O = prim__eqB16 x y
262− | S (S O) = prim__eqB32 x y
263− | S (S (S _)) = prim__eqB64 x y
264−
265−gte : machineTy n -> machineTy n -> Int
266−gte {n=n} x y with n
267− | O = prim__gteB8 x y
268− | S O = prim__gteB16 x y
269− | S (S O) = prim__gteB32 x y
270− | S (S (S _)) = prim__gteB64 x y
271−
272−gt : machineTy n -> machineTy n -> Int
273−gt {n=n} x y with n
274− | O = prim__gtB8 x y
275− | S O = prim__gtB16 x y
276− | S (S O) = prim__gtB32 x y
277− | S (S (S _)) = prim__gtB64 x y
278−
279−instance Eq (Bits n) where
280− (MkBits x) == (MkBits y) = boolOp eq x y
281−
282−instance Ord (Bits n) where
283− (MkBits x) < (MkBits y) = boolOp lt x y
284− (MkBits x) <= (MkBits y) = boolOp lte x y
285− (MkBits x) >= (MkBits y) = boolOp gte x y
286− (MkBits x) > (MkBits y) = boolOp gt x y
287− compare (MkBits x) (MkBits y) =
288− if boolOp lt x y
289− then LT
290− else if boolOp eq x y
291− then EQ
292− else GT
293−
294−complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)
295−complement' {n=n} x with (nextBytes n)
296− | O = let pad = getPad {n=0} n in
297− prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
298− | S O = let pad = getPad {n=1} n in
299− prim__complB16 (x `prim__shlB16` pad) `prim__lshrB16` pad
300− | S (S O) = let pad = getPad {n=2} n in
301− prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad
302− | S (S (S _)) = let pad = getPad {n=3} n in
303− prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
304−
305−public
306−complement : Bits n -> Bits n
307−complement (MkBits x) = MkBits (complement' x)
308−
309−-- TODO: Prove
310−zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
311−zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
312− | (O, O) = believe_me x
313− | (O, S O) = believe_me (prim__zextB8_16 (believe_me x))
314− | (O, S (S O)) = believe_me (prim__zextB8_32 (believe_me x))
315− | (O, S (S (S _))) = believe_me (prim__zextB8_64 (believe_me x))
316− | (S O, S O) = believe_me x
317− | (S O, S (S O)) = believe_me (prim__zextB16_32 (believe_me x))
318− | (S O, S (S (S _))) = believe_me (prim__zextB16_64 (believe_me x))
319− | (S (S O), S (S O)) = believe_me x
320− | (S (S O), S (S (S _))) = believe_me (prim__zextB32_64 (believe_me x))
321− | (S (S (S _)), S (S (S _))) = believe_me x
322−
323−public
324−zeroExtend : Bits n -> Bits (n+m)
325−zeroExtend (MkBits x) = MkBits (zext' x)
326−
327−%assert_total
328−intToBits' : Int -> machineTy (nextBytes n)
329−intToBits' {n=n} x with (nextBytes n)
330− | O = let pad = getPad {n=0} n in
331− prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
332− | S O = let pad = getPad {n=1} n in
333− prim__lshrB16 (prim__shlB16 (prim__intToB16 x) pad) pad
334− | S (S O) = let pad = getPad {n=2} n in
335− prim__lshrB32 (prim__shlB32 (prim__intToB32 x) pad) pad
336− | S (S (S _)) = let pad = getPad {n=3} n in
337− prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
338−
339−public
340−intToBits : Int -> Bits n
341−intToBits n = MkBits (intToBits' n)
342−
343−instance Cast Int (Bits n) where
344− cast = intToBits
345−
346−bitsToInt' : machineTy n -> Int
347−bitsToInt' {n=n} x with n
348− | O = prim__B32ToInt (prim__zextB8_32 x)
349− | S O = prim__B32ToInt (prim__zextB16_32 x)
350− | S (S O) = prim__B32ToInt x
351− | S (S (S _)) = prim__B32ToInt (prim__truncB64_32 x)
352−
353−public
354−bitsToInt : Bits n -> Int
355−bitsToInt (MkBits x) = bitsToInt' x
356−
357−-- Zero out the high bits of a truncated bitstring
358−zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)
359−zeroUnused x = x `and'` complement' (intToBits' 0)
360−
361−instance Cast Nat (Bits n) where
362− cast x = MkBits (zeroUnused (natToBits n))
363−
364−-- TODO: Prove
365−sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
366−sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
367− | (O, O) = let pad = getPad {n=0} n in
368− believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)
369− | (O, S O) = let pad = getPad {n=0} n in
370− believe_me (prim__ashrB16 (prim__sextB8_16 (prim__shlB8 (believe_me x) pad))
371− (prim__zextB8_16 pad))
372− | (O, S (S O)) = let pad = getPad {n=0} n in
373− believe_me (prim__ashrB32 (prim__sextB8_32 (prim__shlB8 (believe_me x) pad))
374− (prim__zextB8_32 pad))
375− | (O, S (S (S _))) = let pad = getPad {n=0} n in
376− believe_me (prim__ashrB64 (prim__sextB8_64 (prim__shlB8 (believe_me x) pad))
377− (prim__zextB8_64 pad))
378− | (S O, S O) = let pad = getPad {n=1} n in
379− believe_me (prim__ashrB16 (prim__shlB16 (believe_me x) pad) pad)
380− | (S O, S (S O)) = let pad = getPad {n=1} n in
381− believe_me (prim__ashrB32 (prim__sextB16_32 (prim__shlB16 (believe_me x) pad))
382− (prim__zextB16_32 pad))
383− | (S O, S (S (S _))) = let pad = getPad {n=1} n in
384− believe_me (prim__ashrB64 (prim__sextB16_64 (prim__shlB16 (believe_me x) pad))
385− (prim__zextB16_64 pad))
386− | (S (S O), S (S O)) = let pad = getPad {n=2} n in
387− believe_me (prim__ashrB32 (prim__shlB32 (believe_me x) pad) pad)
388− | (S (S O), S (S (S _))) = let pad = getPad {n=2} n in
389− believe_me (prim__ashrB64 (prim__sextB32_64 (prim__shlB32 (believe_me x) pad))
390− (prim__zextB32_64 pad))
391− | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
392− believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)
393−
394−public
395−signExtend : Bits n -> Bits (n+m)
396−signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
397−
398−-- TODO: Prove
399−trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)
400−trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
401− | (O, O) = believe_me x
402− | (O, S O) = believe_me (prim__truncB16_8 (believe_me x))
403− | (O, S (S O)) = believe_me (prim__truncB32_8 (believe_me x))
404− | (O, S (S (S _))) = believe_me (prim__truncB64_8 (believe_me x))
405− | (S O, S O) = believe_me x
406− | (S O, S (S O)) = believe_me (prim__truncB32_16 (believe_me x))
407− | (S O, S (S (S _))) = believe_me (prim__truncB64_16 (believe_me x))
408− | (S (S O), S (S O)) = believe_me x
409− | (S (S O), S (S (S _))) = believe_me (prim__truncB64_32 (believe_me x))
410− | (S (S (S _)), S (S (S _))) = believe_me x
411−
412−public
413−truncate : Bits (n+m) -> Bits n
414−truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
415−
416−public
417−bitAt : Fin n -> Bits n
418−bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
419−
420−public
421−getBit : Fin n -> Bits n -> Bool
422−getBit n x = (x `and` (bitAt n)) /= intToBits 0
423−
424−public
425−setBit : Fin n -> Bits n -> Bits n
426−setBit n x = x `or` (bitAt n)
427−
428−public
429−unsetBit : Fin n -> Bits n -> Bits n
430−unsetBit n x = x `and` complement (bitAt n)
431−
432−public
433−bitsToStr : Bits n -> String
434−bitsToStr x = pack (helper last x)
435− where
436− %assert_total
437− helper : Fin (S n) -> Bits n -> List Char
438− helper fO _ = []
439− helper (fS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b
lib/base.ipkg+2−3
@@ -6,8 +6,7 @@ modules = Builtins, Prelude, IO, System,
6 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,
6 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,
7 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
7 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
8 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
8 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
9− Prelude.Heap, Prelude.Complex, Prelude.Functor, Prelude.Modular,
9+ Prelude.Heap, Prelude.Complex, Prelude.Functor,
10− Prelude.Bits,
11
10
12 Network.Cgi,
11 Network.Cgi,
13 Debug.Trace,
12 Debug.Trace,
@@ -16,7 +15,7 @@ modules = Builtins, Prelude, IO, System,
16
15
17 Language.Reflection,
16 Language.Reflection,
18
17
19− Data.Morphisms, Data.Bits,
18+ Data.Morphisms, Data.Bits, Data.Mod2,
20
19
21 Control.Monad.Identity, Control.Monad.State, Control.Category,
20 Control.Monad.Identity, Control.Monad.State, Control.Category,
22 Control.Arrow
21 Control.Arrow
test/test007/test007.idr+1−1
@@ -36,6 +36,6 @@ runEval env e with (eval e) {
36
36
37main : IO ()
37main : IO ()
38main = do print [| (\x => x *2) (Just 4) |]
38main = do print [| (\x => x *2) (Just 4) |]
39− print [| plus (Just 4) (Just 5) |]
39+ print [| plus (Just 4) (Just 5) |]
40 print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))
40 print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))
41 print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))
41 print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))