{-# LANGUAGE BangPatterns           #-}
{-# 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.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 Control.DeepSeq (NFData (..))
import Data.Bin        (BinP (..))
import Data.EqP        (EqP (..))
import Data.GADT.Show  (GShow (..))
import Data.Nat        (Nat (..))
import Data.OrdP       (OrdP (..))
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.Boring     as Boring
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_)
-- >>> import qualified Data.Type.Nat as N
-- >>> import Data.Type.BinP

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

-- | 'PosP' is to 'BinP' is what 'Fin' is to 'Nat', when 'n' is 'Z'.
newtype PosP (b :: BinP) = PosP { forall (b :: BinP). PosP b -> PosP' 'Z b
unPosP :: PosP' 'Z b }
  deriving (PosP b -> PosP b -> Bool
(PosP b -> PosP b -> Bool)
-> (PosP b -> PosP b -> Bool) -> Eq (PosP b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (b :: BinP). PosP b -> PosP b -> Bool
$c== :: forall (b :: BinP). PosP b -> PosP b -> Bool
== :: PosP b -> PosP b -> Bool
$c/= :: forall (b :: BinP). PosP b -> PosP b -> Bool
/= :: PosP b -> PosP b -> Bool
Eq, Eq (PosP b)
Eq (PosP b) =>
(PosP b -> PosP b -> Ordering)
-> (PosP b -> PosP b -> Bool)
-> (PosP b -> PosP b -> Bool)
-> (PosP b -> PosP b -> Bool)
-> (PosP b -> PosP b -> Bool)
-> (PosP b -> PosP b -> PosP b)
-> (PosP b -> PosP b -> PosP b)
-> Ord (PosP b)
PosP b -> PosP b -> Bool
PosP b -> PosP b -> Ordering
PosP b -> PosP b -> PosP b
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (b :: BinP). Eq (PosP b)
forall (b :: BinP). PosP b -> PosP b -> Bool
forall (b :: BinP). PosP b -> PosP b -> Ordering
forall (b :: BinP). PosP b -> PosP b -> PosP b
$ccompare :: forall (b :: BinP). PosP b -> PosP b -> Ordering
compare :: PosP b -> PosP b -> Ordering
$c< :: forall (b :: BinP). PosP b -> PosP b -> Bool
< :: PosP b -> PosP b -> Bool
$c<= :: forall (b :: BinP). PosP b -> PosP b -> Bool
<= :: PosP b -> PosP b -> Bool
$c> :: forall (b :: BinP). PosP b -> PosP b -> Bool
> :: PosP b -> PosP b -> Bool
$c>= :: forall (b :: BinP). PosP b -> PosP b -> Bool
>= :: PosP b -> PosP b -> Bool
$cmax :: forall (b :: BinP). PosP b -> PosP b -> PosP b
max :: PosP b -> PosP b -> PosP b
$cmin :: forall (b :: BinP). PosP b -> PosP b -> PosP b
min :: PosP b -> PosP b -> PosP b
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 :: PosP' n b -> PosP' n b -> Ordering
compare (AtEnd  Wrd n
x) (AtEnd  Wrd n
y) = Wrd n -> Wrd n -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Wrd n
x Wrd n
y
    compare (Here   Wrd n
x) (Here   Wrd n
y) = Wrd n -> Wrd n -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Wrd n
x Wrd n
y
    compare (Here   Wrd n
_) (There1 PosP' ('S n) b
_) = Ordering
LT
    compare (There1 PosP' ('S n) b
_) (Here   Wrd n
_) = Ordering
GT
    compare (There1 PosP' ('S n) b
x) (There1 PosP' ('S n) b
y) = PosP' ('S n) b -> PosP' ('S n) b -> Ordering
forall a. Ord a => a -> a -> Ordering
compare PosP' ('S n) b
x PosP' ('S n) b
PosP' ('S n) b
y
    compare (There0 PosP' ('S n) b
x) (There0 PosP' ('S n) b
y) = PosP' ('S n) b -> PosP' ('S n) b -> Ordering
forall a. Ord a => a -> a -> Ordering
compare PosP' ('S n) b
x PosP' ('S n) b
PosP' ('S n) b
y

-------------------------------------------------------------------------------
-- some
-------------------------------------------------------------------------------

-- | @since 0.1.3
instance EqP PosP where
    eqp :: forall (a :: BinP) (b :: BinP). PosP a -> PosP b -> Bool
eqp PosP a
x PosP b
y = PosP a -> Natural
forall (b :: BinP). PosP b -> Natural
toNatural PosP a
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== PosP b -> Natural
forall (b :: BinP). PosP b -> Natural
toNatural PosP b
y

-- | @since 0.1.3
instance OrdP PosP where
    comparep :: forall (a :: BinP) (b :: BinP). PosP a -> PosP b -> Ordering
comparep PosP a
x PosP b
y = Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (PosP a -> Natural
forall (b :: BinP). PosP b -> Natural
toNatural PosP a
x) (PosP b -> Natural
forall (b :: BinP). PosP b -> Natural
toNatural PosP b
y)

-------------------------------------------------------------------------------
-- Instances
-------------------------------------------------------------------------------

instance Show (PosP b) where
    showsPrec :: Int -> PosP b -> ShowS
showsPrec Int
d = Int -> Natural -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d (Natural -> ShowS) -> (PosP b -> Natural) -> PosP b -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP b -> Natural
forall (b :: BinP). PosP b -> Natural
toNatural

instance N.SNatI n => Show (PosP' n b) where
    showsPrec :: Int -> PosP' n b -> ShowS
showsPrec Int
d = Int -> Natural -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d (Natural -> ShowS) -> (PosP' n b -> Natural) -> PosP' n b -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' n b -> Natural
forall (n :: Nat) (b :: BinP). SNatI n => PosP' n b -> Natural
toNatural'

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

-- | @since 0.1.3
instance N.SNatI n => GShow (PosP' n) where
    gshowsPrec :: forall (a :: BinP). Int -> PosP' n a -> ShowS
gshowsPrec = Int -> PosP' n a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

instance SBinPI b => Bounded (PosP b) where
    minBound :: PosP b
minBound = PosP' 'Z b -> PosP b
forall (b :: BinP). PosP' 'Z b -> PosP b
PosP PosP' 'Z b
forall a. Bounded a => a
minBound
    maxBound :: PosP b
maxBound = PosP' 'Z b -> PosP b
forall (b :: BinP). PosP' 'Z b -> PosP b
PosP PosP' 'Z b
forall a. Bounded a => a
maxBound

instance (N.SNatI n, SBinPI b) => Bounded (PosP' n b) where
    minBound :: PosP' n b
minBound = case SBinP b
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b of
        SBinP b
SBE -> Wrd n -> PosP' n 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd Wrd n
forall a. Bounded a => a
minBound
        SBinP b
SB0 -> PosP' ('S n) b1 -> PosP' n ('B0 b1)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B0 b)
There0 PosP' ('S n) b1
forall a. Bounded a => a
minBound
        SBinP b
SB1 -> Wrd n -> PosP' n ('B1 b1)
forall (n :: Nat) (b :: BinP). Wrd n -> PosP' n ('B1 b)
Here Wrd n
forall a. Bounded a => a
minBound

    maxBound :: PosP' n b
maxBound = case SBinP b
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b of
        SBinP b
SBE -> Wrd n -> PosP' n 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd Wrd n
forall a. Bounded a => a
maxBound
        SBinP b
SB0 -> PosP' ('S n) b1 -> PosP' n ('B0 b1)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B0 b)
There0 PosP' ('S n) b1
forall a. Bounded a => a
maxBound
        SBinP b
SB1 -> PosP' ('S n) b1 -> PosP' n ('B1 b1)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B1 b)
There1 PosP' ('S n) b1
forall a. Bounded a => a
maxBound

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

-- | @since 0.1.2
instance NFData (PosP' n b) where
    rnf :: PosP' n b -> ()
rnf (AtEnd Wrd n
w)  = Wrd n -> ()
forall a. NFData a => a -> ()
rnf Wrd n
w
    rnf (Here Wrd n
w)   = Wrd n -> ()
forall a. NFData a => a -> ()
rnf Wrd n
w
    rnf (There1 PosP' ('S n) b
p) = PosP' ('S n) b -> ()
forall a. NFData a => a -> ()
rnf PosP' ('S n) b
p
    rnf (There0 PosP' ('S n) b
p) = PosP' ('S n) b -> ()
forall a. NFData a => a -> ()
rnf PosP' ('S n) b
p

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

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

instance QC.CoArbitrary (PosP b) where
    coarbitrary :: forall b. PosP 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)
-> (PosP b -> Integer) -> PosP 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) -> (PosP b -> Natural) -> PosP b -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP b -> Natural
forall (b :: BinP). PosP b -> Natural
toNatural

instance SBinPI b => QC.Function (PosP b) where
    function :: forall b. (PosP b -> b) -> PosP b :-> b
function = (PosP b -> PosP' 'Z b)
-> (PosP' 'Z b -> PosP b) -> (PosP b -> b) -> PosP b :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\(PosP PosP' 'Z b
p) -> PosP' 'Z b
p) PosP' 'Z b -> PosP b
forall (b :: BinP). PosP' 'Z b -> PosP b
PosP

instance (N.SNatI n, SBinPI b) => QC.Arbitrary (PosP' n b) where
    arbitrary :: Gen (PosP' n b)
arbitrary = case SBinP b
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b of
        SBinP b
SBE -> (Wrd n -> PosP' n b) -> Gen (Wrd n) -> Gen (PosP' n b)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Wrd n -> PosP' n b
Wrd n -> PosP' n 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd Gen (Wrd n)
forall a. Arbitrary a => Gen a
QC.arbitrary
        SBinP b
SB0 -> (PosP' ('S n) b1 -> PosP' n b)
-> Gen (PosP' ('S n) b1) -> Gen (PosP' n b)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PosP' ('S n) b1 -> PosP' n b
PosP' ('S n) b1 -> PosP' n ('B0 b1)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B0 b)
There0 Gen (PosP' ('S n) b1)
forall a. Arbitrary a => Gen a
QC.arbitrary
        SBinP b
SB1 -> Gen (PosP' n b)
Gen (PosP' n ('B1 b1))
forall (bb :: BinP). SBinPI bb => Gen (PosP' n ('B1 bb))
sb1freq
      where
        sb1freq :: forall bb. SBinPI bb => QC.Gen (PosP' n ('B1 bb))
        sb1freq :: forall (bb :: BinP). SBinPI bb => Gen (PosP' n ('B1 bb))
sb1freq = [(Int, Gen (PosP' n ('B1 bb)))] -> Gen (PosP' n ('B1 bb))
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
QC.frequency
            [ (Int
fHere,  (Wrd n -> PosP' n ('B1 bb))
-> Gen (Wrd n) -> Gen (PosP' n ('B1 bb))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Wrd n -> PosP' n ('B1 bb)
forall (n :: Nat) (b :: BinP). Wrd n -> PosP' n ('B1 b)
Here Gen (Wrd n)
forall a. Arbitrary a => Gen a
QC.arbitrary)
            , (Int
fThere, (PosP' ('S n) bb -> PosP' n ('B1 bb))
-> Gen (PosP' ('S n) bb) -> Gen (PosP' n ('B1 bb))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PosP' ('S n) bb -> PosP' n ('B1 bb)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B1 b)
There1 Gen (PosP' ('S n) bb)
forall a. Arbitrary a => Gen a
QC.arbitrary)
            ]
          where
            fHere :: Int
fHere  = KNat Int n -> Int
forall a (n :: Nat). KNat a n -> a
getKNat (KNat Int n
forall a (n :: Nat). (Num a, SNatI n) => KNat a n
exp2 :: KNat Int n)
            fThere :: Int
fThere = Int
fHere Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Proxy @BinP bb -> Int
forall (b :: BinP) (proxy :: BinP -> *) a.
(SBinPI b, Num a) =>
proxy b -> a
BP.reflectToNum (Proxy @BinP bb
forall {k} (t :: k). Proxy @k t
Proxy :: Proxy bb)

instance N.SNatI n => QC.CoArbitrary (PosP' n b) where
    coarbitrary :: forall b. PosP' n 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)
-> (PosP' n b -> Integer) -> PosP' n 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)
-> (PosP' n b -> Natural) -> PosP' n b -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' n b -> Natural
forall (n :: Nat) (b :: BinP). SNatI n => PosP' n b -> Natural
toNatural'

instance (N.SNatI n, SBinPI b) => QC.Function (PosP' n b) where
    function :: forall b. (PosP' n b -> b) -> PosP' n b :-> b
function = case SBinP b
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b of
        SBinP b
SBE -> (PosP' n b -> Wrd n)
-> (Wrd n -> PosP' n b) -> (PosP' n b -> b) -> PosP' n b :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\(AtEnd Wrd n
t)  -> Wrd n
t) Wrd n -> PosP' n b
Wrd n -> PosP' n 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd
        SBinP b
SB0 -> (PosP' n b -> PosP' ('S n) b1)
-> (PosP' ('S n) b1 -> PosP' n b)
-> (PosP' n b -> b)
-> PosP' n b :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\(There0 PosP' ('S n) b
r) -> PosP' ('S n) b1
PosP' ('S n) b
r) PosP' ('S n) b1 -> PosP' n b
PosP' ('S n) b1 -> PosP' n ('B0 b1)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B0 b)
There0
        SBinP b
SB1 -> (PosP' n b -> Either (Wrd n) (PosP' ('S n) b1))
-> (Either (Wrd n) (PosP' ('S n) b1) -> PosP' n b)
-> (PosP' n b -> b)
-> PosP' n b :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap PosP' n b -> Either (Wrd n) (PosP' ('S n) b1)
PosP' n ('B1 b1) -> Either (Wrd n) (PosP' ('S n) b1)
forall (bb :: BinP).
PosP' n ('B1 bb) -> Either (Wrd n) (PosP' ('S n) bb)
sp ((Wrd n -> PosP' n b)
-> (PosP' ('S n) b1 -> PosP' n b)
-> Either (Wrd n) (PosP' ('S n) b1)
-> PosP' n b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Wrd n -> PosP' n b
Wrd n -> PosP' n ('B1 b1)
forall (n :: Nat) (b :: BinP). Wrd n -> PosP' n ('B1 b)
Here PosP' ('S n) b1 -> PosP' n b
PosP' ('S n) b1 -> PosP' n ('B1 b1)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B1 b)
There1) where
      where
        sp :: PosP' n ('B1 bb) -> Either (Wrd n) (PosP' ('S n) bb)
        sp :: forall (bb :: BinP).
PosP' n ('B1 bb) -> Either (Wrd n) (PosP' ('S n) bb)
sp (Here Wrd n
t)   = Wrd n -> Either (Wrd n) (PosP' ('S n) bb)
forall a b. a -> Either a b
Left Wrd n
t
        sp (There1 PosP' ('S n) b
p) = PosP' ('S n) bb -> Either (Wrd n) (PosP' ('S n) bb)
forall a b. b -> Either a b
Right PosP' ('S n) bb
PosP' ('S n) b
p

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

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

explicitShow' :: PosP' n b -> String
explicitShow' :: forall (n :: Nat) (b :: BinP). PosP' n b -> String
explicitShow' PosP' n b
b = Int -> PosP' n b -> ShowS
forall (n :: Nat) (b :: BinP). Int -> PosP' n b -> ShowS
explicitShowsPrec' Int
0 PosP' n b
b String
""

explicitShowsPrec :: Int -> PosP b ->ShowS
explicitShowsPrec :: forall (b :: BinP). Int -> PosP b -> ShowS
explicitShowsPrec Int
d (PosP PosP' 'Z b
p)
    = 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
"PosP "
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> PosP' 'Z b -> ShowS
forall (n :: Nat) (b :: BinP). Int -> PosP' n b -> ShowS
explicitShowsPrec' Int
11 PosP' 'Z b
p

explicitShowsPrec' :: Int -> PosP' n b ->ShowS
explicitShowsPrec' :: forall (n :: Nat) (b :: BinP). Int -> PosP' n b -> ShowS
explicitShowsPrec' Int
d (AtEnd Wrd n
v)
    = 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
"AtEnd "
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Wrd n -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Wrd n
v
explicitShowsPrec' Int
d (Here Wrd n
v)
    = 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
"Here "
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Wrd n -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Wrd n
v
explicitShowsPrec' Int
d (There1 PosP' ('S n) b
p)
    = 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
"There1 "
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> PosP' ('S n) b -> ShowS
forall (n :: Nat) (b :: BinP). Int -> PosP' n b -> ShowS
explicitShowsPrec' Int
11 PosP' ('S n) b
p
explicitShowsPrec' Int
d (There0 PosP' ('S n) b
p)
    = 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
"There0 "
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> PosP' ('S n) b -> ShowS
forall (n :: Nat) (b :: BinP). Int -> PosP' n b -> ShowS
explicitShowsPrec' Int
11 PosP' ('S n) b
p

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

-- | Convert 'PosP' to 'Natural'.
toNatural :: PosP b -> Natural
toNatural :: forall (b :: BinP). PosP b -> Natural
toNatural (PosP PosP' 'Z b
p) = PosP' 'Z b -> Natural
forall (n :: Nat) (b :: BinP). SNatI n => PosP' n b -> Natural
toNatural' PosP' 'Z b
p -- ' 0 1 p

-- | Convert 'PosP'' to 'Natural'.
toNatural' :: forall n b. N.SNatI n => PosP' n b -> Natural
toNatural' :: forall (n :: Nat) (b :: BinP). SNatI n => PosP' n b -> Natural
toNatural' = Natural -> Natural -> PosP' n b -> Natural
forall (n :: Nat) (b :: BinP).
Natural -> Natural -> PosP' n b -> Natural
toNatural'' Natural
0 (KNat Natural n -> Natural
forall a (n :: Nat). KNat a n -> a
getKNat (KNat Natural n
forall a (n :: Nat). (Num a, SNatI n) => KNat a n
exp2 :: KNat Natural n))

toNatural'' :: Natural -> Natural -> PosP' n b -> Natural
toNatural'' :: forall (n :: Nat) (b :: BinP).
Natural -> Natural -> PosP' n b -> Natural
toNatural'' !Natural
acc !Natural
_     (AtEnd Wrd n
v)  = Natural
acc Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Wrd n -> Natural
forall (n :: Nat). Wrd n -> Natural
W.toNatural Wrd n
v
toNatural'' !Natural
acc !Natural
_     (Here Wrd n
v)   = Natural
acc Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Wrd n -> Natural
forall (n :: Nat). Wrd n -> Natural
W.toNatural Wrd n
v
toNatural'' !Natural
acc !Natural
exp2n (There1 PosP' ('S n) b
v) = Natural -> Natural -> PosP' ('S n) b -> Natural
forall (n :: Nat) (b :: BinP).
Natural -> Natural -> PosP' n b -> Natural
toNatural'' (Natural
acc Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
exp2n) (Natural
2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
exp2n) PosP' ('S n) b
v
toNatural'' !Natural
acc !Natural
exp2n (There0 PosP' ('S n) b
v) = Natural -> Natural -> PosP' ('S n) b -> Natural
forall (n :: Nat) (b :: BinP).
Natural -> Natural -> PosP' n b -> Natural
toNatural'' Natural
acc           (Natural
2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
exp2n) PosP' ('S n) b
v

exp2 :: Num a => N.SNatI n => KNat a n
exp2 :: forall a (n :: Nat). (Num a, SNatI n) => KNat a n
exp2 = KNat a 'Z
-> (forall (m :: Nat). SNatI m => KNat a m -> KNat a ('S m))
-> KNat a n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (a -> KNat a 'Z
forall a (n :: Nat). a -> KNat a n
KNat a
1) (\(KNat a
n) -> a -> KNat a ('S m)
forall a (n :: Nat). a -> KNat a n
KNat (a
n a -> a -> a
forall a. Num a => a -> a -> a
* a
2))

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

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

-- | See 'top'.
pop :: (SBinPI a, B.Pred b ~ 'B.BP a, Succ a ~ b) => PosP a -> PosP b
pop :: forall (a :: BinP) (b :: BinP).
(SBinPI a, (Pred b :: Bin) ~ ('BP a :: Bin),
 (Succ a :: BinP) ~ (b :: BinP)) =>
PosP a -> PosP b
pop = PosP a -> PosP b
PosP a -> PosP (Succ a)
forall (b :: BinP). SBinPI b => PosP b -> PosP (Succ b)
weakenRight1

-------------------------------------------------------------------------------
-- Append and Split
-------------------------------------------------------------------------------

weakenRight1 :: SBinPI b => PosP b -> PosP (Succ b)
weakenRight1 :: forall (b :: BinP). SBinPI b => PosP b -> PosP (Succ b)
weakenRight1 (PosP PosP' 'Z b
n) = PosP' 'Z (Succ b) -> PosP (Succ b)
forall (b :: BinP). PosP' 'Z b -> PosP b
PosP (SBinP b -> PosP' 'Z b -> PosP' 'Z (Succ b)
forall (b :: BinP) (n :: Nat).
SBinP b -> PosP' n b -> PosP' n (Succ b)
weakenRight1' SBinP b
forall (b :: BinP). SBinPI b => SBinP b
sbinp PosP' 'Z b
n)

weakenRight1' :: forall b n. SBinP b -> PosP' n b -> PosP' n (Succ b)
weakenRight1' :: forall (b :: BinP) (n :: Nat).
SBinP b -> PosP' n b -> PosP' n (Succ b)
weakenRight1' SBinP b
SBE (AtEnd Wrd n
v)  = PosP' ('S n) 'BE -> PosP' n ('B0 'BE)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B0 b)
There0 (Wrd ('S n) -> PosP' ('S n) 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd (Wrd n -> Wrd ('S n)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W1 Wrd n
v))
weakenRight1' SBinP b
SB0 (There0 PosP' ('S n) b
p) = PosP' ('S n) b -> PosP' n ('B1 b)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B1 b)
There1 PosP' ('S n) b
p
weakenRight1' SBinP b
SB1 (There1 PosP' ('S n) b
p) = PosP' ('S n) (Succ b1) -> PosP' n ('B0 (Succ b1))
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B0 b)
There0 (SBinP b -> PosP' ('S n) b -> PosP' ('S n) (Succ b)
forall (b :: BinP) (n :: Nat).
SBinP b -> PosP' n b -> PosP' n (Succ b)
weakenRight1' SBinP b
forall (b :: BinP). SBinPI b => SBinP b
sbinp PosP' ('S n) b
p)
weakenRight1' s :: SBinP b
s@SBinP b
SB1 (Here Wrd n
v) = PosP' ('S n) (Succ b1) -> PosP' n ('B0 (Succ b1))
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B0 b)
There0 (PosP' ('S n) (Succ b1) -> PosP' n ('B0 (Succ b1)))
-> PosP' ('S n) (Succ b1) -> PosP' n ('B0 (Succ b1))
forall a b. (a -> b) -> a -> b
$ SBinP ('B1 b1) -> Wrd n -> PosP' ('S n) (Succ b1)
forall (bb :: BinP).
SBinPI bb =>
SBinP ('B1 bb) -> Wrd n -> PosP' ('S n) (Succ bb)
recur SBinP b
SBinP ('B1 b1)
s Wrd n
v where
    recur :: forall bb. SBinPI bb => SBinP ('B1 bb) -> Wrd n -> PosP' ('S n) (Succ bb)
    recur :: forall (bb :: BinP).
SBinPI bb =>
SBinP ('B1 bb) -> Wrd n -> PosP' ('S n) (Succ bb)
recur SBinP ('B1 bb)
_ Wrd n
v' = Proxy @BinP bb
-> (SBinPI (Succ bb) => PosP' ('S n) (Succ bb))
-> PosP' ('S n) (Succ bb)
forall (b :: BinP) r.
SBinPI b =>
Proxy @BinP b -> (SBinPI (Succ b) => r) -> r
withSucc (Proxy @BinP bb
forall {k} (t :: k). Proxy @k t
Proxy :: Proxy bb) ((SBinPI (Succ bb) => PosP' ('S n) (Succ bb))
 -> PosP' ('S n) (Succ bb))
-> (SBinPI (Succ bb) => PosP' ('S n) (Succ bb))
-> PosP' ('S n) (Succ bb)
forall a b. (a -> b) -> a -> b
$ Wrd ('S n) -> PosP' ('S n) (Succ bb)
forall (b :: BinP) (n :: Nat).
SBinPI b =>
Wrd ('S n) -> PosP' ('S n) b
weakenRight1V (Wrd n -> Wrd ('S n)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W1 Wrd n
v')

weakenRight1V :: forall b n. SBinPI b => Wrd ('S n) -> PosP' ('S n) b
weakenRight1V :: forall (b :: BinP) (n :: Nat).
SBinPI b =>
Wrd ('S n) -> PosP' ('S n) b
weakenRight1V Wrd ('S n)
v = case SBinP b
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b of
    SBinP b
SBE -> Wrd ('S n) -> PosP' ('S n) 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd Wrd ('S n)
v
    SBinP b
SB0 -> PosP' ('S ('S n)) b1 -> PosP' ('S n) ('B0 b1)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B0 b)
There0 (Wrd ('S ('S n)) -> PosP' ('S ('S n)) b1
forall (b :: BinP) (n :: Nat).
SBinPI b =>
Wrd ('S n) -> PosP' ('S n) b
weakenRight1V (Wrd ('S n) -> Wrd ('S ('S n))
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W0 Wrd ('S n)
v))
    SBinP b
SB1 -> Wrd ('S n) -> PosP' ('S n) ('B1 b1)
forall (n :: Nat) (b :: BinP). Wrd n -> PosP' n ('B1 b)
Here Wrd ('S n)
v

-------------------------------------------------------------------------------
-- Universe
-------------------------------------------------------------------------------

-- |
--
-- >>> universe :: [PosP BinP9]
-- [0,1,2,3,4,5,6,7,8]
--
universe :: forall b. SBinPI b => [PosP b]
universe :: forall (b :: BinP). SBinPI b => [PosP b]
universe = (PosP' 'Z b -> PosP b) -> [PosP' 'Z b] -> [PosP b]
forall a b. (a -> b) -> [a] -> [b]
map PosP' 'Z b -> PosP b
forall (b :: BinP). PosP' 'Z b -> PosP b
PosP [PosP' 'Z b]
forall (b :: BinP) (n :: Nat). (SNatI n, SBinPI b) => [PosP' n b]
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' :: forall (b :: BinP) (n :: Nat). (SNatI n, SBinPI b) => [PosP' n b]
universe' = case SBinP b
forall (b :: BinP). SBinPI b => SBinP b
B.sbinp :: SBinP b of
    SBinP b
B.SBE -> (Wrd n -> PosP' n b) -> [Wrd n] -> [PosP' n b]
forall a b. (a -> b) -> [a] -> [b]
map Wrd n -> PosP' n b
Wrd n -> PosP' n 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd [Wrd n]
forall (n :: Nat). SNatI n => [Wrd n]
W.universe
    SBinP b
B.SB0 -> (PosP' ('S n) b1 -> PosP' n b) -> [PosP' ('S n) b1] -> [PosP' n b]
forall a b. (a -> b) -> [a] -> [b]
map PosP' ('S n) b1 -> PosP' n b
PosP' ('S n) b1 -> PosP' n ('B0 b1)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B0 b)
There0 [PosP' ('S n) b1]
forall (b :: BinP) (n :: Nat). (SNatI n, SBinPI b) => [PosP' n b]
universe'
    SBinP b
B.SB1 -> (Wrd n -> PosP' n b) -> [Wrd n] -> [PosP' n b]
forall a b. (a -> b) -> [a] -> [b]
map Wrd n -> PosP' n b
Wrd n -> PosP' n ('B1 b1)
forall (n :: Nat) (b :: BinP). Wrd n -> PosP' n ('B1 b)
Here [Wrd n]
forall (n :: Nat). SNatI n => [Wrd n]
W.universe [PosP' n b] -> [PosP' n b] -> [PosP' n b]
forall a. [a] -> [a] -> [a]
++ (PosP' ('S n) b1 -> PosP' n b) -> [PosP' ('S n) b1] -> [PosP' n b]
forall a b. (a -> b) -> [a] -> [b]
map PosP' ('S n) b1 -> PosP' n b
PosP' ('S n) b1 -> PosP' n ('B1 b1)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B1 b)
There1 [PosP' ('S n) b1]
forall (b :: BinP) (n :: Nat). (SNatI n, SBinPI b) => [PosP' n b]
universe'

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

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

-------------------------------------------------------------------------------
-- Helpers
-------------------------------------------------------------------------------

newtype KNat a (n :: Nat) = KNat { forall a (n :: Nat). KNat a n -> a
getKNat :: a }