{-# 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,
explicitShow,
explicitShowsPrec,
toNatural,
absurd,
boring,
weakenRight1,
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
data Pos (b :: Bin) where
Pos :: PosP b -> Pos ('BP b)
deriving (Typeable)
deriving instance Eq (Pos b)
deriving instance Ord (Pos b)
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
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)
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
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
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
instance NFData (Pos b) where
rnf :: Pos b -> ()
rnf (Pos PosP b
p) = forall a. NFData a => a -> ()
rnf PosP b
p
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
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
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
absurd :: Pos 'BZ -> b
absurd :: forall b. Pos 'BZ -> b
absurd Pos 'BZ
x = case Pos 'BZ
x of {}
boring :: Pos ('BP 'BE)
boring :: Pos ('BP 'BE)
boring = forall a. Bounded a => a
minBound
top :: SBinPI b => Pos ('BP b)
top :: forall (b :: BinP). SBinPI b => Pos ('BP b)
top = forall a. Bounded a => a
minBound
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
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)
instance b ~ 'BP 'BE => Boring.Boring (Pos b) where
boring :: Pos b
boring = Pos ('BP 'BE)
boring
instance b ~ 'BZ => Boring.Absurd (Pos b) where
absurd :: forall b. Pos b -> b
absurd = forall b. Pos 'BZ -> b
absurd
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