module OpenTheory.Natural.Bits
where
import qualified OpenTheory.Natural as Natural
import qualified OpenTheory.Primitive.Natural as Primitive.Natural
singleton :: Bool -> Primitive.Natural.Natural
singleton b = if b then 1 else 0
cons :: Bool -> Primitive.Natural.Natural -> Primitive.Natural.Natural
cons h t = singleton h + 2 * t
append :: [Bool] -> Primitive.Natural.Natural -> Primitive.Natural.Natural
append l n = foldr cons n l
headBits :: Primitive.Natural.Natural -> Bool
headBits n = Natural.naturalOdd n
bit :: Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool
bit n i = headBits (Primitive.Natural.shiftRight n i)
bound ::
Primitive.Natural.Natural -> Primitive.Natural.Natural ->
Primitive.Natural.Natural
bound n k =
n Primitive.Natural.shiftLeft (Primitive.Natural.shiftRight n k) k
fromList :: [Bool] -> Primitive.Natural.Natural
fromList l = append l 0
tailBits :: Primitive.Natural.Natural -> Primitive.Natural.Natural
tailBits n = Primitive.Natural.shiftRight n 1
toList :: Primitive.Natural.Natural -> [Bool]
toList n = if n == 0 then [] else headBits n : toList (tailBits n)
toVector ::
Primitive.Natural.Natural -> Primitive.Natural.Natural -> [Bool]
toVector n k =
if k == 0 then [] else headBits n : toVector (tailBits n) (k 1)
width :: Primitive.Natural.Natural -> Primitive.Natural.Natural
width n = if n == 0 then 0 else width (tailBits n) + 1