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

git.iko.soy/Idris-dev

Basic bit-twiddling primitives

commit8216c7f81cbb4af4d8b932ab1b4e220532e34733 authorBenjamin Saunders <besaunde@sfu.ca> dateThu 20 Dec 2012, 16:54 (14 years ago) parent348cf91

3 files changed+108−6

compare with master

unifiedsplit

lib/Prelude/Bits.idr+48−6 src/IRTS/Lang.hs+4 src/Idris/Primitives.hs+56

lib/Prelude/Bits.idr+48−6

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

2222 | Bits32 = prim__intToB32 x

2323 | Bits64 = prim__intToB64 x

2424

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+

2567bitsAdd : {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)

2769 | Bits8 = prim__addB8 x y

2870 | Bits16 = prim__addB16 x y

2971 | Bits32 = prim__addB32 x y

3072 | Bits64 = prim__addB64 x y

3173

3274bitsSub : {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)

3476 | Bits8 = prim__subB8 x y

3577 | Bits16 = prim__subB16 x y

3678 | Bits32 = prim__subB32 x y

3779 | Bits64 = prim__subB64 x y

3880

3981bitsMul : {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)

4183 | Bits8 = prim__mulB8 x y

4284 | Bits16 = prim__mulB16 x y

4385 | Bits32 = prim__mulB32 x y

4486 | Bits64 = prim__mulB64 x y

4587

4688bitsSDiv : {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)

4890 | Bits8 = prim__sdivB8 x y

4991 | Bits16 = prim__sdivB16 x y

5092 | Bits32 = prim__sdivB32 x y

5193 | Bits64 = prim__sdivB64 x y

5294

5395bitsUDiv : {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)

5597 | Bits8 = prim__udivB8 x y

5698 | Bits16 = prim__udivB16 x y

5799 | Bits32 = prim__udivB32 x y

58100 | Bits64 = prim__udivB64 x y

59101

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

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

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

62104 | Bits8 = prim__b8ToStr x

63105 | Bits16 = prim__b16ToStr x

64106 | Bits32 = prim__b32ToStr x

src/IRTS/Lang.hs+4

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

4141 | LPrintNum | LPrintStr | LReadStr

4242

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

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

4851 | LB32Z64 | LB32S64 | LB32T8 | LB32T16

5054 | LB64T8 | LB64T16 | LB64T32

5256 | LB8Str | LB16Str | LB32Str | LB64Str

src/Idris/Primitives.hs+56

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

8989 (2, LB8UDiv) total,

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

9191 (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,

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

93107 (1, LB8Z16) total,

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

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

114128 (2, LB16UDiv) total,

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

116130 (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,

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

118146 (1, LB16Z32) total,

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

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

137165 (2, LB32UDiv) total,

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

139167 (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,

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

141183 (1, LB32Z64) total,

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

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

158200 (2, LB64UDiv) total,

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

160202 (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,

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

162218 (1, LB64T8) total,

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