{-# 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.EqP        (EqP (..))
import Data.GADT.Show  (GShow (..))
import Data.OrdP       (OrdP (..))
import Data.Typeable   (Typeable)
import Numeric.Natural (Natural)

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 = 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

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

-- |
--
-- >>> 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) = PosP b -> PosP b -> Bool
forall k (f :: k -> *) (a :: k) (b :: k).
EqP @k f =>
f a -> f b -> Bool
forall (a :: BinP) (b :: BinP). PosP a -> PosP 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) = PosP b -> PosP b -> Ordering
forall k (f :: k -> *) (a :: k) (b :: k).
OrdP @k f =>
f a -> f b -> Ordering
forall (a :: BinP) (b :: BinP). PosP a -> PosP b -> Ordering
comparep PosP b
x PosP b
y

-- |
--
-- >>> 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

-- | @since 0.1.2
instance NFData (Pos b) where
    rnf :: Pos b -> ()
rnf (Pos PosP b
p) = PosP b -> ()
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 = (PosP n -> Pos b) -> Gen (PosP n) -> Gen (Pos b)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PosP n -> Pos b
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 :: forall b. Pos b -> Gen b -> Gen b
coarbitrary = Integer -> Gen b -> Gen b
forall b. 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 :: forall b. (Pos b -> b) -> Pos b :-> b
function = (Pos b -> PosP n)
-> (PosP n -> Pos b) -> (Pos b -> b) -> Pos b :-> 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 b
PosP n -> Pos ('BP n)
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 = Int -> Pos b -> ShowS
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 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 :: forall (b :: Bin). 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 :: 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 = 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 :: forall (b :: BinP). SBinPI b => 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 :: 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 = Pos ('BP a) -> Pos ('BP b)
Pos ('BP a) -> Pos (Succ'' a)
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) = PosP (Succ b) -> Pos ('BP (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)

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

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

-- | @since 0.1.2
instance b ~ 'BZ => Boring.Absurd (Pos b) where
    absurd :: forall b. Pos b -> b
absurd = Pos b -> b
Pos 'BZ -> b
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 SBin b
forall (b :: Bin). SBinI b => SBin b
B.sbin :: SBin b of
    SBin b
B.SBZ -> []
    SBin b
B.SBP -> (PosP b1 -> Pos b) -> [PosP b1] -> [Pos b]
forall a b. (a -> b) -> [a] -> [b]
map PosP b1 -> Pos b
PosP b1 -> Pos ('BP b1)
forall (b :: BinP). PosP b -> Pos ('BP b)
Pos [PosP b1]
forall (b :: BinP). SBinPI b => [PosP b]
PP.universe