{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE DeriveDataTypeable     #-}
{-# LANGUAGE EmptyCase              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE Safe                   #-}
{-# 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, Ord (..), Bounded (..), ($), (.))
-- >>> import Data.Foldable (traverse_)
-- >>> import Data.Type.Bin

-------------------------------------------------------------------------------
-- Data
-------------------------------------------------------------------------------

-- | 'Pos' is to 'Bin' is what 'Fin' is to 'Nat'.
--
-- The name is picked, as the lack of better 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 :: Int -> Pos b -> ShowS
showsPrec Int
d = Int -> Natural -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d (Natural -> ShowS) -> (Pos b -> Natural) -> Pos b -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pos b -> Natural
forall (b :: Bin). Pos b -> Natural
toNatural

-- |
--
-- >>> minBound < (maxBound :: Pos Bin5)
-- True
instance (SBinPI n, b ~ 'BP n) => Bounded (Pos b) where
    minBound :: Pos b
minBound = PosP n -> Pos ('BP n)
forall (b :: BinP). PosP b -> Pos ('BP b)
Pos PosP n
forall a. Bounded a => a
minBound
    maxBound :: Pos b
maxBound = PosP n -> Pos ('BP n)
forall (b :: BinP). PosP b -> Pos ('BP b)
Pos PosP n
forall a. Bounded a => a
maxBound

-------------------------------------------------------------------------------
-- QuickCheck
-------------------------------------------------------------------------------

instance (SBinPI n, b ~ 'BP n) => QC.Arbitrary (Pos b) where
    arbitrary :: Gen (Pos b)
arbitrary = (PosP n -> Pos ('BP n)) -> Gen (PosP n) -> Gen (Pos ('BP n))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PosP n -> Pos ('BP n)
forall (b :: BinP). PosP b -> Pos ('BP b)
Pos Gen (PosP n)
forall a. Arbitrary a => Gen a
QC.arbitrary

instance QC.CoArbitrary (Pos b) where
    coarbitrary :: Pos b -> Gen b -> Gen b
coarbitrary = Integer -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary (Integer -> Gen b -> Gen b)
-> (Pos b -> Integer) -> Pos b -> Gen b -> Gen b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral :: Natural -> Integer) (Natural -> Integer) -> (Pos b -> Natural) -> Pos b -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pos b -> Natural
forall (b :: Bin). Pos b -> Natural
toNatural

instance (SBinPI n, b ~ 'BP n) => QC.Function (Pos b) where
    function :: (Pos b -> b) -> Pos b :-> b
function = (Pos ('BP n) -> PosP n)
-> (PosP n -> Pos ('BP n))
-> (Pos ('BP n) -> b)
-> Pos ('BP n) :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\(Pos PosP b
p) -> PosP n
PosP b
p) PosP n -> Pos ('BP n)
forall (b :: BinP). PosP b -> Pos ('BP b)
Pos

-------------------------------------------------------------------------------
-- Showing
-------------------------------------------------------------------------------

explicitShow :: Pos b -> String
explicitShow :: Pos b -> String
explicitShow Pos b
b = Int -> Pos b -> ShowS
forall (b :: Bin). Int -> Pos b -> ShowS
explicitShowsPrec Int
0 Pos b
b String
""

explicitShowsPrec :: Int -> Pos b ->ShowS
explicitShowsPrec :: Int -> Pos b -> ShowS
explicitShowsPrec Int
d (Pos PosP b
b)
    = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10)
    (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Pos "
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> PosP b -> ShowS
forall (b :: BinP). Int -> PosP b -> ShowS
PP.explicitShowsPrec Int
11 PosP b
b

-------------------------------------------------------------------------------
-- Conversions
-------------------------------------------------------------------------------

-- | Convert 'Pos' to 'Natural'
--
-- >>> map toNatural (universe :: [Pos Bin7])
-- [0,1,2,3,4,5,6]
toNatural :: Pos b -> Natural
toNatural :: Pos b -> Natural
toNatural (Pos PosP b
p) = PosP b -> Natural
forall (b :: BinP). PosP b -> Natural
PP.toNatural PosP b
p

-------------------------------------------------------------------------------
-- Interesting
-------------------------------------------------------------------------------

-- | @'Pos' 'BZ'@ is not inhabited.
absurd  :: Pos 'BZ -> b
absurd :: Pos 'BZ -> b
absurd Pos 'BZ
x = case Pos 'BZ
x of {}

-- | Counting to one is boring
--
-- >>> boring
-- 0
boring :: Pos ('BP 'BE)
boring :: Pos ('BP 'BE)
boring = Pos ('BP 'BE)
forall a. Bounded a => a
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 :: Pos ('BP b)
top = Pos ('BP b)
forall a. Bounded a => a
minBound

-- | See 'top'.
pop :: (SBinPI a, Pred b ~ 'BP a, BP.Succ a ~ b) => Pos ('BP a) -> Pos ('BP b)
pop :: Pos ('BP a) -> Pos ('BP b)
pop = Pos ('BP a) -> Pos ('BP b)
forall (b :: BinP). SBinPI b => Pos ('BP b) -> Pos (Succ'' b)
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 ('BP b) -> Pos (Succ'' b)
weakenRight1 (Pos PosP b
b) = PosP (Succ b) -> Pos (Succ'' b)
forall (b :: BinP). PosP b -> Pos ('BP b)
Pos (PosP b -> PosP (Succ b)
forall (b :: BinP). SBinPI b => PosP b -> PosP (Succ b)
PP.weakenRight1 PosP b
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 :: [Pos b]
universe = case SBin b
forall (b :: Bin). SBinI b => SBin b
B.sbin :: SBin b of
    SBin b
B.SBZ -> []
    SBin b
B.SBP -> (PosP b -> Pos ('BP b)) -> [PosP b] -> [Pos ('BP b)]
forall a b. (a -> b) -> [a] -> [b]
map PosP b -> Pos ('BP b)
forall (b :: BinP). PosP b -> Pos ('BP b)
Pos [PosP b]
forall (b :: BinP). SBinPI b => [PosP b]
PP.universe