bin (empty) → 0.1
raw patch · 10 files changed
+2475/−0 lines, 10 filesdep +QuickCheckdep +basedep +dec
Dependencies added: QuickCheck, base, dec, deepseq, fin, hashable, nats
Files
- ChangeLog.md +5/−0
- LICENSE +17/−0
- bin.cabal +77/−0
- src/Data/Bin.hs +407/−0
- src/Data/Bin/Pos.hs +206/−0
- src/Data/BinP.hs +310/−0
- src/Data/BinP/PosP.hs +282/−0
- src/Data/Type/Bin.hs +377/−0
- src/Data/Type/BinP.hs +271/−0
- src/Data/Wrd.hs +523/−0
+ ChangeLog.md view
@@ -0,0 +1,5 @@+# Version history for bin++## 0.1++- First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,17 @@+SPDX-License-Identifier: GPL-2.0-or-later++Copyright (c) 2019 Oleg Grenrus <oleg.grenrus@iki.fi>++ This library is free software: you may copy, redistribute and/or modify it+ under the terms of the GNU General Public License as published by the+ Free Software Foundation, either version 2 of the License, or (at your+ option) any later version.++ This library is distributed in the hope that it will be useful, but+ WITHOUT ANY WARRANTY; without even the implied warranty of+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU+ General Public License for more details.++ You should have received a copy of the GNU General Public License+ along with this program (see `LICENSE.GPLv2` and `LICENSE.GPLv3`).+ If not, see <https://www.gnu.org/licenses/gpl-3.0.html>.
+ bin.cabal view
@@ -0,0 +1,77 @@+cabal-version: 2.2+name: bin+version: 0.1+synopsis: Bin: binary natural numbers.+category: Data, Dependent Types, Singletons, Math+description:+ This package provides /binary natural numbers/ ("Data.Bin");+ also utilities to work on the type level with @DataKinds@ ("Data.Type.Bin").+ .+ @+ data Bin+ \ = BZ -- ^ zero+ \ | BP BinP -- ^ non-zero+ .+ data BinP+ \ = BE -- ^ one+ \ | B0 BinP -- ^ double+ \ | B1 BinP -- ^ double plus 1+ @+ .+ There are /ordinals/ in "Data.Bin.Pos" module, as well as+ fixed width integers in "Data.Wrd".+ .+ Another implementation is at <https://hackage.haskell.org/package/nat>,+ this differs in naming, and provides promoted variant.++homepage: https://github.com/phadej/vec+bug-reports: https://github.com/phadej/vec/issues+license: GPL-2.0-or-later+license-file: LICENSE+author: Oleg Grenrus <oleg.grenrus@iki.fi>+maintainer: Oleg.Grenrus <oleg.grenrus@iki.fi>+copyright: (c) 2019 Oleg Grenrus+build-type: Simple+extra-source-files: ChangeLog.md+tested-with:+ GHC ==7.8.4+ || ==7.10.3+ || ==8.0.2+ || ==8.2.2+ || ==8.4.4+ || ==8.6.5+ || ==8.8.1++source-repository head+ type: git+ location: https://github.com/phadej/vec.git+ subdir: bin++library+ default-language: Haskell2010+ hs-source-dirs: src+ ghc-options: -Wall -fprint-explicit-kinds+ exposed-modules:+ Data.Bin+ Data.Bin.Pos+ Data.BinP+ Data.BinP.PosP+ Data.Type.Bin+ Data.Type.BinP+ Data.Wrd++ build-depends:+ , base >=4.7 && <4.14+ , dec ^>=0.0.3+ , deepseq >=1.3.0.2 && <1.5+ , fin ^>=0.1.1+ , hashable >=1.2.7.0 && <1.4+ , QuickCheck ^>=2.13.2++ if !impl(ghc >=7.10)+ build-depends: nats ^>=1.1.2++-- dump-core+-- if impl(ghc >= 8.0)+-- build-depends: dump-core+-- ghc-options: -fplugin=DumpCore -fplugin-opt DumpCore:core-html
+ src/Data/Bin.hs view
@@ -0,0 +1,407 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}++#if __GLASGOW_HASKELL__ < 710+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE StandaloneDeriving #-}+#endif+-- | Binary natural numbers, 'Bin'.+--+-- This module is designed to be imported qualified.+--+module Data.Bin (+ -- * Binary natural numbers+ Bin(..),+ toNatural,+ fromNatural,+ toNat,+ fromNat,+ cata,+ -- * Positive natural numbers+ BinP (..),+ -- * Showing+ explicitShow,+ explicitShowsPrec,+ -- * Extras+ predP,+ mult2,+ mult2Plus1,+ -- ** Data.Bits+ andP,+ xorP,+ complementBitP,+ clearBitP,+ -- * Aliases+ bin0, bin1, bin2, bin3, bin4, bin5, bin6, bin7, bin8, bin9,+ ) where++import Control.DeepSeq (NFData (..))+import Data.Bits (Bits (..))+import Data.Data (Data)+import Data.Hashable (Hashable (..))+import Data.Nat (Nat (..))+import Data.Typeable (Typeable)+import GHC.Exception (ArithException (..), throw)+import Numeric.Natural (Natural)+import Data.BinP (BinP (..))++import qualified Data.Nat as N+import qualified Test.QuickCheck as QC+import qualified Data.BinP as BP++-------------------------------------------------------------------------------+-- Bin+-------------------------------------------------------------------------------++-- | Binary natural numbers.+--+-- Numbers are represented in little-endian order,+-- the representation is unique.+--+-- >>> mapM_ (putStrLn . explicitShow) [0 .. 7]+-- BZ+-- BP BE+-- BP (B0 BE)+-- BP (B1 BE)+-- BP (B0 (B0 BE))+-- BP (B1 (B0 BE))+-- BP (B0 (B1 BE))+-- BP (B1 (B1 BE))+--+data Bin+ = BZ -- ^ zero+ | BP BP.BinP -- ^ non-zero+ deriving (Eq, Ord, Typeable, Data)++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++#if __GLASGOW_HASKELL__ < 710+deriving instance Typeable 'BZ+deriving instance Typeable 'BP+#endif++-- | 'Bin' is printed as 'Natural'.+--+-- To see explicit structure, use 'explicitShow' or 'explicitShowsPrec'+--+instance Show Bin where+ showsPrec d = showsPrec d . toNatural++-- |+--+-- >>> 0 + 2 :: Bin+-- 2+--+-- >>> 1 + 2 :: Bin+-- 3+--+-- >>> 4 * 8 :: Bin+-- 32+--+-- >>> 7 * 7 :: Bin+-- 49+--+instance Num Bin where+ fromInteger = fromNatural . fromInteger++ BZ + b = b+ b@(BP _) + BZ = b+ BP a + BP b = BP (a + b)++ BZ * _ = BZ+ _ * BZ = BZ+ BP a * BP b = BP (a * b)++ abs = id++ signum BZ = BZ+ signum (BP _) = BP BE++ negate _ = error "negate @Bin"++instance Real Bin where+ toRational = toRational . toInteger++instance Integral Bin where+ toInteger = toInteger . toNatural++ quotRem _ _ = error "quotRem @Bin is not implemented"+++-- | >>> take 10 $ iterate succ BZ+-- [0,1,2,3,4,5,6,7,8,9]+--+-- >>> take 10 [BZ ..]+-- [0,1,2,3,4,5,6,7,8,9]+--+instance Enum Bin where+ succ BZ = BP BE+ succ (BP n) = BP (succ n)++ pred BZ = throw Underflow+ pred (BP n) = predP n++ toEnum n = case compare n 0 of+ LT -> throw Underflow+ EQ -> BZ+ GT -> BP (toEnum n)++ fromEnum BZ = 0+ fromEnum (BP n) = fromEnum n++instance NFData Bin where+ rnf BZ = ()+ rnf (BP n) = rnf n++instance Hashable Bin where+ hashWithSalt = undefined++-------------------------------------------------------------------------------+-- Extras+-------------------------------------------------------------------------------++-- | This is a total function.+--+-- >>> map predP [1..10]+-- [0,1,2,3,4,5,6,7,8,9]+--+predP :: BinP -> Bin+predP BE = BZ+predP (B1 n) = BP (B0 n)+predP (B0 n) = BP (go n) where+ go :: BinP -- @00001xyz@+ -> BinP -- @11110xyz@+ go BE = BE+ go (B1 m) = B1 (B0 m)+ go (B0 m) = B1 (go m)++mult2 :: Bin -> Bin+mult2 BZ = BZ+mult2 (BP b) = BP (B0 b)++mult2Plus1 :: Bin -> BinP+mult2Plus1 BZ = BE+mult2Plus1 (BP b) = B1 b++-------------------------------------------------------------------------------+-- QuickCheck+-------------------------------------------------------------------------------++instance QC.Arbitrary Bin where+ arbitrary = QC.frequency [ (1, return BZ), (20, fmap BP QC.arbitrary) ]++ shrink BZ = []+ shrink (BP b) = BZ : map BP (QC.shrink b)++instance QC.CoArbitrary Bin where+ coarbitrary = QC.coarbitrary . sp where+ sp :: Bin -> Maybe BinP+ sp BZ = Nothing+ sp (BP n) = Just n++instance QC.Function Bin where+ function = QC.functionMap sp (maybe BZ BP) where+ sp :: Bin -> Maybe BinP+ sp BZ = Nothing+ sp (BP n) = Just n++-------------------------------------------------------------------------------+-- Showing+-------------------------------------------------------------------------------++-- | 'show' displaying a structure of 'Bin'.+--+-- >>> explicitShow 0+-- "BZ"+--+-- >>> explicitShow 2+-- "BP (B0 BE)"+--+explicitShow :: Bin -> String+explicitShow n = explicitShowsPrec 0 n ""++-- | 'showsPrec' displaying a structure of 'Bin'.+explicitShowsPrec :: Int -> Bin -> ShowS+explicitShowsPrec _ BZ+ = showString "BZ"+explicitShowsPrec d (BP n)+ = showParen (d > 10)+ $ showString "BP "+ . BP.explicitShowsPrec 11 n++-------------------------------------------------------------------------------+-- Bits+-------------------------------------------------------------------------------++instance Bits Bin where+ BZ .&. _ = BZ+ _ .&. BZ = BZ+ BP a .&. BP b = andP a b++ BZ `xor` b = b+ a `xor` BZ = a+ BP a `xor` BP b = xorP a b++ BZ .|. b = b+ a .|. BZ = a+ BP a .|. BP b = BP (a .|. b)++ bit = BP . bit++ clearBit BZ _ = BZ+ clearBit (BP b) n = clearBitP b n++ complementBit BZ n = bit n+ complementBit (BP b) n = complementBitP b n++ zeroBits = BZ++ shiftL BZ _ = BZ+ shiftL (BP b) n = BP (shiftL b n)++ shiftR BZ _ = BZ+ shiftR b n+ | n <= 0 = b+ | otherwise = shiftR (shiftR1 b) (pred n)++ rotateL = shiftL+ rotateR = shiftR++ testBit BZ _ = False+ testBit (BP b) i = testBit b i++ popCount BZ = 0+ popCount (BP n) = popCount n++ -- xor -- tricky+ complement _ = error "compelement @Bin is undefined"+ bitSizeMaybe _ = Nothing+ bitSize _ = error "bitSize @Bin is undefined"+ isSigned _ = False++andP :: BinP -> BinP -> Bin+andP BE BE = BP BE+andP BE (B0 _) = BZ+andP BE (B1 _) = BP BE+andP (B0 _) BE = BZ+andP (B1 _) BE = BP BE+andP (B0 a) (B0 b) = mult2 (andP a b)+andP (B0 a) (B1 b) = mult2 (andP a b)+andP (B1 a) (B0 b) = mult2 (andP a b)+andP (B1 a) (B1 b) = BP (mult2Plus1 (andP a b))++xorP :: BinP -> BinP -> Bin+xorP BE BE = BZ+xorP BE (B0 b) = BP (B1 b)+xorP BE (B1 b) = BP (B0 b)+xorP (B0 b) BE = BP (B1 b)+xorP (B1 b) BE = BP (B0 b)+xorP (B0 a) (B0 b) = mult2 (xorP a b)+xorP (B0 a) (B1 b) = BP (mult2Plus1 (xorP a b))+xorP (B1 a) (B0 b) = BP (mult2Plus1 (xorP a b))+xorP (B1 a) (B1 b) = mult2 (xorP a b)++clearBitP :: BinP -> Int -> Bin+clearBitP BE 0 = BZ+clearBitP BE _ = BP BE+clearBitP (B0 b) 0 = BP (B0 b)+clearBitP (B0 b) n = mult2 (clearBitP b (pred n))+clearBitP (B1 b) 0 = BP (B0 b)+clearBitP (B1 b) n = BP (mult2Plus1 (clearBitP b (pred n)))++complementBitP :: BinP -> Int -> Bin+complementBitP BE 0 = BZ+complementBitP BE n = BP (B1 (bit (pred n)))+complementBitP (B0 b) 0 = BP (B1 b)+complementBitP (B0 b) n = mult2 (complementBitP b (pred n))+complementBitP (B1 b) 0 = BP (B0 b)+complementBitP (B1 b) n = BP (mult2Plus1 (complementBitP b (pred n)))++shiftR1 :: Bin -> Bin+shiftR1 BZ = BZ+shiftR1 (BP BE) = BZ+shiftR1 (BP (B0 b)) = BP b+shiftR1 (BP (B1 b)) = BP b++-------------------------------------------------------------------------------+-- Conversions+-------------------------------------------------------------------------------++-- | Fold 'Bin'.+cata+ :: a -- ^ \(0\)+ -> a -- ^ \(1\)+ -> (a -> a) -- ^ \(2x\)+ -> (a -> a) -- ^ \(2x + 1\)+ -> Bin+ -> a+cata z _ _ _ BZ = z+cata _ h e o (BP b) = BP.cata h e o b++-- | Convert from 'Bin' to 'Nat'.+--+-- >>> toNat 5+-- 5+--+-- >>> N.explicitShow (toNat 5)+-- "S (S (S (S (S Z))))"+--+toNat :: Bin -> Nat+toNat BZ = Z+toNat (BP n) = BP.toNat n++-- | Convert from 'Nat' to 'Bin'.+--+-- >>> fromNat 5+-- 5+--+-- >>> explicitShow (fromNat 5)+-- "BP (B1 (B0 BE))"+--+fromNat :: Nat -> Bin+fromNat = N.cata BZ succ++-- | Convert 'Bin' to 'Natural'+--+-- >>> toNatural 0+-- 0+--+-- >>> toNatural 2+-- 2+--+-- >>> toNatural $ BP $ B0 $ B1 $ BE+-- 6+--+toNatural :: Bin -> Natural+toNatural BZ = 0+toNatural (BP bnz) = BP.toNatural bnz++-- | Convert 'Natural' to 'Nat'+--+-- >>> fromNatural 4+-- 4+--+-- >>> explicitShow (fromNatural 4)+-- "BP (B0 (B0 BE))"+--+fromNatural :: Natural -> Bin+fromNatural 0 = BZ+fromNatural n = BP (BP.fromNatural n)++-------------------------------------------------------------------------------+-- Aliases+-------------------------------------------------------------------------------++bin0, bin1, bin2, bin3, bin4, bin5, bin6, bin7, bin8, bin9 :: Bin+bin0 = BZ+bin1 = BP BP.binP1+bin2 = BP BP.binP2+bin3 = BP BP.binP3+bin4 = BP BP.binP4+bin5 = BP BP.binP5+bin6 = BP BP.binP6+bin7 = BP BP.binP7+bin8 = BP BP.binP8+bin9 = BP BP.binP9
+ src/Data/Bin/Pos.hs view
@@ -0,0 +1,206 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE UndecidableInstances #-}+module Data.Bin.Pos (+ Pos (..), PosP,+ -- * Top & Pop+ top, pop,+ -- * Showing+ explicitShow,+ explicitShowsPrec,+ -- * Conversions+ toNatural,+ -- * Interesting+ absurd,+ boring,+ -- * Weakening (succ)+ weakenRight1,+ -- * Universe+ universe,+ ) where++import Prelude+ (Bounded (..), Eq, Int, Integer, Ord (..), Show (..), ShowS, String,+ fmap, fromIntegral, map, showParen, showString, ($), (.))++import Data.Bin (Bin (..), BinP (..))+import Data.BinP.PosP (PosP (..))+import Data.Typeable (Typeable)+import Numeric.Natural (Natural)++import qualified Data.BinP.PosP as PP+import qualified Data.Type.Bin as B+import qualified Data.Type.BinP as BP+import qualified Test.QuickCheck as QC++import Data.Type.Bin++-- $setup+-- >>> import Prelude (map, putStrLn)+-- >>> import Data.Foldable (traverse_)++-------------------------------------------------------------------------------+-- Data+-------------------------------------------------------------------------------++-- | 'Pos' is to 'Bin' is what 'Fin' is to 'Nat'.+--+-- The name is picked, as sthe lack of beter alternatives.+--+data Pos (b :: Bin) where+ Pos :: PosP b -> Pos ('BP b)+ deriving (Typeable)++deriving instance Eq (Pos b)+deriving instance Ord (Pos b)++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++instance Show (Pos b) where+ showsPrec d = showsPrec d . toNatural++-- |+--+-- >>> minBound < (maxBound :: Pos Bin5)+-- True+instance (SBinPI n, b ~ 'BP n) => Bounded (Pos b) where+ minBound = Pos minBound+ maxBound = Pos maxBound++-------------------------------------------------------------------------------+-- QuickCheck+-------------------------------------------------------------------------------++instance (SBinPI n, b ~ 'BP n) => QC.Arbitrary (Pos b) where+ arbitrary = fmap Pos QC.arbitrary++instance QC.CoArbitrary (Pos b) where+ coarbitrary = QC.coarbitrary . (fromIntegral :: Natural -> Integer) . toNatural++instance (SBinPI n, b ~ 'BP n) => QC.Function (Pos b) where+ function = QC.functionMap (\(Pos p) -> p) Pos++-------------------------------------------------------------------------------+-- Showing+-------------------------------------------------------------------------------++explicitShow :: Pos b -> String+explicitShow b = explicitShowsPrec 0 b ""++explicitShowsPrec :: Int -> Pos b ->ShowS+explicitShowsPrec d (Pos b)+ = showParen (d > 10)+ $ showString "Pos "+ . PP.explicitShowsPrec 11 b++-------------------------------------------------------------------------------+-- Conversions+-------------------------------------------------------------------------------++-- | Convert 'Pos' to 'Natural'+--+-- >>> map toNatural (universe :: [Pos Bin7])+-- [0,1,2,3,4,5,6]+toNatural :: Pos b -> Natural+toNatural (Pos p) = PP.toNatural p++-------------------------------------------------------------------------------+-- Interesting+-------------------------------------------------------------------------------++-- | @'Pos' 'BZ'@ is not inhabited.+absurd :: Pos 'BZ -> b+absurd x = case x of {}++-- | Counting to one is boring+--+-- >>> boring+-- 0+boring :: Pos ('BP 'BE)+boring = minBound++-------------------------------------------------------------------------------+-- min and max, tricky, we need Pred.+-------------------------------------------------------------------------------++-- TBW++-------------------------------------------------------------------------------+-- top & pop+-------------------------------------------------------------------------------++-- | 'top' and 'pop' serve as 'FZ' and 'FS', with types specified so+-- type-inference works backwards from the result.+--+-- >>> top :: Pos Bin4+-- 0+--+-- >>> pop (pop top) :: Pos Bin4+-- 2+--+-- >>> pop (pop top) :: Pos Bin9+-- 2+--+top :: SBinPI b => Pos ('BP b)+top = minBound++-- | See 'top'.+pop :: (SBinPI a, Pred b ~ 'BP a, BP.Succ a ~ b) => Pos ('BP a) -> Pos ('BP b)+pop = weakenRight1++-------------------------------------------------------------------------------+-- Append and Split+-------------------------------------------------------------------------------++-- | Like 'FS' for 'Fin'.+--+-- Some tests:+--+-- >>> map weakenRight1 $ (universe :: [Pos Bin2])+-- [1,2]+--+-- >>> map weakenRight1 $ (universe :: [Pos Bin3])+-- [1,2,3]+--+-- >>> map weakenRight1 $ (universe :: [Pos Bin4])+-- [1,2,3,4]+--+-- >>> map weakenRight1 $ (universe :: [Pos Bin5])+-- [1,2,3,4,5]+--+-- >>> map weakenRight1 $ (universe :: [Pos Bin6])+-- [1,2,3,4,5,6]+--+weakenRight1 :: SBinPI b => Pos ('BP b) -> Pos (Succ'' b)+weakenRight1 (Pos b) = Pos (PP.weakenRight1 b)++-------------------------------------------------------------------------------+-- Universe+-------------------------------------------------------------------------------++-- | Universe, i.e. all @[Pos b]@+--+-- >>> universe :: [Pos Bin9]+-- [0,1,2,3,4,5,6,7,8]+--+-- >>> traverse_ (putStrLn . explicitShow) (universe :: [Pos Bin5])+-- Pos (PosP (Here WE))+-- Pos (PosP (There1 (There0 (AtEnd 0b00))))+-- Pos (PosP (There1 (There0 (AtEnd 0b01))))+-- Pos (PosP (There1 (There0 (AtEnd 0b10))))+-- Pos (PosP (There1 (There0 (AtEnd 0b11))))+--+universe :: forall b. B.SBinI b => [Pos b]+universe = case B.sbin :: SBin b of+ B.SBZ -> []+ B.SBP -> map Pos PP.universe
+ src/Data/BinP.hs view
@@ -0,0 +1,310 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}++#if __GLASGOW_HASKELL__ < 710+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE StandaloneDeriving #-}+#endif+-- | Positive binary natural numbers, 'BinP'.+--+-- This module is designed to be imported qualified.+--+module Data.BinP (+ BinP(..),+ -- * Conversions+ cata,+ toNatural,+ fromNatural,+ toNat,+ -- * Showing+ explicitShow,+ explicitShowsPrec,+ -- * Extras+ predMaybe,+ -- * Aliases+ binP1, binP2, binP3, binP4, binP5, binP6, binP7, binP8, binP9,+ ) where++import Control.DeepSeq (NFData (..))+import Data.Bits (Bits (..))+import Data.Data (Data)+import Data.Hashable (Hashable (..))+import Data.Monoid (mappend)+import Data.Nat (Nat (..))+import Data.Typeable (Typeable)+import GHC.Exception (ArithException (..), throw)+import Numeric.Natural (Natural)++import qualified Data.Nat as N+import qualified Test.QuickCheck as QC++-- $setup+-- >>> import Data.List (sort)++-------------------------------------------------------------------------------+-- BinP+-------------------------------------------------------------------------------++-- | Non-zero binary natural numbers.+--+-- We could have called this type @Bin1@,+-- but that's used as type alias for promoted @'BP' 'BE'@ in "Data.Type.Bin".+data BinP+ = BE -- ^ one+ | B0 BinP -- ^ mult2+ | B1 BinP -- ^ mult2 plus 1+ deriving (Eq, Typeable, Data)++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++#if __GLASGOW_HASKELL__ < 710+deriving instance Typeable 'BE+deriving instance Typeable 'B0+deriving instance Typeable 'B1+#endif++-- | >>> sort [1 .. 9 :: BinP]+-- [1,2,3,4,5,6,7,8,9]+--+instance Ord BinP where+ compare BE BE = EQ+ compare BE _ = LT+ compare _ BE = GT+ compare (B0 a) (B0 b) = compare a b+ compare (B1 a) (B1 b) = compare a b+ compare (B0 a) (B1 b) = compare a b `mappend` LT+ compare (B1 a) (B0 b) = compare a b `mappend` GT++instance Show BinP where+ showsPrec d = showsPrec d . toNatural++instance Num BinP where+ fromInteger = fromNatural . fromInteger++ BE + b = succ b+ b + BE = succ b+ B0 a + B0 b = B0 (a + b)+ B0 a + B1 b = B1 (a + b)+ B1 a + B0 b = B1 (a + b)+ B1 a + B1 b = B0 (succ (a + b))++ BE * b = b+ a * BE = a+ B0 a * B0 b = B0 (B0 (a * b))+ B1 a * B0 b = B0 (B0 (a * b)) + B0 b+ B0 a * B1 b = B0 (B0 (a * b)) + B0 a+ B1 a * B1 b = B1 (B0 (a * b)) + B0 a + B0 b++ abs = id++ signum _ = BE++ negate _ = error "negate @Bin"++instance Real BinP where+ toRational = toRational . toInteger++instance Integral BinP where+ toInteger = toInteger . toNatural++ quotRem _ _ = error "quotRem @Bin is not implemented"++instance Enum BinP where+ succ BE = B0 BE+ succ (B0 n) = B1 n+ succ (B1 n) = B0 (succ n)++ pred n = case predMaybe n of+ Nothing -> throw Underflow+ Just m -> m++ toEnum n = case compare n 1 of+ LT -> throw Underflow+ EQ -> BE+ GT -> case n `divMod` 2 of+ (m, 0) -> B0 (toEnum m)+ (m, _) -> B1 (toEnum m)++ fromEnum BE = 1+ fromEnum (B0 n) = 2 * fromEnum n+ fromEnum (B1 n) = succ (2 * fromEnum n)++instance NFData BinP where+ rnf BE = ()+ rnf (B0 n) = rnf n+ rnf (B1 n) = rnf n++instance Hashable BinP where+ hashWithSalt = undefined++predMaybe :: BinP -> Maybe BinP+predMaybe BE = Nothing+predMaybe (B1 n) = Just (B0 n)+predMaybe (B0 n) = Just (mult2Plus1 (predMaybe n))+ where+ mult2Plus1 :: Maybe BinP -> BinP+ mult2Plus1 = maybe BE B1++-------------------------------------------------------------------------------+-- Bits+-------------------------------------------------------------------------------++-- | __NOTE__: '.&.', 'xor', 'shiftR' and 'rotateR' are __NOT_ implemented.+-- They may make number zero.+--+instance Bits BinP where+ B0 a .|. B0 b = B0 (a .|. b)+ B0 a .|. B1 b = B1 (a .|. b)+ B1 a .|. B0 b = B1 (a .|. b)+ B1 a .|. B1 b = B1 (a .|. b)++ BE .|. B0 b = B1 b+ BE .|. B1 b = B1 b+ B0 b .|. BE = B1 b+ B1 b .|. BE = B1 b++ BE .|. BE = BE++ bit n+ | n <= 0 = BE+ | otherwise = B0 (bit (pred n))++ shiftL b n+ | n <= 0 = b+ | otherwise = shiftL (B0 b) (pred n)++ rotateL = shiftL++ popCount = go 1 where+ go !acc BE = acc+ go !acc (B0 b) = go acc b+ go !acc (B1 b) = go (succ acc) b++ testBit BE 0 = True+ testBit (B0 _) 0 = False+ testBit (B1 _) 0 = True+ testBit BE _ = False+ testBit (B0 b) n = testBit b (pred n)+ testBit (B1 b) n = testBit b (pred n)++ zeroBits = error "zeroBits @BinP is undefined"+ clearBit _ _ = error "clearBit @BinP is undefined"+ complementBit _ _ = error "complementBit @BinP is undefined"+ xor _ _ = error "xor @BinP is undefined"+ (.&.) _ _ = error "(.&.) @BinP is undefined"+ shiftR _ = error "shiftR @BinP is undefined"+ rotateR _ = error "shiftL @BinP is undefined"+ complement _ = error "compelement @BinP is undefined"+ bitSizeMaybe _ = Nothing+ bitSize _ = error "bitSize @BinP is undefined"+ isSigned _ = True++-------------------------------------------------------------------------------+-- QuickCheck+-------------------------------------------------------------------------------++instance QC.Arbitrary BinP where+ arbitrary = do+ bs <- QC.arbitrary :: QC.Gen [Bool]+ return (foldr (\b -> if b then B1 else B0) BE bs)++ shrink BE = []+ shrink (B1 b) = b : B0 b : map B1 (QC.shrink b)+ shrink (B0 b) = b : map B0 (QC.shrink b)++instance QC.CoArbitrary BinP where+ coarbitrary = QC.coarbitrary . sp where+ sp :: BinP -> Maybe (Either BinP BinP)+ sp BE = Nothing+ sp (B0 b) = Just (Left b)+ sp (B1 b) = Just (Right b)++instance QC.Function BinP where+ function = QC.functionMap sp (maybe BE (either B0 B1)) where+ sp :: BinP -> Maybe (Either BinP BinP)+ sp BE = Nothing+ sp (B0 b) = Just (Left b)+ sp (B1 b) = Just (Right b)++-------------------------------------------------------------------------------+-- Showing+-------------------------------------------------------------------------------++-- | 'show' displaying a structure of 'BinP'.+--+-- >>> explicitShow 11+-- "B1 (B1 (B0 BE))"+explicitShow :: BinP -> String+explicitShow n = explicitShowsPrec 0 n ""++-- | 'showsPrec' displaying a structure of 'BinP'.+explicitShowsPrec :: Int -> BinP -> ShowS+explicitShowsPrec _ BE+ = showString "BE"+explicitShowsPrec d (B0 n)+ = showParen (d > 10)+ $ showString "B0 "+ . explicitShowsPrec 11 n+explicitShowsPrec d (B1 n)+ = showParen (d > 10)+ $ showString "B1 "+ . explicitShowsPrec 11 n++-------------------------------------------------------------------------------+-- Conversions+-------------------------------------------------------------------------------++-- | 'toNatural' for 'BinP'.+toNatural :: BinP -> Natural+toNatural BE = 1+toNatural (B0 n) = 2 * toNatural n+toNatural (B1 n) = 2 * toNatural n + 1++-- | 'fromNatural' for 'BinP'.+--+-- Throws when given 0.+fromNatural :: Natural -> BinP+fromNatural 0 = throw Underflow+fromNatural 1 = BE+fromNatural n = case n `divMod` 2 of+ (m, 0) -> B0 (fromNatural m)+ (m, _) -> B1 (fromNatural m)++-- | Fold 'BinP'.+cata+ :: a -- ^ \(1\)+ -> (a -> a) -- ^ \(2x\)+ -> (a -> a) -- ^ \(2x + 1\)+ -> BinP+ -> a+cata z o i = go where+ go BE = z+ go (B0 b) = o (go b)+ go (B1 b) = i (go b)++-- | Convert from 'BinP' to 'Nat'.+toNat :: BinP -> Nat+toNat = cata (S Z) o i where+ o :: Nat -> Nat+ o = N.cata Z (S . S)++ i :: Nat -> Nat+ i = S . o++-------------------------------------------------------------------------------+-- Aliases+-------------------------------------------------------------------------------++binP1, binP2, binP3, binP4, binP5, binP6, binP7, binP8, binP9 :: BinP+binP1 = BE+binP2 = B0 BE+binP3 = B1 BE+binP4 = B0 binP2+binP5 = B1 binP2+binP6 = B0 binP3+binP7 = B1 binP3+binP8 = B0 binP4+binP9 = B1 binP4
+ src/Data/BinP/PosP.hs view
@@ -0,0 +1,282 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE UndecidableInstances #-}+module Data.BinP.PosP (+ PosP (..),+ PosP' (..),+ -- * Top & Pop+ top, pop,+ -- * Showing+ explicitShow,+ explicitShow',+ explicitShowsPrec,+ explicitShowsPrec',+ -- * Conversions+ toNatural, toNatural',+ -- * Interesting+ boring,+ -- * Weakening (succ)+ weakenRight1, weakenRight1',+ -- * Universe+ universe, universe',+ ) where++import Prelude+ (Bounded (..), Either (..), Eq, Int, Integer, Num, Ord (..),+ Ordering (..), Show (..), ShowS, String, either, fmap, fromIntegral,+ map, showParen, showString, ($), (*), (+), (++), (.))++import Data.Bin (BinP (..))+import Data.Nat (Nat (..))+import Data.Proxy (Proxy (..))+import Data.Typeable (Typeable)+import Data.Wrd (Wrd (..))+import Numeric.Natural (Natural)++import qualified Data.Bin as B+import qualified Data.Type.Bin as B+import qualified Data.Type.BinP as BP+import qualified Data.Type.Nat as N+import qualified Data.Wrd as W+import qualified Test.QuickCheck as QC++import Data.Type.BinP++-- $setup+-- >>> import Prelude (map, putStrLn)+-- >>> import Data.Foldable (traverse_)++-------------------------------------------------------------------------------+-- Data+-------------------------------------------------------------------------------++-- | 'PosP' is to 'BinP' is what 'Fin' is to 'Nat', when 'n' is 'Z'.+newtype PosP (b :: BinP) = PosP { unPosP :: PosP' 'Z b }+ deriving (Eq, Ord, Typeable)++-- | 'PosP'' is a structure inside 'PosP'.+data PosP' (n :: Nat) (b :: BinP) where+ AtEnd :: Wrd n -> PosP' n 'BE -- ^ position is either at the last digit;+ Here :: Wrd n -> PosP' n ('B1 b) -- ^ somewhere here+ There1 :: PosP' ('S n) b -> PosP' n ('B1 b) -- ^ or there, if the bit is one;+ There0 :: PosP' ('S n) b -> PosP' n ('B0 b) -- ^ or only there if it is none.+ deriving (Typeable)++deriving instance Eq (PosP' n b)+instance Ord (PosP' n b) where+ compare (AtEnd x) (AtEnd y) = compare x y+ compare (Here x) (Here y) = compare x y+ compare (Here _) (There1 _) = LT+ compare (There1 _) (Here _) = GT+ compare (There1 x) (There1 y) = compare x y+ compare (There0 x) (There0 y) = compare x y++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++instance Show (PosP b) where+ showsPrec d = showsPrec d . toNatural++instance N.SNatI n => Show (PosP' n b) where+ showsPrec d = showsPrec d . toNatural'++instance SBinPI b => Bounded (PosP b) where+ minBound = PosP minBound+ maxBound = PosP maxBound++instance (N.SNatI n, SBinPI b) => Bounded (PosP' n b) where+ minBound = case sbinp :: SBinP b of+ SBE -> AtEnd minBound+ SB0 -> There0 minBound+ SB1 -> Here minBound++ maxBound = case sbinp :: SBinP b of+ SBE -> AtEnd maxBound+ SB0 -> There0 maxBound+ SB1 -> There1 maxBound++-------------------------------------------------------------------------------+-- QuickCheck+-------------------------------------------------------------------------------++instance SBinPI b => QC.Arbitrary (PosP b) where+ arbitrary = fmap PosP QC.arbitrary++instance QC.CoArbitrary (PosP b) where+ coarbitrary = QC.coarbitrary . (fromIntegral :: Natural -> Integer) . toNatural++instance SBinPI b => QC.Function (PosP b) where+ function = QC.functionMap (\(PosP p) -> p) PosP++instance (N.SNatI n, SBinPI b) => QC.Arbitrary (PosP' n b) where+ arbitrary = case sbinp :: SBinP b of+ SBE -> fmap AtEnd QC.arbitrary+ SB0 -> fmap There0 QC.arbitrary+ SB1 -> sb1freq+ where+ sb1freq :: forall bb. SBinPI bb => QC.Gen (PosP' n ('B1 bb))+ sb1freq = QC.frequency+ [ (fHere, fmap Here QC.arbitrary)+ , (fThere, fmap There1 QC.arbitrary)+ ]+ where+ fHere = getKNat (exp2 :: KNat Int n)+ fThere = fHere * 2 * BP.reflectToNum (Proxy :: Proxy bb)++instance N.SNatI n => QC.CoArbitrary (PosP' n b) where+ coarbitrary = QC.coarbitrary . (fromIntegral :: Natural -> Integer) . toNatural'++instance (N.SNatI n, SBinPI b) => QC.Function (PosP' n b) where+ function = case sbinp :: SBinP b of+ SBE -> QC.functionMap (\(AtEnd t) -> t) AtEnd+ SB0 -> QC.functionMap (\(There0 r) -> r) There0+ SB1 -> QC.functionMap sp (either Here There1) where+ where+ sp :: PosP' n ('B1 bb) -> Either (Wrd n) (PosP' ('S n) bb)+ sp (Here t) = Left t+ sp (There1 p) = Right p++-------------------------------------------------------------------------------+-- Showing+-------------------------------------------------------------------------------++explicitShow :: PosP b -> String+explicitShow b = explicitShowsPrec 0 b ""++explicitShow' :: PosP' n b -> String+explicitShow' b = explicitShowsPrec' 0 b ""++explicitShowsPrec :: Int -> PosP b ->ShowS+explicitShowsPrec d (PosP p)+ = showParen (d > 10)+ $ showString "PosP "+ . explicitShowsPrec' 11 p++explicitShowsPrec' :: Int -> PosP' n b ->ShowS+explicitShowsPrec' d (AtEnd v)+ = showParen (d > 10)+ $ showString "AtEnd "+ . showsPrec 11 v+explicitShowsPrec' d (Here v)+ = showParen (d > 10)+ $ showString "Here "+ . showsPrec 11 v+explicitShowsPrec' d (There1 p)+ = showParen (d > 10)+ $ showString "There1 "+ . explicitShowsPrec' 11 p+explicitShowsPrec' d (There0 p)+ = showParen (d > 10)+ $ showString "There0 "+ . explicitShowsPrec' 11 p++-------------------------------------------------------------------------------+-- Conversions+-------------------------------------------------------------------------------++-- | Convert 'PosP' to 'Natural'.+toNatural :: PosP b -> Natural+toNatural (PosP p) = toNatural' p++-- | Convert 'PosP'' to 'Natural'.+toNatural' :: forall n b. N.SNatI n => PosP' n b -> Natural+toNatural' (AtEnd v) = W.toNatural v+toNatural' (Here v) = W.toNatural v+toNatural' (There1 p) = getKNat (exp2 :: KNat Natural n) + toNatural' p+toNatural' (There0 p) = toNatural' p++exp2 :: Num a => N.SNatI n => KNat a n+exp2 = N.induction (KNat 1) (\(KNat n) -> KNat (n * 2))++-------------------------------------------------------------------------------+-- Interesting+-------------------------------------------------------------------------------++-- | Counting to one is boring+--+-- >>> boring+-- 0+boring :: PosP 'BE+boring = minBound++-------------------------------------------------------------------------------+-- top & pop+-------------------------------------------------------------------------------++-- | 'top' and 'pop' serve as 'FZ' and 'FS', with types specified so+-- type-inference works backwards from the result.+--+-- >>> top :: PosP BinP4+-- 0+--+-- >>> pop (pop top) :: PosP BinP4+-- 2+--+-- >>> pop (pop top) :: PosP BinP9+-- 2+--+top :: SBinPI b => PosP b+top = minBound++-- | See 'top'.+pop :: (SBinPI a, B.Pred b ~ 'B.BP a, Succ a ~ b) => PosP a -> PosP b+pop = weakenRight1++-------------------------------------------------------------------------------+-- Append and Split+-------------------------------------------------------------------------------++weakenRight1 :: SBinPI b => PosP b -> PosP (Succ b)+weakenRight1 (PosP n) = PosP (weakenRight1' sbinp n)++weakenRight1' :: forall b n. SBinP b -> PosP' n b -> PosP' n (Succ b)+weakenRight1' SBE (AtEnd v) = There0 (AtEnd (W1 v))+weakenRight1' SB0 (There0 p) = There1 p+weakenRight1' SB1 (There1 p) = There0 (weakenRight1' sbinp p)+weakenRight1' s@SB1 (Here v) = There0 $ recur s v where+ recur :: forall bb. SBinPI bb => SBinP ('B1 bb) -> Wrd n -> PosP' ('S n) (Succ bb)+ recur _ v' = withSucc (Proxy :: Proxy bb) $ weakenRight1V (W1 v')++weakenRight1V :: forall b n. SBinPI b => Wrd ('S n) -> PosP' ('S n) b+weakenRight1V v = case sbinp :: SBinP b of+ SBE -> AtEnd v+ SB0 -> There0 (weakenRight1V (W0 v))+ SB1 -> Here v++-------------------------------------------------------------------------------+-- Universe+-------------------------------------------------------------------------------++-- |+--+-- >>> universe :: [PosP BinP9]+-- [0,1,2,3,4,5,6,7,8]+--+universe :: forall b. SBinPI b => [PosP b]+universe = map PosP universe'++-- | This gives a hint, what the @n@ parameter means in 'PosP''.+--+-- >>> universe' :: [PosP' N.Nat2 BinP2]+-- [0,1,2,3,4,5,6,7]+--+universe' :: forall b n. (N.SNatI n, SBinPI b) => [PosP' n b]+universe' = case B.sbinp :: SBinP b of+ B.SBE -> map AtEnd W.universe+ B.SB0 -> map There0 universe'+ B.SB1 -> map Here W.universe ++ map There1 universe'++-------------------------------------------------------------------------------+-- Helpers+-------------------------------------------------------------------------------++newtype KNat a (n :: Nat) = KNat { getKNat :: a }
+ src/Data/Type/Bin.hs view
@@ -0,0 +1,377 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+-- | Binary natural numbers. @DataKinds@ stuff.+module Data.Type.Bin (+ -- * Singleton+ SBin (..), SBinP (..),+ sbinToBin, BP.sbinpToBinP,+ sbinToNatural, BP.sbinpToNatural,+ -- * Implicit+ SBinI (..), SBinPI (..),+ withSBin, BP.withSBinP,+ reify,+ reflect,+ reflectToNum,+ -- * Type equality+ eqBin,+ -- * Induction+ induction,+ -- * Arithmetic+ -- ** Successor+ Succ, Succ', Succ'',+ withSucc,+ -- ** Predecessor+ Pred,+ -- ** Addition+ Plus,+ -- ** Extras+ Mult2, Mult2Plus1,+ -- * Conversions+ -- ** To GHC Nat+ ToGHC, FromGHC,+ -- ** To fin Nat+ ToNat, FromNat,+ -- * Aliases+ Bin0, Bin1, Bin2, Bin3, Bin4, Bin5, Bin6, Bin7, Bin8, Bin9,+ ) where++import Data.Bin (Bin (..), BinP (..))+import Data.Nat (Nat (..))+import Data.Proxy (Proxy (..))+import Data.Type.Equality ((:~:) (..), TestEquality (..))+import Data.Typeable (Typeable)+import Numeric.Natural (Natural)+import Data.Type.BinP (SBinP (..), SBinPI (..))++import qualified Data.Type.Nat as N+import qualified GHC.TypeLits as GHC+import qualified Data.Type.BinP as BP++-- $setup+-- >>> :set -XDataKinds+-- >>> import Data.Bin+-- >>> import Data.Type.BinP (BinP2, BinP3)++-------------------------------------------------------------------------------+-- Singletons+-------------------------------------------------------------------------------++-- | Singleton of 'Bin'.+data SBin (b :: Bin) where+ SBZ :: SBin 'BZ+ SBP :: SBinPI b => SBin ('BP b)+ deriving (Typeable)++-------------------------------------------------------------------------------+-- Implicits+-------------------------------------------------------------------------------++-- | Let constraint solver construct 'SBin'.+class SBinI (b :: Bin) where sbin :: SBin b+instance SBinI 'BZ where sbin = SBZ+instance SBinPI b => SBinI ('BP b ) where sbin = SBP++-------------------------------------------------------------------------------+-- Conversions+-------------------------------------------------------------------------------++-- | Construct 'SBinI' dictionary from 'SBin'.+withSBin :: SBin b -> (SBinI b => r) -> r+withSBin SBZ k = k+withSBin SBP k = k++-- | Reify 'Bin'+--+-- >>> reify bin3 reflect+-- 3+--+reify :: forall r. Bin -> (forall b. SBinI b => Proxy b -> r) -> r+reify BZ k = k (Proxy :: Proxy 'BZ)+reify (BP b) k = BP.reify b (\(_ :: Proxy b) -> k (Proxy :: Proxy ('BP b)))++-- | Reflect type-level 'Bin' to the term level.+reflect :: forall b proxy. SBinI b => proxy b -> Bin+reflect p = case sbin :: SBin b of+ SBZ -> BZ+ SBP -> BP (aux p)+ where+ aux :: forall bn. SBinPI bn => proxy ('BP bn) -> BinP+ aux _ = BP.reflect (Proxy :: Proxy bn)++-- | Reflect type-level 'Bin' to the term level 'Num'.+reflectToNum :: forall b proxy a. (SBinI b, Num a) => proxy b -> a+reflectToNum p = case sbin :: SBin b of+ SBZ -> 0+ SBP -> aux p+ where+ aux :: forall bn. SBinPI bn => proxy ('BP bn) -> a+ aux _ = BP.reflectToNum (Proxy :: Proxy bn)++-- | Convert 'SBin' to 'Bin'.+sbinToBin :: forall n. SBin n -> Bin+sbinToBin SBZ = BZ+sbinToBin s@SBP = aux s where+ aux :: forall m. SBinPI m => SBin ('BP m) -> Bin+ aux _ = BP (BP.sbinpToBinP (sbinp :: SBinP m))++-- | Convert 'SBin' to 'Natural'.+--+-- >>> sbinToNatural (sbin :: SBin Bin9)+-- 9+--+sbinToNatural :: forall n. SBin n -> Natural+sbinToNatural SBZ = 0+sbinToNatural s@SBP = aux s where+ aux :: forall m. SBinPI m => SBin ('BP m) -> Natural+ aux _ = BP.sbinpToNatural (sbinp :: SBinP m)++-------------------------------------------------------------------------------+-- Equality+-------------------------------------------------------------------------------++eqBin :: forall a b. (SBinI a, SBinI b) => Maybe (a :~: b)+eqBin = case (sbin :: SBin a, sbin :: SBin b) of+ (SBZ, SBZ) -> Just Refl+ (SBP, SBP) -> recur where+ recur :: forall n m. (SBinPI n, SBinPI m) => Maybe ('BP n :~: 'BP m)+ recur = do+ Refl <- BP.eqBinP :: Maybe (n :~: m)+ return Refl++ _ -> Nothing++instance TestEquality SBin where+ testEquality SBZ SBZ = Just Refl+ testEquality SBP SBP = recur where+ recur :: forall n m. (SBinPI n, SBinPI m) => Maybe ('BP n :~: 'BP m)+ recur = do+ Refl <- BP.eqBinP :: Maybe (n :~: m)+ return Refl+ testEquality _ _ = Nothing++-------------------------------------------------------------------------------+-- Induction+-------------------------------------------------------------------------------++-- | Induction on 'Bin'.+induction+ :: forall b f. SBinI b+ => f 'BZ -- ^ \(P(0)\)+ -> f ('BP 'BE) -- ^ \(P(1)\)+ -> (forall bb. SBinPI bb => f ('BP bb) -> f ('BP ('B0 bb))) -- ^ \(\forall b. P(b) \to P(2b)\)+ -> (forall bb. SBinPI bb => f ('BP bb) -> f ('BP ('B1 bb))) -- ^ \(\forall b. P(b) \to P(2b + 1)\)+ -> f b+induction z e o i = case sbin :: SBin b of+ SBZ -> z+ SBP -> go+ where+ go :: forall bb. SBinPI bb => f ('BP bb)+ go = case sbinp :: SBinP bb of+ SBE -> e+ SB0 -> o go+ SB1 -> i go++-------------------------------------------------------------------------------+-- Conversion to GHC Nat+-------------------------------------------------------------------------------++-- | Convert to GHC 'GHC.Nat'.+--+-- >>> :kind! ToGHC Bin5+-- ToGHC Bin5 :: GHC.Nat+-- = 5+--+type family ToGHC (b :: Bin) :: GHC.Nat where+ ToGHC 'BZ = 0+ ToGHC ('BP n) = BP.ToGHC n++-- | Convert from GHC 'GHC.Nat'.+--+-- >>> :kind! FromGHC 7+-- FromGHC 7 :: Bin+-- = 'BP ('B1 ('B1 'BE))+--+type family FromGHC (n :: GHC.Nat) :: Bin where+ FromGHC n = FromGHC' (GhcDivMod2 n)++type family FromGHC' (p :: (GHC.Nat, Bool)) :: Bin where+ FromGHC' '(0, 'False) = 'BZ+ FromGHC' '(0, 'True) = 'BP 'BE+ FromGHC' '(n, 'False) = Mult2 (FromGHC n)+ FromGHC' '(n, 'True) = 'BP (Mult2Plus1 (FromGHC n))++-- | >>> :kind! GhcDivMod2 13+-- GhcDivMod2 13 :: (GHC.Nat, Bool)+-- = '(6, 'True)+--+type family GhcDivMod2 (n :: GHC.Nat) :: (GHC.Nat, Bool) where+ GhcDivMod2 0 = '(0, 'False)+ GhcDivMod2 1 = '(0, 'True)+ GhcDivMod2 n = GhcDivMod2' (GhcDivMod2 (n GHC.- 2))++type family GhcDivMod2' (p :: (GHC.Nat, Bool)) :: (GHC.Nat, Bool) where+ GhcDivMod2' '(n, b) = '(1 GHC.+ n, b)++-------------------------------------------------------------------------------+-- Conversion to Nat+-------------------------------------------------------------------------------++-- | Convert to @fin@ 'Nat'.+--+-- >>> :kind! ToNat Bin5+-- ToNat Bin5 :: Nat+-- = 'S ('S ('S ('S ('S 'Z))))+--+type family ToNat (b :: Bin) :: Nat where+ ToNat 'BZ = 'Z+ ToNat ('BP n) = BP.ToNat n++-- | Convert from @fin@ 'Nat'.+--+-- >>> :kind! FromNat N.Nat5+-- FromNat N.Nat5 :: Bin+-- = 'BP ('B1 ('B0 'BE))+--+type family FromNat (n :: Nat) :: Bin where+ FromNat n = FromNat' (N.DivMod2 n)++type family FromNat' (p :: (Nat, Bool)) :: Bin where+ FromNat' '( 'Z, 'False) = 'BZ+ FromNat' '( 'Z, 'True) = 'BP 'BE+ FromNat' '( n, 'False) = Mult2 (FromNat n)+ FromNat' '( n, 'True) = 'BP (Mult2Plus1 (FromNat n))++-------------------------------------------------------------------------------+-- Extras+-------------------------------------------------------------------------------++-- | Multiply by two.+--+-- >>> :kind! Mult2 Bin0+-- Mult2 Bin0 :: Bin+-- = 'BZ+--+-- >>> :kind! Mult2 Bin7+-- Mult2 Bin7 :: Bin+-- = 'BP ('B0 ('B1 BinP3))+type family Mult2 (b :: Bin) :: Bin where+ Mult2 'BZ = 'BZ+ Mult2 ('BP n) = 'BP ('B0 n)++-- | Multiply by two and add one.+--+-- >>> :kind! Mult2Plus1 Bin0+-- Mult2Plus1 Bin0 :: BinP+-- = 'BE+--+-- >>> :kind! Mult2Plus1 Bin5+-- Mult2Plus1 Bin5 :: BinP+-- = 'B1 ('B1 BinP2)+type family Mult2Plus1 (b :: Bin) :: BinP where+ Mult2Plus1 'BZ = 'BE+ Mult2Plus1 ('BP n) = ('B1 n)++-------------------------------------------------------------------------------+-- Arithmetic: Succ+-------------------------------------------------------------------------------++-- | Successor type family.+--+-- >>> :kind! Succ Bin5+-- Succ Bin5 :: Bin+-- = 'BP ('B0 ('B1 'BE))+-- +-- @+-- `Succ` :: 'Bin' -> 'Bin'+-- `Succ'` :: 'Bin' -> 'BinP'+-- `Succ''` :: 'BinP' -> 'Bin'+-- @+type Succ b = 'BP (Succ' b)++type family Succ' (b :: Bin) :: BinP where+ Succ' 'BZ = 'BE+ Succ' ('BP b) = BP.Succ b++type Succ'' b = 'BP (BP.Succ b)++withSucc :: forall b r. SBinI b => Proxy b -> (SBinPI (Succ' b) => r) -> r+withSucc p k = case sbin :: SBin b of+ SBZ -> k+ SBP -> withSucc' p k++withSucc' :: forall b r. SBinPI b => Proxy ('BP b) -> (SBinPI (BP.Succ b) => r) -> r+withSucc' _ k = BP.withSucc (Proxy :: Proxy b) k++-------------------------------------------------------------------------------+-- Predecessor+-------------------------------------------------------------------------------++-- | Predecessor type family..+--+-- >>> :kind! Pred BP.BinP1+-- Pred BP.BinP1 :: Bin+-- = 'BZ+--+-- >>> :kind! Pred BP.BinP5+-- Pred BP.BinP5 :: Bin+-- = 'BP ('B0 ('B0 BP.BinP1))+--+-- >>> :kind! Pred BP.BinP8+-- Pred BP.BinP8 :: Bin+-- = 'BP ('B1 ('B1 'BE))+--+-- >>> :kind! Pred BP.BinP6+-- Pred BP.BinP6 :: Bin+-- = 'BP ('B1 ('B0 'BE))+--+type family Pred (b :: BinP) :: Bin where+ Pred 'BE = 'BZ+ Pred ('B1 n) = 'BP ('B0 n)+ Pred ('B0 n) = 'BP (Pred' n)++type family Pred' (b :: BinP) :: BinP where+ Pred' 'BE = 'BE+ Pred' ('B1 m) = 'B1 ('B0 m)+ Pred' ('B0 m) = 'B1 (Pred' m)++-------------------------------------------------------------------------------+-- Arithmetic: Plus+-------------------------------------------------------------------------------++-- | Addition.+--+-- >>> :kind! Plus Bin7 Bin7+-- Plus Bin7 Bin7 :: Bin+-- = 'BP ('B0 ('B1 ('B1 'BE)))+--+-- >>> :kind! Mult2 Bin7+-- Mult2 Bin7 :: Bin+-- = 'BP ('B0 ('B1 BinP3))+--+type family Plus (a :: Bin) (b :: Bin) :: Bin where+ Plus 'BZ b = b+ Plus a 'BZ = a+ Plus ('BP a) ('BP b) = 'BP (BP.Plus a b)++-------------------------------------------------------------------------------+--- Aliases of Bin+-------------------------------------------------------------------------------++type Bin0 = 'BZ+type Bin1 = 'BP BP.BinP1+type Bin2 = 'BP BP.BinP2+type Bin3 = 'BP BP.BinP3+type Bin4 = 'BP BP.BinP4+type Bin5 = 'BP BP.BinP5+type Bin6 = 'BP BP.BinP6+type Bin7 = 'BP BP.BinP7+type Bin8 = 'BP BP.BinP8+type Bin9 = 'BP BP.BinP9
+ src/Data/Type/BinP.hs view
@@ -0,0 +1,271 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+-- | Positive binary natural numbers. @DataKinds@ stuff.+module Data.Type.BinP (+ -- * Singleton+ SBinP (..),+ sbinpToBinP,+ sbinpToNatural,+ -- * Implicit+ SBinPI (..),+ withSBinP,+ reify,+ reflect,+ reflectToNum,+ -- * Type equality+ eqBinP,+ -- * Induction+ induction,+ -- * Arithmetic+ -- ** Successor+ Succ,+ withSucc,+ -- ** Addition+ Plus,+ -- * Conversions+ -- ** To GHC Nat+ ToGHC, FromGHC,+ -- ** To fin Nat+ ToNat,+ -- * Aliases+ BinP1, BinP2, BinP3, BinP4, BinP5, BinP6, BinP7, BinP8, BinP9,+ ) where++import Data.BinP (BinP (..))+import Data.Coerce (coerce)+import Data.Nat (Nat (..))+import Data.Proxy (Proxy (..))+import Data.Type.Equality ((:~:) (..), TestEquality (..))+import Data.Typeable (Typeable)+import Numeric.Natural (Natural)++import qualified Data.Type.Nat as N+import qualified GHC.TypeLits as GHC++-- $setup+-- >>> :set -XDataKinds+-- >>> import Data.Bin++-------------------------------------------------------------------------------+-- Singletons+-------------------------------------------------------------------------------++-- | Singleton of 'BinP'.+data SBinP (b :: BinP) where+ SBE :: SBinP 'BE+ SB0 :: SBinPI b => SBinP ('B0 b)+ SB1 :: SBinPI b => SBinP ('B1 b)+ deriving (Typeable)++-------------------------------------------------------------------------------+-- Implicits+-------------------------------------------------------------------------------++-- | Let constraint solver construct 'SBinP'.+class SBinPI (b :: BinP) where sbinp :: SBinP b+instance SBinPI 'BE where sbinp = SBE+instance SBinPI b => SBinPI ('B0 b) where sbinp = SB0+instance SBinPI b => SBinPI ('B1 b) where sbinp = SB1++-------------------------------------------------------------------------------+-- Conversions+-------------------------------------------------------------------------------++-- | Construct 'SBinPI' dictionary from 'SBinP'.+withSBinP :: SBinP b -> (SBinPI b => r) -> r+withSBinP SBE k = k+withSBinP SB0 k = k+withSBinP SB1 k = k++-- | Reify 'BinP'.+reify :: forall r. BinP -> (forall b. SBinPI b => Proxy b -> r) -> r+reify BE k = k (Proxy :: Proxy 'BE)+reify (B0 b) k = reify b (\(_ :: Proxy b) -> k (Proxy :: Proxy ('B0 b)))+reify (B1 b) k = reify b (\(_ :: Proxy b) -> k (Proxy :: Proxy ('B1 b)))++-- | Reflect type-level 'BinP' to the term level.+reflect :: forall b proxy. SBinPI b => proxy b -> BinP+reflect _ = unKP (induction (KP BE) (mapKP B0) (mapKP B1) :: KP BinP b)++-- | Reflect type-level 'BinP' to the term level 'Num'.+reflectToNum :: forall b proxy a. (SBinPI b, Num a) => proxy b -> a+reflectToNum _ = unKP (induction (KP 1) (mapKP (2*)) (mapKP (\x -> 2 * x + 1)) :: KP a b)++-- | Cconvert 'SBinP' to 'BinP'.+sbinpToBinP :: forall n. SBinP n -> BinP+sbinpToBinP s = withSBinP s $ reflect (Proxy :: Proxy n)++-- | Convert 'SBinP' to 'Natural'.+--+-- >>> sbinpToNatural (sbinp :: SBinP BinP8)+-- 8+--+sbinpToNatural :: forall n. SBinP n -> Natural+sbinpToNatural s = withSBinP s $ unKP (induction+ (KP 1)+ (mapKP (2 *))+ (mapKP (\x -> succ (2 * x))) :: KP Natural n)++-------------------------------------------------------------------------------+-- Equality+-------------------------------------------------------------------------------++eqBinP :: forall a b. (SBinPI a, SBinPI b) => Maybe (a :~: b)+eqBinP = case (sbinp :: SBinP a, sbinp :: SBinP b) of+ (SBE, SBE) -> Just Refl+ (SB0, SB0) -> recur where+ recur :: forall n m. (SBinPI n, SBinPI m) => Maybe ('B0 n :~: 'B0 m)+ recur = do+ Refl <- eqBinP :: Maybe (n :~: m)+ return Refl+ (SB1, SB1) -> recur where+ recur :: forall n m. (SBinPI n, SBinPI m) => Maybe ('B1 n :~: 'B1 m)+ recur = do+ Refl <- eqBinP :: Maybe (n :~: m)+ return Refl+ _ -> Nothing++instance TestEquality SBinP where+ testEquality SBE SBE = Just Refl+ testEquality SB0 SB0 = eqBinP+ testEquality SB1 SB1 = eqBinP++ testEquality _ _ = Nothing++-------------------------------------------------------------------------------+-- Convert to GHC Nat+-------------------------------------------------------------------------------++type family ToGHC (b :: BinP) :: GHC.Nat where+ ToGHC 'BE = 1+ ToGHC ('B0 b) = 2 GHC.* (ToGHC b)+ ToGHC ('B1 b) = 1 GHC.+ 2 GHC.* (ToGHC b)++type family FromGHC (n :: GHC.Nat) :: BinP where+ FromGHC n = FromGHC' (FromGHCMaybe n)++-- internals++type family FromGHC' (b :: Maybe BinP) :: BinP where+ FromGHC' ('Just b) = b++type family FromGHCMaybe (n :: GHC.Nat) :: Maybe BinP where+ FromGHCMaybe n = FromGHCMaybe' (GhcDivMod2 n)++type family FromGHCMaybe' (p :: (GHC.Nat, Bool)) :: Maybe BinP where+ FromGHCMaybe' '(0, 'False) = 'Nothing+ FromGHCMaybe' '(0, 'True) = 'Just 'BE+ FromGHCMaybe' '(n, 'False) = Mult2 (FromGHCMaybe n)+ FromGHCMaybe' '(n, 'True) = 'Just (Mult2Plus1 (FromGHCMaybe n))++-- | >>> :kind! GhcDivMod2 13+-- GhcDivMod2 13 :: (GHC.Nat, Bool)+-- = '(6, 'True)+--+type family GhcDivMod2 (n :: GHC.Nat) :: (GHC.Nat, Bool) where+ GhcDivMod2 0 = '(0, 'False)+ GhcDivMod2 1 = '(0, 'True)+ GhcDivMod2 n = GhcDivMod2' (GhcDivMod2 (n GHC.- 2))++type family GhcDivMod2' (p :: (GHC.Nat, Bool)) :: (GHC.Nat, Bool) where+ GhcDivMod2' '(n, b) = '(1 GHC.+ n, b)++type family Mult2 (b :: Maybe BinP) :: Maybe BinP where+ Mult2 'Nothing = 'Nothing+ Mult2 ('Just n) = 'Just ('B0 n)++type family Mult2Plus1 (b :: Maybe BinP) :: BinP where+ Mult2Plus1 'Nothing = 'BE+ Mult2Plus1 ('Just n) = ('B1 n)++-------------------------------------------------------------------------------+-- Conversion to Nat+-------------------------------------------------------------------------------++type family ToNat (b :: BinP) :: Nat where+ ToNat 'BE = 'S 'Z+ ToNat ('B0 b) = N.Mult2 (ToNat b)+ ToNat ('B1 b) = 'S (N.Mult2 (ToNat b))++-------------------------------------------------------------------------------+-- Arithmetic: Succ+-------------------------------------------------------------------------------++type family Succ (b :: BinP) :: BinP where+ Succ 'BE = 'B0 'BE+ Succ ('B0 n) = 'B1 n+ Succ ('B1 n) = 'B0 (Succ n)++withSucc :: forall b r. SBinPI b => Proxy b -> (SBinPI (Succ b) => r) -> r+withSucc p k = case sbinp :: SBinP b of+ SBE -> k+ SB0 -> k+ SB1 -> recur p k+ where+ -- eta needed for older GHC+ recur :: forall m s. SBinPI m => Proxy ('B1 m) -> (SBinPI ('B0 (Succ m)) => s) -> s+ recur _ k' = withSucc (Proxy :: Proxy m) k'++-------------------------------------------------------------------------------+-- Arithmetic: Plus+-------------------------------------------------------------------------------++type family Plus (a :: BinP) (b :: BinP) :: BinP where+ Plus 'BE b = Succ b+ Plus a 'BE = Succ a+ Plus ('B0 a) ('B0 b) = 'B0 (Plus a b)+ Plus ('B1 a) ('B0 b) = 'B1 (Plus a b)+ Plus ('B0 a) ('B1 b) = 'B1 (Plus a b)+ Plus ('B1 a) ('B1 b) = 'B0 (Succ (Plus a b))++-------------------------------------------------------------------------------+-- Induction+-------------------------------------------------------------------------------++-- | Induction on 'BinP'.+induction+ :: forall b f. SBinPI b+ => f 'BE -- ^ \(P(1)\)+ -> (forall bb. SBinPI bb => f bb -> f ('B0 bb)) -- ^ \(\forall b. P(b) \to P(2b)\)+ -> (forall bb. SBinPI bb => f bb -> f ('B1 bb)) -- ^ \(\forall b. P(b) \to P(2b + 1)\)+ -> f b+induction e o i = go where+ go :: forall bb. SBinPI bb => f bb+ go = case sbinp :: SBinP bb of+ SBE -> e+ SB0 -> o go+ SB1 -> i go++-------------------------------------------------------------------------------+-- Aliases of BinP+-------------------------------------------------------------------------------++type BinP1 = 'BE+type BinP2 = 'B0 BinP1+type BinP3 = 'B1 BinP1+type BinP4 = 'B0 BinP2+type BinP5 = 'B1 BinP2+type BinP6 = 'B0 BinP3+type BinP7 = 'B1 BinP3+type BinP8 = 'B0 BinP4+type BinP9 = 'B1 BinP4++-------------------------------------------------------------------------------+-- Aux+-------------------------------------------------------------------------------++newtype KP a (b :: BinP) = KP a++unKP :: KP a b -> a+unKP = coerce++mapKP :: (a -> b) -> KP a bn -> KP b bn'+mapKP = coerce
+ src/Data/Wrd.hs view
@@ -0,0 +1,523 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+-- | Fixed-'Wrd'th (unsigned) integers.+module Data.Wrd (+ Wrd (..),+ -- * Showing+ explicitShow,+ explicitShowsPrec,+ -- * Conversions+ toNatural,+ -- * Universe+ universe,+ -- * Bits+ --+ -- | We have implementation of some 'Bits' members, which doesn't+ -- need 'N.SNatI' constraint.+ xor,+ (.&.),+ (.|.),+ complement,+ complement2,+ shiftR,+ shiftL,+ rotateL,+ rotateR,+ popCount,+ setBit,+ clearBit,+ complementBit,+ testBit,+ -- * Extras+ shiftL1,+ shiftR1,+ rotateL1,+ rotateR1,+ ) where++import Control.DeepSeq (NFData (..))+import Data.Hashable (Hashable (..))+import Data.Nat (Nat (..))+import Data.Proxy (Proxy (..))+import Data.Typeable (Typeable)+import Numeric.Natural (Natural)++import qualified Data.Type.Nat as N+import qualified Test.QuickCheck as QC++import qualified Data.Bits as I (Bits (..), FiniteBits (..))++-- $setup+-- >>> :set -XDataKinds++-------------------------------------------------------------------------------+-- Data+-------------------------------------------------------------------------------++-- | Fixed-width unsigned integers, 'Wrd's for short.+--+-- The number is thought to be stored in big-endian format,+-- i.e. most-significant bit first. (as in binary literals).+--+data Wrd (n :: Nat) where+ WE :: Wrd 'Z+ W0 :: Wrd n -> Wrd ('S n)+ W1 :: Wrd n -> Wrd ('S n)+ deriving (Typeable)++deriving instance Eq (Wrd n)++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++instance Ord (Wrd n) where+ compare WE WE = EQ+ compare (W0 a) (W0 b) = compare a b+ compare (W0 _) (W1 _) = LT+ compare (W1 _) (W0 _) = GT+ compare (W1 a) (W1 b) = compare a b++-- | 'Wrd' is printed as a binary literal.+--+-- >>> let i = W1 $ W0 $ W1 $ W0 WE+-- >>> i+-- 0b1010+--+-- >>> explicitShow i+-- "W1 $ W0 $ W1 $ W0 WE"+--+-- At the time being, there is no 'Num' instance.+--+instance Show (Wrd n) where+ showsPrec _ WE = showString "WE"+ showsPrec _ w = showString "0b" . foldr f id (goBits w)+ where+ f True acc = showChar '1' . acc+ f False acc = showChar '0' . acc++ goBits :: Wrd m -> [Bool]+ goBits WE = []+ goBits (W0 n) = False : goBits n+ goBits (W1 n) = True : goBits n++instance NFData (Wrd n) where+ rnf WE = ()+ rnf (W0 w) = rnf w+ rnf (W1 w) = rnf w++instance Hashable (Wrd n) where+ hashWithSalt salt WE = salt `hashWithSalt` (0 :: Int)+ hashWithSalt salt (W0 w) = salt `hashWithSalt` (1 :: Int) `hashWithSalt` w+ hashWithSalt salt (W1 w) = salt `hashWithSalt` (2 :: Int) `hashWithSalt` w++instance N.SNatI n => Bounded (Wrd n) where+ minBound = N.induction WE W0+ maxBound = N.induction WE W1++instance N.SNatI n => Num (Wrd n) where+ fromInteger = snd . wrdScanl0 f where+ f :: Integer -> (Integer, Bool)+ f i =+ let (i', m) = i `divMod` 2+ in (i', m /= 0)++ a + b = snd (wrdScanl2 f False a b) where+ f False False False = (False, False)+ f False False True = (False, True)+ f False True False = (False, True)+ f False True True = (True, False)+ f True False False = (False, True)+ f True False True = (True, False)+ f True True False = (True, False)+ f True True True = (True, True)++ a * b = snd $ fst $ wrdScanl f (a, I.zeroBits) b where+ f :: (Wrd n, Wrd n) -> Bool -> ((Wrd n, Wrd n), Bool)+ f (a', acc) True = ((shiftL1 a', a' + acc), False)+ f (a', acc) False = ((shiftL1 a', acc), False)++ abs = id+ negate = complement2++ signum = go False where+ go :: Bool -> Wrd m -> Wrd m+ go _ WE = WE+ go True (W0 WE) = W1 WE+ go False (W0 WE) = W0 WE+ go True (W1 WE) = W1 WE+ go False (W1 WE) = W1 WE+ go b (W0 w) = W0 (go b w)+ go _ (W1 w) = W0 (go True w) ++-------------------------------------------------------------------------------+-- Bits & FiniteBits+-------------------------------------------------------------------------------++-- |+--+-- >>> let u = W0 $ W0 $ W1 $ W1 WE+-- >>> let v = W0 $ W1 $ W0 $ W1 WE+-- >>> (u, v)+-- (0b0011,0b0101)+--+-- >>> (complement u, complement v)+-- (0b1100,0b1010)+--+-- >>> (u .&. v, u .|. v, u `xor` v)+-- (0b0001,0b0111,0b0110)+--+-- >>> (shiftR v 1, shiftL v 1)+-- (0b0010,0b1010)+--+-- >>> (rotateR u 1, rotateL u 3)+-- (0b1001,0b1001)+--+-- >>> popCount u+-- 2+--+instance N.SNatI n => I.Bits (Wrd n) where+ complement = complement+ (.&.) = (.&.)+ (.|.) = (.|.)+ xor = xor++ isSigned _ = False++ shiftR = shiftR+ shiftL = shiftL+ rotateR = rotateR+ rotateL = rotateL++ clearBit = clearBit+ complementBit = complementBit+ setBit = setBit+ testBit = testBit++ zeroBits = N.induction WE W0++ popCount = popCount++ -- this is good enough+ bit = setBit I.zeroBits++ bitSizeMaybe = Just . I.finiteBitSize+ bitSize = I.finiteBitSize++instance N.SNatI n => I.FiniteBits (Wrd n) where+ finiteBitSize _ = N.reflectToNum (Proxy :: Proxy n)++#if MIN_VERSION_base(4,8,0)+ countLeadingZeros = countLeadingZeros+#endif++testBit :: Wrd n -> Int -> Bool+testBit w0 i = snd (go 0 w0) where+ go :: Int -> Wrd n -> (Int, Bool)+ go j WE = (j, False)+ go j (W0 w) =+ let j'' = succ j'+ (j', b') = go j w+ in (j'', if i == j' then False else b')+ go j (W1 w) =+ let j'' = succ j'+ (j', b') = go j w+ in (j'', if i == j' then True else b')++clearBit :: Wrd n -> Int -> Wrd n+clearBit w i = mapWithBit (\j b -> if j == i then False else b) w++setBit :: Wrd n -> Int -> Wrd n+setBit w i = mapWithBit (\j b -> if j == i then True else b) w++complementBit :: Wrd n -> Int -> Wrd n+complementBit w i = mapWithBit (\j b -> if j == i then not b else b) w++complement :: Wrd n -> Wrd n+complement WE = WE+complement (W0 w) = W1 (complement w)+complement (W1 w) = W0 (complement w)++-- | @'complement2' w = 'complement' w + 1@+complement2 :: Wrd n -> Wrd n+complement2 = snd . wrdScanl f True where+ f :: Bool -> Bool -> (Bool, Bool)+ f False False = (False, True)+ f False True = (False, False)+ f True False = (True, False)+ f True True = (False, True)++(.&.) :: Wrd n -> Wrd n -> Wrd n+WE .&. _ = WE+W1 a .&. W1 b = W1 (a .&. b)+W1 a .&. W0 b = W0 (a .&. b)+W0 a .&. W1 b = W0 (a .&. b)+W0 a .&. W0 b = W0 (a .&. b)++(.|.) :: Wrd n -> Wrd n -> Wrd n+WE .|. _ = WE+W1 a .|. W1 b = W1 (a .|. b)+W1 a .|. W0 b = W1 (a .|. b)+W0 a .|. W1 b = W1 (a .|. b)+W0 a .|. W0 b = W0 (a .|. b)++xor :: Wrd n -> Wrd n -> Wrd n+xor WE _ = WE+xor (W1 a) (W1 b) = W0 (xor a b)+xor (W1 a) (W0 b) = W1 (xor a b)+xor (W0 a) (W1 b) = W1 (xor a b)+xor (W0 a) (W0 b) = W0 (xor a b)++shiftR :: Wrd n -> Int -> Wrd n+shiftR w n+ | n <= 0 = w+ | otherwise = shiftR (shiftR1 w) (pred n)++shiftL :: Wrd n -> Int -> Wrd n+shiftL w n+ | n <= 0 = w+ | otherwise = shiftL (shiftL1 w) (pred n)++rotateR :: Wrd n -> Int -> Wrd n+rotateR w n+ | n <= 0 = w+ | otherwise = rotateR (rotateR1 w) (pred n)++rotateL :: Wrd n -> Int -> Wrd n+rotateL w n+ | n <= 0 = w+ | otherwise = rotateL (rotateL1 w) (pred n)++popCount :: Wrd n -> Int+popCount = go 0 where+ go :: Int -> Wrd m -> Int+ go !acc WE = acc+ go !acc (W0 w) = go acc w+ go !acc (W1 w) = go (succ acc) w++shiftL1 :: Wrd n -> Wrd n+shiftL1 WE = WE+shiftL1 (W0 w) = pushBack w+shiftL1 (W1 w) = pushBack w++shiftR1 :: Wrd n -> Wrd n+shiftR1 WE = WE+shiftR1 w@(W0 _) = W0 (dropLast w)+shiftR1 w@(W1 _) = W0 (dropLast w)++rotateL1 :: Wrd n -> Wrd n+rotateL1 WE = WE+rotateL1 (W0 w) = pushBack' w False+rotateL1 (W1 w) = pushBack' w True++rotateR1 :: Wrd n -> Wrd n+rotateR1 WE = WE+rotateR1 w@(W0 _) = case dropLast' w of+ (True, w') -> W1 w'+ (False, w') -> W0 w'+rotateR1 w@(W1 _) = case dropLast' w of+ (True, w') -> W1 w'+ (False, w') -> W0 w'++pushBack :: Wrd n -> Wrd ('S n)+pushBack WE = W0 WE+pushBack (W0 w) = W0 (pushBack w)+pushBack (W1 w) = W1 (pushBack w)++pushBack' :: Wrd n -> Bool -> Wrd ('S n)+pushBack' WE False = W0 WE+pushBack' WE True = W1 WE+pushBack' (W0 w) b = W0 (pushBack' w b)+pushBack' (W1 w) b = W1 (pushBack' w b)++dropLast :: Wrd ('S n) -> Wrd n+dropLast (W0 WE) = WE+dropLast (W1 WE) = WE+dropLast (W0 w@(W0 _)) = W0 (dropLast w)+dropLast (W0 w@(W1 _)) = W0 (dropLast w)+dropLast (W1 w@(W0 _)) = W1 (dropLast w)+dropLast (W1 w@(W1 _)) = W1 (dropLast w)++dropLast' :: Wrd ('S n) -> (Bool, Wrd n)+dropLast' (W0 WE) = (False, WE)+dropLast' (W1 WE) = (True, WE)+dropLast' (W0 w@(W0 _)) = fmap W0 (dropLast' w)+dropLast' (W0 w@(W1 _)) = fmap W0 (dropLast' w)+dropLast' (W1 w@(W0 _)) = fmap W1 (dropLast' w)+dropLast' (W1 w@(W1 _)) = fmap W1 (dropLast' w)++countLeadingZeros :: Wrd n -> Int+countLeadingZeros = go 0 where+ go :: Int -> Wrd m -> Int+ go !acc WE = acc+ go !acc (W0 w) = go (succ acc) w+ go !acc (W1 _) = acc++-------------------------------------------------------------------------------+-- QuickCheck+-------------------------------------------------------------------------------++instance N.SNatI n => QC.Arbitrary (Wrd n) where+ arbitrary = case N.snat :: N.SNat n of+ N.SZ -> return WE+ N.SS -> QC.oneof [ fmap W0 QC.arbitrary, fmap W1 QC.arbitrary ]++ shrink = shrink++shrink :: Wrd n -> [Wrd n]+shrink WE = []+shrink (W1 w) = W0 w : fmap W1 (shrink w)+shrink (W0 w) = fmap W0 (shrink w)++instance QC.CoArbitrary (Wrd n) where+ coarbitrary WE = id+ coarbitrary (W0 w) = QC.coarbitrary (False, w)+ coarbitrary (W1 w) = QC.coarbitrary (True, w)++instance N.SNatI n => QC.Function (Wrd n) where+ function = case N.snat :: N.SNat n of+ N.SZ -> QC.functionMap (const ()) (const WE)+ N.SS -> QC.functionMap toPair fromPair+ where+ toPair :: Wrd ('S m) -> (Bool, Wrd m)+ toPair (W0 w) = (False, w)+ toPair (W1 w) = (True, w)++ fromPair :: (Bool, Wrd m) -> Wrd ('S m)+ fromPair (False, w) = W0 w+ fromPair (True, w) = W1 w++-------------------------------------------------------------------------------+-- Showing+-------------------------------------------------------------------------------++-- | 'show' displaying a structure of @'Wrd' n@+--+-- >>> explicitShow WE+-- "WE"+--+-- >>> explicitShow $ W0 WE+-- "W0 WE"+--+-- >>> explicitShow $ W1 $ W0 $ W1 $ W0 WE+-- "W1 $ W0 $ W1 $ W0 WE"+--+explicitShow :: Wrd n -> String+explicitShow w = explicitShowsPrec 0 w ""++-- | 'showsPrec' displaying a structure of @'Wrd' n@.+--+-- >>> explicitShowsPrec 0 (W0 WE) ""+-- "W0 WE"+--+-- >>> explicitShowsPrec 1 (W0 WE) ""+-- "(W0 WE)"+--+explicitShowsPrec :: Int -> Wrd n -> ShowS+explicitShowsPrec _ WE = showString "WE"+explicitShowsPrec d w = showParen (d > 0) $+ go (goBits w)+ where+ go [] = showString "WE"+ go [False] = showString "W0 WE"+ go [True] = showString "W1 WE"+ go (False : bs) = showString "W0 $ " . go bs+ go (True : bs) = showString "W1 $ " . go bs++ goBits :: Wrd m -> [Bool]+ goBits WE = []+ goBits (W0 n) = False : goBits n+ goBits (W1 n) = True : goBits n++-------------------------------------------------------------------------------+-- Conversions+-------------------------------------------------------------------------------++-- | Convert to 'Natural' number+--+-- >>> let u = W0 $ W1 $ W1 $ W1 $ W0 $ W1 $ W0 WE+-- >>> u+-- 0b0111010+--+-- >>> toNatural u+-- 58+--+-- >>> map toNatural (universe :: [Wrd N.Nat3])+-- [0,1,2,3,4,5,6,7]+--+toNatural :: Wrd n -> Natural+toNatural = go 0 where+ go :: Natural -> Wrd m -> Natural+ go !acc WE = acc+ go !acc (W0 w) = go (2 * acc) w+ go !acc (W1 w) = go (2 * acc + 1) w++-------------------------------------------------------------------------------+-- Universe+-------------------------------------------------------------------------------++-- | All values, i.e. universe of @'Wrd' @.+--+-- >>> universe :: [Wrd 'Z]+-- [WE]+--+-- >>> universe :: [Wrd N.Nat3]+-- [0b000,0b001,0b010,0b011,0b100,0b101,0b110,0b111]+universe :: forall n. N.SNatI n => [Wrd n]+universe = getUniverse $ N.induction (Universe [WE]) go where+ go :: Universe m -> Universe ('S m)+ go (Universe u) = Universe (map W0 u ++ map W1 u)++newtype Universe n = Universe { getUniverse :: [Wrd n] }++-------------------------------------------------------------------------------+-- Scans+-------------------------------------------------------------------------------++mapWithBit :: (Int -> Bool -> Bool) -> Wrd n -> Wrd n+mapWithBit f = snd . wrdScanl g 0 where+ g i b = (succ i, f i b)++wrdScanl0 :: forall s n. N.SNatI n => (s -> (s, Bool)) -> s -> (s, Wrd n)+wrdScanl0 g = go where+ go :: forall m. N.SNatI m => s -> (s, Wrd m)+ go s = case N.snat :: N.SNat m of+ N.SZ -> (s, WE)+ N.SS -> + let (s'', b) = g s'+ (s' , w') = go s+ in (s'', if b then W1 w' else W0 w')++wrdScanl :: forall s n. (s -> Bool -> (s, Bool)) -> s -> Wrd n -> (s, Wrd n)+wrdScanl g = go where+ go :: s -> Wrd m -> (s, Wrd m)+ go s WE = (s, WE)+ go s (W0 w) =+ let (s'', b) = g s' False+ (s' , w') = go s w+ in (s'', if b then W1 w' else W0 w')+ go s (W1 w) =+ let (s'', b) = g s' True+ (s' , w') = go s w+ in (s'', if b then W1 w' else W0 w')+ +wrdScanl2 :: forall s n. (s -> Bool -> Bool -> (s, Bool)) -> s -> Wrd n -> Wrd n -> (s, Wrd n)+wrdScanl2 g = go where+ go :: s -> Wrd m -> Wrd m -> (s, Wrd m)+ go s WE _ = (s, WE)+ go s (W0 w) (W0 w') = go' s False False w w'+ go s (W0 w) (W1 w') = go' s False True w w'+ go s (W1 w) (W0 w') = go' s True False w w'+ go s (W1 w) (W1 w') = go' s True True w w'++ go' :: s -> Bool -> Bool -> Wrd m -> Wrd m -> (s, Wrd ('S m))+ go' s i j w u =+ let (s'', b) = g s' i j+ (s' , v) = go s w u+ in (s'', if b then W1 v else W0 v)