git.iko.soy/Idris-dev
on master help sign in
In-lang stringification of Bits
commit5f6ac6739878049a99f04668edffd6e3613defc8 authorBenjamin Saunders <besaunde@sfu.ca> dateWed 9 Jan 2013, 14:25 (14 years ago) parent9909d70
3 files changed+11−20
compare with master
unifiedsplit
lib/Prelude/Bits.idr+11−11 src/IRTS/Lang.hs−1 src/Idris/Primitives.hs−8
lib/Prelude/Bits.idr+11−11
@@ -185,17 +185,6 @@ public
185185bitsUDiv : Bits n -> Bits n -> Bits n
186186bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
187187
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−
199188-- TODO: Proofy comparisons via postulates
200189bitsLt' : (x : nextBits n) -> (y : nextBits n) -> Int
201190bitsLt' {n=n} x y with (nextBits n)
@@ -251,3 +240,14 @@ bitsGt' {n=n} x y with (nextBits n)
251240public
252241bitsGt : (x : Bits n) -> (y : Bits n) -> Bool
253242bitsGt (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
5757 | LB64Shl | LB64LShr | LB64AShr | LB64And | LB64Or | LB64Xor | LB64Compl
5858 | LB64T8 | LB64T16 | LB64T32
5959 | LIntB8 | LIntB16 | LIntB32 | LIntB64 | LB32Int
60− | LB8Str | LB16Str | LB32Str | LB64Str
6160
6261 | LFExp | LFLog | LFSin | LFCos | LFTan | LFASin | LFACos | LFATan
6362 | LFSqrt | LFFloor | LFCeil
src/Idris/Primitives.hs−8
@@ -87,8 +87,6 @@ primitives =
8787 (2, LB8Gte) total,
8888 Prim (UN "prim__gtB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (>=))
8989 (2, LB8Gt) total,
90− Prim (UN "prim__b8ToStr") (ty [B8Type] StrType) 1 (b8ToStr)
91− (1, LB8Str) total,
9290 Prim (UN "prim__addB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (+))
9391 (2, LB8Plus) total,
9492 Prim (UN "prim__subB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (-))
@@ -138,8 +136,6 @@ primitives =
138136 (2, LB16Gte) total,
139137 Prim (UN "prim__gtB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (>=))
140138 (2, LB16Gt) total,
141− Prim (UN "prim__b16ToStr") (ty [B16Type] StrType) 1 (b16ToStr)
142− (1, LB16Str) total,
143139 Prim (UN "prim__addB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (+))
144140 (2, LB16Plus) total,
145141 Prim (UN "prim__subB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (-))
@@ -187,8 +183,6 @@ primitives =
187183 (2, LB32Gte) total,
188184 Prim (UN "prim__gtB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (>=))
189185 (2, LB32Gt) total,
190− Prim (UN "prim__b32ToStr") (ty [B32Type] StrType) 1 (b32ToStr)
191− (1, LB32Str) total,
192186 Prim (UN "prim__addB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (+))
193187 (2, LB32Plus) total,
194188 Prim (UN "prim__subB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (-))
@@ -234,8 +228,6 @@ primitives =
234228 (2, LB64Gte) total,
235229 Prim (UN "prim__gtB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (>=))
236230 (2, LB64Gt) total,
237− Prim (UN "prim__b64ToStr") (ty [B64Type] StrType) 1 (b64ToStr)
238− (1, LB64Str) total,
239231 Prim (UN "prim__addB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (+))
240232 (2, LB64Plus) total,
241233 Prim (UN "prim__subB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (-))