module Data.Type.Witness.Specific.Concat where

import Data.Type.Witness.General.Representative
import Data.Type.Witness.Specific.List.List
import Import

type Concat :: forall k. [k] -> [k] -> [k]
type family Concat a b where
    Concat '[] bb = bb
    Concat (a ': aa) bb = a ': (Concat aa bb)

concatEmptyRefl :: ListType w a -> Concat a '[] :~: a
concatEmptyRefl :: forall {k} (w :: k -> Type) (a :: [k]).
ListType w a -> Concat a '[] :~: a
concatEmptyRefl ListType w a
NilListType = a :~: a
Concat a '[] :~: a
forall {k} (a :: k). a :~: a
Refl
concatEmptyRefl (ConsListType w a
_ ListType w lt1
la) =
    case ListType w lt1 -> Concat lt1 '[] :~: lt1
forall {k} (w :: k -> Type) (a :: [k]).
ListType w a -> Concat a '[] :~: a
concatEmptyRefl ListType w lt1
la of
        Concat lt1 '[] :~: lt1
Refl -> a :~: a
Concat a '[] :~: a
forall {k} (a :: k). a :~: a
Refl

concatIsDict ::
       forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]). (Representative w, Is (ListType w) aa, Is (ListType w) bb)
    => Dict (Is (ListType w) (Concat aa bb))
concatIsDict :: forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict = let
    build :: forall aa'. ListType w aa' -> Dict (Is (ListType w) (Concat aa' bb))
    build :: forall (aa' :: [k]).
ListType w aa' -> Dict (Is (ListType w) (Concat aa' bb))
build ListType w aa'
NilListType = Dict (Is (ListType w) bb)
Dict (Is (ListType w) (Concat aa' bb))
forall (a :: Constraint). a => Dict a
Dict
    build (ConsListType w a
wa ListType w lt1
la) =
        case ListType w lt1 -> Dict (Is (ListType w) (Concat lt1 bb))
forall (aa' :: [k]).
ListType w aa' -> Dict (Is (ListType w) (Concat aa' bb))
build ListType w lt1
la of
            Dict (Is (ListType w) (Concat lt1 bb))
Dict ->
                case w a -> Dict (Is w a)
Subrepresentative w w
forall k (rep :: k -> Type).
Representative rep =>
Subrepresentative rep rep
getRepWitness w a
wa of
                    Dict (Is w a)
Dict -> Dict (Is (ListType w) (a : Concat lt1 bb))
Dict (Is (ListType w) (Concat aa' bb))
forall (a :: Constraint). a => Dict a
Dict
    in ListType w aa -> Dict (Is (ListType w) (Concat aa bb))
forall (aa' :: [k]).
ListType w aa' -> Dict (Is (ListType w) (Concat aa' bb))
build (ListType w aa -> Dict (Is (ListType w) (Concat aa bb)))
-> ListType w aa -> Dict (Is (ListType w) (Concat aa bb))
forall a b. (a -> b) -> a -> b
$ forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListType w) @aa

withConcatIs ::
       forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r. (Representative w, Is (ListType w) aa, Is (ListType w) bb)
    => (Is (ListType w) (Concat aa bb) => r)
    -> r
withConcatIs :: forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs Is (ListType w) (Concat aa bb) => r
call =
    case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict @k @w @aa @bb of
        Dict (Is (ListType w) (Concat aa bb))
Dict -> r
Is (ListType w) (Concat aa bb) => r
call

concatListType ::
       forall k (w :: k -> Type) (a :: [k]) (b :: [k]). ListType w a -> ListType w b -> ListType w (Concat a b)
concatListType :: forall k (w :: k -> Type) (a :: [k]) (b :: [k]).
ListType w a -> ListType w b -> ListType w (Concat a b)
concatListType ListType w a
NilListType ListType w b
lb = ListType w b
ListType w (Concat a b)
lb
concatListType (ConsListType w a
wa ListType w lt1
la) ListType w b
lb = w a -> ListType w (Concat lt1 b) -> ListType w (a : Concat lt1 b)
forall {k} (w :: k -> Type) (a :: k) (lt1 :: [k]).
w a -> ListType w lt1 -> ListType w (a : lt1)
ConsListType w a
wa (ListType w (Concat lt1 b) -> ListType w (a : Concat lt1 b))
-> ListType w (Concat lt1 b) -> ListType w (a : Concat lt1 b)
forall a b. (a -> b) -> a -> b
$ ListType w lt1 -> ListType w b -> ListType w (Concat lt1 b)
forall k (w :: k -> Type) (a :: [k]) (b :: [k]).
ListType w a -> ListType w b -> ListType w (Concat a b)
concatListType ListType w lt1
la ListType w b
lb