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