git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1061 from sellout/master
78dff26Edwin Brady
libs/base/Data/Bits.idr+7−7
compare with master
unifiedsplit
@@ -356,8 +356,8 @@ bitsToInt : Bits n -> Integer
356bitsToInt (MkBits x) = bitsToInt' x
356bitsToInt (MkBits x) = bitsToInt' x
357
357
358-- Zero out the high bits of a truncated bitstring
358-- Zero out the high bits of a truncated bitstring
359−--zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)
359+zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)
360−--zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
360+zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
361
361
362--instance Cast Nat (Bits n) where
362--instance Cast Nat (Bits n) where
363-- cast x = MkBits (zeroUnused (natToBits n))
363-- cast x = MkBits (zeroUnused (natToBits n))
@@ -399,8 +399,8 @@ sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
399
399
400-- TODO: Prove
400-- TODO: Prove
401%assert_total -- can't verify coverage of with block
401%assert_total -- can't verify coverage of with block
402−trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)
402+trunc' : machineTy (nextBytes (m+n)) -> machineTy (nextBytes n)
403−trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
403+trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))
404 | (Z, Z) = believe_me x
404 | (Z, Z) = believe_me x
405 | (Z, S Z) = believe_me (prim__truncB16_B8 (believe_me x))
405 | (Z, S Z) = believe_me (prim__truncB16_B8 (believe_me x))
406 | (Z, S (S Z)) = believe_me (prim__truncB32_B8 (believe_me x))
406 | (Z, S (S Z)) = believe_me (prim__truncB32_B8 (believe_me x))
@@ -412,9 +412,9 @@ trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
412 | (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))
412 | (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))
413 | (S (S (S _)), S (S (S _))) = believe_me x
413 | (S (S (S _)), S (S (S _))) = believe_me x
414
414
415−--public
415+public
416−--truncate : Bits (n+m) -> Bits n
416+truncate : Bits (m+n) -> Bits n
417−--truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
417+truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
418
418
419public
419public
420bitAt : Fin n -> Bits n
420bitAt : Fin n -> Bits n
libs/prelude/Prelude/Vect.idr+8
@@ -254,6 +254,14 @@ concat : Vect m (Vect n a) -> Vect (m * n) a
254concat [] = []
254concat [] = []
255concat (v::vs) = v ++ concat vs
255concat (v::vs) = v ++ concat vs
256
256
257+--------------------------------------------------------------------------------
258+-- Scans
259+--------------------------------------------------------------------------------
260+
261+scanl : (b -> a -> b) -> b -> Vect n a -> Vect (S n) b
262+scanl f q [] = [q]
263+scanl f q (x::xs) = q :: scanl f (f q x) xs
264+
257--------------------------------------------------------------------------------
265--------------------------------------------------------------------------------
258-- Membership tests
266-- Membership tests
259--------------------------------------------------------------------------------
267--------------------------------------------------------------------------------