ea11519 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Comment out most of Data.Bits and Data.Mod2

ea11519Edwin Brady13 years ago

lib/Data/Bits.idr+14−10

compare with master

unifiedsplit

@@ -32,16 +32,16 @@ natToBits' : machineTy n -> Nat -> machineTy n

32natToBits' a O = a

33natToBits' {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'

35+ natToBits' a (S x') | S O = natToBits' {n = S O} (prim__addB16 a (prim__intToB16 1)) x'

36− natToBits' a (S x') | S (S O) = natToBits' (prim__addB32 a (prim__intToB32 1)) x'

36+ natToBits' a (S x') | S (S O) = natToBits' {n=S (S O)} (prim__addB32 a (prim__intToB32 1)) x'

37− natToBits' a (S x') | S (S (S _)) = natToBits' (prim__addB64 a (prim__intToB64 1)) x'

37+ natToBits' a (S x') | S (S (S k)) = natToBits' {n = S (S (S k))} (prim__addB64 a (prim__intToB64 1)) x'

39natToBits : Nat -> machineTy n

40natToBits {n=n} x with n

41− | O = natToBits' (prim__intToB8 0) x

41+ | O = natToBits' {n=O} (prim__intToB8 0) x

42− | S O = natToBits' (prim__intToB16 0) x

42+ | S O = natToBits' {n=S O} (prim__intToB16 0) x

43− | S (S O) = natToBits' (prim__intToB32 0) x

43+ | S (S O) = natToBits' {n=S (S O)} (prim__intToB32 0) x

44− | S (S (S _)) = natToBits' (prim__intToB64 0) x

44+ | S (S (S k)) = natToBits' {n=S (S (S k))} (prim__intToB64 0) x

46getPad : Nat -> machineTy n

47getPad n = natToBits ((bitsUsed (nextBytes n)) - n)

@@ -111,7 +111,8 @@ shiftRightLogical' {n=n} x c with n

111

112public

113shiftRightLogical : Bits n -> Bits n -> Bits n

114−shiftRightLogical (MkBits x) (MkBits y) = MkBits (shiftRightLogical' x y)

114+shiftRightLogical {n} (MkBits x) (MkBits y)

115+ = MkBits {n} (shiftRightLogical' {n=nextBytes n} x y)

115

116

116shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

117shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

117shiftRightArithmetic' {n=n} x c with (nextBytes n)

118shiftRightArithmetic' {n=n} x c with (nextBytes n)

@@ -133,7 +134,7 @@ and' {n=n} x y with n

133

134

134public

135public

135and : Bits n -> Bits n -> Bits n

136and : Bits n -> Bits n -> Bits n

136−and (MkBits x) (MkBits y) = MkBits (and' x y)

137+and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)

137

138

138or' : machineTy n -> machineTy n -> machineTy n

139or' : machineTy n -> machineTy n -> machineTy n

139or' {n=n} x y with n

140or' {n=n} x y with n

@@ -144,7 +145,7 @@ or' {n=n} x y with n

144

145

145public

146public

146or : Bits n -> Bits n -> Bits n

147or : Bits n -> Bits n -> Bits n

147−or (MkBits x) (MkBits y) = MkBits (or' x y)

148+or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)

148

149

149xor' : machineTy n -> machineTy n -> machineTy n

150xor' : machineTy n -> machineTy n -> machineTy n

150xor' {n=n} x y with n

151xor' {n=n} x y with n

@@ -153,6 +154,7 @@ xor' {n=n} x y with n

153 | S (S O) = prim__xorB32 x y

154 | S (S O) = prim__xorB32 x y

154 | S (S (S _)) = prim__xorB64 x y

155 | S (S (S _)) = prim__xorB64 x y

155

156

157+{-

156public

158public

157xor : Bits n -> Bits n -> Bits n

159xor : Bits n -> Bits n -> Bits n

158xor (MkBits x) (MkBits y) = MkBits (xor' x y)

160xor (MkBits x) (MkBits y) = MkBits (xor' x y)

@@ -437,3 +439,5 @@ bitsToStr x = pack (helper last x)

437

439

438instance Show (Bits n) where

440instance Show (Bits n) where

439 show = bitsToStr

441 show = bitsToStr

442+

443+-}

lib/Data/Mod2.idr+2

@@ -4,6 +4,7 @@ import Data.Bits

5%default total

7+{-

7-- Integers modulo 2^n

8-- Integers modulo 2^n

8public

9public

9data Mod2 : Nat -> Type where

10data Mod2 : Nat -> Type where

@@ -62,3 +63,4 @@ modToStr x = pack (reverse (helper x))

63instance Show (Mod2 n) where

64instance Show (Mod2 n) where

64 show = modToStr

65 show = modToStr

66+-}