module Data.Type.Witness.Specific.List.Element where

import Data.PeanoNat
import Data.Type.Witness.General.Order
import Data.Type.Witness.Specific.List.List
import Data.Type.Witness.Specific.PeanoNat
import Data.Type.Witness.Specific.Some
import Import

type ListElementType :: forall k. [k] -> k -> Type
type role ListElementType nominal nominal
data ListElementType kk t where
    FirstElementType :: ListElementType (t ': tt) t
    RestElementType :: ListElementType aa t -> ListElementType (a ': aa) t

instance TestEquality (ListElementType tt) where
    testEquality :: forall (a :: k) (b :: k).
ListElementType tt a -> ListElementType tt b -> Maybe (a :~: b)
testEquality ListElementType tt a
FirstElementType ListElementType tt b
FirstElementType = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    testEquality (RestElementType ListElementType aa a
lt1) (RestElementType ListElementType aa b
lt2) = do
        a :~: b
Refl <- ListElementType aa a -> ListElementType aa b -> Maybe (a :~: b)
forall (a :: k) (b :: k).
ListElementType aa a -> ListElementType aa b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality ListElementType aa a
lt1 ListElementType aa b
ListElementType aa b
lt2
        (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    testEquality ListElementType tt a
_ ListElementType tt b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance TestOrder (ListElementType tt) where
    testCompare :: forall (a :: k) (b :: k).
ListElementType tt a -> ListElementType tt b -> WOrdering a b
testCompare ListElementType tt a
FirstElementType ListElementType tt b
FirstElementType = WOrdering a a
WOrdering a b
forall k (a :: k). WOrdering a a
WEQ
    testCompare (RestElementType ListElementType aa a
a) (RestElementType ListElementType aa b
b) =
        case ListElementType aa a -> ListElementType aa b -> WOrdering a b
forall (a :: k) (b :: k).
ListElementType aa a -> ListElementType aa b -> WOrdering a b
forall k (w :: k -> Type) (a :: k) (b :: k).
TestOrder w =>
w a -> w b -> WOrdering a b
testCompare ListElementType aa a
a ListElementType aa b
ListElementType aa b
b of
            WOrdering a b
WLT -> WOrdering a b
forall k (a :: k) (b :: k). WOrdering a b
WLT
            WOrdering a b
WGT -> WOrdering a b
forall k (a :: k) (b :: k). WOrdering a b
WGT
            WOrdering a b
WEQ -> WOrdering a a
WOrdering a b
forall k (a :: k). WOrdering a a
WEQ
    testCompare (RestElementType ListElementType aa a
_) ListElementType tt b
FirstElementType = WOrdering a b
forall k (a :: k) (b :: k). WOrdering a b
WGT
    testCompare ListElementType tt a
FirstElementType (RestElementType ListElementType aa b
_) = WOrdering a b
forall k (a :: k) (b :: k). WOrdering a b
WLT

instance Searchable (ListElementType '[] t) where
    search :: forall b. (ListElementType '[] t -> Maybe b) -> Maybe b
search = (ListElementType '[] t -> Maybe b) -> Maybe b
forall a b. Finite a => (a -> Maybe b) -> Maybe b
finiteSearch

instance Eq (ListElementType tt t) where
    ListElementType tt t
lt1 == :: ListElementType tt t -> ListElementType tt t -> Bool
== ListElementType tt t
lt2 = Maybe (t :~: t) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (t :~: t) -> Bool) -> Maybe (t :~: t) -> Bool
forall a b. (a -> b) -> a -> b
$ ListElementType tt t -> ListElementType tt t -> Maybe (t :~: t)
forall (a :: k) (b :: k).
ListElementType tt a -> ListElementType tt b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality ListElementType tt t
lt1 ListElementType tt t
lt2

instance Countable (ListElementType '[] t) where
    countPrevious :: ListElementType '[] t -> Maybe (ListElementType '[] t)
countPrevious = ListElementType '[] t -> Maybe (ListElementType '[] t)
forall a. Finite a => a -> Maybe a
finiteCountPrevious
    countMaybeNext :: Maybe (ListElementType '[] t) -> Maybe (ListElementType '[] t)
countMaybeNext = Maybe (ListElementType '[] t) -> Maybe (ListElementType '[] t)
forall a. Finite a => Maybe a -> Maybe a
finiteCountMaybeNext

instance Finite (ListElementType '[] t) where
    allValues :: [ListElementType '[] t]
allValues = []

instance Empty (ListElementType '[] t) where
    never :: forall a. ListElementType '[] t -> a
never ListElementType '[] t
lt = case ListElementType '[] t
lt of {}

pickListElement :: forall k (w :: k -> Type) (t :: k) (lt :: [k]). ListElementType lt t -> ListType w lt -> w t
pickListElement :: forall k (w :: k -> Type) (t :: k) (lt :: [k]).
ListElementType lt t -> ListType w lt -> w t
pickListElement ListElementType lt t
FirstElementType (ConsListType w a
wt ListType w lt1
_) = w t
w a
wt
pickListElement (RestElementType ListElementType aa t
n) (ConsListType w a
_ ListType w lt1
l) = ListElementType aa t -> ListType w aa -> w t
forall k (w :: k -> Type) (t :: k) (lt :: [k]).
ListElementType lt t -> ListType w lt -> w t
pickListElement ListElementType aa t
n ListType w aa
ListType w lt1
l

lookUpListElement ::
       forall k (w :: k -> Type) (t :: k) (lt :: [k]). TestEquality w
    => w t
    -> ListType w lt
    -> Maybe (ListElementType lt t)
lookUpListElement :: forall k (w :: k -> Type) (t :: k) (lt :: [k]).
TestEquality w =>
w t -> ListType w lt -> Maybe (ListElementType lt t)
lookUpListElement w t
_ ListType w lt
NilListType = Maybe (ListElementType lt t)
forall a. Maybe a
Nothing
lookUpListElement w t
wt (ConsListType w a
wt' ListType w lt1
_)
    | Just t :~: a
Refl <- w t -> w a -> Maybe (t :~: a)
forall (a :: k) (b :: k). w a -> w b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality w t
wt w a
wt' = ListElementType lt t -> Maybe (ListElementType lt t)
forall a. a -> Maybe a
Just ListElementType lt t
ListElementType (t : lt1) t
forall {k} (t :: k) (aa :: [k]). ListElementType (t : aa) t
FirstElementType
lookUpListElement w t
wt (ConsListType w a
_ ListType w lt1
lt) = do
    ListElementType lt1 t
et <- w t -> ListType w lt1 -> Maybe (ListElementType lt1 t)
forall k (w :: k -> Type) (t :: k) (lt :: [k]).
TestEquality w =>
w t -> ListType w lt -> Maybe (ListElementType lt t)
lookUpListElement w t
wt ListType w lt1
lt
    ListElementType lt t -> Maybe (ListElementType lt t)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ListElementType lt t -> Maybe (ListElementType lt t))
-> ListElementType lt t -> Maybe (ListElementType lt t)
forall a b. (a -> b) -> a -> b
$ ListElementType lt1 t -> ListElementType (a : lt1) t
forall {k} (aa :: [k]) (t :: k) (a :: k).
ListElementType aa t -> ListElementType (a : aa) t
RestElementType ListElementType lt1 t
et

countListType :: ListType w lt -> ListType (ListElementType lt) lt
countListType :: forall {k} (w :: k -> Type) (lt :: [k]).
ListType w lt -> ListType (ListElementType lt) lt
countListType ListType w lt
NilListType = ListType (ListElementType lt) lt
ListType (ListElementType lt) '[]
forall {k} (w :: k -> Type). ListType w '[]
NilListType
countListType (ConsListType w a
_ ListType w lt1
lt) = ListElementType lt a
-> ListType (ListElementType lt) lt1
-> ListType (ListElementType lt) (a : lt1)
forall {k} (w :: k -> Type) (a :: k) (lt1 :: [k]).
w a -> ListType w lt1 -> ListType w (a : lt1)
ConsListType ListElementType lt a
ListElementType (a : lt1) a
forall {k} (t :: k) (aa :: [k]). ListElementType (t : aa) t
FirstElementType ((forall (t' :: k). ListElementType lt1 t' -> ListElementType lt t')
-> ListType (ListElementType lt1) lt1
-> ListType (ListElementType lt) lt1
forall {k} (wita :: k -> Type) (witb :: k -> Type) (t :: [k]).
(forall (t' :: k). wita t' -> witb t')
-> ListType wita t -> ListType witb t
mapListType ListElementType lt1 t' -> ListElementType lt t'
ListElementType lt1 t' -> ListElementType (a : lt1) t'
forall (t' :: k). ListElementType lt1 t' -> ListElementType lt t'
forall {k} (aa :: [k]) (t :: k) (a :: k).
ListElementType aa t -> ListElementType (a : aa) t
RestElementType (ListType (ListElementType lt1) lt1
 -> ListType (ListElementType lt) lt1)
-> ListType (ListElementType lt1) lt1
-> ListType (ListElementType lt) lt1
forall a b. (a -> b) -> a -> b
$ ListType w lt1 -> ListType (ListElementType lt1) lt1
forall {k} (w :: k -> Type) (lt :: [k]).
ListType w lt -> ListType (ListElementType lt) lt
countListType ListType w lt1
lt)

listElementTypeIndex :: Some (ListElementType lt) -> Some (Greater (ListLength lt))
listElementTypeIndex :: forall {k} (lt :: [k]).
Some (ListElementType lt) -> Some (Greater (ListLength lt))
listElementTypeIndex (MkSome ListElementType lt a
FirstElementType) = Greater (ListLength lt) 'Zero -> Some (Greater (ListLength lt))
forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome (Greater (ListLength lt) 'Zero -> Some (Greater (ListLength lt)))
-> Greater (ListLength lt) 'Zero -> Some (Greater (ListLength lt))
forall a b. (a -> b) -> a -> b
$ GreaterEqual (ListLength tt) 'Zero
-> Greater ('Succ (ListLength tt)) 'Zero
forall (a1 :: PeanoNat) (b :: PeanoNat).
GreaterEqual a1 b -> Greater ('Succ a1) b
MkGreater GreaterEqual (ListLength tt) 'Zero
forall (a :: PeanoNat). GreaterEqual a 'Zero
ZeroGreaterEqual
listElementTypeIndex (MkSome (RestElementType ListElementType aa a
n)) =
    case Some (ListElementType aa) -> Some (Greater (ListLength aa))
forall {k} (lt :: [k]).
Some (ListElementType lt) -> Some (Greater (ListLength lt))
listElementTypeIndex (Some (ListElementType aa) -> Some (Greater (ListLength aa)))
-> Some (ListElementType aa) -> Some (Greater (ListLength aa))
forall a b. (a -> b) -> a -> b
$ ListElementType aa a -> Some (ListElementType aa)
forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome ListElementType aa a
n of
        MkSome (MkGreater GreaterEqual a1 a
n') -> Greater (ListLength lt) ('Succ a) -> Some (Greater (ListLength lt))
forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome (Greater (ListLength lt) ('Succ a)
 -> Some (Greater (ListLength lt)))
-> Greater (ListLength lt) ('Succ a)
-> Some (Greater (ListLength lt))
forall a b. (a -> b) -> a -> b
$ GreaterEqual ('Succ a1) ('Succ a)
-> Greater ('Succ ('Succ a1)) ('Succ a)
forall (a1 :: PeanoNat) (b :: PeanoNat).
GreaterEqual a1 b -> Greater ('Succ a1) b
MkGreater (GreaterEqual ('Succ a1) ('Succ a)
 -> Greater ('Succ ('Succ a1)) ('Succ a))
-> GreaterEqual ('Succ a1) ('Succ a)
-> Greater ('Succ ('Succ a1)) ('Succ a)
forall a b. (a -> b) -> a -> b
$ GreaterEqual a1 a -> GreaterEqual ('Succ a1) ('Succ a)
forall (a1 :: PeanoNat) (b1 :: PeanoNat).
GreaterEqual a1 b1 -> GreaterEqual ('Succ a1) ('Succ b1)
SuccGreaterEqual GreaterEqual a1 a
n'

indexListElementType :: ListType w lt -> Some (Greater (ListLength lt)) -> SomeFor w (ListElementType lt)
indexListElementType :: forall {k} (w :: k -> Type) (lt :: [k]).
ListType w lt
-> Some (Greater (ListLength lt)) -> SomeFor w (ListElementType lt)
indexListElementType (ConsListType w a
wa ListType w lt1
_) (MkSome (MkGreater GreaterEqual a1 a
ZeroGreaterEqual)) = ListElementType lt a -> w a -> SomeFor w (ListElementType lt)
forall k (f :: k -> Type) (w :: k -> Type) (a :: k).
w a -> f a -> SomeFor f w
MkSomeFor ListElementType lt a
ListElementType (a : lt1) a
forall {k} (t :: k) (aa :: [k]). ListElementType (t : aa) t
FirstElementType w a
wa
indexListElementType (ConsListType w a
_ ListType w lt1
lt) (MkSome (MkGreater (SuccGreaterEqual GreaterEqual a1 b1
n))) =
    case ListType w lt1
-> Some (Greater (ListLength lt1))
-> SomeFor w (ListElementType lt1)
forall {k} (w :: k -> Type) (lt :: [k]).
ListType w lt
-> Some (Greater (ListLength lt)) -> SomeFor w (ListElementType lt)
indexListElementType ListType w lt1
lt (Greater ('Succ a1) b1 -> Some (Greater ('Succ a1))
forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome (GreaterEqual a1 b1 -> Greater ('Succ a1) b1
forall (a1 :: PeanoNat) (b :: PeanoNat).
GreaterEqual a1 b -> Greater ('Succ a1) b
MkGreater GreaterEqual a1 b1
n)) of
        MkSomeFor ListElementType lt1 a
n' w a
wa -> ListElementType lt a -> w a -> SomeFor w (ListElementType lt)
forall k (f :: k -> Type) (w :: k -> Type) (a :: k).
w a -> f a -> SomeFor f w
MkSomeFor (ListElementType lt1 a -> ListElementType (a : lt1) a
forall {k} (aa :: [k]) (t :: k) (a :: k).
ListElementType aa t -> ListElementType (a : aa) t
RestElementType ListElementType lt1 a
n') w a
wa
indexListElementType ListType w lt
NilListType (MkSome Greater 'Zero a
n) = Greater 'Zero a -> SomeFor w (ListElementType lt)
forall n a. Empty n => n -> a
forall a. Greater 'Zero a -> a
never Greater 'Zero a
n