5f6ac67 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

In-lang stringification of Bits

5f6ac67Benjamin Saunders14 years ago

lib/Prelude/Bits.idr+11−11

compare with master

unifiedsplit

@@ -185,17 +185,6 @@ public

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

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

187

188−bitsToStr' : {n : Nat} -> nextBits n -> String

189−bitsToStr' {n=n} x with (nextBits n)

190− | Bits8 = prim__b8ToStr x

191− | Bits16 = prim__b16ToStr x

192− | Bits32 = prim__b32ToStr x

193− | Bits64 = prim__b64ToStr x

194−

195−public

196−bitsToStr : Bits n -> String

197−bitsToStr (MkBits x) = bitsToStr' x

198−

199-- TODO: Proofy comparisons via postulates

188-- TODO: Proofy comparisons via postulates

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

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

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

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

@@ -251,3 +240,14 @@ bitsGt' {n=n} x y with (nextBits n)

251public

240public

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

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

253bitsGt (MkBits x) (MkBits y) = bitsGt' x y /= 0

242bitsGt (MkBits x) (MkBits y) = bitsGt' x y /= 0

243+

244+public

245+bitsToStr : Bits n -> String

246+bitsToStr {n=n} x = helper n x

247+ where

248+ helper : Nat -> Bits n -> String

249+ helper (S x) b = (if bitsAnd (bitsShl (intToBits 1) (intToBits (cast x))) b `bitsEq` (intToBits 0)

250+ then "0"

251+ else "1"

252+ ) ++ helper x b

253+ helper O _ = ""

src/IRTS/Lang.hs−1

@@ -57,7 +57,6 @@ data PrimFn = LPlus | LMinus | LTimes | LDiv | LMod

58 | LB64T8 | LB64T16 | LB64T32

60− | LB8Str | LB16Str | LB32Str | LB64Str

63 | LFSqrt | LFFloor | LFCeil

62 | LFSqrt | LFFloor | LFCeil

src/Idris/Primitives.hs−8

@@ -87,8 +87,6 @@ primitives =

87 (2, LB8Gte) total,

88 Prim (UN "prim__gtB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (>=))

89 (2, LB8Gt) total,

90− Prim (UN "prim__b8ToStr") (ty [B8Type] StrType) 1 (b8ToStr)

91− (1, LB8Str) total,

92 Prim (UN "prim__addB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (+))

90 Prim (UN "prim__addB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (+))

93 (2, LB8Plus) total,

91 (2, LB8Plus) total,

94 Prim (UN "prim__subB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (-))

92 Prim (UN "prim__subB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (-))

@@ -138,8 +136,6 @@ primitives =

138 (2, LB16Gte) total,

136 (2, LB16Gte) total,

139 Prim (UN "prim__gtB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (>=))

137 Prim (UN "prim__gtB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (>=))

140 (2, LB16Gt) total,

138 (2, LB16Gt) total,

141− Prim (UN "prim__b16ToStr") (ty [B16Type] StrType) 1 (b16ToStr)

142− (1, LB16Str) total,

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

139 Prim (UN "prim__addB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (+))

144 (2, LB16Plus) total,

140 (2, LB16Plus) total,

145 Prim (UN "prim__subB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (-))

141 Prim (UN "prim__subB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (-))

@@ -187,8 +183,6 @@ primitives =

187 (2, LB32Gte) total,

183 (2, LB32Gte) total,

188 Prim (UN "prim__gtB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (>=))

184 Prim (UN "prim__gtB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (>=))

189 (2, LB32Gt) total,

185 (2, LB32Gt) total,

190− Prim (UN "prim__b32ToStr") (ty [B32Type] StrType) 1 (b32ToStr)

191− (1, LB32Str) total,

192 Prim (UN "prim__addB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (+))

186 Prim (UN "prim__addB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (+))

193 (2, LB32Plus) total,

187 (2, LB32Plus) total,

194 Prim (UN "prim__subB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (-))

188 Prim (UN "prim__subB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (-))

@@ -234,8 +228,6 @@ primitives =

234 (2, LB64Gte) total,

228 (2, LB64Gte) total,

235 Prim (UN "prim__gtB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (>=))

229 Prim (UN "prim__gtB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (>=))

236 (2, LB64Gt) total,

230 (2, LB64Gt) total,

237− Prim (UN "prim__b64ToStr") (ty [B64Type] StrType) 1 (b64ToStr)

238− (1, LB64Str) total,

239 Prim (UN "prim__addB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (+))

231 Prim (UN "prim__addB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (+))

240 (2, LB64Plus) total,

232 (2, LB64Plus) total,

241 Prim (UN "prim__subB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (-))

233 Prim (UN "prim__subB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (-))