git.iko.soy/Idris-dev
on master help sign in
Strip access qualifiers pending resolution of issue #143
ee40d17Benjamin Saunders
lib/Prelude/Bits.idr+3−21
compare with master
unifiedsplit
@@ -15,7 +15,6 @@ nextBits x with (log2ceil x)
15 | (S (S (S (S O)))) = Bits16
15 | (S (S (S (S O)))) = Bits16
16 | _ = Bits8
16 | _ = Bits8
17
17
18−abstract
19data Bits : Nat -> Type where
18data Bits : Nat -> Type where
20 MkBits : {n : Nat} -> nextBits n -> Bits n
19 MkBits : {n : Nat} -> nextBits n -> Bits n
21
20
@@ -57,7 +56,6 @@ intToBits' {n=n} x with (nextBits n)
57 | Bits64 = let pad = (prim__intToB64 (cast (64-n))) in
56 | Bits64 = let pad = (prim__intToB64 (cast (64-n))) in
58 prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
57 prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
59
58
60−public
61intToBits : {n : Nat} -> Int -> Bits n
59intToBits : {n : Nat} -> Int -> Bits n
62intToBits n = MkBits (intToBits' n)
60intToBits n = MkBits (intToBits' n)
63
61
@@ -71,7 +69,6 @@ bitsShl' {n=n} x c with (nextBits n)
71 | Bits32 = pad32 n prim__shlB32 x c
69 | Bits32 = pad32 n prim__shlB32 x c
72 | Bits64 = pad64 n prim__shlB64 x c
70 | Bits64 = pad64 n prim__shlB64 x c
73
71
74−public
75bitsShl : Bits n -> Bits n -> Bits n
72bitsShl : Bits n -> Bits n -> Bits n
76bitsShl (MkBits x) (MkBits y) = MkBits (bitsShl' x y)
73bitsShl (MkBits x) (MkBits y) = MkBits (bitsShl' x y)
77
74
@@ -82,7 +79,6 @@ bitsLShr' {n=n} x c with (nextBits n)
82 | Bits32 = prim__lshrB32 x c
79 | Bits32 = prim__lshrB32 x c
83 | Bits64 = prim__lshrB64 x c
80 | Bits64 = prim__lshrB64 x c
84
81
85−public
86bitsLShr : Bits n -> Bits n -> Bits n
82bitsLShr : Bits n -> Bits n -> Bits n
87bitsLShr (MkBits x) (MkBits y) = MkBits (bitsLShr' x y)
83bitsLShr (MkBits x) (MkBits y) = MkBits (bitsLShr' x y)
88
84
@@ -93,7 +89,6 @@ bitsAShr' {n=n} x c with (nextBits n)
93 | Bits32 = prim__ashrB32 x c
89 | Bits32 = prim__ashrB32 x c
94 | Bits64 = prim__ashrB64 x c
90 | Bits64 = prim__ashrB64 x c
95
91
96−public
97bitsAShr : Bits n -> Bits n -> Bits n
92bitsAShr : Bits n -> Bits n -> Bits n
98bitsAShr (MkBits x) (MkBits y) = MkBits (bitsAShr' x y)
93bitsAShr (MkBits x) (MkBits y) = MkBits (bitsAShr' x y)
99
94
@@ -104,7 +99,6 @@ bitsAnd' {n=n} x y with (nextBits n)
104 | Bits32 = prim__andB32 x y
99 | Bits32 = prim__andB32 x y
105 | Bits64 = prim__andB64 x y
100 | Bits64 = prim__andB64 x y
106
101
107−public
108bitsAnd : Bits n -> Bits n -> Bits n
102bitsAnd : Bits n -> Bits n -> Bits n
109bitsAnd (MkBits x) (MkBits y) = MkBits (bitsAnd' x y)
103bitsAnd (MkBits x) (MkBits y) = MkBits (bitsAnd' x y)
110
104
@@ -115,7 +109,6 @@ bitsOr' {n=n} x y with (nextBits n)
115 | Bits32 = prim__orB32 x y
109 | Bits32 = prim__orB32 x y
116 | Bits64 = prim__orB64 x y
110 | Bits64 = prim__orB64 x y
117
111
118−public
119bitsOr : Bits n -> Bits n -> Bits n
112bitsOr : Bits n -> Bits n -> Bits n
120bitsOr (MkBits x) (MkBits y) = MkBits (bitsOr' x y)
113bitsOr (MkBits x) (MkBits y) = MkBits (bitsOr' x y)
121
114
@@ -126,7 +119,6 @@ bitsXOr' {n=n} x y with (nextBits n)
126 | Bits32 = prim__xorB32 x y
119 | Bits32 = prim__xorB32 x y
127 | Bits64 = prim__xorB64 x y
120 | Bits64 = prim__xorB64 x y
128
121
129−public
130bitsXOr : Bits n -> Bits n -> Bits n
122bitsXOr : Bits n -> Bits n -> Bits n
131bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)
123bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)
132
124
@@ -137,7 +129,6 @@ bitsAdd' {n=n} x y with (nextBits n)
137 | Bits32 = pad32 n prim__addB32 x y
129 | Bits32 = pad32 n prim__addB32 x y
138 | Bits64 = pad64 n prim__addB64 x y
130 | Bits64 = pad64 n prim__addB64 x y
139
131
140−public
141bitsAdd : Bits n -> Bits n -> Bits n
132bitsAdd : Bits n -> Bits n -> Bits n
142bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)
133bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)
143
134
@@ -148,7 +139,6 @@ bitsSub' {n=n} x y with (nextBits n)
148 | Bits32 = pad32 n prim__subB32 x y
139 | Bits32 = pad32 n prim__subB32 x y
149 | Bits64 = pad64 n prim__subB64 x y
140 | Bits64 = pad64 n prim__subB64 x y
150
141
151−public
152bitsSub : Bits n -> Bits n -> Bits n
142bitsSub : Bits n -> Bits n -> Bits n
153bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)
143bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)
154
144
@@ -159,7 +149,6 @@ bitsMul' {n=n} x y with (nextBits n)
159 | Bits32 = pad32 n prim__mulB32 x y
149 | Bits32 = pad32 n prim__mulB32 x y
160 | Bits64 = pad64 n prim__mulB64 x y
150 | Bits64 = pad64 n prim__mulB64 x y
161
151
162−public
163bitsMul : Bits n -> Bits n -> Bits n
152bitsMul : Bits n -> Bits n -> Bits n
164bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)
153bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)
165
154
@@ -170,7 +159,6 @@ bitsSDiv' {n=n} x y with (nextBits n)
170 | Bits32 = prim__sdivB32 x y
159 | Bits32 = prim__sdivB32 x y
171 | Bits64 = prim__sdivB64 x y
160 | Bits64 = prim__sdivB64 x y
172
161
173−public
174bitsSDiv : Bits n -> Bits n -> Bits n
162bitsSDiv : Bits n -> Bits n -> Bits n
175bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)
163bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)
176
164
@@ -181,7 +169,6 @@ bitsUDiv' {n=n} x y with (nextBits n)
181 | Bits32 = prim__udivB32 x y
169 | Bits32 = prim__udivB32 x y
182 | Bits64 = prim__udivB64 x y
170 | Bits64 = prim__udivB64 x y
183
171
184−public
185bitsUDiv : Bits n -> Bits n -> Bits n
172bitsUDiv : Bits n -> Bits n -> Bits n
186bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
173bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
187
174
@@ -192,7 +179,6 @@ bitsToStr' {n=n} x with (nextBits n)
192 | Bits32 = prim__b32ToStr x
179 | Bits32 = prim__b32ToStr x
193 | Bits64 = prim__b64ToStr x
180 | Bits64 = prim__b64ToStr x
194
181
195−public
196bitsToStr : Bits n -> String
182bitsToStr : Bits n -> String
197bitsToStr (MkBits x) = bitsToStr' x
183bitsToStr (MkBits x) = bitsToStr' x
198
184
@@ -203,12 +189,8 @@ bitsEq' {n=n} x y with (nextBits n)
203 | Bits32 = prim__eqB32 x y
189 | Bits32 = prim__eqB32 x y
204 | Bits64 = prim__eqB64 x y
190 | Bits64 = prim__eqB64 x y
205
191
206−public
207−bitsEq : (x : Bits n) -> (y : Bits n) -> Equality x y
192+bitsEq : (x : Bits n) -> (y : Bits n) -> Bool
208bitsEq (MkBits x) (MkBits y) =
193bitsEq (MkBits x) (MkBits y) =
209 case (bitsEq' x y) of
194 case (bitsEq' x y) of
210− 0 => Unequal uneq
195+ 0 => False
211− _ => Equal eq
196+ _ => True
212− where
213− postulate uneq : {x : Bits n} -> {y : Bits n} -> x = y -> _|_
214− postulate eq : {x : Bits n} -> {y : Bits n} -> x = y
lib/Prelude/Modular.idr−9
@@ -5,40 +5,31 @@ import Prelude.Bits
5%default total
5%default total
6
6
7-- Integers modulo 2^n
7-- Integers modulo 2^n
8−abstract
9data Mod2 : Nat -> Type where
8data Mod2 : Nat -> Type where
10 MkMod2 : {n : Nat} -> Bits n -> Mod2 n
9 MkMod2 : {n : Nat} -> Bits n -> Mod2 n
11
10
12−public
13modAdd : Mod2 n -> Mod2 n -> Mod2 n
11modAdd : Mod2 n -> Mod2 n -> Mod2 n
14modAdd (MkMod2 x) (MkMod2 y) = MkMod2 (bitsAdd x y)
12modAdd (MkMod2 x) (MkMod2 y) = MkMod2 (bitsAdd x y)
15
13
16−public
17modSub : Mod2 n -> Mod2 n -> Mod2 n
14modSub : Mod2 n -> Mod2 n -> Mod2 n
18modSub (MkMod2 x) (MkMod2 y) = MkMod2 (bitsSub x y)
15modSub (MkMod2 x) (MkMod2 y) = MkMod2 (bitsSub x y)
19
16
20−public
21modMul : Mod2 n -> Mod2 n -> Mod2 n
17modMul : Mod2 n -> Mod2 n -> Mod2 n
22modMul (MkMod2 x) (MkMod2 y) = MkMod2 (bitsMul x y)
18modMul (MkMod2 x) (MkMod2 y) = MkMod2 (bitsMul x y)
23
19
24−public
25modDiv : Mod2 n -> Mod2 n -> Mod2 n
20modDiv : Mod2 n -> Mod2 n -> Mod2 n
26modDiv (MkMod2 x) (MkMod2 y) = MkMod2 (bitsUDiv x y)
21modDiv (MkMod2 x) (MkMod2 y) = MkMod2 (bitsUDiv x y)
27
22
28−public
29modToStr : Mod2 n -> String
23modToStr : Mod2 n -> String
30modToStr (MkMod2 x) = bitsToStr x
24modToStr (MkMod2 x) = bitsToStr x
31
25
32%assert_total
26%assert_total
33−public
34intToMod : {n : Nat} -> Int -> Mod2 n
27intToMod : {n : Nat} -> Int -> Mod2 n
35intToMod {n=n} x = MkMod2 (intToBits x)
28intToMod {n=n} x = MkMod2 (intToBits x)
36
29
37−public
38modToBits : Mod2 n -> Bits n
30modToBits : Mod2 n -> Bits n
39modToBits (MkMod2 x) = x
31modToBits (MkMod2 x) = x
40
32
41−public
42bitsToMod : Bits n -> Mod2 n
33bitsToMod : Bits n -> Mod2 n
43bitsToMod x = MkMod2 x
34bitsToMod x = MkMod2 x
44
35