{-# 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 { 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
/= :: 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
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
min :: PosP b -> PosP b -> PosP b
$cmin :: forall (b :: BinP). PosP b -> PosP b -> PosP b
max :: PosP b -> PosP b -> PosP b
$cmax :: forall (b :: BinP). PosP b -> PosP b -> PosP b
>= :: 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
$c< :: forall (b :: BinP). PosP b -> PosP b -> Bool
compare :: PosP b -> PosP b -> Ordering
$ccompare :: forall (b :: BinP). PosP b -> PosP b -> Ordering
$cp1Ord :: forall (b :: BinP). Eq (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

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

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) b -> PosP' n ('B0 b)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B0 b)
There0 PosP' ('S n) b
forall a. Bounded a => a
minBound
        SBinP b
SB1 -> Wrd n -> PosP' n ('B1 b)
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) b -> PosP' n ('B0 b)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B0 b)
There0 PosP' ('S n) b
forall a. Bounded a => a
maxBound
        SBinP b
SB1 -> 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
forall a. Bounded a => a
maxBound

-------------------------------------------------------------------------------
-- 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 (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 :: PosP 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)
-> (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 :: (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 'BE) -> Gen (Wrd n) -> Gen (PosP' n 'BE)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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) b -> PosP' n ('B0 b))
-> Gen (PosP' ('S n) b) -> Gen (PosP' n ('B0 b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PosP' ('S n) b -> PosP' n ('B0 b)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B0 b)
There0 Gen (PosP' ('S n) b)
forall a. Arbitrary a => Gen a
QC.arbitrary
        SBinP b
SB1 -> Gen (PosP' n b)
forall (bb :: BinP). SBinPI bb => Gen (PosP' n ('B1 bb))
sb1freq
      where
        sb1freq :: forall bb. SBinPI bb => QC.Gen (PosP' n ('B1 bb))
        sb1freq :: Gen (PosP' n ('B1 bb))
sb1freq = [(Int, Gen (PosP' n ('B1 bb)))] -> Gen (PosP' n ('B1 bb))
forall a. [(Int, Gen a)] -> Gen a
QC.frequency
            [ (Int
fHere,  (Wrd n -> PosP' n ('B1 bb))
-> Gen (Wrd n) -> Gen (PosP' n ('B1 bb))
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 (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 :: PosP' n 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)
-> (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 :: (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 'BE -> Wrd n)
-> (Wrd n -> PosP' n 'BE)
-> (PosP' n 'BE -> b)
-> PosP' n 'BE :-> 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 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd
        SBinP b
SB0 -> (PosP' n ('B0 b) -> PosP' ('S n) b)
-> (PosP' ('S n) b -> PosP' n ('B0 b))
-> (PosP' n ('B0 b) -> b)
-> PosP' n ('B0 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) b
PosP' ('S n) b
r) PosP' ('S n) b -> PosP' n ('B0 b)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B0 b)
There0
        SBinP b
SB1 -> (PosP' n ('B1 b) -> Either (Wrd n) (PosP' ('S n) b))
-> (Either (Wrd n) (PosP' ('S n) b) -> PosP' n ('B1 b))
-> (PosP' n ('B1 b) -> b)
-> PosP' n ('B1 b) :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap PosP' n ('B1 b) -> Either (Wrd n) (PosP' ('S n) b)
forall (bb :: BinP).
PosP' n ('B1 bb) -> Either (Wrd n) (PosP' ('S n) bb)
sp ((Wrd n -> PosP' n ('B1 b))
-> (PosP' ('S n) b -> PosP' n ('B1 b))
-> Either (Wrd n) (PosP' ('S n) b)
-> PosP' n ('B1 b)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Wrd n -> PosP' n ('B1 b)
forall (n :: Nat) (b :: BinP). Wrd n -> PosP' n ('B1 b)
Here PosP' ('S n) b -> PosP' n ('B1 b)
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 :: 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) b -> Either (Wrd n) (PosP' ('S n) b)
forall a b. b -> Either a b
Right PosP' ('S n) b
p

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

explicitShow :: PosP b -> String
explicitShow :: 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' :: 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 :: 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' :: 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 :: 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

-- | Convert 'PosP'' to 'Natural'.
toNatural' :: forall n b. N.SNatI n => PosP' n b -> Natural
toNatural' :: PosP' n b -> Natural
toNatural' (AtEnd Wrd n
v)  = Wrd n -> Natural
forall (n :: Nat). Wrd n -> Natural
W.toNatural Wrd n
v
toNatural' (Here Wrd n
v)   = Wrd n -> Natural
forall (n :: Nat). Wrd n -> Natural
W.toNatural Wrd n
v
toNatural' (There1 PosP' ('S n) b
p) = 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) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ PosP' ('S n) b -> Natural
forall (n :: Nat) (b :: BinP). SNatI n => PosP' n b -> Natural
toNatural' PosP' ('S n) b
p
toNatural' (There0 PosP' ('S n) b
p) = PosP' ('S n) b -> Natural
forall (n :: Nat) (b :: BinP). SNatI n => PosP' n b -> Natural
toNatural' PosP' ('S n) b
p

exp2 :: Num a => N.SNatI n => KNat a n
exp2 :: 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
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 :: 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 :: PosP a -> PosP b
pop = PosP a -> PosP b
forall (b :: BinP). SBinPI b => PosP b -> PosP (Succ b)
weakenRight1

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

weakenRight1 :: SBinPI b => PosP b -> PosP (Succ b)
weakenRight1 :: 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' :: 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 (n :: Nat). Wrd n -> Wrd ('S n)
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 b) -> PosP' n ('B0 (Succ b))
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 b) -> PosP' n ('B0 (Succ b))
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B0 b)
There0 (PosP' ('S n) (Succ b) -> PosP' n ('B0 (Succ b)))
-> PosP' ('S n) (Succ b) -> PosP' n ('B0 (Succ b))
forall a b. (a -> b) -> a -> b
$ SBinP ('B1 b) -> Wrd n -> PosP' ('S n) (Succ b)
forall (bb :: BinP).
SBinPI bb =>
SBinP ('B1 bb) -> Wrd n -> PosP' ('S n) (Succ bb)
recur SBinP b
SBinP ('B1 b)
s Wrd n
v where
    recur :: forall bb. SBinPI bb => SBinP ('B1 bb) -> Wrd n -> PosP' ('S n) (Succ bb)
    recur :: 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 (n :: Nat). Wrd n -> Wrd ('S n)
W1 Wrd n
v')

weakenRight1V :: forall b n. SBinPI b => Wrd ('S n) -> PosP' ('S n) b
weakenRight1V :: 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)) b -> PosP' ('S n) ('B0 b)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B0 b)
There0 (Wrd ('S ('S n)) -> PosP' ('S ('S n)) b
forall (b :: BinP) (n :: Nat).
SBinPI b =>
Wrd ('S n) -> PosP' ('S n) b
weakenRight1V (Wrd ('S n) -> Wrd ('S ('S n))
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 Wrd ('S n)
v))
    SBinP b
SB1 -> Wrd ('S n) -> PosP' ('S n) ('B1 b)
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 :: [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' :: [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 'BE) -> [Wrd n] -> [PosP' n 'BE]
forall a b. (a -> b) -> [a] -> [b]
map 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) b -> PosP' n ('B0 b))
-> [PosP' ('S n) b] -> [PosP' n ('B0 b)]
forall a b. (a -> b) -> [a] -> [b]
map PosP' ('S n) b -> PosP' n ('B0 b)
forall (n :: Nat) (b :: BinP). PosP' ('S n) b -> PosP' n ('B0 b)
There0 [PosP' ('S n) b]
forall (b :: BinP) (n :: Nat). (SNatI n, SBinPI b) => [PosP' n b]
universe'
    SBinP b
B.SB1 -> (Wrd n -> PosP' n ('B1 b)) -> [Wrd n] -> [PosP' n ('B1 b)]
forall a b. (a -> b) -> [a] -> [b]
map Wrd n -> PosP' n ('B1 b)
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 ('B1 b)] -> [PosP' n ('B1 b)] -> [PosP' n ('B1 b)]
forall a. [a] -> [a] -> [a]
++ (PosP' ('S n) b -> PosP' n ('B1 b))
-> [PosP' ('S n) b] -> [PosP' n ('B1 b)]
forall a b. (a -> b) -> [a] -> [b]
map 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]
forall (b :: BinP) (n :: Nat). (SNatI n, SBinPI b) => [PosP' n b]
universe'

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

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