{-# LANGUAGE GHC2021 #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use camelCase" #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Vary.Utils(
(:|),
KnownPrefix(..),
Length,
Subset(..),
Index,
IndexOf,
Mappable,
pop,
size,
activeIndex,
natValue,
) where
import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy (..))
import GHC.TypeLits
( ErrorMessage (ShowType, Text, (:$$:), (:<>:)),
KnownNat,
Nat,
TypeError,
natVal,
type (+),
type (-),
)
import Vary.Core (Vary (..), pop)
type (:|) e es = Member e es
size :: forall xs. (KnownNat (Length xs)) => Vary xs -> Word
size :: forall (xs :: [*]). KnownNat (Length xs) => Vary xs -> Word
size Vary xs
_ = forall (n :: Nat) a. (KnownNat n, Num a) => a
natValue @(Length xs)
activeIndex :: Vary a -> Word
activeIndex :: forall (a :: [*]). Vary a -> Word
activeIndex (Vary Word
idx Any
_) = Word
idx
class (KnownPrefix es) => Subset (xs :: [Type]) (es :: [Type]) where
subsetFullyKnown :: Bool
subsetFullyKnown =
[Char] -> Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"subsetFullyKnown"
morph' :: Vary xs -> Vary ys
morph' =
[Char] -> Vary xs -> Vary ys
forall a. HasCallStack => [Char] -> a
error [Char]
"morph' was unexpectedly called"
instance
{-# INCOHERENT #-}
( KnownPrefix es,
xs `IsUnknownSuffixOf` es
) =>
Subset xs es
where
subsetFullyKnown :: Bool
subsetFullyKnown = Bool
False
instance (KnownPrefix es) => Subset '[] es where
subsetFullyKnown :: Bool
subsetFullyKnown = Bool
True
instance (e :| es, Subset xs es) => Subset (e : xs) es where
subsetFullyKnown :: Bool
subsetFullyKnown = forall (xs :: [*]) (es :: [*]). Subset xs es => Bool
subsetFullyKnown @xs @es
morph' :: forall (ys :: [*]). Vary (e : xs) -> Vary ys
morph' (Vary Word
0 Any
a) = Word -> Any -> Vary ys
forall (possibilities :: [*]). Word -> Any -> Vary possibilities
Vary (forall (n :: Nat) a. (KnownNat n, Num a) => a
natValue @(IndexOf e es)) Any
a
morph' (Vary Word
n Any
a) = forall (xs :: [*]) (es :: [*]) (ys :: [*]).
Subset xs es =>
Vary xs -> Vary ys
morph' @xs @es (Word -> Any -> Vary xs
forall (possibilities :: [*]). Word -> Any -> Vary possibilities
Vary (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) Any
a)
class KnownPrefix (es :: [Type]) where
prefixLength :: Int
instance (KnownPrefix es) => KnownPrefix (e : es) where
prefixLength :: Int
prefixLength = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ forall (es :: [*]). KnownPrefix es => Int
prefixLength @es
instance {-# INCOHERENT #-} KnownPrefix es where
prefixLength :: Int
prefixLength = Int
0
class (xs :: [k]) `IsUnknownSuffixOf` (es :: [k])
instance {-# INCOHERENT #-} (xs ~ es) => xs `IsUnknownSuffixOf` es
instance (xs `IsUnknownSuffixOf` es) => xs `IsUnknownSuffixOf` (e : es)
type family Length (xs :: [k]) :: Nat where
Length xs = Length' 0 xs
type family Length' n (xs :: [k]) :: Nat where
Length' n '[] = n
Length' n (x ': xs) = Length' (n + 1) xs
natValue :: forall (n :: Nat) a. (KnownNat n, Num a) => a
{-# INLINEABLE natValue #-}
natValue :: forall (n :: Nat) a. (KnownNat n, Num a) => a
natValue = Integer -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
type Mappable a b xs ys = (a :| xs, b :| ys, ys ~ Mapped a b xs)
type family Mapped (a :: Type) (b :: Type) (as :: [Type]) = (bs :: [Type]) where
Mapped a b (a ': as) = (b ': as)
Mapped a b (x ': as) = x ': Mapped a b as
Mapped a b l = TypeError (
'Text "Cannot map from " ':<>: 'ShowType a ':<>: 'Text " into " ':<>: 'ShowType b
:$$: 'Text "as it cannot be found in the list " ':<>: 'ShowType l)
type IndexOf (x :: k) (xs :: [k]) = IndexOf' (MaybeIndexOf x xs) x xs
type family IndexOf' (i :: Nat) (a :: k) (l :: [k]) :: Nat where
IndexOf' 0 x l =
TypeError
( 'ShowType x
':<>: 'Text " not found in list:"
':$$: 'Text " "
':<>: 'ShowType l
)
IndexOf' i _ _ = i - 1
type family MaybeIndexOf (a :: k) (l :: [k]) where
MaybeIndexOf x xs = MaybeIndexOf' 0 x xs
type family MaybeIndexOf' (n :: Nat) (a :: k) (l :: [k]) where
MaybeIndexOf' n x '[] = 0
MaybeIndexOf' n x (x ': xs) = n + 1
MaybeIndexOf' n x (y ': xs) = MaybeIndexOf' (n + 1) x xs
type Index (n :: Nat) (l :: [k]) = Type_List_Too_Vague___Please_Specify_Prefix_Of_List_Including_The_Desired_Type's_Location n l l
type family Type_List_Too_Vague___Please_Specify_Prefix_Of_List_Including_The_Desired_Type's_Location (n :: Nat) (l :: [k]) (l2 :: [k]) :: k where
Type_List_Too_Vague___Please_Specify_Prefix_Of_List_Including_The_Desired_Type's_Location 0 (x ': _ ) _ = x
Type_List_Too_Vague___Please_Specify_Prefix_Of_List_Including_The_Desired_Type's_Location n (_ ': xs) l2 = Type_List_Too_Vague___Please_Specify_Prefix_Of_List_Including_The_Desired_Type's_Location (n-1) xs l2
Type_List_Too_Vague___Please_Specify_Prefix_Of_List_Including_The_Desired_Type's_Location n '[] l2 = TypeError ( 'Text "Index "
':<>: 'ShowType n
':<>: 'Text " out of bounds for list:"
':$$: 'Text " "
':<>: 'ShowType l2 )
type family Member x xs :: Constraint where
Member x xs = MemberAtIndex (IndexOf x xs) x xs
type MemberAtIndex i x xs =
( x ~ Index i xs,
KnownNat i
)
type family Remove (a :: k) (l :: [k]) :: [k] where
Remove a '[] = '[]
Remove a (a ': as) = as
Remove a (b ': as) = b ': Remove a as