{-# OPTIONS_GHC -Wno-orphans #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Morley.Util.Peano
(
Peano
, Nat (Z, S)
, ToPeano
, FromPeano
, SingNat (SZ, SS)
, Decrement
, type (>)
, peanoSing
, type (>=)
, peanoSingDecrement
, Length
, At
, Drop
, Take
, IsLongerThan
, LongerThan
, RequireLongerThan
, IsLongerOrSameLength
, LongerOrSameLength
, RequireLongerOrSameLength
, requireLongerThan
, requireLongerOrSameLength
, isGreaterThan
, isGreaterEqualThan
) where
import Data.Constraint (Dict(..))
import Data.Singletons (Sing, SingI(..))
import Data.Vinyl (Rec(..))
import Data.Vinyl.TypeLevel (Nat(..), RLength)
import GHC.TypeLits (ErrorMessage(..), TypeError)
import GHC.TypeNats (type (+), type (-))
import qualified GHC.TypeNats as GHC
import Unsafe.Coerce (unsafeCoerce)
import Morley.Util.Type
type Peano = Nat
type family ToPeano (n :: GHC.Nat) :: Peano where
ToPeano 0 = 'Z
ToPeano a = 'S (ToPeano (a - 1))
type family FromPeano (n :: Peano) :: GHC.Nat where
FromPeano 'Z = 0
FromPeano ('S a) = 1 + FromPeano a
peanoSing :: forall (n :: GHC.Nat). SingI (ToPeano n) => SingNat (ToPeano n)
peanoSing :: SingNat (ToPeano n)
peanoSing = SingI (ToPeano n) => Sing (ToPeano n)
forall k (a :: k). SingI a => Sing a
sing @(ToPeano n)
data SingNat (n :: Nat) where
SZ :: SingNat 'Z
SS :: !(SingNat n) -> SingNat ('S n)
deriving stock instance Show (SingNat (n :: Nat))
deriving stock instance Eq (SingNat (n :: Nat))
instance NFData (SingNat (n :: Nat)) where
rnf :: SingNat n -> ()
rnf SingNat n
SZ = ()
rnf (SS SingNat n
n) = SingNat n -> ()
forall a. NFData a => a -> ()
rnf SingNat n
n
type instance Sing = SingNat
instance SingI 'Z where
sing :: Sing 'Z
sing = Sing 'Z
SingNat 'Z
SZ
instance SingI n => SingI ('S n) where
sing :: Sing ('S n)
sing = SingNat n -> SingNat ('S n)
forall (n :: Peano). SingNat n -> SingNat ('S n)
SS (SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @n)
type family Decrement (a :: Peano) :: Peano where
Decrement 'Z = TypeError ('Text "Expected n > 0")
Decrement ('S n) = n
peanoSingDecrement :: Sing n -> Maybe (Sing (Decrement n))
peanoSingDecrement :: Sing n -> Maybe (Sing (Decrement n))
peanoSingDecrement = \case
Sing n
SZ -> Maybe (Sing (Decrement n))
forall a. Maybe a
Nothing
SS n -> SingNat n -> Maybe (SingNat n)
forall (f :: * -> *) a. Applicative f => a -> f a
pure SingNat n
n
type family (>) (x :: Peano) (y :: Peano) :: Bool where
'Z > _ = 'False
'S _ > 'Z = 'True
'S x > 'S y = x > y
type family (>=) (x :: Peano) (y :: Peano) :: Bool where
_ >= 'Z = 'True
'Z >= _ = 'False
('S x) >= ('S y) = x >= y
type family Length l :: Peano where
Length l = RLength l
type family At (n :: Peano) s where
At 'Z (x ': _) = x
At ('S n) (_ ': xs) = At n xs
At a '[] =
TypeError
('Text "You tried to access a non-existing element of the stack, n = " ':<>:
'ShowType (FromPeano a))
type family Drop (n :: Peano) (s :: [k]) :: [k] where
Drop 'Z s = s
Drop ('S _) '[] = '[]
Drop ('S n) (_ ': s) = Drop n s
type family Take (n :: Peano) (s :: [k]) :: [k] where
Take 'Z _ = '[]
Take _ '[] = '[]
Take ('S n) (a ': s) = a ': Take n s
type family IsLongerThan (l :: [k]) (a :: Peano) :: Bool where
IsLongerThan (_ ': _) 'Z = 'True
IsLongerThan (_ ': xs) ('S a) = IsLongerThan xs a
IsLongerThan '[] _ = 'False
type LongerThan l a = IsLongerThan l a ~ 'True
type family IsLongerOrSameLength (l :: [k]) (a :: Peano) :: Bool where
IsLongerOrSameLength _ 'Z = 'True
IsLongerOrSameLength (_ ': xs) ('S a) = IsLongerOrSameLength xs a
IsLongerOrSameLength '[] ('S _) = 'False
type LongerOrSameLength l a = IsLongerOrSameLength l a ~ 'True
type family OfLengthWithTail (acc :: GHC.Nat) (l :: [k]) :: GHC.Nat where
OfLengthWithTail a '[] = a
OfLengthWithTail a (_ ': xs) = OfLengthWithTail (a + 1) xs
type LengthWithTail l = OfLengthWithTail 0 l
type family RequireLongerThan' (l :: [k]) (a :: Nat) :: Constraint where
RequireLongerThan' l a =
If (IsLongerThan l a)
(() :: Constraint)
(TypeError
('Text "Stack element #" ':<>: 'ShowType (FromPeano a) ':<>:
'Text " is not accessible" ':$$:
'Text "Current stack has size of only " ':<>:
'ShowType (LengthWithTail l) ':<>:
'Text ":" ':$$: 'ShowType l
))
class (RequireLongerThan' l a, LongerThan l a) =>
RequireLongerThan (l :: [k]) (a :: Peano)
instance (RequireLongerThan' l a, LongerThan l a) =>
RequireLongerThan l a
type family RequireLongerOrSameLength' (l :: [k]) (a :: Peano) :: Constraint where
RequireLongerOrSameLength' l a =
If (IsLongerOrSameLength l a)
(() :: Constraint)
(TypeError
('Text "Expected stack with length >= " ':<>: 'ShowType (FromPeano a) ':$$:
'Text "Current stack has size of only " ':<>:
'ShowType (LengthWithTail l) ':<>:
'Text ":" ':$$: 'ShowType l
))
class (RequireLongerOrSameLength' l a, LongerOrSameLength l a) =>
RequireLongerOrSameLength (l :: [k]) (a :: Peano)
instance (RequireLongerOrSameLength' l a, LongerOrSameLength l a) =>
RequireLongerOrSameLength l a
instance MockableConstraint (RequireLongerOrSameLength l a) where
unsafeProvideConstraint :: Dict (RequireLongerOrSameLength l a)
unsafeProvideConstraint = Dict (RequireLongerOrSameLength '[] 'Z)
-> Dict (RequireLongerOrSameLength l a)
forall a b. a -> b
unsafeCoerce (Dict (RequireLongerOrSameLength '[] 'Z)
-> Dict (RequireLongerOrSameLength l a))
-> Dict (RequireLongerOrSameLength '[] 'Z)
-> Dict (RequireLongerOrSameLength l a)
forall a b. (a -> b) -> a -> b
$ RequireLongerOrSameLength '[] 'Z =>
Dict (RequireLongerOrSameLength '[] 'Z)
forall (a :: Constraint). a => Dict a
Dict @(RequireLongerOrSameLength '[] 'Z)
instance MockableConstraint (RequireLongerThan l a) where
unsafeProvideConstraint :: Dict (RequireLongerThan l a)
unsafeProvideConstraint = Dict (RequireLongerThan '[()] 'Z) -> Dict (RequireLongerThan l a)
forall a b. a -> b
unsafeCoerce (Dict (RequireLongerThan '[()] 'Z) -> Dict (RequireLongerThan l a))
-> Dict (RequireLongerThan '[()] 'Z)
-> Dict (RequireLongerThan l a)
forall a b. (a -> b) -> a -> b
$ RequireLongerThan '[()] 'Z => Dict (RequireLongerThan '[()] 'Z)
forall (a :: Constraint). a => Dict a
Dict @(RequireLongerThan '[()] 'Z)
requireLongerThan
:: Rec any stk
-> Sing n
-> Maybe (Dict (RequireLongerThan stk n))
requireLongerThan :: Rec any stk -> Sing n -> Maybe (Dict (RequireLongerThan stk n))
requireLongerThan Rec any stk
RNil Sing n
_ = Maybe (Dict (RequireLongerThan stk n))
forall a. Maybe a
Nothing
requireLongerThan (any r
_ :& Rec any rs
_xs) Sing n
SZ = Dict (RequireLongerThan stk n)
-> Maybe (Dict (RequireLongerThan stk n))
forall a. a -> Maybe a
Just Dict (RequireLongerThan stk n)
forall (a :: Constraint). a => Dict a
Dict
requireLongerThan (any r
_ :& Rec any rs
xs) (SS n) = do
Dict (RequireLongerThan rs n)
Dict <- Rec any rs -> Sing n -> Maybe (Dict (RequireLongerThan rs n))
forall k (any :: k -> *) (stk :: [k]) (n :: Peano).
Rec any stk -> Sing n -> Maybe (Dict (RequireLongerThan stk n))
requireLongerThan Rec any rs
xs Sing n
SingNat n
n
Dict (RequireLongerThan stk n)
-> Maybe (Dict (RequireLongerThan stk n))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (RequireLongerThan stk n)
forall (a :: Constraint). a => Dict a
Dict
requireLongerOrSameLength
:: Rec any stk
-> Sing n
-> Maybe (Dict (RequireLongerOrSameLength stk n))
requireLongerOrSameLength :: Rec any stk
-> Sing n -> Maybe (Dict (RequireLongerOrSameLength stk n))
requireLongerOrSameLength Rec any stk
_ Sing n
SZ = Dict (RequireLongerOrSameLength stk n)
-> Maybe (Dict (RequireLongerOrSameLength stk n))
forall a. a -> Maybe a
Just Dict (RequireLongerOrSameLength stk n)
forall (a :: Constraint). a => Dict a
Dict
requireLongerOrSameLength Rec any stk
RNil (SS _) = Maybe (Dict (RequireLongerOrSameLength stk n))
forall a. Maybe a
Nothing
requireLongerOrSameLength (any r
_ :& Rec any rs
xs) (SS n) = do
Dict (RequireLongerOrSameLength rs n)
Dict <- Rec any rs
-> Sing n -> Maybe (Dict (RequireLongerOrSameLength rs n))
forall k (any :: k -> *) (stk :: [k]) (n :: Peano).
Rec any stk
-> Sing n -> Maybe (Dict (RequireLongerOrSameLength stk n))
requireLongerOrSameLength Rec any rs
xs Sing n
SingNat n
n
Dict (RequireLongerOrSameLength stk n)
-> Maybe (Dict (RequireLongerOrSameLength stk n))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (RequireLongerOrSameLength stk n)
forall (a :: Constraint). a => Dict a
Dict
isGreaterThan
:: Sing a -> Sing b
-> Maybe (Dict ((a > b) ~ 'True))
isGreaterThan :: Sing a -> Sing b -> Maybe (Dict ((a > b) ~ 'True))
isGreaterThan Sing a
SZ Sing b
_ = Maybe (Dict ((a > b) ~ 'True))
forall a. Maybe a
Nothing
isGreaterThan (SS _) Sing b
SZ = Dict ('True ~ 'True) -> Maybe (Dict ('True ~ 'True))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict ('True ~ 'True)
forall (a :: Constraint). a => Dict a
Dict
isGreaterThan (SS a) (SS b) = Sing n -> Sing n -> Maybe (Dict ((n > n) ~ 'True))
forall (a :: Peano) (b :: Peano).
Sing a -> Sing b -> Maybe (Dict ((a > b) ~ 'True))
isGreaterThan Sing n
SingNat n
a Sing n
SingNat n
b
isGreaterEqualThan
:: Sing a -> Sing b
-> Maybe (Dict ((a >= b) ~ 'True))
isGreaterEqualThan :: Sing a -> Sing b -> Maybe (Dict ((a >= b) ~ 'True))
isGreaterEqualThan Sing a
_ Sing b
SZ = Dict ('True ~ 'True) -> Maybe (Dict ('True ~ 'True))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict ('True ~ 'True)
forall (a :: Constraint). a => Dict a
Dict
isGreaterEqualThan Sing a
SZ Sing b
_ = Maybe (Dict ((a >= b) ~ 'True))
forall a. Maybe a
Nothing
isGreaterEqualThan (SS a) (SS b) = Sing n -> Sing n -> Maybe (Dict ((n >= n) ~ 'True))
forall (a :: Peano) (b :: Peano).
Sing a -> Sing b -> Maybe (Dict ((a >= b) ~ 'True))
isGreaterEqualThan Sing n
SingNat n
a Sing n
SingNat n
b