358c623 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Partially restore access qualifiers

358c623Benjamin Saunders14 years ago

lib/Prelude/Bits.idr+19

compare with master

unifiedsplit

@@ -15,6 +15,7 @@ nextBits x with (log2ceil x)

15 | (S (S (S (S O)))) = Bits16

16 | _ = Bits8

18+public

18data Bits : Nat -> Type where

19data Bits : Nat -> Type where

19 MkBits : {n : Nat} -> nextBits n -> Bits n

20 MkBits : {n : Nat} -> nextBits n -> Bits n

@@ -56,6 +57,7 @@ intToBits' {n=n} x with (nextBits n)

56 | Bits64 = let pad = (prim__intToB64 (cast (64-n))) in

57 | Bits64 = let pad = (prim__intToB64 (cast (64-n))) in

57 prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad

58 prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad

60+public

59intToBits : {n : Nat} -> Int -> Bits n

61intToBits : {n : Nat} -> Int -> Bits n

60intToBits n = MkBits (intToBits' n)

62intToBits n = MkBits (intToBits' n)

@@ -69,6 +71,7 @@ bitsShl' {n=n} x c with (nextBits n)

69 | Bits32 = pad32 n prim__shlB32 x c

71 | Bits32 = pad32 n prim__shlB32 x c

70 | Bits64 = pad64 n prim__shlB64 x c

72 | Bits64 = pad64 n prim__shlB64 x c

74+public

72bitsShl : Bits n -> Bits n -> Bits n

75bitsShl : Bits n -> Bits n -> Bits n

73bitsShl (MkBits x) (MkBits y) = MkBits (bitsShl' x y)

76bitsShl (MkBits x) (MkBits y) = MkBits (bitsShl' x y)

@@ -79,6 +82,7 @@ bitsLShr' {n=n} x c with (nextBits n)

79 | Bits32 = prim__lshrB32 x c

82 | Bits32 = prim__lshrB32 x c

80 | Bits64 = prim__lshrB64 x c

83 | Bits64 = prim__lshrB64 x c

85+public

82bitsLShr : Bits n -> Bits n -> Bits n

86bitsLShr : Bits n -> Bits n -> Bits n

83bitsLShr (MkBits x) (MkBits y) = MkBits (bitsLShr' x y)

87bitsLShr (MkBits x) (MkBits y) = MkBits (bitsLShr' x y)

@@ -89,6 +93,7 @@ bitsAShr' {n=n} x c with (nextBits n)

89 | Bits32 = prim__ashrB32 x c

93 | Bits32 = prim__ashrB32 x c

90 | Bits64 = prim__ashrB64 x c

94 | Bits64 = prim__ashrB64 x c

96+public

92bitsAShr : Bits n -> Bits n -> Bits n

97bitsAShr : Bits n -> Bits n -> Bits n

93bitsAShr (MkBits x) (MkBits y) = MkBits (bitsAShr' x y)

98bitsAShr (MkBits x) (MkBits y) = MkBits (bitsAShr' x y)

@@ -99,6 +104,7 @@ bitsAnd' {n=n} x y with (nextBits n)

99 | Bits32 = prim__andB32 x y

104 | Bits32 = prim__andB32 x y

100 | Bits64 = prim__andB64 x y

105 | Bits64 = prim__andB64 x y

101

106

107+public

102bitsAnd : Bits n -> Bits n -> Bits n

108bitsAnd : Bits n -> Bits n -> Bits n

103bitsAnd (MkBits x) (MkBits y) = MkBits (bitsAnd' x y)

109bitsAnd (MkBits x) (MkBits y) = MkBits (bitsAnd' x y)

104

110

@@ -109,6 +115,7 @@ bitsOr' {n=n} x y with (nextBits n)

109 | Bits32 = prim__orB32 x y

115 | Bits32 = prim__orB32 x y

110 | Bits64 = prim__orB64 x y

116 | Bits64 = prim__orB64 x y

111

117

118+public

112bitsOr : Bits n -> Bits n -> Bits n

119bitsOr : Bits n -> Bits n -> Bits n

113bitsOr (MkBits x) (MkBits y) = MkBits (bitsOr' x y)

120bitsOr (MkBits x) (MkBits y) = MkBits (bitsOr' x y)

114

121

@@ -119,6 +126,7 @@ bitsXOr' {n=n} x y with (nextBits n)

119 | Bits32 = prim__xorB32 x y

126 | Bits32 = prim__xorB32 x y

120 | Bits64 = prim__xorB64 x y

127 | Bits64 = prim__xorB64 x y

121

128

129+public

122bitsXOr : Bits n -> Bits n -> Bits n

130bitsXOr : Bits n -> Bits n -> Bits n

123bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)

131bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)

124

132

@@ -129,6 +137,7 @@ bitsAdd' {n=n} x y with (nextBits n)

129 | Bits32 = pad32 n prim__addB32 x y

137 | Bits32 = pad32 n prim__addB32 x y

130 | Bits64 = pad64 n prim__addB64 x y

138 | Bits64 = pad64 n prim__addB64 x y

131

139

140+public

132bitsAdd : Bits n -> Bits n -> Bits n

141bitsAdd : Bits n -> Bits n -> Bits n

133bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)

142bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)

134

143

@@ -139,6 +148,7 @@ bitsSub' {n=n} x y with (nextBits n)

139 | Bits32 = pad32 n prim__subB32 x y

148 | Bits32 = pad32 n prim__subB32 x y

140 | Bits64 = pad64 n prim__subB64 x y

149 | Bits64 = pad64 n prim__subB64 x y

141

150

151+public

142bitsSub : Bits n -> Bits n -> Bits n

152bitsSub : Bits n -> Bits n -> Bits n

143bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)

153bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)

144

154

@@ -149,6 +159,7 @@ bitsMul' {n=n} x y with (nextBits n)

149 | Bits32 = pad32 n prim__mulB32 x y

159 | Bits32 = pad32 n prim__mulB32 x y

150 | Bits64 = pad64 n prim__mulB64 x y

160 | Bits64 = pad64 n prim__mulB64 x y

151

161

162+public

152bitsMul : Bits n -> Bits n -> Bits n

163bitsMul : Bits n -> Bits n -> Bits n

153bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)

164bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)

154

165

@@ -159,6 +170,7 @@ bitsSDiv' {n=n} x y with (nextBits n)

159 | Bits32 = prim__sdivB32 x y

170 | Bits32 = prim__sdivB32 x y

160 | Bits64 = prim__sdivB64 x y

171 | Bits64 = prim__sdivB64 x y

161

172

173+public

162bitsSDiv : Bits n -> Bits n -> Bits n

174bitsSDiv : Bits n -> Bits n -> Bits n

163bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)

175bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)

164

176

@@ -169,6 +181,7 @@ bitsUDiv' {n=n} x y with (nextBits n)

169 | Bits32 = prim__udivB32 x y

181 | Bits32 = prim__udivB32 x y

170 | Bits64 = prim__udivB64 x y

182 | Bits64 = prim__udivB64 x y

171

183

184+public

172bitsUDiv : Bits n -> Bits n -> Bits n

185bitsUDiv : Bits n -> Bits n -> Bits n

173bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)

186bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)

174

187

@@ -179,6 +192,7 @@ bitsToStr' {n=n} x with (nextBits n)

179 | Bits32 = prim__b32ToStr x

192 | Bits32 = prim__b32ToStr x

180 | Bits64 = prim__b64ToStr x

193 | Bits64 = prim__b64ToStr x

181

194

195+public

182bitsToStr : Bits n -> String

196bitsToStr : Bits n -> String

183bitsToStr (MkBits x) = bitsToStr' x

197bitsToStr (MkBits x) = bitsToStr' x

184

198

@@ -190,6 +204,7 @@ bitsLt' {n=n} x y with (nextBits n)

190 | Bits32 = prim__ltB32 x y

204 | Bits32 = prim__ltB32 x y

191 | Bits64 = prim__ltB64 x y

205 | Bits64 = prim__ltB64 x y

192

206

207+public

193bitsLt : (x : Bits n) -> (y : Bits n) -> Bool

208bitsLt : (x : Bits n) -> (y : Bits n) -> Bool

194bitsLt (MkBits x) (MkBits y) =

209bitsLt (MkBits x) (MkBits y) =

195 case (bitsLt' x y) of

210 case (bitsLt' x y) of

@@ -203,6 +218,7 @@ bitsLte' {n=n} x y with (nextBits n)

203 | Bits32 = prim__lteB32 x y

218 | Bits32 = prim__lteB32 x y

204 | Bits64 = prim__lteB64 x y

219 | Bits64 = prim__lteB64 x y

205

220

221+public

206bitsLte : (x : Bits n) -> (y : Bits n) -> Bool

222bitsLte : (x : Bits n) -> (y : Bits n) -> Bool

207bitsLte (MkBits x) (MkBits y) =

223bitsLte (MkBits x) (MkBits y) =

208 case (bitsLte' x y) of

224 case (bitsLte' x y) of

@@ -216,6 +232,7 @@ bitsEq' {n=n} x y with (nextBits n)

216 | Bits32 = prim__eqB32 x y

232 | Bits32 = prim__eqB32 x y

217 | Bits64 = prim__eqB64 x y

233 | Bits64 = prim__eqB64 x y

218

234

235+public

219bitsEq : (x : Bits n) -> (y : Bits n) -> Bool

236bitsEq : (x : Bits n) -> (y : Bits n) -> Bool

220bitsEq (MkBits x) (MkBits y) =

237bitsEq (MkBits x) (MkBits y) =

221 case (bitsEq' x y) of

238 case (bitsEq' x y) of

@@ -229,6 +246,7 @@ bitsGte' {n=n} x y with (nextBits n)

229 | Bits32 = prim__gteB32 x y

246 | Bits32 = prim__gteB32 x y

230 | Bits64 = prim__gteB64 x y

247 | Bits64 = prim__gteB64 x y

231

248

249+public

232bitsGte : (x : Bits n) -> (y : Bits n) -> Bool

250bitsGte : (x : Bits n) -> (y : Bits n) -> Bool

233bitsGte (MkBits x) (MkBits y) =

251bitsGte (MkBits x) (MkBits y) =

234 case (bitsGte' x y) of

252 case (bitsGte' x y) of

@@ -242,6 +260,7 @@ bitsGt' {n=n} x y with (nextBits n)

242 | Bits32 = prim__gtB32 x y

260 | Bits32 = prim__gtB32 x y

243 | Bits64 = prim__gtB64 x y

261 | Bits64 = prim__gtB64 x y

244

262

263+public

245bitsGt : (x : Bits n) -> (y : Bits n) -> Bool

264bitsGt : (x : Bits n) -> (y : Bits n) -> Bool

246bitsGt (MkBits x) (MkBits y) =

265bitsGt (MkBits x) (MkBits y) =

247 case (bitsGt' x y) of

266 case (bitsGt' x y) of

lib/Prelude/Modular.idr+9

@@ -5,31 +5,40 @@ import Prelude.Bits

5%default total

7-- Integers modulo 2^n

8+public

8data Mod2 : Nat -> Type where

9data Mod2 : Nat -> Type where

9 MkMod2 : {n : Nat} -> Bits n -> Mod2 n

10 MkMod2 : {n : Nat} -> Bits n -> Mod2 n

12+public

11modAdd : Mod2 n -> Mod2 n -> Mod2 n

13modAdd : Mod2 n -> Mod2 n -> Mod2 n

12modAdd (MkMod2 x) (MkMod2 y) = MkMod2 (bitsAdd x y)

14modAdd (MkMod2 x) (MkMod2 y) = MkMod2 (bitsAdd x y)

16+public

14modSub : Mod2 n -> Mod2 n -> Mod2 n

17modSub : Mod2 n -> Mod2 n -> Mod2 n

15modSub (MkMod2 x) (MkMod2 y) = MkMod2 (bitsSub x y)

18modSub (MkMod2 x) (MkMod2 y) = MkMod2 (bitsSub x y)

20+public

17modMul : Mod2 n -> Mod2 n -> Mod2 n

21modMul : Mod2 n -> Mod2 n -> Mod2 n

18modMul (MkMod2 x) (MkMod2 y) = MkMod2 (bitsMul x y)

22modMul (MkMod2 x) (MkMod2 y) = MkMod2 (bitsMul x y)

24+public

20modDiv : Mod2 n -> Mod2 n -> Mod2 n

25modDiv : Mod2 n -> Mod2 n -> Mod2 n

21modDiv (MkMod2 x) (MkMod2 y) = MkMod2 (bitsUDiv x y)

26modDiv (MkMod2 x) (MkMod2 y) = MkMod2 (bitsUDiv x y)

28+public

23modToStr : Mod2 n -> String

29modToStr : Mod2 n -> String

24modToStr (MkMod2 x) = bitsToStr x

30modToStr (MkMod2 x) = bitsToStr x

26%assert_total

32%assert_total

33+public

27intToMod : {n : Nat} -> Int -> Mod2 n

34intToMod : {n : Nat} -> Int -> Mod2 n

28intToMod {n=n} x = MkMod2 (intToBits x)

35intToMod {n=n} x = MkMod2 (intToBits x)

37+public

30modToBits : Mod2 n -> Bits n

38modToBits : Mod2 n -> Bits n

31modToBits (MkMod2 x) = x

39modToBits (MkMod2 x) = x

41+public

33bitsToMod : Bits n -> Mod2 n

42bitsToMod : Bits n -> Mod2 n

34bitsToMod x = MkMod2 x

43bitsToMod x = MkMod2 x