diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,5 @@ +# Version history for bin + +## 0.1 + +- First version. Released on an unsuspecting world. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,17 @@ +SPDX-License-Identifier: GPL-2.0-or-later + +Copyright (c) 2019 Oleg Grenrus + + 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 . diff --git a/bin.cabal b/bin.cabal new file mode 100644 --- /dev/null +++ b/bin.cabal @@ -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 , + 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 +maintainer: Oleg.Grenrus +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 diff --git a/src/Data/Bin.hs b/src/Data/Bin.hs new file mode 100644 --- /dev/null +++ b/src/Data/Bin.hs @@ -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 diff --git a/src/Data/Bin/Pos.hs b/src/Data/Bin/Pos.hs new file mode 100644 --- /dev/null +++ b/src/Data/Bin/Pos.hs @@ -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 diff --git a/src/Data/BinP.hs b/src/Data/BinP.hs new file mode 100644 --- /dev/null +++ b/src/Data/BinP.hs @@ -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 diff --git a/src/Data/BinP/PosP.hs b/src/Data/BinP/PosP.hs new file mode 100644 --- /dev/null +++ b/src/Data/BinP/PosP.hs @@ -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 } diff --git a/src/Data/Type/Bin.hs b/src/Data/Type/Bin.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Bin.hs @@ -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 diff --git a/src/Data/Type/BinP.hs b/src/Data/Type/BinP.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/BinP.hs @@ -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 diff --git a/src/Data/Wrd.hs b/src/Data/Wrd.hs new file mode 100644 --- /dev/null +++ b/src/Data/Wrd.hs @@ -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)