9e543e6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Remainder primitives for bits

9e543e6Benjamin Saunders14 years ago

lib/Prelude/Bits.idr+22

compare with master

unifiedsplit

@@ -185,6 +185,28 @@ public

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

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

187

188+bitsSRem' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n

189+bitsSRem' {n=n} x y with (nextBits n)

190+ | Bits8 = prim__sremB8 x y

191+ | Bits16 = prim__sremB16 x y

192+ | Bits32 = prim__sremB32 x y

193+ | Bits64 = prim__sremB64 x y

194+

195+public

196+bitsSRem : Bits n -> Bits n -> Bits n

197+bitsSRem (MkBits x) (MkBits y) = MkBits (bitsSRem' x y)

198+

199+bitsURem' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n

200+bitsURem' {n=n} x y with (nextBits n)

201+ | Bits8 = prim__uremB8 x y

202+ | Bits16 = prim__uremB16 x y

203+ | Bits32 = prim__uremB32 x y

204+ | Bits64 = prim__uremB64 x y

205+

206+public

207+bitsURem : Bits n -> Bits n -> Bits n

208+bitsURem (MkBits x) (MkBits y) = MkBits (bitsURem' x y)

209+

188-- TODO: Proofy comparisons via postulates

210-- TODO: Proofy comparisons via postulates

189bitsLt' : (x : nextBits n) -> (y : nextBits n) -> Int

211bitsLt' : (x : nextBits n) -> (y : nextBits n) -> Int

190bitsLt' {n=n} x y with (nextBits n)

212bitsLt' {n=n} x y with (nextBits n)

src/IRTS/Lang.hs+4−4

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

41 | LPrintNum | LPrintStr | LReadStr

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

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

54 | LB32Z64 | LB32S64 | LB32T8 | LB32T16

58 | LB64T8 | LB64T16 | LB64T32

src/Idris/Primitives.hs+28

@@ -97,6 +97,10 @@ primitives =

97 (2, LB8UDiv) total,

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

99 (2, LB8SDiv) total,

100+ Prim (UN "prim__uremB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin rem)

101+ (2, LB8URem) total,

102+ Prim (UN "prim__sremB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8rem)

103+ (2, LB8SRem) total,

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

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

101 (2, LB8Shl) total,

105 (2, LB8Shl) total,

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

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

@@ -146,6 +150,10 @@ primitives =

146 (2, LB16UDiv) total,

150 (2, LB16UDiv) total,

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

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

148 (2, LB16SDiv) total,

152 (2, LB16SDiv) total,

153+ Prim (UN "prim__uremB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin rem)

154+ (2, LB16URem) total,

155+ Prim (UN "prim__sremB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin s16rem)

156+ (2, LB16SRem) total,

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

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

150 (2, LB16Shl) total,

158 (2, LB16Shl) total,

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

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

@@ -193,6 +201,10 @@ primitives =

193 (2, LB32UDiv) total,

201 (2, LB32UDiv) total,

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

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

195 (2, LB32SDiv) total,

203 (2, LB32SDiv) total,

204+ Prim (UN "prim__uremB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin rem)

205+ (2, LB32URem) total,

206+ Prim (UN "prim__sremB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin s32rem)

207+ (2, LB32SRem) total,

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

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

197 (2, LB32Shl) total,

209 (2, LB32Shl) total,

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

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

@@ -238,6 +250,10 @@ primitives =

238 (2, LB64UDiv) total,

250 (2, LB64UDiv) total,

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

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

240 (2, LB64SDiv) total,

252 (2, LB64SDiv) total,

253+ Prim (UN "prim__uremB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin rem)

254+ (2, LB64URem) total,

255+ Prim (UN "prim__sremB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin s64rem)

256+ (2, LB64SRem) total,

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

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

242 (2, LB64Shl) total,

258 (2, LB64Shl) total,

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

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

@@ -435,6 +451,18 @@ s32div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int32)

435s64div :: Word64 -> Word64 -> Word64

451s64div :: Word64 -> Word64 -> Word64

436s64div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int64)

452s64div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int64)

437

453

454+s8rem :: Word8 -> Word8 -> Word8

455+s8rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8)

456+

457+s16rem :: Word16 -> Word16 -> Word16

458+s16rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16)

459+

460+s32rem :: Word32 -> Word32 -> Word32

461+s32rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32)

462+

463+s64rem :: Word64 -> Word64 -> Word64

464+s64rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64)

465+

438b8ToStr [VConstant (B8 x)] = Just $ VConstant (Str (show x))

466b8ToStr [VConstant (B8 x)] = Just $ VConstant (Str (show x))

439b8ToStr _ = Nothing

467b8ToStr _ = Nothing

440

468