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
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 = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    testEquality (RestElementType ListElementType aa a
lt1) (RestElementType ListElementType aa b
lt2) = do
        a :~: b
Refl <- 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
lt2
        forall (m :: Type -> Type) a. Monad m => a -> m a
return forall {k} (a :: k). a :~: a
Refl
    testEquality ListElementType tt a
_ ListElementType tt 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 = forall k (a :: k). WOrdering a a
WEQ
    testCompare (RestElementType ListElementType aa a
a) (RestElementType ListElementType aa b
b) =
        case 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
b of
            WOrdering a b
WLT -> forall k (a :: k) (b :: k). WOrdering a b
WLT
            WOrdering a b
WGT -> forall k (a :: k) (b :: k). WOrdering a b
WGT
            WOrdering a b
WEQ -> forall k (a :: k). WOrdering a a
WEQ
    testCompare (RestElementType ListElementType aa a
_) ListElementType tt b
FirstElementType = forall k (a :: k) (b :: k). WOrdering a b
WGT
    testCompare ListElementType tt a
FirstElementType (RestElementType ListElementType aa 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 = 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 = forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> 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 = forall a. Finite a => a -> Maybe a
finiteCountPrevious
    countMaybeNext :: Maybe (ListElementType '[] t) -> Maybe (ListElementType '[] t)
countMaybeNext = 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 a
wt
pickListElement (RestElementType ListElementType aa t
n) (ConsListType w a
_ ListType w lt1
l) = forall k (w :: k -> Type) (t :: k) (lt :: [k]).
ListElementType lt t -> ListType w lt -> w t
pickListElement ListElementType aa t
n 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 = forall a. Maybe a
Nothing
lookUpListElement w t
wt (ConsListType w a
wt' ListType w lt1
_)
    | Just t :~: a
Refl <- 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' = forall a. a -> Maybe a
Just 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 <- 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
    forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall {k} (w :: k -> Type). ListType w '[]
NilListType
countListType (ConsListType w a
_ ListType w lt1
lt) = forall {k} (w :: k -> Type) (a :: k) (lt1 :: [k]).
w a -> ListType w lt1 -> ListType w (a : lt1)
ConsListType forall {k} (t :: k) (aa :: [k]). ListElementType (t : aa) t
FirstElementType (forall {k} (wita :: k -> Type) (witb :: k -> Type) (t :: [k]).
(forall (t' :: k). wita t' -> witb t')
-> ListType wita t -> ListType witb t
mapListType forall {k} (aa :: [k]) (t :: k) (a :: k).
ListElementType aa t -> ListElementType (a : aa) t
RestElementType forall a b. (a -> b) -> a -> b
$ 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) = forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome forall a b. (a -> b) -> a -> b
$ forall (a1 :: PeanoNat) (b :: PeanoNat).
GreaterEqual a1 b -> Greater ('Succ a1) b
MkGreater forall (a :: PeanoNat). GreaterEqual a 'Zero
ZeroGreaterEqual
listElementTypeIndex (MkSome (RestElementType ListElementType aa a
n)) =
    case forall {k} (lt :: [k]).
Some (ListElementType lt) -> Some (Greater (ListLength lt))
listElementTypeIndex forall a b. (a -> b) -> a -> b
$ forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome ListElementType aa a
n of
        MkSome (MkGreater GreaterEqual a1 a
n') -> forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome forall a b. (a -> b) -> a -> b
$ forall (a1 :: PeanoNat) (b :: PeanoNat).
GreaterEqual a1 b -> Greater ('Succ a1) b
MkGreater forall a b. (a -> b) -> a -> b
$ 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)) = forall k (f :: k -> Type) (w :: k -> Type) (a :: k).
w a -> f a -> SomeFor f w
MkSomeFor 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 forall {k} (w :: k -> Type) (lt :: [k]).
ListType w lt
-> Some (Greater (ListLength lt)) -> SomeFor w (ListElementType lt)
indexListElementType ListType w lt1
lt (forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome (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 -> forall k (f :: k -> Type) (w :: k -> Type) (a :: k).
w a -> f a -> SomeFor f w
MkSomeFor (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) = forall n a. Empty n => n -> a
never Greater 'Zero a
n