{-# LANGUAGE CPP                    #-}
{-# 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 Control.DeepSeq (NFData (..))
import Data.Bin        (Bin (..), BinP (..))
import Data.BinP.PosP  (PosP (..))
import Data.GADT.Show  (GShow (..))
import Data.Typeable   (Typeable)
import Numeric.Natural (Natural)

#if MIN_VERSION_some(1,0,5)
import Data.EqP  (EqP (..))
import Data.OrdP (OrdP (..))
#endif

import qualified Data.BinP.PosP  as PP
import qualified Data.Boring     as Boring
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 (..), ($), (.), print)
-- >>> import Data.Foldable (traverse_)
-- >>> import Data.Type.Bin
-- >>> import Data.EqP (eqp)
-- >>> import Data.OrdP (comparep)
-- >>> :set -XTypeApplications

-------------------------------------------------------------------------------
-- 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 = forall a. Show a => Int -> a -> ShowS
showsPrec Int
d forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (b :: Bin). Pos b -> Natural
toNatural

-- | @since 0.1.3
instance GShow Pos where
    gshowsPrec :: forall (b :: Bin). Int -> Pos b -> ShowS
gshowsPrec = forall a. Show a => Int -> a -> ShowS
showsPrec

#if MIN_VERSION_some(1,0,5)
-- |
--
-- >>> eqp (top :: Pos Bin4) (top :: Pos Bin6)
-- True
--
-- >>> let xs = universe @Bin4; ys = universe @Bin6 in traverse_ print [ [ eqp x y | y <- ys ] | x <- xs ]
-- [True,False,False,False,False,False]
-- [False,True,False,False,False,False]
-- [False,False,True,False,False,False]
-- [False,False,False,True,False,False]
--
-- @since 0.1.3
instance EqP Pos where
    eqp :: forall (a :: Bin) (b :: Bin). Pos a -> Pos b -> Bool
eqp (Pos PosP b
x) (Pos PosP b
y) = forall k (f :: k -> *) (a :: k) (b :: k).
EqP @k f =>
f a -> f b -> Bool
eqp PosP b
x PosP b
y

-- |
--
-- >>> let xs = universe @Bin4; ys = universe @Bin6 in traverse_ print [ [ comparep x y | y <- ys ] | x <- xs ]
-- [EQ,LT,LT,LT,LT,LT]
-- [GT,EQ,LT,LT,LT,LT]
-- [GT,GT,EQ,LT,LT,LT]
-- [GT,GT,GT,EQ,LT,LT]
--
-- @since 0.1.3
--
instance OrdP Pos where
    comparep :: forall (a :: Bin) (b :: Bin). Pos a -> Pos b -> Ordering
comparep (Pos PosP b
x) (Pos PosP b
y) = forall k (f :: k -> *) (a :: k) (b :: k).
OrdP @k f =>
f a -> f b -> Ordering
comparep PosP b
x PosP b
y
#endif

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

-- | @since 0.1.2
instance NFData (Pos b) where
    rnf :: Pos b -> ()
rnf (Pos PosP b
p) = forall a. NFData a => a -> ()
rnf PosP b
p

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

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

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

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

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

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

explicitShowsPrec :: Int -> Pos b ->ShowS
explicitShowsPrec :: forall (b :: Bin). Int -> Pos b -> ShowS
explicitShowsPrec Int
d (Pos PosP b
b)
    = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10)
    forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Pos "
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (b :: Bin). Pos b -> Natural
toNatural (Pos PosP b
p) = forall (b :: BinP). PosP b -> Natural
PP.toNatural PosP b
p

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

-- | @'Pos' 'BZ'@ is not inhabited.
absurd  :: Pos 'BZ -> b
absurd :: forall b. 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 = 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 :: forall (b :: BinP). SBinPI b => Pos ('BP b)
top = 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 :: forall (a :: BinP) (b :: BinP).
(SBinPI a, (Pred b :: Bin) ~ ('BP a :: Bin),
 (Succ a :: BinP) ~ (b :: BinP)) =>
Pos ('BP a) -> Pos ('BP b)
pop = 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 :: forall (b :: BinP). SBinPI b => Pos ('BP b) -> Pos (Succ'' b)
weakenRight1 (Pos PosP b
b) = forall (b :: BinP). PosP b -> Pos ('BP b)
Pos (forall (b :: BinP). SBinPI b => PosP b -> PosP (Succ b)
PP.weakenRight1 PosP b
b)

-------------------------------------------------------------------------------
-- Boring
-------------------------------------------------------------------------------

-- | @since 0.1.2
instance b ~ 'BP 'BE => Boring.Boring (Pos b) where
    boring :: Pos b
boring = Pos ('BP 'BE)
boring

-- | @since 0.1.2
instance b ~ 'BZ => Boring.Absurd (Pos b) where
    absurd :: forall b. Pos b -> b
absurd = forall b. Pos 'BZ -> b
absurd

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