{-# LANGUAGE CPP #-}
{-# 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,
explicitShow,
explicitShow',
explicitShowsPrec,
explicitShowsPrec',
toNatural, toNatural',
boring,
weakenRight1, weakenRight1',
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.GADT.Show (GShow (..))
import Data.Nat (Nat (..))
import Data.Proxy (Proxy (..))
import Data.Typeable (Typeable)
import Data.Wrd (Wrd (..))
import Numeric.Natural (Natural)
#if MIN_VERSION_some(1,0,5)
import Data.EqP (EqP (..))
import Data.OrdP (OrdP (..))
#endif
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
newtype PosP (b :: BinP) = PosP { forall (b :: BinP). PosP b -> PosP' 'Z b
unPosP :: PosP' 'Z b }
deriving (PosP b -> PosP b -> Bool
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, 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
Ord, Typeable)
data PosP' (n :: Nat) (b :: BinP) where
AtEnd :: Wrd n -> PosP' n 'BE
Here :: Wrd n -> PosP' n ('B1 b)
There1 :: PosP' ('S n) b -> PosP' n ('B1 b)
There0 :: PosP' ('S n) b -> PosP' n ('B0 b)
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) = forall a. Ord a => a -> a -> Ordering
compare Wrd n
x Wrd n
y
compare (Here Wrd n
x) (Here Wrd n
y) = 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) = forall a. Ord a => a -> a -> Ordering
compare PosP' ('S n) b
x PosP' ('S n) b
y
compare (There0 PosP' ('S n) b
x) (There0 PosP' ('S n) b
y) = forall a. Ord a => a -> a -> Ordering
compare PosP' ('S n) b
x PosP' ('S n) b
y
#if MIN_VERSION_some(1,0,5)
instance EqP PosP where
eqp :: forall (a :: BinP) (b :: BinP). PosP a -> PosP b -> Bool
eqp PosP a
x PosP b
y = forall (b :: BinP). PosP b -> Natural
toNatural PosP a
x forall a. Eq a => a -> a -> Bool
== forall (b :: BinP). PosP b -> Natural
toNatural PosP b
y
instance OrdP PosP where
comparep :: forall (a :: BinP) (b :: BinP). PosP a -> PosP b -> Ordering
comparep PosP a
x PosP b
y = forall a. Ord a => a -> a -> Ordering
compare (forall (b :: BinP). PosP b -> Natural
toNatural PosP a
x) (forall (b :: BinP). PosP b -> Natural
toNatural PosP b
y)
#endif
instance Show (PosP b) where
showsPrec :: Int -> PosP 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 :: BinP). PosP b -> Natural
toNatural
instance N.SNatI n => Show (PosP' n b) where
showsPrec :: Int -> PosP' n 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 (n :: Nat) (b :: BinP). SNatI n => PosP' n b -> Natural
toNatural'
instance GShow PosP where
gshowsPrec :: forall (b :: BinP). Int -> PosP b -> ShowS
gshowsPrec = forall a. Show a => Int -> a -> ShowS
showsPrec
instance N.SNatI n => GShow (PosP' n) where
gshowsPrec :: forall (a :: BinP). Int -> PosP' n a -> ShowS
gshowsPrec = forall a. Show a => Int -> a -> ShowS
showsPrec
instance SBinPI b => Bounded (PosP b) where
minBound :: PosP b
minBound = forall (b :: BinP). PosP' 'Z b -> PosP b
PosP forall a. Bounded a => a
minBound
maxBound :: PosP b
maxBound = forall (b :: BinP). PosP' 'Z b -> PosP b
PosP forall a. Bounded a => a
maxBound
instance (N.SNatI n, SBinPI b) => Bounded (PosP' n b) where
minBound :: PosP' n b
minBound = case forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b of
SBinP b
SBE -> forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd forall a. Bounded a => a
minBound
SBinP b
SB0 -> forall (n :: Nat) (n :: BinP). PosP' ('S n) n -> PosP' n ('B0 n)
There0 forall a. Bounded a => a
minBound
SBinP b
SB1 -> forall (n :: Nat) (n :: BinP). Wrd n -> PosP' n ('B1 n)
Here forall a. Bounded a => a
minBound
maxBound :: PosP' n b
maxBound = case forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b of
SBinP b
SBE -> forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd forall a. Bounded a => a
maxBound
SBinP b
SB0 -> forall (n :: Nat) (n :: BinP). PosP' ('S n) n -> PosP' n ('B0 n)
There0 forall a. Bounded a => a
maxBound
SBinP b
SB1 -> forall (n :: Nat) (n :: BinP). PosP' ('S n) n -> PosP' n ('B1 n)
There1 forall a. Bounded a => a
maxBound
instance NFData (PosP b) where
rnf :: PosP b -> ()
rnf (PosP PosP' 'Z b
p) = forall a. NFData a => a -> ()
rnf PosP' 'Z b
p
instance NFData (PosP' n b) where
rnf :: PosP' n b -> ()
rnf (AtEnd Wrd n
w) = forall a. NFData a => a -> ()
rnf Wrd n
w
rnf (Here Wrd n
w) = forall a. NFData a => a -> ()
rnf Wrd n
w
rnf (There1 PosP' ('S n) b
p) = forall a. NFData a => a -> ()
rnf PosP' ('S n) b
p
rnf (There0 PosP' ('S n) b
p) = forall a. NFData a => a -> ()
rnf PosP' ('S n) b
p
instance SBinPI b => QC.Arbitrary (PosP b) where
arbitrary :: Gen (PosP b)
arbitrary = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (b :: BinP). PosP' 'Z b -> PosP b
PosP forall a. Arbitrary a => Gen a
QC.arbitrary
instance QC.CoArbitrary (PosP b) where
coarbitrary :: forall b. PosP 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 :: BinP). PosP b -> Natural
toNatural
instance SBinPI b => QC.Function (PosP b) where
function :: forall b. (PosP b -> b) -> PosP b :-> b
function = 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) 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 forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b of
SBinP b
SBE -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd forall a. Arbitrary a => Gen a
QC.arbitrary
SBinP b
SB0 -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat) (n :: BinP). PosP' ('S n) n -> PosP' n ('B0 n)
There0 forall a. Arbitrary a => Gen a
QC.arbitrary
SBinP b
SB1 -> 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 = forall a. [(Int, Gen a)] -> Gen a
QC.frequency
[ (Int
fHere, forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat) (n :: BinP). Wrd n -> PosP' n ('B1 n)
Here forall a. Arbitrary a => Gen a
QC.arbitrary)
, (Int
fThere, forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat) (n :: BinP). PosP' ('S n) n -> PosP' n ('B1 n)
There1 forall a. Arbitrary a => Gen a
QC.arbitrary)
]
where
fHere :: Int
fHere = forall a (n :: Nat). KNat a n -> a
getKNat (forall a (n :: Nat). (Num a, SNatI n) => KNat a n
exp2 :: KNat Int n)
fThere :: Int
fThere = Int
fHere forall a. Num a => a -> a -> a
* Int
2 forall a. Num a => a -> a -> a
* forall (b :: BinP) (proxy :: BinP -> *) a.
(SBinPI b, Num a) =>
proxy b -> a
BP.reflectToNum (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 = 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 (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 forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b of
SBinP b
SBE -> forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\(AtEnd Wrd n
t) -> Wrd n
t) forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd
SBinP b
SB0 -> 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
r) forall (n :: Nat) (n :: BinP). PosP' ('S n) n -> PosP' n ('B0 n)
There0
SBinP b
SB1 -> forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap forall (bb :: BinP).
PosP' n ('B1 bb) -> Either (Wrd n) (PosP' ('S n) bb)
sp (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall (n :: Nat) (n :: BinP). Wrd n -> PosP' n ('B1 n)
Here forall (n :: Nat) (n :: BinP). PosP' ('S n) n -> PosP' n ('B1 n)
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) = forall a b. a -> Either a b
Left Wrd n
t
sp (There1 PosP' ('S n) b
p) = forall a b. b -> Either a b
Right PosP' ('S n) b
p
explicitShow :: PosP b -> String
explicitShow :: forall (b :: BinP). PosP b -> String
explicitShow PosP b
b = 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 = 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 forall a. Ord a => a -> a -> Bool
> Int
10)
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"PosP "
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. Ord a => a -> a -> Bool
> Int
10)
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"AtEnd "
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. Ord a => a -> a -> Bool
> Int
10)
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Here "
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. Ord a => a -> a -> Bool
> Int
10)
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"There1 "
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. Ord a => a -> a -> Bool
> Int
10)
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"There0 "
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) (b :: BinP). Int -> PosP' n b -> ShowS
explicitShowsPrec' Int
11 PosP' ('S n) b
p
toNatural :: PosP b -> Natural
toNatural :: forall (b :: BinP). PosP b -> Natural
toNatural (PosP PosP' 'Z b
p) = forall (n :: Nat) (b :: BinP). SNatI n => PosP' n b -> Natural
toNatural' PosP' 'Z b
p
toNatural' :: forall n b. N.SNatI n => PosP' n b -> Natural
toNatural' :: forall (n :: Nat) (b :: BinP). SNatI n => PosP' n b -> Natural
toNatural' = forall (n :: Nat) (b :: BinP).
Natural -> Natural -> PosP' n b -> Natural
toNatural'' Natural
0 (forall a (n :: Nat). KNat a n -> a
getKNat (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 forall a. Num a => a -> a -> a
+ forall (n :: Nat). Wrd n -> Natural
W.toNatural Wrd n
v
toNatural'' !Natural
acc !Natural
_ (Here Wrd n
v) = Natural
acc forall a. Num a => a -> a -> a
+ forall (n :: Nat). Wrd n -> Natural
W.toNatural Wrd n
v
toNatural'' !Natural
acc !Natural
exp2n (There1 PosP' ('S n) b
v) = forall (n :: Nat) (b :: BinP).
Natural -> Natural -> PosP' n b -> Natural
toNatural'' (Natural
acc forall a. Num a => a -> a -> a
+ Natural
exp2n) (Natural
2 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) = forall (n :: Nat) (b :: BinP).
Natural -> Natural -> PosP' n b -> Natural
toNatural'' Natural
acc (Natural
2 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 = forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (forall a (n :: Nat). a -> KNat a n
KNat a
1) (\(KNat a
n) -> forall a (n :: Nat). a -> KNat a n
KNat (a
n forall a. Num a => a -> a -> a
* a
2))
boring :: PosP 'BE
boring :: PosP 'BE
boring = forall a. Bounded a => a
minBound
top :: SBinPI b => PosP b
top :: forall (b :: BinP). SBinPI b => PosP b
top = forall a. Bounded a => a
minBound
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 = forall (b :: BinP). SBinPI b => PosP b -> PosP (Succ b)
weakenRight1
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) = forall (b :: BinP). PosP' 'Z b -> PosP b
PosP (forall (b :: BinP) (n :: Nat).
SBinP b -> PosP' n b -> PosP' n (Succ b)
weakenRight1' 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) = forall (n :: Nat) (n :: BinP). PosP' ('S n) n -> PosP' n ('B0 n)
There0 (forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd (forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 Wrd n
v))
weakenRight1' SBinP b
SB0 (There0 PosP' ('S n) b
p) = forall (n :: Nat) (n :: BinP). PosP' ('S n) n -> PosP' n ('B1 n)
There1 PosP' ('S n) b
p
weakenRight1' SBinP b
SB1 (There1 PosP' ('S n) b
p) = forall (n :: Nat) (n :: BinP). PosP' ('S n) n -> PosP' n ('B0 n)
There0 (forall (b :: BinP) (n :: Nat).
SBinP b -> PosP' n b -> PosP' n (Succ b)
weakenRight1' 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) = forall (n :: Nat) (n :: BinP). PosP' ('S n) n -> PosP' n ('B0 n)
There0 forall a b. (a -> b) -> a -> b
$ forall (bb :: BinP).
SBinPI bb =>
SBinP ('B1 bb) -> Wrd n -> PosP' ('S n) (Succ bb)
recur SBinP b
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' = forall (b :: BinP) r.
SBinPI b =>
Proxy @BinP b -> (SBinPI (Succ b) => r) -> r
withSucc (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy bb) forall a b. (a -> b) -> a -> b
$ forall (b :: BinP) (n :: Nat).
SBinPI b =>
Wrd ('S n) -> PosP' ('S n) b
weakenRight1V (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 :: forall (b :: BinP) (n :: Nat).
SBinPI b =>
Wrd ('S n) -> PosP' ('S n) b
weakenRight1V Wrd ('S n)
v = case forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b of
SBinP b
SBE -> forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd Wrd ('S n)
v
SBinP b
SB0 -> forall (n :: Nat) (n :: BinP). PosP' ('S n) n -> PosP' n ('B0 n)
There0 (forall (b :: BinP) (n :: Nat).
SBinPI b =>
Wrd ('S n) -> PosP' ('S n) b
weakenRight1V (forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 Wrd ('S n)
v))
SBinP b
SB1 -> forall (n :: Nat) (n :: BinP). Wrd n -> PosP' n ('B1 n)
Here Wrd ('S n)
v
universe :: forall b. SBinPI b => [PosP b]
universe :: forall (b :: BinP). SBinPI b => [PosP b]
universe = forall a b. (a -> b) -> [a] -> [b]
map forall (b :: BinP). PosP' 'Z b -> PosP b
PosP forall (b :: BinP) (n :: Nat). (SNatI n, SBinPI b) => [PosP' n b]
universe'
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 forall (b :: BinP). SBinPI b => SBinP b
B.sbinp :: SBinP b of
SBinP b
B.SBE -> forall a b. (a -> b) -> [a] -> [b]
map forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd forall (n :: Nat). SNatI n => [Wrd n]
W.universe
SBinP b
B.SB0 -> forall a b. (a -> b) -> [a] -> [b]
map forall (n :: Nat) (n :: BinP). PosP' ('S n) n -> PosP' n ('B0 n)
There0 forall (b :: BinP) (n :: Nat). (SNatI n, SBinPI b) => [PosP' n b]
universe'
SBinP b
B.SB1 -> forall a b. (a -> b) -> [a] -> [b]
map forall (n :: Nat) (n :: BinP). Wrd n -> PosP' n ('B1 n)
Here forall (n :: Nat). SNatI n => [Wrd n]
W.universe forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall (n :: Nat) (n :: BinP). PosP' ('S n) n -> PosP' n ('B1 n)
There1 forall (b :: BinP) (n :: Nat). (SNatI n, SBinPI b) => [PosP' n b]
universe'
instance b ~ 'BE => Boring.Boring (PosP b) where
boring :: PosP b
boring = PosP 'BE
boring
newtype KNat a (n :: Nat) = KNat { forall a (n :: Nat). KNat a n -> a
getKNat :: a }