8216c7f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Basic bit-twiddling primitives

8216c7fBenjamin Saunders14 years ago

lib/Prelude/Bits.idr+48−6

compare with master

unifiedsplit

@@ -22,43 +22,85 @@ intToBits {n=n} x with (Bits n)

22 | Bits32 = prim__intToB32 x

23 | Bits64 = prim__intToB64 x

25+bitsShl : {n: Nat} -> Bits n -> Bits n -> Bits n

26+bitsShl {n=n} x c with (Bits n)

27+ | Bits8 = prim__shlB8 x c

28+ | Bits16 = prim__shlB16 x c

29+ | Bits32 = prim__shlB32 x c

30+ | Bits64 = prim__shlB64 x c

31+

32+bitsLShr : {n: Nat} -> Bits n -> Bits n -> Bits n

33+bitsLShr {n=n} x c with (Bits n)

34+ | Bits8 = prim__lshrB8 x c

35+ | Bits16 = prim__lshrB16 x c

36+ | Bits32 = prim__lshrB32 x c

37+ | Bits64 = prim__lshrB64 x c

38+

39+bitsAShr : {n: Nat} -> Bits n -> Bits n -> Bits n

40+bitsAShr {n=n} x c with (Bits n)

41+ | Bits8 = prim__ashrB8 x c

42+ | Bits16 = prim__ashrB16 x c

43+ | Bits32 = prim__ashrB32 x c

44+ | Bits64 = prim__ashrB64 x c

45+

46+bitsAnd : {n: Nat} -> Bits n -> Bits n -> Bits n

47+bitsAnd {n=n} x y with (Bits n)

48+ | Bits8 = prim__andB8 x y

49+ | Bits16 = prim__andB16 x y

50+ | Bits32 = prim__andB32 x y

51+ | Bits64 = prim__andB64 x y

52+

53+bitsOr : {n: Nat} -> Bits n -> Bits n -> Bits n

54+bitsOr {n=n} x y with (Bits n)

55+ | Bits8 = prim__orB8 x y

56+ | Bits16 = prim__orB16 x y

57+ | Bits32 = prim__orB32 x y

58+ | Bits64 = prim__orB64 x y

59+

60+bitsXOr : {n: Nat} -> Bits n -> Bits n -> Bits n

61+bitsXOr {n=n} x y with (Bits n)

62+ | Bits8 = prim__xorB8 x y

63+ | Bits16 = prim__xorB16 x y

64+ | Bits32 = prim__xorB32 x y

65+ | Bits64 = prim__xorB64 x y

66+

25bitsAdd : {n : Nat} -> Bits n -> Bits n -> Bits n

67bitsAdd : {n : Nat} -> Bits n -> Bits n -> Bits n

26−bitsAdd {n=m} x y with (Bits m)

68+bitsAdd {n=n} x y with (Bits n)

27 | Bits8 = prim__addB8 x y

69 | Bits8 = prim__addB8 x y

28 | Bits16 = prim__addB16 x y

70 | Bits16 = prim__addB16 x y

29 | Bits32 = prim__addB32 x y

71 | Bits32 = prim__addB32 x y

30 | Bits64 = prim__addB64 x y

72 | Bits64 = prim__addB64 x y

32bitsSub : {n : Nat} -> Bits n -> Bits n -> Bits n

74bitsSub : {n : Nat} -> Bits n -> Bits n -> Bits n

33−bitsSub {n=m} x y with (Bits m)

75+bitsSub {n=n} x y with (Bits n)

34 | Bits8 = prim__subB8 x y

76 | Bits8 = prim__subB8 x y

35 | Bits16 = prim__subB16 x y

77 | Bits16 = prim__subB16 x y

36 | Bits32 = prim__subB32 x y

78 | Bits32 = prim__subB32 x y

37 | Bits64 = prim__subB64 x y

79 | Bits64 = prim__subB64 x y

39bitsMul : {n : Nat} -> Bits n -> Bits n -> Bits n

81bitsMul : {n : Nat} -> Bits n -> Bits n -> Bits n

40−bitsMul {n=m} x y with (Bits m)

82+bitsMul {n=n} x y with (Bits n)

41 | Bits8 = prim__mulB8 x y

83 | Bits8 = prim__mulB8 x y

42 | Bits16 = prim__mulB16 x y

84 | Bits16 = prim__mulB16 x y

43 | Bits32 = prim__mulB32 x y

85 | Bits32 = prim__mulB32 x y

44 | Bits64 = prim__mulB64 x y

86 | Bits64 = prim__mulB64 x y

46bitsSDiv : {n : Nat} -> Bits n -> Bits n -> Bits n

88bitsSDiv : {n : Nat} -> Bits n -> Bits n -> Bits n

47−bitsSDiv {n=m} x y with (Bits m)

89+bitsSDiv {n=n} x y with (Bits n)

48 | Bits8 = prim__sdivB8 x y

90 | Bits8 = prim__sdivB8 x y

49 | Bits16 = prim__sdivB16 x y

91 | Bits16 = prim__sdivB16 x y

50 | Bits32 = prim__sdivB32 x y

92 | Bits32 = prim__sdivB32 x y

51 | Bits64 = prim__sdivB64 x y

93 | Bits64 = prim__sdivB64 x y

53bitsUDiv : {n : Nat} -> Bits n -> Bits n -> Bits n

95bitsUDiv : {n : Nat} -> Bits n -> Bits n -> Bits n

54−bitsUDiv {n=m} x y with (Bits m)

96+bitsUDiv {n=n} x y with (Bits n)

55 | Bits8 = prim__udivB8 x y

97 | Bits8 = prim__udivB8 x y

56 | Bits16 = prim__udivB16 x y

98 | Bits16 = prim__udivB16 x y

57 | Bits32 = prim__udivB32 x y

99 | Bits32 = prim__udivB32 x y

58 | Bits64 = prim__udivB64 x y

100 | Bits64 = prim__udivB64 x y

101

60bitsToStr : {n : Nat} -> Bits n -> String

102bitsToStr : {n : Nat} -> Bits n -> String

61−bitsToStr {n=m} x with (Bits m)

103+bitsToStr {n=n} x with (Bits n)

62 | Bits8 = prim__b8ToStr x

104 | Bits8 = prim__b8ToStr x

63 | Bits16 = prim__b16ToStr x

105 | Bits16 = prim__b16ToStr x

64 | Bits32 = prim__b32ToStr x

106 | Bits32 = prim__b32ToStr x

src/IRTS/Lang.hs+4

@@ -41,12 +41,16 @@ data PrimFn = LPlus | LMinus | LTimes | LDiv | LMod

41 | LPrintNum | LPrintStr | LReadStr

44 | LB8Z16 | LB8Z32 | LB8Z64 | LB8S16 | LB8S32 | LB8S64 -- Zero/Sign extension

45 | LB8Z16 | LB8Z32 | LB8Z64 | LB8S16 | LB8S32 | LB8S64 -- Zero/Sign extension

46 | LB16Z32 | LB16Z64 | LB16S32 | LB16S64 | LB16T8 -- and Truncation

48 | LB16Z32 | LB16Z64 | LB16S32 | LB16S64 | LB16T8 -- and Truncation

48 | LB32Z64 | LB32S64 | LB32T8 | LB32T16

51 | LB32Z64 | LB32S64 | LB32T8 | LB32T16

50 | LB64T8 | LB64T16 | LB64T32

54 | LB64T8 | LB64T16 | LB64T32

52 | LB8Str | LB16Str | LB32Str | LB64Str

56 | LB8Str | LB16Str | LB32Str | LB64Str

src/Idris/Primitives.hs+56

@@ -89,6 +89,20 @@ primitives =

89 (2, LB8UDiv) total,

90 Prim (UN "prim__sdivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8div)

91 (2, LB8SDiv) total,

92+ Prim (UN "prim__shlB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> shiftL x (fromIntegral y)))

93+ (2, LB8Shl) total,

94+ Prim (UN "prim__lshrB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> shiftR x (fromIntegral y)))

95+ (2, LB8AShr) total,

96+ Prim (UN "prim__ashrB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> fromIntegral $

97+ shiftR (fromIntegral x :: Int8)

98+ (fromIntegral y)))

99+ (2, LB8LShr) total,

100+ Prim (UN "prim__andB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (.&.))

101+ (2, LB8And) total,

102+ Prim (UN "prim__orB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (.|.))

103+ (2, LB8Or) total,

104+ Prim (UN "prim__xorB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin xor)

105+ (2, LB8Xor) total,

92 Prim (UN "prim__zextB8_16") (ty [B8Type] B16Type) 1 zext8_16

106 Prim (UN "prim__zextB8_16") (ty [B8Type] B16Type) 1 zext8_16

93 (1, LB8Z16) total,

107 (1, LB8Z16) total,

94 Prim (UN "prim__zextB8_32") (ty [B8Type] B32Type) 1 zext8_32

108 Prim (UN "prim__zextB8_32") (ty [B8Type] B32Type) 1 zext8_32

@@ -114,6 +128,20 @@ primitives =

114 (2, LB16UDiv) total,

128 (2, LB16UDiv) total,

115 Prim (UN "prim__sdivB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin s16div)

129 Prim (UN "prim__sdivB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin s16div)

116 (2, LB16SDiv) total,

130 (2, LB16SDiv) total,

131+ Prim (UN "prim__shlB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> shiftL x (fromIntegral y)))

132+ (2, LB16Shl) total,

133+ Prim (UN "prim__lshrB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> shiftR x (fromIntegral y)))

134+ (2, LB16AShr) total,

135+ Prim (UN "prim__ashrB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> fromIntegral $

136+ shiftR (fromIntegral x :: Int16)

137+ (fromIntegral y)))

138+ (2, LB16LShr) total,

139+ Prim (UN "prim__andB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (.&.))

140+ (2, LB16And) total,

141+ Prim (UN "prim__orB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (.|.))

142+ (2, LB16Or) total,

143+ Prim (UN "prim__xorB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin xor)

144+ (2, LB16Xor) total,

117 Prim (UN "prim__zextB16_32") (ty [B16Type] B32Type) 1 zext16_32

145 Prim (UN "prim__zextB16_32") (ty [B16Type] B32Type) 1 zext16_32

118 (1, LB16Z32) total,

146 (1, LB16Z32) total,

119 Prim (UN "prim__zextB16_64") (ty [B16Type] B64Type) 1 zext16_64

147 Prim (UN "prim__zextB16_64") (ty [B16Type] B64Type) 1 zext16_64

@@ -137,6 +165,20 @@ primitives =

137 (2, LB32UDiv) total,

165 (2, LB32UDiv) total,

138 Prim (UN "prim__sdivB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin s32div)

166 Prim (UN "prim__sdivB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin s32div)

139 (2, LB32SDiv) total,

167 (2, LB32SDiv) total,

168+ Prim (UN "prim__shlB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> shiftL x (fromIntegral y)))

169+ (2, LB32Shl) total,

170+ Prim (UN "prim__lshrB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> shiftR x (fromIntegral y)))

171+ (2, LB32AShr) total,

172+ Prim (UN "prim__ashrB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> fromIntegral $

173+ shiftR (fromIntegral x :: Int32)

174+ (fromIntegral y)))

175+ (2, LB32LShr) total,

176+ Prim (UN "prim__andB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (.&.))

177+ (2, LB32And) total,

178+ Prim (UN "prim__orB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (.|.))

179+ (2, LB32Or) total,

180+ Prim (UN "prim__xorB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin xor)

181+ (2, LB32Xor) total,

140 Prim (UN "prim__zextB32_64") (ty [B32Type] B64Type) 1 zext32_64

182 Prim (UN "prim__zextB32_64") (ty [B32Type] B64Type) 1 zext32_64

141 (1, LB32Z64) total,

183 (1, LB32Z64) total,

142 Prim (UN "prim__sextB32_64") (ty [B32Type] B64Type) 1 sext32_64

184 Prim (UN "prim__sextB32_64") (ty [B32Type] B64Type) 1 sext32_64

@@ -158,6 +200,20 @@ primitives =

158 (2, LB64UDiv) total,

200 (2, LB64UDiv) total,

159 Prim (UN "prim__sdivB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin s64div)

201 Prim (UN "prim__sdivB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin s64div)

160 (2, LB64SDiv) total,

202 (2, LB64SDiv) total,

203+ Prim (UN "prim__shlB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> shiftL x (fromIntegral y)))

204+ (2, LB64Shl) total,

205+ Prim (UN "prim__lshrB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> shiftR x (fromIntegral y)))

206+ (2, LB64AShr) total,

207+ Prim (UN "prim__ashrB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> fromIntegral $

208+ shiftR (fromIntegral x :: Int64)

209+ (fromIntegral y)))

210+ (2, LB64LShr) total,

211+ Prim (UN "prim__andB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (.&.))

212+ (2, LB64And) total,

213+ Prim (UN "prim__orB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (.|.))

214+ (2, LB64Or) total,

215+ Prim (UN "prim__xorB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin xor)

216+ (2, LB64Xor) total,

161 Prim (UN "prim__truncB64_8") (ty [B64Type] B8Type) 1 trunc64_8

217 Prim (UN "prim__truncB64_8") (ty [B64Type] B8Type) 1 trunc64_8

162 (1, LB64T8) total,

218 (1, LB64T8) total,

163 Prim (UN "prim__truncB64_16") (ty [B64Type] B16Type) 1 trunc64_16

219 Prim (UN "prim__truncB64_16") (ty [B64Type] B16Type) 1 trunc64_16