{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

-- |
-- Module      : Data.Type.List.Sublist
-- Copyright   : (c) Justin Le 2023
-- License     : BSD3
--
-- Maintainer  : justin@jle.im
-- Stability   : experimental
-- Portability : non-portable
--
-- Witnesses regarding sublists of lists.
module Data.Type.List.Sublist (
  -- * Prefix and Suffix

  -- ** Prefix
  Prefix (..),
  IsPrefix,
  autoPrefix,
  takeRec,
  prefixLens,
  takeIndex,
  weakenIndex,
  prefixShape,

  -- ** Suffix
  Suffix (..),
  IsSuffix,
  autoSuffix,
  dropRec,
  suffixLens,
  dropIndex,
  shiftIndex,

  -- * Append
  Append (..),
  IsAppend,
  autoAppend,
  withAppend,
  prefixToAppend,
  suffixToAppend,
  appendToPrefix,
  appendToSuffix,
  splitAppend,
  appendShape,

  -- ** Application
  splitRec,
  appendRec,
  splitRecIso,
  splitIndex,

  -- ** Witnesses

  -- *** Singletons
  pattern AppendWit,
  appendWit,
  implyAppend,
  unAppendWit,

  -- *** Vinyl
  pattern AppendWitV,
  appendWitV,
  implyAppendV,
  unAppendWitV,

  -- *** Both
  pattern AppendWit',
  convertAppends,
  AppendedTo,

  -- * Interleave
  Interleave (..),
  IsInterleave,
  autoInterleave,
  interleaveRec,
  unweaveRec,
  interleaveRecIso,
  injectIndexL,
  injectIndexR,
  unweaveIndex,
  interleavedIxes,
  swapInterleave,
  interleaveShapes,

  -- * Subset
  Subset (..),
  IsSubset,
  autoSubset,
  subsetComplement,
  interleaveRToSubset,
  interleaveLToSubset,
  subsetToInterleaveL,
  subsetToInterleaveR,
  subsetRec,
  getSubset,
  subsetShapes,
  subsetIxes,
  weakenSubsetIndex,
  strengthenSubsetIndex,
) where

import Data.Bifunctor
import Data.Functor.Compose
import Data.Kind
import Data.List.Singletons (SList (..), type (++))
import Data.Profunctor
import Data.Singletons
import Data.Singletons.Decide
import Data.Singletons.Sigma
import Data.Type.Functor.Product
import Data.Type.Predicate
import Data.Type.Predicate.Auto
import Data.Type.Predicate.Param
import Data.Vinyl hiding ((:~:))
import qualified Data.Vinyl.Recursive as VR
import qualified Data.Vinyl.TypeLevel as V
import GHC.Generics ((:+:) (..))
import Lens.Micro hiding ((%~))
import Lens.Micro.Extras

-- | A @'Prefix' as bs@ witnesses that @as@ is a prefix of @bs@.
--
-- Some examples:
--
-- @
-- PreZ                    :: Prefix '[]      '[1,2,3]
-- PreS PreZ               :: Prefix '[1]     '[1,2,3]
-- PreS (PreS PreZ)        :: Prefix '[1,2]   '[1,2,3]
-- PreS (PreS (PreS PreZ)) :: Prefix '[1,2,3] '[1,2,3]
-- @
--
-- Rule of thumb for construction: the number of 'PreS' is the number of
-- items in the prefix.
--
-- This is essentially the first half of an 'Append', but is conceptually
-- easier to work with.
data Prefix :: [k] -> [k] -> Type where
  PreZ :: Prefix '[] as
  PreS :: Prefix as bs -> Prefix (a ': as) (a ': bs)

deriving instance Show (Prefix as bs)

-- | A lens into the prefix of a 'Rec'.
prefixLens :: Prefix as bs -> Lens' (Rec f bs) (Rec f as)
prefixLens :: forall {u} (as :: [u]) (bs :: [u]) (f :: u -> *).
Prefix as bs -> Lens' (Rec f bs) (Rec f as)
prefixLens Prefix as bs
p = Prefix as bs
-> (forall {bs :: [u]}.
    Append as bs bs
    -> (Rec f as -> f (Rec f as)) -> Rec f bs -> f (Rec f bs))
-> (Rec f as -> f (Rec f as))
-> Rec f bs
-> f (Rec f bs)
forall {k} (as :: [k]) (cs :: [k]) r.
Prefix as cs -> (forall (bs :: [k]). Append as bs cs -> r) -> r
prefixToAppend Prefix as bs
p ((forall {bs :: [u]}.
  Append as bs bs
  -> (Rec f as -> f (Rec f as)) -> Rec f bs -> f (Rec f bs))
 -> (Rec f as -> f (Rec f as)) -> Rec f bs -> f (Rec f bs))
-> (forall {bs :: [u]}.
    Append as bs bs
    -> (Rec f as -> f (Rec f as)) -> Rec f bs -> f (Rec f bs))
-> (Rec f as -> f (Rec f as))
-> Rec f bs
-> f (Rec f bs)
forall a b. (a -> b) -> a -> b
$ \Append as bs bs
a -> Append as bs bs
-> ((Rec f as, Rec f bs) -> f (Rec f as, Rec f bs))
-> Rec f bs
-> f (Rec f bs)
forall {u} (p :: * -> * -> *) (f :: * -> *) (as :: [u]) (bs :: [u])
       (cs :: [u]) (g :: u -> *).
(Profunctor p, Functor f) =>
Append as bs cs
-> p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs))
-> p (Rec g cs) (f (Rec g cs))
splitRecIso Append as bs bs
a (((Rec f as, Rec f bs) -> f (Rec f as, Rec f bs))
 -> Rec f bs -> f (Rec f bs))
-> ((Rec f as -> f (Rec f as))
    -> (Rec f as, Rec f bs) -> f (Rec f as, Rec f bs))
-> (Rec f as -> f (Rec f as))
-> Rec f bs
-> f (Rec f bs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rec f as -> f (Rec f as))
-> (Rec f as, Rec f bs) -> f (Rec f as, Rec f bs)
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (Rec f as, Rec f bs) (Rec f as, Rec f bs) (Rec f as) (Rec f as)
_1

-- | Take items from a 'Rec' corresponding to a given 'Prefix'.
takeRec :: Prefix as bs -> Rec f bs -> Rec f as
takeRec :: forall {u} (as :: [u]) (bs :: [u]) (f :: u -> *).
Prefix as bs -> Rec f bs -> Rec f as
takeRec Prefix as bs
p = Getting (Rec f as) (Rec f bs) (Rec f as) -> Rec f bs -> Rec f as
forall a s. Getting a s a -> s -> a
view (Prefix as bs -> Lens' (Rec f bs) (Rec f as)
forall {u} (as :: [u]) (bs :: [u]) (f :: u -> *).
Prefix as bs -> Lens' (Rec f bs) (Rec f as)
prefixLens Prefix as bs
p)

-- | A type-level predicate that a given list has @as@ as a prefix.
--
-- @since 0.1.2.0
type IsPrefix as = TyPred (Prefix as)

instance Auto (IsPrefix '[]) bs where
  auto :: IsPrefix '[] @@ bs
auto = IsPrefix '[] @@ bs
Prefix '[] bs
forall {k} (as :: [k]). Prefix '[] as
PreZ

instance Auto (IsPrefix as) bs => Auto (IsPrefix (a ': as)) (a ': bs) where
  auto :: IsPrefix (a : as) @@ (a : bs)
auto = Prefix as bs -> Prefix (a : as) (a : bs)
forall {k} (bs :: [k]) (b :: [k]) (a :: k).
Prefix bs b -> Prefix (a : bs) (a : b)
PreS (forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsPrefix as) @bs)

instance (SDecide k, SingI (as :: [k])) => Decidable (IsPrefix as) where
  decide :: Decide (IsPrefix as)
decide = case forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as of
    Sing as
SList as
SNil -> \Sing a
_ -> Prefix '[] a -> Decision (Prefix '[] a)
forall a. a -> Decision a
Proved Prefix '[] a
forall {k} (as :: [k]). Prefix '[] as
PreZ
    Sing n1
x `SCons` (Sing n2
Sing :: Sing as') -> \case
      Sing a
SList a
SNil -> Refuted (IsPrefix as @@ a) -> Decision (IsPrefix as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsPrefix as @@ a) -> Decision (IsPrefix as @@ a))
-> Refuted (IsPrefix as @@ a) -> Decision (IsPrefix as @@ a)
forall a b. (a -> b) -> a -> b
$ \case {}
      Sing n1
y `SCons` (Sing n2
ys :: Sing bs') -> case Sing n1
x Sing n1 -> Sing n1 -> Decision (n1 :~: n1)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
y of
        Proved n1 :~: n1
Refl -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: [k] ~> *). Decidable p => Decide p
decide @(IsPrefix as') Sing n2
ys of
          Proved IsPrefix n2 @@ n2
p -> Prefix (n1 : n2) (n1 : n2) -> Decision (Prefix (n1 : n2) (n1 : n2))
forall a. a -> Decision a
Proved (Prefix n2 n2 -> Prefix (n1 : n2) (n1 : n2)
forall {k} (bs :: [k]) (b :: [k]) (a :: k).
Prefix bs b -> Prefix (a : bs) (a : b)
PreS IsPrefix n2 @@ n2
Prefix n2 n2
p)
          Disproved Refuted (IsPrefix n2 @@ n2)
v -> Refuted (IsPrefix as @@ a) -> Decision (IsPrefix as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsPrefix as @@ a) -> Decision (IsPrefix as @@ a))
-> Refuted (IsPrefix as @@ a) -> Decision (IsPrefix as @@ a)
forall a b. (a -> b) -> a -> b
$ \case
            PreS Prefix as bs
p -> Refuted (IsPrefix n2 @@ n2)
v IsPrefix n2 @@ n2
Prefix as bs
p
        Disproved Refuted (n1 :~: n1)
v -> Refuted (IsPrefix as @@ a) -> Decision (IsPrefix as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsPrefix as @@ a) -> Decision (IsPrefix as @@ a))
-> Refuted (IsPrefix as @@ a) -> Decision (IsPrefix as @@ a)
forall a b. (a -> b) -> a -> b
$ \case
          PreS Prefix as bs
_ -> Refuted (n1 :~: n1)
v n1 :~: n1
n1 :~: n1
forall {k} (a :: k). a :~: a
Refl

-- | Automatically generate a 'Prefix' if @as@ and @bs@ are known
-- statically.
--
-- @since 0.1.2.0
autoPrefix :: forall as bs. Auto (IsPrefix as) bs => Prefix as bs
autoPrefix :: forall {k} (as :: [k]) (bs :: [k]).
Auto (IsPrefix as) bs =>
Prefix as bs
autoPrefix = forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsPrefix as) @bs

-- | Get the 'Shape' associated with a 'Prefix'.
--
-- @since 0.1.3.0
prefixShape ::
  Prefix as bs ->
  Shape [] as
prefixShape :: forall {k} (as :: [k]) (bs :: [k]). Prefix as bs -> Shape [] as
prefixShape = \case
  Prefix as bs
PreZ -> Rec Proxy '[]
Shape [] as
forall {u} (a :: u -> *). Rec a '[]
RNil
  PreS Prefix as bs
p -> Proxy a
forall {k} (t :: k). Proxy t
Proxy Proxy a -> Rec Proxy as -> Rec Proxy (a : as)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Prefix as bs -> Shape [] as
forall {k} (as :: [k]) (bs :: [k]). Prefix as bs -> Shape [] as
prefixShape Prefix as bs
p

-- | A @'Suffix' as bs@ witnesses that @as@ is a suffix of @bs@.
--
-- Some examples:
--
-- @
-- SufZ                    :: Suffix '[1,2,3] '[1,2,3]
-- SufS SufZ               :: Suffix   '[2,3] '[1,2,3]
-- SufS (SufS SufZ)        :: Suffix     '[3] '[1,2,3]
-- SufS (SufS (SufS SufZ)) :: Suffix      '[] '[1,2,3]
-- @
--
-- Rule of thumb for construction: the number of 'SufS' is the number of
-- items to "drop" before getting the suffix.
--
-- This is essentially the second half of an 'Append', but is conceptually
-- easier to work with.
data Suffix :: [k] -> [k] -> Type where
  SufZ :: Suffix as as
  SufS :: Suffix as bs -> Suffix as (b ': bs)

deriving instance Show (Suffix as bs)

-- | A type-level predicate that a given list has @as@ as a suffix.
--
-- @since 0.1.2.0
type IsSuffix as = TyPred (Suffix as)

instance Auto (IsSuffix '[]) '[] where
  auto :: IsSuffix '[] @@ '[]
auto = IsSuffix '[] @@ '[]
Suffix '[] '[]
forall {k} (as :: [k]). Suffix as as
SufZ

instance {-# OVERLAPPABLE #-} Auto (IsSuffix (a ': as)) (a ': as) where
  auto :: IsSuffix (a : as) @@ (a : as)
auto = IsSuffix (a : as) @@ (a : as)
Suffix (a : as) (a : as)
forall {k} (as :: [k]). Suffix as as
SufZ

instance {-# OVERLAPPABLE #-} Auto (IsSuffix as) bs => Auto (IsSuffix as) (b ': bs) where
  auto :: IsSuffix as @@ (b : bs)
auto = Suffix as bs -> Suffix as (b : bs)
forall {k} (as :: [k]) (bs :: [k]) (b :: k).
Suffix as bs -> Suffix as (b : bs)
SufS (forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsSuffix as) @bs)

instance (SDecide k, SingI (as :: [k])) => Decidable (IsSuffix as) where
  decide :: Decide (IsSuffix as)
decide = \case
    Sing a
SList a
SNil -> case forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as of
      Sing as
SList as
SNil -> Suffix '[] '[] -> Decision (Suffix '[] '[])
forall a. a -> Decision a
Proved Suffix '[] '[]
forall {k} (as :: [k]). Suffix as as
SufZ
      Sing n1
_ `SCons` Sing n2
_ -> Refuted (IsSuffix as @@ a) -> Decision (IsSuffix as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsSuffix as @@ a) -> Decision (IsSuffix as @@ a))
-> Refuted (IsSuffix as @@ a) -> Decision (IsSuffix as @@ a)
forall a b. (a -> b) -> a -> b
$ \case {}
    Sing n1
_ `SCons` Sing n2
ys -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: [k] ~> *). Decidable p => Decide p
decide @(IsSuffix as) Sing n2
ys of
      Proved IsSuffix as @@ n2
s -> (IsSuffix as @@ a) -> Decision (IsSuffix as @@ a)
forall a. a -> Decision a
Proved ((IsSuffix as @@ a) -> Decision (IsSuffix as @@ a))
-> (IsSuffix as @@ a) -> Decision (IsSuffix as @@ a)
forall a b. (a -> b) -> a -> b
$ Suffix as n2 -> Suffix as (n1 : n2)
forall {k} (as :: [k]) (bs :: [k]) (b :: k).
Suffix as bs -> Suffix as (b : bs)
SufS IsSuffix as @@ n2
Suffix as n2
s
      Disproved Refuted (IsSuffix as @@ n2)
v -> Refuted (IsSuffix as @@ a) -> Decision (IsSuffix as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsSuffix as @@ a) -> Decision (IsSuffix as @@ a))
-> Refuted (IsSuffix as @@ a) -> Decision (IsSuffix as @@ a)
forall a b. (a -> b) -> a -> b
$ \case
        IsSuffix as @@ a
Suffix as (n1 : n2)
SufZ -> String -> Void
forall a. HasCallStack => String -> a
error String
"help me"
        SufS Suffix as bs
s -> Refuted (IsSuffix as @@ n2)
v IsSuffix as @@ n2
Suffix as bs
s

-- | Automatically generate a 'Suffix' if @as@ and @bs@ are known
-- statically.
--
-- @since 0.1.2.0
autoSuffix :: forall as bs. Auto (IsSuffix as) bs => Suffix as bs
autoSuffix :: forall {k} (as :: [k]) (bs :: [k]).
Auto (IsSuffix as) bs =>
Suffix as bs
autoSuffix = forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsSuffix as) @bs

-- | A lens into the suffix of a 'Rec'.
suffixLens :: Suffix as bs -> Lens' (Rec f bs) (Rec f as)
suffixLens :: forall {u} (as :: [u]) (bs :: [u]) (f :: u -> *).
Suffix as bs -> Lens' (Rec f bs) (Rec f as)
suffixLens Suffix as bs
p = Suffix as bs
-> (forall {as :: [u]}.
    Append as as bs
    -> (Rec f as -> f (Rec f as)) -> Rec f bs -> f (Rec f bs))
-> (Rec f as -> f (Rec f as))
-> Rec f bs
-> f (Rec f bs)
forall {k} (bs :: [k]) (cs :: [k]) r.
Suffix bs cs -> (forall (as :: [k]). Append as bs cs -> r) -> r
suffixToAppend Suffix as bs
p ((forall {as :: [u]}.
  Append as as bs
  -> (Rec f as -> f (Rec f as)) -> Rec f bs -> f (Rec f bs))
 -> (Rec f as -> f (Rec f as)) -> Rec f bs -> f (Rec f bs))
-> (forall {as :: [u]}.
    Append as as bs
    -> (Rec f as -> f (Rec f as)) -> Rec f bs -> f (Rec f bs))
-> (Rec f as -> f (Rec f as))
-> Rec f bs
-> f (Rec f bs)
forall a b. (a -> b) -> a -> b
$ \Append as as bs
a -> Append as as bs
-> ((Rec f as, Rec f as) -> f (Rec f as, Rec f as))
-> Rec f bs
-> f (Rec f bs)
forall {u} (p :: * -> * -> *) (f :: * -> *) (as :: [u]) (bs :: [u])
       (cs :: [u]) (g :: u -> *).
(Profunctor p, Functor f) =>
Append as bs cs
-> p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs))
-> p (Rec g cs) (f (Rec g cs))
splitRecIso Append as as bs
a (((Rec f as, Rec f as) -> f (Rec f as, Rec f as))
 -> Rec f bs -> f (Rec f bs))
-> ((Rec f as -> f (Rec f as))
    -> (Rec f as, Rec f as) -> f (Rec f as, Rec f as))
-> (Rec f as -> f (Rec f as))
-> Rec f bs
-> f (Rec f bs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rec f as -> f (Rec f as))
-> (Rec f as, Rec f as) -> f (Rec f as, Rec f as)
forall s t a b. Field2 s t a b => Lens s t a b
Lens
  (Rec f as, Rec f as) (Rec f as, Rec f as) (Rec f as) (Rec f as)
_2

-- | Drop items from a 'Rec' corresponding to a given 'Suffix'.
dropRec :: Suffix as bs -> Rec f bs -> Rec f as
dropRec :: forall {u} (as :: [u]) (bs :: [u]) (f :: u -> *).
Suffix as bs -> Rec f bs -> Rec f as
dropRec Suffix as bs
p = Getting (Rec f as) (Rec f bs) (Rec f as) -> Rec f bs -> Rec f as
forall a s. Getting a s a -> s -> a
view (Suffix as bs -> Lens' (Rec f bs) (Rec f as)
forall {u} (as :: [u]) (bs :: [u]) (f :: u -> *).
Suffix as bs -> Lens' (Rec f bs) (Rec f as)
suffixLens Suffix as bs
p)

-- | An @'Append' as bs cs@ witnesses that @cs@ is the result of appending
-- @as@ and @bs@.
--
-- Some examples:
--
-- @
-- AppZ                     :: Append '[]  '[1,2]   '[1,2]
-- AppZ                     :: Append '[]  '[1,2,3] '[1,2,3]
-- AppS AppZ                :: Append '[0] '[1,2]   '[0,1,2]
-- @
--
-- Rule of thumb for construction: the number of 'AppS' is the number of
-- items in the /first/ list.
--
-- This basically combines 'Prefix' and 'Suffix'.
data Append :: [k] -> [k] -> [k] -> Type where
  AppZ :: Append '[] as as
  AppS :: Append as bs cs -> Append (a ': as) bs (a ': cs)

deriving instance Show (Append as bs cs)

-- | A type-level predicate that a given list is the result of appending of
-- @as@ and @bs@.
--
-- @since 0.1.2.0
type IsAppend as bs = TyPred (Append as bs)

-- | A parameterized predicate that you can use with 'select': With an
-- @'AppendedTo' as@, you can give @bs@ and get @cs@ in return, where @cs@
-- is the appending of @as@ and @bs@.
--
-- Run it with:
--
-- @
-- 'selectTC' :: SingI as => Sing bs -> 'Σ' [k] ('IsAppend' as bs)
-- @
--
-- 'select' for 'AppendedTo' is pretty much just 'withAppend'.
--
-- @since 0.1.2.0
type AppendedTo as = TyPP (Append as)

instance Auto (IsAppend '[] as) as where
  auto :: IsAppend '[] as @@ as
auto = IsAppend '[] as @@ as
Append '[] as as
forall {k} (as :: [k]). Append '[] as as
AppZ

instance Auto (IsAppend as bs) cs => Auto (IsAppend (a ': as) bs) (a ': cs) where
  auto :: IsAppend (a : as) bs @@ (a : cs)
auto = Append as bs cs -> Append (a : as) bs (a : cs)
forall {k} (bs :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Append bs bs b -> Append (a : bs) bs (a : b)
AppS (forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsAppend as bs) @cs)

instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsAppend as bs) where
  decide :: Decide (IsAppend as bs)
decide = case forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as of
    Sing as
SList as
SNil -> \Sing a
cs -> case forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @bs Sing bs -> Sing a -> Decision (bs :~: a)
forall (a :: [k]) (b :: [k]).
Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing a
cs of
      Proved bs :~: a
Refl -> Append '[] bs bs -> Decision (Append '[] bs bs)
forall a. a -> Decision a
Proved Append '[] bs bs
forall {k} (as :: [k]). Append '[] as as
AppZ
      Disproved Refuted (bs :~: a)
v -> Refuted (IsAppend as bs @@ a) -> Decision (IsAppend as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsAppend as bs @@ a) -> Decision (IsAppend as bs @@ a))
-> Refuted (IsAppend as bs @@ a) -> Decision (IsAppend as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
        IsAppend as bs @@ a
Append '[] bs a
AppZ -> Refuted (bs :~: a)
v bs :~: bs
bs :~: a
forall {k} (a :: k). a :~: a
Refl
    Sing n1
x `SCons` (Sing n2
Sing :: Sing as') -> \case
      Sing a
SList a
SNil -> Refuted (IsAppend as bs @@ a) -> Decision (IsAppend as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsAppend as bs @@ a) -> Decision (IsAppend as bs @@ a))
-> Refuted (IsAppend as bs @@ a) -> Decision (IsAppend as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case {}
      Sing n1
y `SCons` (Sing n2
ys :: Sing bs') -> case Sing n1
x Sing n1 -> Sing n1 -> Decision (n1 :~: n1)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
y of
        Proved n1 :~: n1
Refl -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: [k] ~> *). Decidable p => Decide p
decide @(IsAppend as' bs) Sing n2
ys of
          Proved IsAppend n2 bs @@ n2
p -> Append (n1 : n2) bs (n1 : n2)
-> Decision (Append (n1 : n2) bs (n1 : n2))
forall a. a -> Decision a
Proved (Append n2 bs n2 -> Append (n1 : n2) bs (n1 : n2)
forall {k} (bs :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Append bs bs b -> Append (a : bs) bs (a : b)
AppS IsAppend n2 bs @@ n2
Append n2 bs n2
p)
          Disproved Refuted (IsAppend n2 bs @@ n2)
v -> Refuted (IsAppend as bs @@ a) -> Decision (IsAppend as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsAppend as bs @@ a) -> Decision (IsAppend as bs @@ a))
-> Refuted (IsAppend as bs @@ a) -> Decision (IsAppend as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
            AppS Append as bs cs
p -> Refuted (IsAppend n2 bs @@ n2)
v IsAppend n2 bs @@ n2
Append as bs cs
p
        Disproved Refuted (n1 :~: n1)
v -> Refuted (IsAppend as bs @@ a) -> Decision (IsAppend as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsAppend as bs @@ a) -> Decision (IsAppend as bs @@ a))
-> Refuted (IsAppend as bs @@ a) -> Decision (IsAppend as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
          AppS Append as bs cs
_ -> Refuted (n1 :~: n1)
v n1 :~: n1
n1 :~: n1
forall {k} (a :: k). a :~: a
Refl

instance SingI as => Decidable (Found (AppendedTo as))
instance SingI as => Provable (Found (AppendedTo as)) where
  prove :: Prove (Found (AppendedTo as))
prove Sing a
ys = Rec Sing as
-> Rec Sing a
-> (forall {cs :: [k]}.
    Rec Sing cs -> Append as a cs -> Found (AppendedTo as) @@ a)
-> Found (AppendedTo as) @@ a
forall {u} (f :: u -> *) (as :: [u]) (bs :: [u]) r.
Rec f as
-> Rec f bs
-> (forall (cs :: [u]). Rec f cs -> Append as bs cs -> r)
-> r
withAppend (Sing as -> Prod [] Sing as
forall {k} (as :: [k]). Sing as -> Prod [] Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd (forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as)) (Sing a -> Prod [] Sing a
forall {k} (as :: [k]). Sing as -> Prod [] Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd Sing a
ys) ((forall {cs :: [k]}.
  Rec Sing cs -> Append as a cs -> Found (AppendedTo as) @@ a)
 -> Found (AppendedTo as) @@ a)
-> (forall {cs :: [k]}.
    Rec Sing cs -> Append as a cs -> Found (AppendedTo as) @@ a)
-> Found (AppendedTo as) @@ a
forall a b. (a -> b) -> a -> b
$ \Rec Sing cs
s Append as a cs
x -> Prod [] Sing cs -> Sing cs
forall {k} (as :: [k]). Prod [] Sing as -> Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Prod f Sing as -> Sing as
prodSing Rec Sing cs
Prod [] Sing cs
s Sing cs
-> (TyPP (Append as) a @@ cs) -> Sigma [k] (TyPP (Append as) a)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: TyPP (Append as) a @@ cs
Append as a cs
x

-- | Automatically generate an 'Append' if @as@, @bs@ and @cs@ are known
-- statically.
--
-- @since 0.1.2.0
autoAppend :: forall as bs cs. Auto (IsAppend as bs) cs => Append as bs cs
autoAppend :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Auto (IsAppend as bs) cs =>
Append as bs cs
autoAppend = forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsAppend as bs) @cs

-- | Witness that @'Append' as bs cs@ implies @(as ++ bs) ~ cs@, using
-- @++@ from "Data.Singletons.Prelude.List".
--
-- @since 0.1.2.0
appendWit :: Append as bs cs -> (as ++ bs) :~: cs
appendWit :: forall {a} (as :: [a]) (bs :: [a]) (cs :: [a]).
Append as bs cs -> (as ++ bs) :~: cs
appendWit = \case
  Append as bs cs
AppZ -> cs :~: cs
(as ++ bs) :~: cs
forall {k} (a :: k). a :~: a
Refl
  AppS Append as bs cs
a -> case Append as bs cs -> (as ++ bs) :~: cs
forall {a} (as :: [a]) (bs :: [a]) (cs :: [a]).
Append as bs cs -> (as ++ bs) :~: cs
appendWit Append as bs cs
a of
    (as ++ bs) :~: cs
Refl -> cs :~: cs
(as ++ bs) :~: cs
forall {k} (a :: k). a :~: a
Refl

-- | The inverse of 'appendWit': if we know @(as ++ bs) ~ cs@ (using @++@
-- from "Data.Singletons.Prelude.List"), we can create an @'Append' as bs
-- cs@ given structure witnesses 'Sing'.
--
-- @since 0.1.2.0
unAppendWit ::
  (as ++ bs) ~ cs =>
  Rec f as ->
  Rec f bs ->
  Append as bs cs
unAppendWit :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (f :: k -> *).
((as ++ bs) ~ cs) =>
Rec f as -> Rec f bs -> Append as bs cs
unAppendWit = \case
  Rec f as
RNil -> \Rec f bs
_ -> Append as bs cs
Append '[] bs bs
forall {k} (as :: [k]). Append '[] as as
AppZ
  f r
_ :& Rec f rs
xs -> Append rs bs (rs ++ bs) -> Append as bs cs
Append rs bs (rs ++ bs) -> Append (r : rs) bs (r : (rs ++ bs))
forall {k} (bs :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Append bs bs b -> Append (a : bs) bs (a : b)
AppS (Append rs bs (rs ++ bs) -> Append as bs cs)
-> (Rec f bs -> Append rs bs (rs ++ bs))
-> Rec f bs
-> Append as bs cs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec f rs -> Rec f bs -> Append rs bs (rs ++ bs)
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (f :: k -> *).
((as ++ bs) ~ cs) =>
Rec f as -> Rec f bs -> Append as bs cs
unAppendWit Rec f rs
xs

-- | A useful pattern synonym for using 'Append' with @++@ from
-- "Data.Singletons.Prelude.List".
--
-- As a /pattern/, this brings @(as ++ bs) ~ cs@ into the context whenever
-- you use it to match on an @'Append' as bs cs@.
--
-- As an /expression/, this constructs an @'Append' as bs cs@ as long as
-- you have @(as ++ bs) ~ cs@ in the context.
--
-- @since 0.1.2.0
pattern AppendWit ::
  forall as bs cs. (RecApplicative as, RecApplicative bs) => (as ++ bs) ~ cs => Append as bs cs
pattern $mAppendWit :: forall {r} {k} {as :: [k]} {bs :: [k]} {cs :: [k]}.
(RecApplicative as, RecApplicative bs) =>
Append as bs cs -> (((as ++ bs) ~ cs) => r) -> ((# #) -> r) -> r
$bAppendWit :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
(RecApplicative as, RecApplicative bs, (as ++ bs) ~ cs) =>
Append as bs cs
AppendWit <- (appendWit @as @bs @cs -> Refl)
  where
    AppendWit = forall (as :: [k]) (bs :: [k]) (cs :: [k]) (f :: k -> *).
((as ++ bs) ~ cs) =>
Rec f as -> Rec f bs -> Append as bs cs
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (f :: k -> *).
((as ++ bs) ~ cs) =>
Rec f as -> Rec f bs -> Append as bs cs
unAppendWit @as @bs @cs Rec Proxy as
Shape [] as
forall {k} (f :: * -> *) (as :: f k). PureProd f as => Shape f as
pureShape Rec Proxy bs
Shape [] bs
forall {k} (f :: * -> *) (as :: f k). PureProd f as => Shape f as
pureShape

{-# COMPLETE AppendWit #-}

-- | 'appendWit' stated as a 'Predicate' implication.
--
-- @since 0.1.2.0
implyAppend :: IsAppend as bs --> EqualTo (as ++ bs)
implyAppend :: forall {a} (as :: [a]) (bs :: [a]) (a :: [a]).
Sing a -> (IsAppend as bs @@ a) -> EqualTo (as ++ bs) @@ a
implyAppend Sing a
_ = Apply (TyCon (Append as bs)) a
-> Apply (TyCon ((:~:) (as ++ bs))) a
Append as bs a -> (as ++ bs) :~: a
forall {a} (as :: [a]) (bs :: [a]) (cs :: [a]).
Append as bs cs -> (as ++ bs) :~: cs
appendWit

-- | Witness that @'Append' as bs cs@ implies @(as ++ bs) ~ cs@, using
-- @++@ from "Data.Vinyl.TypeLevel".
--
-- @since 0.1.2.0
appendWitV :: Append as bs cs -> (as V.++ bs) :~: cs
appendWitV :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Append as bs cs -> (as ++ bs) :~: cs
appendWitV = \case
  Append as bs cs
AppZ -> cs :~: cs
(as ++ bs) :~: cs
forall {k} (a :: k). a :~: a
Refl
  AppS Append as bs cs
a -> case Append as bs cs -> (as ++ bs) :~: cs
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Append as bs cs -> (as ++ bs) :~: cs
appendWitV Append as bs cs
a of
    (as ++ bs) :~: cs
Refl -> cs :~: cs
(as ++ bs) :~: cs
forall {k} (a :: k). a :~: a
Refl

-- | The inverse of 'appendWitV': if we know @(as ++ bs) ~ cs@ (using @++@
-- from "Data.Vinyl.TypeLevel"), we can create an @'Append' as bs cs@ given
-- structure witnesses 'Sing'.
--
-- @since 0.1.2.0
unAppendWitV ::
  (as V.++ bs) ~ cs =>
  Rec f as ->
  Rec f bs ->
  Append as bs cs
unAppendWitV :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (f :: k -> *).
((as ++ bs) ~ cs) =>
Rec f as -> Rec f bs -> Append as bs cs
unAppendWitV = \case
  Rec f as
RNil -> \Rec f bs
_ -> Append as bs cs
Append '[] bs bs
forall {k} (as :: [k]). Append '[] as as
AppZ
  f r
_ :& Rec f rs
xs -> Append rs bs (rs ++ bs) -> Append as bs cs
Append rs bs (rs ++ bs) -> Append (r : rs) bs (r : (rs ++ bs))
forall {k} (bs :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Append bs bs b -> Append (a : bs) bs (a : b)
AppS (Append rs bs (rs ++ bs) -> Append as bs cs)
-> (Rec f bs -> Append rs bs (rs ++ bs))
-> Rec f bs
-> Append as bs cs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec f rs -> Rec f bs -> Append rs bs (rs ++ bs)
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (f :: k -> *).
((as ++ bs) ~ cs) =>
Rec f as -> Rec f bs -> Append as bs cs
unAppendWitV Rec f rs
xs

-- | A useful pattern synonym for using 'Append' with @++@ from
-- "Data.Vinyl.TypeLevel".
--
-- As a /pattern/, this brings @(as ++ bs) ~ cs@ into the context whenever
-- you use it to match on an @'Append' as bs cs@.
--
-- As an /expression/, this constructs an @'Append' as bs cs@ as long as
-- you have @(as ++ bs) ~ cs@ in the context.
--
-- @since 0.1.2.0
pattern AppendWitV ::
  forall as bs cs. (RecApplicative as, RecApplicative bs) => (as V.++ bs) ~ cs => Append as bs cs
pattern $mAppendWitV :: forall {r} {k} {as :: [k]} {bs :: [k]} {cs :: [k]}.
(RecApplicative as, RecApplicative bs) =>
Append as bs cs -> (((as ++ bs) ~ cs) => r) -> ((# #) -> r) -> r
$bAppendWitV :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
(RecApplicative as, RecApplicative bs, (as ++ bs) ~ cs) =>
Append as bs cs
AppendWitV <- (appendWitV @as @bs @cs -> Refl)
  where
    AppendWitV = forall (as :: [k]) (bs :: [k]) (cs :: [k]) (f :: k -> *).
((as ++ bs) ~ cs) =>
Rec f as -> Rec f bs -> Append as bs cs
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (f :: k -> *).
((as ++ bs) ~ cs) =>
Rec f as -> Rec f bs -> Append as bs cs
unAppendWitV @as @bs @cs Rec Proxy as
Shape [] as
forall {k} (f :: * -> *) (as :: f k). PureProd f as => Shape f as
pureShape Rec Proxy bs
Shape [] bs
forall {k} (f :: * -> *) (as :: f k). PureProd f as => Shape f as
pureShape

{-# COMPLETE AppendWitV #-}

-- | Combine the powers of 'AppendWit' and 'AppendWitV' by matching on an
-- 'Append' to witness @(as ++ bs) ~ cs@ for /both/ @++@ from
-- "Data.Singletons.Prelude.List" and "Data.Vinyl.TypeLevel".  This also
-- witnesses that @(as ++ bs) ~ (as ++ bs)@ (for the two different @++@s)
-- by transitive property.
--
-- @since 0.1.2.0
pattern AppendWit' ::
  forall as bs cs.
  (RecApplicative as, RecApplicative bs) =>
  ((as ++ bs) ~ cs, (as V.++ bs) ~ cs) =>
  Append as bs cs
pattern $mAppendWit' :: forall {r} {k} {as :: [k]} {bs :: [k]} {cs :: [k]}.
(RecApplicative as, RecApplicative bs) =>
Append as bs cs
-> (((as ++ bs) ~ cs, (as ++ bs) ~ cs) => r) -> ((# #) -> r) -> r
$bAppendWit' :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
(RecApplicative as, RecApplicative bs, (as ++ bs) ~ cs,
 (as ++ bs) ~ cs) =>
Append as bs cs
AppendWit' <- ((\Append as bs cs
a -> (Append as bs cs
a, Append as bs cs
a)) -> (AppendWit, AppendWitV))
  where
    AppendWit' = Append as bs cs
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
(RecApplicative as, RecApplicative bs, (as ++ bs) ~ cs) =>
Append as bs cs
AppendWit

{-# COMPLETE AppendWitV #-}

-- | 'appendWitV' stated as a 'Predicate' implication.
--
-- @since 0.1.2.0
implyAppendV :: IsAppend as bs --> EqualTo (as V.++ bs)
implyAppendV :: forall {k} (as :: [k]) (bs :: [k]) (a :: [k]).
Sing a -> (IsAppend as bs @@ a) -> EqualTo (as ++ bs) @@ a
implyAppendV Sing a
_ = Apply (TyCon (Append as bs)) a
-> Apply (TyCon ((:~:) (as ++ bs))) a
Append as bs a -> (as ++ bs) :~: a
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Append as bs cs -> (as ++ bs) :~: cs
appendWitV

-- | Given a witness @'Append' as bs cs@, prove that singleton's @++@ from
-- "Data.Singletons.Prelude.List" is the same as vinyl's @++@
-- "Data.Vinyl.TypeLevel".
convertAppends :: Append as bs cs -> (as ++ bs) :~: (as V.++ bs)
convertAppends :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Append as bs cs -> (as ++ bs) :~: (as ++ bs)
convertAppends Append as bs cs
a = case Append as bs cs -> (as ++ bs) :~: cs
forall {a} (as :: [a]) (bs :: [a]) (cs :: [a]).
Append as bs cs -> (as ++ bs) :~: cs
appendWit Append as bs cs
a of
  (as ++ bs) :~: cs
Refl -> case Append as bs cs -> (as ++ bs) :~: cs
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Append as bs cs -> (as ++ bs) :~: cs
appendWitV Append as bs cs
a of
    (as ++ bs) :~: cs
Refl -> cs :~: cs
(as ++ bs) :~: (as ++ bs)
forall {k} (a :: k). a :~: a
Refl

-- | Given @as@ and @bs@, create an @'Append' as bs cs@ with, with @cs@
-- existentially quantified
withAppend :: Rec f as -> Rec f bs -> (forall cs. Rec f cs -> Append as bs cs -> r) -> r
withAppend :: forall {u} (f :: u -> *) (as :: [u]) (bs :: [u]) r.
Rec f as
-> Rec f bs
-> (forall (cs :: [u]). Rec f cs -> Append as bs cs -> r)
-> r
withAppend = \case
  Rec f as
RNil -> \Rec f bs
ys forall (cs :: [u]). Rec f cs -> Append as bs cs -> r
f -> Rec f bs -> Append as bs bs -> r
forall (cs :: [u]). Rec f cs -> Append as bs cs -> r
f Rec f bs
ys Append as bs bs
Append '[] bs bs
forall {k} (as :: [k]). Append '[] as as
AppZ
  f r
x :& Rec f rs
xs -> \Rec f bs
ys forall (cs :: [u]). Rec f cs -> Append as bs cs -> r
f -> Rec f rs
-> Rec f bs
-> (forall {cs :: [u]}. Rec f cs -> Append rs bs cs -> r)
-> r
forall {u} (f :: u -> *) (as :: [u]) (bs :: [u]) r.
Rec f as
-> Rec f bs
-> (forall (cs :: [u]). Rec f cs -> Append as bs cs -> r)
-> r
withAppend Rec f rs
xs Rec f bs
ys ((forall {cs :: [u]}. Rec f cs -> Append rs bs cs -> r) -> r)
-> (forall {cs :: [u]}. Rec f cs -> Append rs bs cs -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Rec f cs
zs Append rs bs cs
a ->
    Rec f (r : cs) -> Append as bs (r : cs) -> r
forall (cs :: [u]). Rec f cs -> Append as bs cs -> r
f (f r
x f r -> Rec f cs -> Rec f (r : cs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec f cs
zs) (Append rs bs cs -> Append (r : rs) bs (r : cs)
forall {k} (bs :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Append bs bs b -> Append (a : bs) bs (a : b)
AppS Append rs bs cs
a)

-- | Get the 'Shape' associated with an 'Append''s prefix.
--
-- @since 0.1.3.0
appendShape ::
  Append as bs cs ->
  Shape [] as
appendShape :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Append as bs cs -> Shape [] as
appendShape = \case
  Append as bs cs
AppZ -> Rec Proxy '[]
Shape [] as
forall {u} (a :: u -> *). Rec a '[]
RNil
  AppS Append as bs cs
a -> Proxy a
forall {k} (t :: k). Proxy t
Proxy Proxy a -> Rec Proxy as -> Rec Proxy (a : as)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Append as bs cs -> Shape [] as
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Append as bs cs -> Shape [] as
appendShape Append as bs cs
a

-- | Witness an isomorphism between 'Rec' and two parts that compose it.
--
-- Read this type signature as:
--
-- @
-- 'splitRecIso'
--     :: Append as  bs  cs
--     -> Iso' (Rec f cs) (Rec f as, Rec f bs)
-- @
--
-- This can be used with the combinators from the lens library.
--
-- The 'Append' tells the point to split the 'Rec' at.
splitRecIso ::
  (Profunctor p, Functor f) =>
  Append as bs cs ->
  p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs)) ->
  p (Rec g cs) (f (Rec g cs))
splitRecIso :: forall {u} (p :: * -> * -> *) (f :: * -> *) (as :: [u]) (bs :: [u])
       (cs :: [u]) (g :: u -> *).
(Profunctor p, Functor f) =>
Append as bs cs
-> p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs))
-> p (Rec g cs) (f (Rec g cs))
splitRecIso Append as bs cs
a = (Rec g cs -> (Rec g as, Rec g bs))
-> (f (Rec g as, Rec g bs) -> f (Rec g cs))
-> p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs))
-> p (Rec g cs) (f (Rec g cs))
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (Append as bs cs -> Rec g cs -> (Rec g as, Rec g bs)
forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]) (f :: u -> *).
Append as bs cs -> Rec f cs -> (Rec f as, Rec f bs)
splitRec Append as bs cs
a) ((((Rec g as, Rec g bs) -> Rec g cs)
-> f (Rec g as, Rec g bs) -> f (Rec g cs)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Rec g as, Rec g bs) -> Rec g cs)
 -> f (Rec g as, Rec g bs) -> f (Rec g cs))
-> ((Rec g as -> Rec g bs -> Rec g cs)
    -> (Rec g as, Rec g bs) -> Rec g cs)
-> (Rec g as -> Rec g bs -> Rec g cs)
-> f (Rec g as, Rec g bs)
-> f (Rec g cs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rec g as -> Rec g bs -> Rec g cs)
-> (Rec g as, Rec g bs) -> Rec g cs
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry) (Append as bs cs -> Rec g as -> Rec g bs -> Rec g cs
forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]) (f :: u -> *).
Append as bs cs -> Rec f as -> Rec f bs -> Rec f cs
appendRec Append as bs cs
a))

-- | Split a 'Rec' into a prefix and suffix.  Basically 'takeRec'
-- and 'dropRec' combined.
splitRec ::
  Append as bs cs ->
  Rec f cs ->
  (Rec f as, Rec f bs)
splitRec :: forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]) (f :: u -> *).
Append as bs cs -> Rec f cs -> (Rec f as, Rec f bs)
splitRec = \case
  Append as bs cs
AppZ -> (Rec f '[]
forall {u} (a :: u -> *). Rec a '[]
RNil,)
  AppS Append as bs cs
a -> \case
    f r
x :& Rec f rs
xs -> (Rec f as -> Rec f as)
-> (Rec f as, Rec f bs) -> (Rec f as, Rec f bs)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (f r
x f r -> Rec f as -> Rec f (r : as)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) ((Rec f as, Rec f bs) -> (Rec f as, Rec f bs))
-> (Rec f rs -> (Rec f as, Rec f bs))
-> Rec f rs
-> (Rec f as, Rec f bs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Append as bs rs -> Rec f rs -> (Rec f as, Rec f bs)
forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]) (f :: u -> *).
Append as bs cs -> Rec f cs -> (Rec f as, Rec f bs)
splitRec Append as bs cs
Append as bs rs
a (Rec f rs -> (Rec f as, Rec f bs))
-> Rec f rs -> (Rec f as, Rec f bs)
forall a b. (a -> b) -> a -> b
$ Rec f rs
xs

-- | Append two 'Rec's together according to an 'Append'.
appendRec ::
  Append as bs cs ->
  Rec f as ->
  Rec f bs ->
  Rec f cs
appendRec :: forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]) (f :: u -> *).
Append as bs cs -> Rec f as -> Rec f bs -> Rec f cs
appendRec = \case
  Append as bs cs
AppZ -> \Rec f as
_ -> Rec f bs -> Rec f bs
Rec f bs -> Rec f cs
forall a. a -> a
id
  AppS Append as bs cs
a -> \case
    f r
x :& Rec f rs
xs -> (f r
x f r -> Rec f cs -> Rec f (r : cs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) (Rec f cs -> Rec f cs)
-> (Rec f bs -> Rec f cs) -> Rec f bs -> Rec f cs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Append as bs cs -> Rec f as -> Rec f bs -> Rec f cs
forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]) (f :: u -> *).
Append as bs cs -> Rec f as -> Rec f bs -> Rec f cs
appendRec Append as bs cs
a Rec f as
Rec f rs
xs

-- | Convert a 'Prefix' to an 'Append', with an existential @bs@.
prefixToAppend ::
  Prefix as cs ->
  (forall bs. Append as bs cs -> r) ->
  r
prefixToAppend :: forall {k} (as :: [k]) (cs :: [k]) r.
Prefix as cs -> (forall (bs :: [k]). Append as bs cs -> r) -> r
prefixToAppend = \case
  Prefix as cs
PreZ -> ((Append as cs cs -> r) -> Append as cs cs -> r
forall a b. (a -> b) -> a -> b
$ Append as cs cs
Append '[] cs cs
forall {k} (as :: [k]). Append '[] as as
AppZ)
  PreS Prefix as bs
p -> \forall (bs :: [k]). Append as bs cs -> r
f -> Prefix as bs -> (forall (bs :: [k]). Append as bs bs -> r) -> r
forall {k} (as :: [k]) (cs :: [k]) r.
Prefix as cs -> (forall (bs :: [k]). Append as bs cs -> r) -> r
prefixToAppend Prefix as bs
p (Append as bs cs -> r
forall (bs :: [k]). Append as bs cs -> r
f (Append as bs cs -> r)
-> (Append as bs bs -> Append as bs cs) -> Append as bs bs -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Append as bs bs -> Append as bs cs
Append as bs bs -> Append (a : as) bs (a : bs)
forall {k} (bs :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Append bs bs b -> Append (a : bs) bs (a : b)
AppS)

-- | Convert a 'Suffix' to an 'Append', with an existential @as@.
suffixToAppend ::
  Suffix bs cs ->
  (forall as. Append as bs cs -> r) ->
  r
suffixToAppend :: forall {k} (bs :: [k]) (cs :: [k]) r.
Suffix bs cs -> (forall (as :: [k]). Append as bs cs -> r) -> r
suffixToAppend = \case
  Suffix bs cs
SufZ -> ((Append '[] bs cs -> r) -> Append '[] bs cs -> r
forall a b. (a -> b) -> a -> b
$ Append '[] bs bs
Append '[] bs cs
forall {k} (as :: [k]). Append '[] as as
AppZ)
  SufS Suffix bs bs
s -> \forall (as :: [k]). Append as bs cs -> r
f -> Suffix bs bs -> (forall (as :: [k]). Append as bs bs -> r) -> r
forall {k} (bs :: [k]) (cs :: [k]) r.
Suffix bs cs -> (forall (as :: [k]). Append as bs cs -> r) -> r
suffixToAppend Suffix bs bs
s (Append (b : as) bs cs -> r
forall (as :: [k]). Append as bs cs -> r
f (Append (b : as) bs cs -> r)
-> (Append as bs bs -> Append (b : as) bs cs)
-> Append as bs bs
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Append as bs bs -> Append (b : as) bs cs
Append as bs bs -> Append (b : as) bs (b : bs)
forall {k} (bs :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Append bs bs b -> Append (a : bs) bs (a : b)
AppS)

-- | Split an 'Append' into a 'Prefix' and 'Suffix'.  Basically
-- 'appendToPrefix' and 'appendToSuffix' at the same time.
splitAppend ::
  Append as bs cs ->
  (Prefix as cs, Suffix bs cs)
splitAppend :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Append as bs cs -> (Prefix as cs, Suffix bs cs)
splitAppend = \case
  Append as bs cs
AppZ -> (Prefix as cs
Prefix '[] cs
forall {k} (as :: [k]). Prefix '[] as
PreZ, Suffix bs bs
Suffix bs cs
forall {k} (as :: [k]). Suffix as as
SufZ)
  AppS Append as bs cs
a -> (Prefix as cs -> Prefix as cs)
-> (Suffix bs cs -> Suffix bs cs)
-> (Prefix as cs, Suffix bs cs)
-> (Prefix as cs, Suffix bs cs)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Prefix as cs -> Prefix as cs
Prefix as cs -> Prefix (a : as) (a : cs)
forall {k} (bs :: [k]) (b :: [k]) (a :: k).
Prefix bs b -> Prefix (a : bs) (a : b)
PreS Suffix bs cs -> Suffix bs cs
Suffix bs cs -> Suffix bs (a : cs)
forall {k} (as :: [k]) (bs :: [k]) (b :: k).
Suffix as bs -> Suffix as (b : bs)
SufS ((Prefix as cs, Suffix bs cs) -> (Prefix as cs, Suffix bs cs))
-> (Append as bs cs -> (Prefix as cs, Suffix bs cs))
-> Append as bs cs
-> (Prefix as cs, Suffix bs cs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Append as bs cs -> (Prefix as cs, Suffix bs cs)
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Append as bs cs -> (Prefix as cs, Suffix bs cs)
splitAppend (Append as bs cs -> (Prefix as cs, Suffix bs cs))
-> Append as bs cs -> (Prefix as cs, Suffix bs cs)
forall a b. (a -> b) -> a -> b
$ Append as bs cs
a

-- | Convert an 'Append' to a 'Prefix', forgetting the suffix.
appendToPrefix :: Append as bs cs -> Prefix as cs
appendToPrefix :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Append as bs cs -> Prefix as cs
appendToPrefix = \case
  Append as bs cs
AppZ -> Prefix as cs
Prefix '[] cs
forall {k} (as :: [k]). Prefix '[] as
PreZ
  AppS Append as bs cs
a -> Prefix as cs -> Prefix as cs
Prefix as cs -> Prefix (a : as) (a : cs)
forall {k} (bs :: [k]) (b :: [k]) (a :: k).
Prefix bs b -> Prefix (a : bs) (a : b)
PreS (Prefix as cs -> Prefix as cs)
-> (Append as bs cs -> Prefix as cs)
-> Append as bs cs
-> Prefix as cs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Append as bs cs -> Prefix as cs
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Append as bs cs -> Prefix as cs
appendToPrefix (Append as bs cs -> Prefix as cs)
-> Append as bs cs -> Prefix as cs
forall a b. (a -> b) -> a -> b
$ Append as bs cs
a

-- | Convert an 'Append' to a 'Suffix', forgetting the prefix
appendToSuffix :: Append as bs cs -> Suffix bs cs
appendToSuffix :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Append as bs cs -> Suffix bs cs
appendToSuffix = \case
  Append as bs cs
AppZ -> Suffix bs bs
Suffix bs cs
forall {k} (as :: [k]). Suffix as as
SufZ
  AppS Append as bs cs
a -> Suffix bs cs -> Suffix bs cs
Suffix bs cs -> Suffix bs (a : cs)
forall {k} (as :: [k]) (bs :: [k]) (b :: k).
Suffix as bs -> Suffix as (b : bs)
SufS (Suffix bs cs -> Suffix bs cs)
-> (Append as bs cs -> Suffix bs cs)
-> Append as bs cs
-> Suffix bs cs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Append as bs cs -> Suffix bs cs
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Append as bs cs -> Suffix bs cs
appendToSuffix (Append as bs cs -> Suffix bs cs)
-> Append as bs cs -> Suffix bs cs
forall a b. (a -> b) -> a -> b
$ Append as bs cs
a

-- | Split an 'Index' by an 'Append'.  If the 'Index' was in the first part
-- of the list, it'll return 'Left'.  If it was in the second part, it'll
-- return 'Right'.
--
-- This is essentially 'takeIndex' and 'dropIndex' at the same time.
splitIndex ::
  Append as bs cs ->
  Index cs x ->
  Either (Index as x) (Index bs x)
splitIndex :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (x :: k).
Append as bs cs -> Index cs x -> Either (Index as x) (Index bs x)
splitIndex = \case
  Append as bs cs
AppZ -> Index cs x -> Either (Index as x) (Index bs x)
Index cs x -> Either (Index as x) (Index cs x)
forall a b. b -> Either a b
Right
  AppS Append as bs cs
a -> \case
    Index cs x
IZ -> Index as x -> Either (Index as x) (Index bs x)
forall a b. a -> Either a b
Left Index as x
Index (x : as) x
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
    IS Index bs x
i -> (Index as x -> Index as x)
-> Either (Index as x) (Index bs x)
-> Either (Index as x) (Index bs x)
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Index as x -> Index as x
Index as x -> Index (a : as) x
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS (Either (Index as x) (Index bs x)
 -> Either (Index as x) (Index bs x))
-> (Index bs x -> Either (Index as x) (Index bs x))
-> Index bs x
-> Either (Index as x) (Index bs x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Append as bs bs -> Index bs x -> Either (Index as x) (Index bs x)
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (x :: k).
Append as bs cs -> Index cs x -> Either (Index as x) (Index bs x)
splitIndex Append as bs cs
Append as bs bs
a (Index bs x -> Either (Index as x) (Index bs x))
-> Index bs x -> Either (Index as x) (Index bs x)
forall a b. (a -> b) -> a -> b
$ Index bs x
i

-- | Shave off the final inhabitants of an 'Index', keeping only indices
-- a part of a given prefix.  If the index is out of range, 'Nothing' will
-- be returned.
--
-- This is essentially 'splitIndex', but taking only 'Left' results.
takeIndex ::
  Prefix as bs ->
  Index bs x ->
  Maybe (Index as x)
takeIndex :: forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Prefix as bs -> Index bs x -> Maybe (Index as x)
takeIndex Prefix as bs
p Index bs x
i =
  Prefix as bs
-> (forall {bs :: [k]}. Append as bs bs -> Maybe (Index as x))
-> Maybe (Index as x)
forall {k} (as :: [k]) (cs :: [k]) r.
Prefix as cs -> (forall (bs :: [k]). Append as bs cs -> r) -> r
prefixToAppend Prefix as bs
p ((forall {bs :: [k]}. Append as bs bs -> Maybe (Index as x))
 -> Maybe (Index as x))
-> (forall {bs :: [k]}. Append as bs bs -> Maybe (Index as x))
-> Maybe (Index as x)
forall a b. (a -> b) -> a -> b
$
    (Index as x -> Maybe (Index as x))
-> (Index bs x -> Maybe (Index as x))
-> Either (Index as x) (Index bs x)
-> Maybe (Index as x)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Index as x -> Maybe (Index as x)
forall a. a -> Maybe a
Just (Maybe (Index as x) -> Index bs x -> Maybe (Index as x)
forall a b. a -> b -> a
const Maybe (Index as x)
forall a. Maybe a
Nothing)
      (Either (Index as x) (Index bs x) -> Maybe (Index as x))
-> (Append as bs bs -> Either (Index as x) (Index bs x))
-> Append as bs bs
-> Maybe (Index as x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Append as bs bs -> Index bs x -> Either (Index as x) (Index bs x)
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (x :: k).
Append as bs cs -> Index cs x -> Either (Index as x) (Index bs x)
`splitIndex` Index bs x
i)

-- | Shave off the initial inhabitants of an 'Index', keeping only indices
-- a part of a given suffix  If the index is out of range, 'Nothing' will
-- be returned.
--
-- This is essentially 'splitIndex', but taking only 'Right' results.
dropIndex ::
  Suffix as bs ->
  Index bs x ->
  Maybe (Index as x)
dropIndex :: forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Suffix as bs -> Index bs x -> Maybe (Index as x)
dropIndex Suffix as bs
s Index bs x
i =
  Suffix as bs
-> (forall {as :: [k]}. Append as as bs -> Maybe (Index as x))
-> Maybe (Index as x)
forall {k} (bs :: [k]) (cs :: [k]) r.
Suffix bs cs -> (forall (as :: [k]). Append as bs cs -> r) -> r
suffixToAppend Suffix as bs
s ((forall {as :: [k]}. Append as as bs -> Maybe (Index as x))
 -> Maybe (Index as x))
-> (forall {as :: [k]}. Append as as bs -> Maybe (Index as x))
-> Maybe (Index as x)
forall a b. (a -> b) -> a -> b
$
    (Index as x -> Maybe (Index as x))
-> (Index as x -> Maybe (Index as x))
-> Either (Index as x) (Index as x)
-> Maybe (Index as x)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe (Index as x) -> Index as x -> Maybe (Index as x)
forall a b. a -> b -> a
const Maybe (Index as x)
forall a. Maybe a
Nothing) Index as x -> Maybe (Index as x)
forall a. a -> Maybe a
Just
      (Either (Index as x) (Index as x) -> Maybe (Index as x))
-> (Append as as bs -> Either (Index as x) (Index as x))
-> Append as as bs
-> Maybe (Index as x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Append as as bs -> Index bs x -> Either (Index as x) (Index as x)
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (x :: k).
Append as bs cs -> Index cs x -> Either (Index as x) (Index bs x)
`splitIndex` Index bs x
i)

-- | An index pointing to a given item in a prefix is also an index
-- pointing to the same item in the full list.  This "weakens" the bounds
-- of an index, widening the list at the end but preserving the original
-- index.  This is the inverse of 'takeIndex'.
weakenIndex ::
  Prefix as bs ->
  Index as x ->
  Index bs x
weakenIndex :: forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Prefix as bs -> Index as x -> Index bs x
weakenIndex = \case
  Prefix as bs
PreZ -> \case {}
  PreS Prefix as bs
p -> \case
    Index as x
IZ -> Index bs x
Index (x : bs) x
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
    IS Index bs x
i -> Index bs x -> Index (a : bs) x
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS (Prefix as bs -> Index as x -> Index bs x
forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Prefix as bs -> Index as x -> Index bs x
weakenIndex Prefix as bs
p Index as x
Index bs x
i)

-- | An index pointing to a given item in a suffix can be transformed into
-- an index pointing to the same item in the full list.  This is the
-- inverse of 'dropIndex'.
shiftIndex ::
  Suffix as bs ->
  Index as x ->
  Index bs x
shiftIndex :: forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Suffix as bs -> Index as x -> Index bs x
shiftIndex = \case
  Suffix as bs
SufZ -> Index as x -> Index as x
Index as x -> Index bs x
forall a. a -> a
id
  SufS Suffix as bs
s -> Index bs x -> Index bs x
Index bs x -> Index (b : bs) x
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS (Index bs x -> Index bs x)
-> (Index as x -> Index bs x) -> Index as x -> Index bs x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Suffix as bs -> Index as x -> Index bs x
forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Suffix as bs -> Index as x -> Index bs x
shiftIndex Suffix as bs
s

-- | A @'Interleave' as bs cs@ witnesses that @cs@ is @as@ interleaved with
-- @bs@. It is constructed by selectively zipping items from @as@ and @bs@
-- together, like mergesort or riffle shuffle.
--
-- You construct an 'Interleave' from @as@ and @bs@ by picking "which item" from
-- @as@ and @bs@ to add to @cs@.
--
-- Some examples:
--
-- @
-- IntL (IntL (IntR (IntR IntZ))) :: Interleave '[1,2] '[3,4] '[1,2,3,4]
-- IntR (IntR (IntL (IntL IntZ))) :: Interleave '[1,2] '[3,4] '[3,4,1,2]
-- IntL (IntR (IntL (IntR IntZ))) :: Interleave '[1,2] '[3,4] '[1,3,2,4]
-- IntR (IntL (IntR (IntL IntZ))) :: Interleave '[1,2] '[3,4] '[3,1,4,2]
-- @
--
-- @since 0.1.1.0
data Interleave :: [k] -> [k] -> [k] -> Type where
  IntZ :: Interleave '[] '[] '[]
  IntL :: Interleave as bs cs -> Interleave (a ': as) bs (a ': cs)
  IntR :: Interleave as bs cs -> Interleave as (b ': bs) (b ': cs)

deriving instance Show (Interleave as bs cs)

-- | A type-level predicate that a given list is the "interleave" of @as@
-- and @bs@.
--
-- @since 0.1.2.0
type IsInterleave as bs = TyPred (Interleave as bs)

instance Auto (IsInterleave '[] '[]) '[] where
  auto :: IsInterleave '[] '[] @@ '[]
auto = IsInterleave '[] '[] @@ '[]
Interleave '[] '[] '[]
forall {k}. Interleave '[] '[] '[]
IntZ

-- | Prefers 'IntL' if there is an ambiguity.
instance Auto (IsInterleave as bs) cs => Auto (IsInterleave (a ': as) bs) (a ': cs) where
  auto :: IsInterleave (a : as) bs @@ (a : cs)
auto = Interleave as bs cs -> Interleave (a : as) bs (a : cs)
forall {k} (bs :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Interleave bs bs b -> Interleave (a : bs) bs (a : b)
IntL (forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsInterleave as bs) @cs)

instance {-# INCOHERENT #-} Auto (IsInterleave as bs) cs => Auto (IsInterleave as (b ': bs)) (b ': cs) where
  auto :: IsInterleave as (b : bs) @@ (b : cs)
auto = Interleave as bs cs -> Interleave as (b : bs) (b : cs)
forall {k} (as :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Interleave as bs b -> Interleave as (a : bs) (a : b)
IntR (forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsInterleave as bs) @cs)

instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsInterleave as bs) where
  decide :: Decide (IsInterleave as bs)
decide = case forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as of
    Sing as
SList as
SNil -> case forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @bs of
      Sing bs
SList bs
SNil -> \case
        Sing a
SList a
SNil -> Interleave '[] '[] '[] -> Decision (Interleave '[] '[] '[])
forall a. a -> Decision a
Proved Interleave '[] '[] '[]
forall {k}. Interleave '[] '[] '[]
IntZ
        Sing n1
_ `SCons` Sing n2
_ -> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInterleave as bs @@ a)
 -> Decision (IsInterleave as bs @@ a))
-> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case {}
      Sing n1
y `SCons` (Sing n2
Sing :: Sing bs') -> \case
        Sing n1
z `SCons` (Sing n2
zs :: Sing cs') -> case Sing n1
y Sing n1 -> Sing n1 -> Decision (n1 :~: n1)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
z of
          Proved n1 :~: n1
Refl -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: [k] ~> *). Decidable p => Decide p
decide @(IsInterleave '[] bs') Sing n2
zs of
            Proved IsInterleave '[] n2 @@ n2
i -> (IsInterleave as bs @@ a) -> Decision (IsInterleave as bs @@ a)
forall a. a -> Decision a
Proved ((IsInterleave as bs @@ a) -> Decision (IsInterleave as bs @@ a))
-> (IsInterleave as bs @@ a) -> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ Interleave '[] n2 n2 -> Interleave '[] (n1 : n2) (n1 : n2)
forall {k} (as :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Interleave as bs b -> Interleave as (a : bs) (a : b)
IntR IsInterleave '[] n2 @@ n2
Interleave '[] n2 n2
i
            Disproved Refuted (IsInterleave '[] n2 @@ n2)
v -> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInterleave as bs @@ a)
 -> Decision (IsInterleave as bs @@ a))
-> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
              IntR Interleave '[] bs cs
i -> Refuted (IsInterleave '[] n2 @@ n2)
v IsInterleave '[] n2 @@ n2
Interleave '[] bs cs
i
          Disproved Refuted (n1 :~: n1)
v -> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInterleave as bs @@ a)
 -> Decision (IsInterleave as bs @@ a))
-> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
            IntR Interleave '[] bs cs
_ -> Refuted (n1 :~: n1)
v n1 :~: n1
n1 :~: n1
forall {k} (a :: k). a :~: a
Refl
        Sing a
SList a
SNil -> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInterleave as bs @@ a)
 -> Decision (IsInterleave as bs @@ a))
-> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case {}
    Sing n1
x `SCons` (Sing n2
Sing :: Sing as') -> case forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @bs of
      Sing bs
SList bs
SNil -> \case
        Sing n1
z `SCons` (Sing n2
zs :: Sing cs') -> case Sing n1
x Sing n1 -> Sing n1 -> Decision (n1 :~: n1)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
z of
          Proved n1 :~: n1
Refl -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: [k] ~> *). Decidable p => Decide p
decide @(IsInterleave as' '[]) Sing n2
zs of
            Proved IsInterleave n2 '[] @@ n2
i -> (IsInterleave as bs @@ a) -> Decision (IsInterleave as bs @@ a)
forall a. a -> Decision a
Proved ((IsInterleave as bs @@ a) -> Decision (IsInterleave as bs @@ a))
-> (IsInterleave as bs @@ a) -> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ Interleave n2 '[] n2 -> Interleave (n1 : n2) '[] (n1 : n2)
forall {k} (bs :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Interleave bs bs b -> Interleave (a : bs) bs (a : b)
IntL IsInterleave n2 '[] @@ n2
Interleave n2 '[] n2
i
            Disproved Refuted (IsInterleave n2 '[] @@ n2)
v -> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInterleave as bs @@ a)
 -> Decision (IsInterleave as bs @@ a))
-> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
              IntL Interleave as '[] cs
i -> Refuted (IsInterleave n2 '[] @@ n2)
v IsInterleave n2 '[] @@ n2
Interleave as '[] cs
i
          Disproved Refuted (n1 :~: n1)
v -> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInterleave as bs @@ a)
 -> Decision (IsInterleave as bs @@ a))
-> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
            IntL Interleave as '[] cs
_ -> Refuted (n1 :~: n1)
v n1 :~: n1
n1 :~: n1
forall {k} (a :: k). a :~: a
Refl
        Sing a
SList a
SNil -> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInterleave as bs @@ a)
 -> Decision (IsInterleave as bs @@ a))
-> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case {}
      Sing n1
y `SCons` (Sing n2
Sing :: Sing bs') -> \case
        Sing a
SList a
SNil -> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInterleave as bs @@ a)
 -> Decision (IsInterleave as bs @@ a))
-> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case {}
        Sing n1
z `SCons` (Sing n2
zs :: Sing cs') -> case Sing n1
x Sing n1 -> Sing n1 -> Decision (n1 :~: n1)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
z of
          Proved n1 :~: n1
Refl -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: [k] ~> *). Decidable p => Decide p
decide @(IsInterleave as' bs) Sing n2
zs of
            Proved IsInterleave n2 bs @@ n2
i -> (IsInterleave as bs @@ a) -> Decision (IsInterleave as bs @@ a)
forall a. a -> Decision a
Proved ((IsInterleave as bs @@ a) -> Decision (IsInterleave as bs @@ a))
-> (IsInterleave as bs @@ a) -> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ Interleave n2 (n1 : n2) n2
-> Interleave (n1 : n2) (n1 : n2) (n1 : n2)
forall {k} (bs :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Interleave bs bs b -> Interleave (a : bs) bs (a : b)
IntL IsInterleave n2 bs @@ n2
Interleave n2 (n1 : n2) n2
i
            Disproved Refuted (IsInterleave n2 bs @@ n2)
v -> case Sing n1
y Sing n1 -> Sing n1 -> Decision (n1 :~: n1)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
Sing n1
z of
              Proved n1 :~: n1
Refl -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: [k] ~> *). Decidable p => Decide p
decide @(IsInterleave as bs') Sing n2
zs of
                Proved IsInterleave as n2 @@ n2
i -> (IsInterleave as bs @@ a) -> Decision (IsInterleave as bs @@ a)
forall a. a -> Decision a
Proved ((IsInterleave as bs @@ a) -> Decision (IsInterleave as bs @@ a))
-> (IsInterleave as bs @@ a) -> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ Interleave (n1 : n2) n2 n2
-> Interleave (n1 : n2) (n1 : n2) (n1 : n2)
forall {k} (as :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Interleave as bs b -> Interleave as (a : bs) (a : b)
IntR IsInterleave as n2 @@ n2
Interleave (n1 : n2) n2 n2
i
                Disproved Refuted (IsInterleave as n2 @@ n2)
u -> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInterleave as bs @@ a)
 -> Decision (IsInterleave as bs @@ a))
-> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
                  IntL Interleave as (n1 : n2) cs
i -> Refuted (IsInterleave n2 bs @@ n2)
v IsInterleave n2 bs @@ n2
Interleave as (n1 : n2) cs
i
                  IntR Interleave (n1 : n2) bs cs
i -> Refuted (IsInterleave as n2 @@ n2)
u IsInterleave as n2 @@ n2
Interleave (n1 : n2) bs cs
i
              Disproved Refuted (n1 :~: n1)
u -> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInterleave as bs @@ a)
 -> Decision (IsInterleave as bs @@ a))
-> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
                IntL Interleave as (n1 : n2) cs
i -> Refuted (IsInterleave n2 bs @@ n2)
v IsInterleave n2 bs @@ n2
Interleave as (n1 : n2) cs
i
                IntR Interleave (n1 : n2) bs cs
_ -> Refuted (n1 :~: n1)
u n1 :~: n1
n1 :~: n1
forall {k} (a :: k). a :~: a
Refl
          Disproved Refuted (n1 :~: n1)
v -> case Sing n1
y Sing n1 -> Sing n1 -> Decision (n1 :~: n1)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
z of
            Proved n1 :~: n1
Refl -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: [k] ~> *). Decidable p => Decide p
decide @(IsInterleave as bs') Sing n2
zs of
              Proved IsInterleave as n2 @@ n2
i -> (IsInterleave as bs @@ a) -> Decision (IsInterleave as bs @@ a)
forall a. a -> Decision a
Proved ((IsInterleave as bs @@ a) -> Decision (IsInterleave as bs @@ a))
-> (IsInterleave as bs @@ a) -> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ Interleave (n1 : n2) n2 n2
-> Interleave (n1 : n2) (n1 : n2) (n1 : n2)
forall {k} (as :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Interleave as bs b -> Interleave as (a : bs) (a : b)
IntR IsInterleave as n2 @@ n2
Interleave (n1 : n2) n2 n2
i
              Disproved Refuted (IsInterleave as n2 @@ n2)
u -> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInterleave as bs @@ a)
 -> Decision (IsInterleave as bs @@ a))
-> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
                IntL Interleave as (n1 : n2) cs
_ -> Refuted (n1 :~: n1)
v n1 :~: n1
n1 :~: n1
forall {k} (a :: k). a :~: a
Refl
                IntR Interleave (n1 : n2) bs cs
i -> Refuted (IsInterleave as n2 @@ n2)
u IsInterleave as n2 @@ n2
Interleave (n1 : n2) bs cs
i
            Disproved Refuted (n1 :~: n1)
u -> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInterleave as bs @@ a)
 -> Decision (IsInterleave as bs @@ a))
-> Refuted (IsInterleave as bs @@ a)
-> Decision (IsInterleave as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
              IntL Interleave as (n1 : n2) cs
_ -> Refuted (n1 :~: n1)
v n1 :~: n1
n1 :~: n1
forall {k} (a :: k). a :~: a
Refl
              IntR Interleave (n1 : n2) bs cs
_ -> Refuted (n1 :~: n1)
u n1 :~: n1
n1 :~: n1
forall {k} (a :: k). a :~: a
Refl

-- | Automatically generate an 'Interleave' if @as@, @bs@, and @cs@ are
-- known statically.
--
-- Prefers the left side if there is an ambiguity:
--
-- @
-- IntL (IntR (IntR IntZ) :: Interleave '[1] '[1,2] '[1,1,2]
-- IntR (IntL (IntR IntZ) :: Interleave '[1] '[1,2] '[1,1,2]
--
-- autoInterleave @'[1] @'[1,2] '[1,1,2] == IntL (IntR (IntR IntZ)
-- @
--
-- @since 0.1.2.0
autoInterleave :: forall as bs cs. Auto (IsInterleave as bs) cs => Interleave as bs cs
autoInterleave :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Auto (IsInterleave as bs) cs =>
Interleave as bs cs
autoInterleave = forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsInterleave as bs) @cs

-- | Given two 'Rec's, interleave the two to create a combined 'Rec'.
--
-- @since 0.1.1.0
interleaveRec :: Interleave as bs cs -> Rec f as -> Rec f bs -> Rec f cs
interleaveRec :: forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]) (f :: u -> *).
Interleave as bs cs -> Rec f as -> Rec f bs -> Rec f cs
interleaveRec = \case
  Interleave as bs cs
IntZ -> \case
    Rec f as
RNil -> \case
      Rec f bs
RNil -> Rec f cs
Rec f '[]
forall {u} (a :: u -> *). Rec a '[]
RNil
  IntL Interleave as bs cs
m -> \case
    f r
x :& Rec f rs
xs -> \Rec f bs
ys -> f r
x f r -> Rec f cs -> Rec f (r : cs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Interleave as bs cs -> Rec f as -> Rec f bs -> Rec f cs
forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]) (f :: u -> *).
Interleave as bs cs -> Rec f as -> Rec f bs -> Rec f cs
interleaveRec Interleave as bs cs
m Rec f as
Rec f rs
xs Rec f bs
ys
  IntR Interleave as bs cs
m -> \Rec f as
xs -> \case
    f r
y :& Rec f rs
ys -> f r
y f r -> Rec f cs -> Rec f (r : cs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Interleave as bs cs -> Rec f as -> Rec f bs -> Rec f cs
forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]) (f :: u -> *).
Interleave as bs cs -> Rec f as -> Rec f bs -> Rec f cs
interleaveRec Interleave as bs cs
m Rec f as
xs Rec f bs
Rec f rs
ys

-- | Given a 'Rec', disinterleave it into two 'Rec's corresponding to an
-- 'Interleave'.
--
-- @since 0.1.1.0
unweaveRec :: Interleave as bs cs -> Rec f cs -> (Rec f as, Rec f bs)
unweaveRec :: forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]) (f :: u -> *).
Interleave as bs cs -> Rec f cs -> (Rec f as, Rec f bs)
unweaveRec = \case
  Interleave as bs cs
IntZ -> \case
    Rec f cs
RNil -> (Rec f as
Rec f '[]
forall {u} (a :: u -> *). Rec a '[]
RNil, Rec f bs
Rec f '[]
forall {u} (a :: u -> *). Rec a '[]
RNil)
  IntL Interleave as bs cs
m -> \case
    f r
x :& Rec f rs
xs -> (Rec f as -> Rec f as)
-> (Rec f as, Rec f bs) -> (Rec f as, Rec f bs)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (f r
x f r -> Rec f as -> Rec f (r : as)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) ((Rec f as, Rec f bs) -> (Rec f as, Rec f bs))
-> (Rec f rs -> (Rec f as, Rec f bs))
-> Rec f rs
-> (Rec f as, Rec f bs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interleave as bs rs -> Rec f rs -> (Rec f as, Rec f bs)
forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]) (f :: u -> *).
Interleave as bs cs -> Rec f cs -> (Rec f as, Rec f bs)
unweaveRec Interleave as bs cs
Interleave as bs rs
m (Rec f rs -> (Rec f as, Rec f bs))
-> Rec f rs -> (Rec f as, Rec f bs)
forall a b. (a -> b) -> a -> b
$ Rec f rs
xs
  IntR Interleave as bs cs
m -> \case
    f r
x :& Rec f rs
xs -> (Rec f bs -> Rec f bs)
-> (Rec f as, Rec f bs) -> (Rec f as, Rec f bs)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (f r
x f r -> Rec f bs -> Rec f (r : bs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) ((Rec f as, Rec f bs) -> (Rec f as, Rec f bs))
-> (Rec f rs -> (Rec f as, Rec f bs))
-> Rec f rs
-> (Rec f as, Rec f bs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interleave as bs rs -> Rec f rs -> (Rec f as, Rec f bs)
forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]) (f :: u -> *).
Interleave as bs cs -> Rec f cs -> (Rec f as, Rec f bs)
unweaveRec Interleave as bs cs
Interleave as bs rs
m (Rec f rs -> (Rec f as, Rec f bs))
-> Rec f rs -> (Rec f as, Rec f bs)
forall a b. (a -> b) -> a -> b
$ Rec f rs
xs

-- | Turn an 'Interleave' into a 'Rec' of indices from either sublist.
--
-- Warning: O(n^2)
--
-- @since 0.1.2.0
interleavedIxes :: Interleave as bs cs -> Rec (Index as :+: Index bs) cs
interleavedIxes :: forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]).
Interleave as bs cs -> Rec (Index as :+: Index bs) cs
interleavedIxes = \case
  Interleave as bs cs
IntZ -> Rec (Index as :+: Index bs) cs
Rec (Index as :+: Index bs) '[]
forall {u} (a :: u -> *). Rec a '[]
RNil
  IntL Interleave as bs cs
i ->
    Index as a -> (:+:) (Index as) (Index bs) a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 Index as a
Index (a : as) a
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
      (:+:) (Index as) (Index bs) a
-> Rec (Index as :+: Index bs) cs
-> Rec (Index as :+: Index bs) (a : cs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& (forall (x :: u).
 (:+:) (Index as) (Index bs) x -> (:+:) (Index as) (Index bs) x)
-> Rec (Index as :+: Index bs) cs -> Rec (Index as :+: Index bs) cs
forall {u} (f :: u -> *) (g :: u -> *) (rs :: [u]).
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
VR.rmap
        (\case L1 Index as x
i' -> Index as x -> (:+:) (Index as) (Index bs) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (Index as x -> Index (a : as) x
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS Index as x
i'); R1 Index bs x
j -> Index bs x -> (:+:) (Index as) (Index bs) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 Index bs x
j)
        (Interleave as bs cs -> Rec (Index as :+: Index bs) cs
forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]).
Interleave as bs cs -> Rec (Index as :+: Index bs) cs
interleavedIxes Interleave as bs cs
i)
  IntR Interleave as bs cs
j ->
    Index bs b -> (:+:) (Index as) (Index bs) b
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 Index bs b
Index (b : bs) b
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
      (:+:) (Index as) (Index bs) b
-> Rec (Index as :+: Index bs) cs
-> Rec (Index as :+: Index bs) (b : cs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& (forall (x :: u).
 (:+:) (Index as) (Index bs) x -> (:+:) (Index as) (Index bs) x)
-> Rec (Index as :+: Index bs) cs -> Rec (Index as :+: Index bs) cs
forall {u} (f :: u -> *) (g :: u -> *) (rs :: [u]).
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
VR.rmap
        (\case L1 Index as x
i -> Index as x -> (:+:) (Index as) (Index bs) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 Index as x
i; R1 Index bs x
j' -> Index bs x -> (:+:) (Index as) (Index bs) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (Index bs x -> Index (b : bs) x
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS Index bs x
j'))
        (Interleave as bs cs -> Rec (Index as :+: Index bs) cs
forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]).
Interleave as bs cs -> Rec (Index as :+: Index bs) cs
interleavedIxes Interleave as bs cs
j)

-- | Interleave an 'Index' on @as@ into a full index on @cs@, which is @as@
-- interleaved with @bs@.
--
-- @since 0.1.1.0
injectIndexL :: Interleave as bs cs -> Index as a -> Index cs a
injectIndexL :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (a :: k).
Interleave as bs cs -> Index as a -> Index cs a
injectIndexL = \case
  Interleave as bs cs
IntZ -> \case {}
  IntL Interleave as bs cs
m -> \case
    Index as a
IZ -> Index cs a
Index (a : cs) a
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
    IS Index bs a
i -> Index cs a -> Index (a : cs) a
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS (Interleave as bs cs -> Index as a -> Index cs a
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (a :: k).
Interleave as bs cs -> Index as a -> Index cs a
injectIndexL Interleave as bs cs
m Index as a
Index bs a
i)
  IntR Interleave as bs cs
m -> Index cs a -> Index cs a
Index cs a -> Index (b : cs) a
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS (Index cs a -> Index cs a)
-> (Index as a -> Index cs a) -> Index as a -> Index cs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interleave as bs cs -> Index as a -> Index cs a
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (a :: k).
Interleave as bs cs -> Index as a -> Index cs a
injectIndexL Interleave as bs cs
m

-- | Interleave an 'Index' on @bs@ into a full index on @cs@, which is @as@
-- interleaved with @bs@.
--
-- @since 0.1.1.0
injectIndexR :: Interleave as bs cs -> Index bs b -> Index cs b
injectIndexR :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (b :: k).
Interleave as bs cs -> Index bs b -> Index cs b
injectIndexR = \case
  Interleave as bs cs
IntZ -> \case {}
  IntL Interleave as bs cs
m -> Index cs b -> Index cs b
Index cs b -> Index (a : cs) b
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS (Index cs b -> Index cs b)
-> (Index bs b -> Index cs b) -> Index bs b -> Index cs b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interleave as bs cs -> Index bs b -> Index cs b
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (b :: k).
Interleave as bs cs -> Index bs b -> Index cs b
injectIndexR Interleave as bs cs
m
  IntR Interleave as bs cs
m -> \case
    Index bs b
IZ -> Index cs b
Index (b : cs) b
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
    IS Index bs b
i -> Index cs b -> Index (b : cs) b
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS (Interleave as bs cs -> Index bs b -> Index cs b
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (b :: k).
Interleave as bs cs -> Index bs b -> Index cs b
injectIndexR Interleave as bs cs
m Index bs b
Index bs b
i)

-- | Given an index on @cs@, disinterleave it into either an index on @as@
-- or on @bs@.
--
-- @since 0.1.1.0
unweaveIndex :: Interleave as bs cs -> Index cs c -> Either (Index as c) (Index bs c)
unweaveIndex :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (c :: k).
Interleave as bs cs
-> Index cs c -> Either (Index as c) (Index bs c)
unweaveIndex = \case
  Interleave as bs cs
IntZ -> \case {}
  IntL Interleave as bs cs
m -> \case
    Index cs c
IZ -> Index as c -> Either (Index as c) (Index bs c)
forall a b. a -> Either a b
Left Index as c
Index (c : as) c
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
    IS Index bs c
i -> (Index as c -> Index as c)
-> Either (Index as c) (Index bs c)
-> Either (Index as c) (Index bs c)
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Index as c -> Index as c
Index as c -> Index (a : as) c
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS (Either (Index as c) (Index bs c)
 -> Either (Index as c) (Index bs c))
-> Either (Index as c) (Index bs c)
-> Either (Index as c) (Index bs c)
forall a b. (a -> b) -> a -> b
$ Interleave as bs cs
-> Index cs c -> Either (Index as c) (Index bs c)
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (c :: k).
Interleave as bs cs
-> Index cs c -> Either (Index as c) (Index bs c)
unweaveIndex Interleave as bs cs
m Index cs c
Index bs c
i
  IntR Interleave as bs cs
m -> \case
    Index cs c
IZ -> Index bs c -> Either (Index as c) (Index bs c)
forall a b. b -> Either a b
Right Index bs c
Index (c : bs) c
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
    IS Index bs c
i -> (Index bs c -> Index bs c)
-> Either (Index as c) (Index bs c)
-> Either (Index as c) (Index bs c)
forall b c a. (b -> c) -> Either a b -> Either a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Index bs c -> Index bs c
Index bs c -> Index (b : bs) c
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS (Either (Index as c) (Index bs c)
 -> Either (Index as c) (Index bs c))
-> Either (Index as c) (Index bs c)
-> Either (Index as c) (Index bs c)
forall a b. (a -> b) -> a -> b
$ Interleave as bs cs
-> Index cs c -> Either (Index as c) (Index bs c)
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]) (c :: k).
Interleave as bs cs
-> Index cs c -> Either (Index as c) (Index bs c)
unweaveIndex Interleave as bs cs
m Index cs c
Index bs c
i

-- | Witness an isomorphism between 'Rec' and two parts that interleave it.
--
-- Read this type signature as:
--
-- @
-- 'interleaveRecIso'
--     :: Interleave as  bs  cs
--     -> Iso' (Rec f cs) (Rec f as, Rec f bs)
-- @
--
-- This can be used with the combinators from the lens library.
--
-- The 'Interleave' tells how to unweave the 'Rec'.
--
-- @since 0.1.1.0
interleaveRecIso ::
  (Profunctor p, Functor f) =>
  Interleave as bs cs ->
  p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs)) ->
  p (Rec g cs) (f (Rec g cs))
interleaveRecIso :: forall {u} (p :: * -> * -> *) (f :: * -> *) (as :: [u]) (bs :: [u])
       (cs :: [u]) (g :: u -> *).
(Profunctor p, Functor f) =>
Interleave as bs cs
-> p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs))
-> p (Rec g cs) (f (Rec g cs))
interleaveRecIso Interleave as bs cs
m = (Rec g cs -> (Rec g as, Rec g bs))
-> (f (Rec g as, Rec g bs) -> f (Rec g cs))
-> p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs))
-> p (Rec g cs) (f (Rec g cs))
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (Interleave as bs cs -> Rec g cs -> (Rec g as, Rec g bs)
forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]) (f :: u -> *).
Interleave as bs cs -> Rec f cs -> (Rec f as, Rec f bs)
unweaveRec Interleave as bs cs
m) ((((Rec g as, Rec g bs) -> Rec g cs)
-> f (Rec g as, Rec g bs) -> f (Rec g cs)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Rec g as, Rec g bs) -> Rec g cs)
 -> f (Rec g as, Rec g bs) -> f (Rec g cs))
-> ((Rec g as -> Rec g bs -> Rec g cs)
    -> (Rec g as, Rec g bs) -> Rec g cs)
-> (Rec g as -> Rec g bs -> Rec g cs)
-> f (Rec g as, Rec g bs)
-> f (Rec g cs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rec g as -> Rec g bs -> Rec g cs)
-> (Rec g as, Rec g bs) -> Rec g cs
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry) (Interleave as bs cs -> Rec g as -> Rec g bs -> Rec g cs
forall {u} (as :: [u]) (bs :: [u]) (cs :: [u]) (f :: u -> *).
Interleave as bs cs -> Rec f as -> Rec f bs -> Rec f cs
interleaveRec Interleave as bs cs
m))

-- | Swap the two halves of an 'Interleave'.
--
-- @since 0.1.3.0
swapInterleave ::
  Interleave as bs cs ->
  Interleave bs as cs
swapInterleave :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Interleave as bs cs -> Interleave bs as cs
swapInterleave = \case
  Interleave as bs cs
IntZ -> Interleave bs as cs
Interleave '[] '[] '[]
forall {k}. Interleave '[] '[] '[]
IntZ
  IntL Interleave as bs cs
i -> Interleave bs as cs -> Interleave bs (a : as) (a : cs)
forall {k} (as :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Interleave as bs b -> Interleave as (a : bs) (a : b)
IntR (Interleave bs as cs -> Interleave bs (a : as) (a : cs))
-> Interleave bs as cs -> Interleave bs (a : as) (a : cs)
forall a b. (a -> b) -> a -> b
$ Interleave as bs cs -> Interleave bs as cs
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Interleave as bs cs -> Interleave bs as cs
swapInterleave Interleave as bs cs
i
  IntR Interleave as bs cs
i -> Interleave bs as cs -> Interleave (b : bs) as (b : cs)
forall {k} (bs :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Interleave bs bs b -> Interleave (a : bs) bs (a : b)
IntL (Interleave bs as cs -> Interleave (b : bs) as (b : cs))
-> Interleave bs as cs -> Interleave (b : bs) as (b : cs)
forall a b. (a -> b) -> a -> b
$ Interleave as bs cs -> Interleave bs as cs
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Interleave as bs cs -> Interleave bs as cs
swapInterleave Interleave as bs cs
i

-- | Get the 'Shape's associated with an 'Interleave'.
--
-- @since 0.1.3.0
interleaveShapes ::
  Interleave as bs cs ->
  (Shape [] as, Shape [] bs, Shape [] cs)
interleaveShapes :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Interleave as bs cs -> (Shape [] as, Shape [] bs, Shape [] cs)
interleaveShapes = \case
  Interleave as bs cs
IntZ -> (Rec Proxy '[]
Shape [] as
forall {u} (a :: u -> *). Rec a '[]
RNil, Rec Proxy '[]
Shape [] bs
forall {u} (a :: u -> *). Rec a '[]
RNil, Rec Proxy '[]
Shape [] cs
forall {u} (a :: u -> *). Rec a '[]
RNil)
  IntL Interleave as bs cs
i ->
    let (Shape [] as
as, Shape [] bs
bs, Shape [] cs
cs) = Interleave as bs cs -> (Shape [] as, Shape [] bs, Shape [] cs)
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Interleave as bs cs -> (Shape [] as, Shape [] bs, Shape [] cs)
interleaveShapes Interleave as bs cs
i
     in (Proxy a
forall {k} (t :: k). Proxy t
Proxy Proxy a -> Rec Proxy as -> Rec Proxy (a : as)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Proxy as
Shape [] as
as, Shape [] bs
bs, Proxy a
forall {k} (t :: k). Proxy t
Proxy Proxy a -> Rec Proxy cs -> Rec Proxy (a : cs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Proxy cs
Shape [] cs
cs)
  IntR Interleave as bs cs
i ->
    let (Shape [] as
as, Shape [] bs
bs, Shape [] cs
cs) = Interleave as bs cs -> (Shape [] as, Shape [] bs, Shape [] cs)
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Interleave as bs cs -> (Shape [] as, Shape [] bs, Shape [] cs)
interleaveShapes Interleave as bs cs
i
     in (Shape [] as
as, Proxy b
forall {k} (t :: k). Proxy t
Proxy Proxy b -> Rec Proxy bs -> Rec Proxy (b : bs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Proxy bs
Shape [] bs
bs, Proxy b
forall {k} (t :: k). Proxy t
Proxy Proxy b -> Rec Proxy cs -> Rec Proxy (b : cs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Proxy cs
Shape [] cs
cs)

-- | A @'Subset' as bs@ witnesses that @as@ is some subset of @bs@, with
-- items in the same order.  It is constructed by specifying
-- what item to include or exclude in @bs@ from @as@.  It is essentially
-- 'Interleave', but without one of the two initial parameters.
--
-- You construct an 'Subset' from @cs@ by picking "which item" from
-- @bs@ to add to @as@.
--
-- Some examples:
--
-- @
-- SubsetNo  (SubsetNo  (SubsetNo  SubsetNil)) :: Subset '[]      '[1,2,3]
-- SubsetYes (SubsetNo  (SubsetNo  SubsetNil)) :: Subset '[1]     '[1,2,3]
-- SubsetNo  (SubsetNo  (SubsetYes SubsetNil)) :: Subset '[3]     '[1,2,3]
-- SubsetYes (SubsetNo  (SubsetYes SubsetNil)) :: Subset '[1,3]   '[1,2,3]
-- SubsetYes (SubsetYes (SubsetYes SubsetNil)) :: Subset '[1,2,3] '[1,2,3]
-- @
--
-- @since 0.1.3.0
data Subset :: [k] -> [k] -> Type where
  SubsetNil :: Subset '[] '[]
  SubsetNo :: Subset as bs -> Subset as (b ': bs)
  SubsetYes :: Subset as bs -> Subset (a ': as) (a ': bs)

-- | Drop the right side of an 'Interleave', leaving only the left side.
interleaveLToSubset :: Interleave as bs cs -> Subset as cs
interleaveLToSubset :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Interleave as bs cs -> Subset as cs
interleaveLToSubset = \case
  Interleave as bs cs
IntZ -> Subset as cs
Subset '[] '[]
forall {k}. Subset '[] '[]
SubsetNil
  IntL Interleave as bs cs
i -> Subset as cs -> Subset as cs
Subset as cs -> Subset (a : as) (a : cs)
forall {k} (bs :: [k]) (b :: [k]) (a :: k).
Subset bs b -> Subset (a : bs) (a : b)
SubsetYes (Subset as cs -> Subset as cs)
-> (Interleave as bs cs -> Subset as cs)
-> Interleave as bs cs
-> Subset as cs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interleave as bs cs -> Subset as cs
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Interleave as bs cs -> Subset as cs
interleaveLToSubset (Interleave as bs cs -> Subset as cs)
-> Interleave as bs cs -> Subset as cs
forall a b. (a -> b) -> a -> b
$ Interleave as bs cs
i
  IntR Interleave as bs cs
i -> Subset as cs -> Subset as cs
Subset as cs -> Subset as (b : cs)
forall {k} (as :: [k]) (bs :: [k]) (b :: k).
Subset as bs -> Subset as (b : bs)
SubsetNo (Subset as cs -> Subset as cs)
-> (Interleave as bs cs -> Subset as cs)
-> Interleave as bs cs
-> Subset as cs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interleave as bs cs -> Subset as cs
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Interleave as bs cs -> Subset as cs
interleaveLToSubset (Interleave as bs cs -> Subset as cs)
-> Interleave as bs cs -> Subset as cs
forall a b. (a -> b) -> a -> b
$ Interleave as bs cs
i

-- | Drop the left side of an 'Interleave', leaving only the right side.
interleaveRToSubset :: Interleave as bs cs -> Subset bs cs
interleaveRToSubset :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Interleave as bs cs -> Subset bs cs
interleaveRToSubset = \case
  Interleave as bs cs
IntZ -> Subset bs cs
Subset '[] '[]
forall {k}. Subset '[] '[]
SubsetNil
  IntL Interleave as bs cs
i -> Subset bs cs -> Subset bs cs
Subset bs cs -> Subset bs (a : cs)
forall {k} (as :: [k]) (bs :: [k]) (b :: k).
Subset as bs -> Subset as (b : bs)
SubsetNo (Subset bs cs -> Subset bs cs)
-> (Interleave as bs cs -> Subset bs cs)
-> Interleave as bs cs
-> Subset bs cs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interleave as bs cs -> Subset bs cs
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Interleave as bs cs -> Subset bs cs
interleaveRToSubset (Interleave as bs cs -> Subset bs cs)
-> Interleave as bs cs -> Subset bs cs
forall a b. (a -> b) -> a -> b
$ Interleave as bs cs
i
  IntR Interleave as bs cs
i -> Subset bs cs -> Subset bs cs
Subset bs cs -> Subset (b : bs) (b : cs)
forall {k} (bs :: [k]) (b :: [k]) (a :: k).
Subset bs b -> Subset (a : bs) (a : b)
SubsetYes (Subset bs cs -> Subset bs cs)
-> (Interleave as bs cs -> Subset bs cs)
-> Interleave as bs cs
-> Subset bs cs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interleave as bs cs -> Subset bs cs
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Interleave as bs cs -> Subset bs cs
interleaveRToSubset (Interleave as bs cs -> Subset bs cs)
-> Interleave as bs cs -> Subset bs cs
forall a b. (a -> b) -> a -> b
$ Interleave as bs cs
i

-- | Convert a 'Subset' into an left 'Interleave', recovering the dropped
-- items.
subsetToInterleaveL ::
  Subset as cs ->
  (forall bs. Interleave as bs cs -> r) ->
  r
subsetToInterleaveL :: forall {k} (as :: [k]) (cs :: [k]) r.
Subset as cs -> (forall (bs :: [k]). Interleave as bs cs -> r) -> r
subsetToInterleaveL = \case
  Subset as cs
SubsetNil -> \forall (bs :: [k]). Interleave as bs cs -> r
f -> Interleave as '[] cs -> r
forall (bs :: [k]). Interleave as bs cs -> r
f Interleave as '[] cs
Interleave '[] '[] '[]
forall {k}. Interleave '[] '[] '[]
IntZ
  SubsetNo Subset as bs
s -> \forall (bs :: [k]). Interleave as bs cs -> r
f -> Subset as bs -> (forall (bs :: [k]). Interleave as bs bs -> r) -> r
forall {k} (as :: [k]) (cs :: [k]) r.
Subset as cs -> (forall (bs :: [k]). Interleave as bs cs -> r) -> r
subsetToInterleaveL Subset as bs
s (Interleave as (b : bs) cs -> r
forall (bs :: [k]). Interleave as bs cs -> r
f (Interleave as (b : bs) cs -> r)
-> (Interleave as bs bs -> Interleave as (b : bs) cs)
-> Interleave as bs bs
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interleave as bs bs -> Interleave as (b : bs) cs
Interleave as bs bs -> Interleave as (b : bs) (b : bs)
forall {k} (as :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Interleave as bs b -> Interleave as (a : bs) (a : b)
IntR)
  SubsetYes Subset as bs
s -> \forall (bs :: [k]). Interleave as bs cs -> r
f -> Subset as bs -> (forall (bs :: [k]). Interleave as bs bs -> r) -> r
forall {k} (as :: [k]) (cs :: [k]) r.
Subset as cs -> (forall (bs :: [k]). Interleave as bs cs -> r) -> r
subsetToInterleaveL Subset as bs
s (Interleave as bs cs -> r
forall (bs :: [k]). Interleave as bs cs -> r
f (Interleave as bs cs -> r)
-> (Interleave as bs bs -> Interleave as bs cs)
-> Interleave as bs bs
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interleave as bs bs -> Interleave as bs cs
Interleave as bs bs -> Interleave (a : as) bs (a : bs)
forall {k} (bs :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Interleave bs bs b -> Interleave (a : bs) bs (a : b)
IntL)

-- | Convert a 'Subset' into an right 'Interleave', recovering the dropped
-- items.
subsetToInterleaveR ::
  Subset bs cs ->
  (forall as. Interleave as bs cs -> r) ->
  r
subsetToInterleaveR :: forall {k} (bs :: [k]) (cs :: [k]) r.
Subset bs cs -> (forall (as :: [k]). Interleave as bs cs -> r) -> r
subsetToInterleaveR = \case
  Subset bs cs
SubsetNil -> \forall (as :: [k]). Interleave as bs cs -> r
f -> Interleave '[] bs cs -> r
forall (as :: [k]). Interleave as bs cs -> r
f Interleave '[] bs cs
Interleave '[] '[] '[]
forall {k}. Interleave '[] '[] '[]
IntZ
  SubsetNo Subset bs bs
s -> \forall (as :: [k]). Interleave as bs cs -> r
f -> Subset bs bs -> (forall (as :: [k]). Interleave as bs bs -> r) -> r
forall {k} (bs :: [k]) (cs :: [k]) r.
Subset bs cs -> (forall (as :: [k]). Interleave as bs cs -> r) -> r
subsetToInterleaveR Subset bs bs
s (Interleave (b : as) bs cs -> r
forall (as :: [k]). Interleave as bs cs -> r
f (Interleave (b : as) bs cs -> r)
-> (Interleave as bs bs -> Interleave (b : as) bs cs)
-> Interleave as bs bs
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interleave as bs bs -> Interleave (b : as) bs cs
Interleave as bs bs -> Interleave (b : as) bs (b : bs)
forall {k} (bs :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Interleave bs bs b -> Interleave (a : bs) bs (a : b)
IntL)
  SubsetYes Subset as bs
s -> \forall (as :: [k]). Interleave as bs cs -> r
f -> Subset as bs -> (forall (as :: [k]). Interleave as as bs -> r) -> r
forall {k} (bs :: [k]) (cs :: [k]) r.
Subset bs cs -> (forall (as :: [k]). Interleave as bs cs -> r) -> r
subsetToInterleaveR Subset as bs
s (Interleave as bs cs -> r
forall (as :: [k]). Interleave as bs cs -> r
f (Interleave as bs cs -> r)
-> (Interleave as as bs -> Interleave as bs cs)
-> Interleave as as bs
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interleave as as bs -> Interleave as bs cs
Interleave as as bs -> Interleave as (a : as) (a : bs)
forall {k} (as :: [k]) (bs :: [k]) (b :: [k]) (a :: k).
Interleave as bs b -> Interleave as (a : bs) (a : b)
IntR)

-- | @as@ is a subset of @cs@; this function recovers @bs@, the subset of
-- @cs@ that is not @as@.
subsetComplement ::
  Subset as cs ->
  (forall bs. Subset bs cs -> r) ->
  r
subsetComplement :: forall {k} (as :: [k]) (cs :: [k]) r.
Subset as cs -> (forall (bs :: [k]). Subset bs cs -> r) -> r
subsetComplement = \case
  Subset as cs
SubsetNil -> \forall (bs :: [k]). Subset bs cs -> r
f -> Subset '[] cs -> r
forall (bs :: [k]). Subset bs cs -> r
f Subset '[] cs
Subset '[] '[]
forall {k}. Subset '[] '[]
SubsetNil
  SubsetNo Subset as bs
s -> \forall (bs :: [k]). Subset bs cs -> r
f -> Subset as bs -> (forall (bs :: [k]). Subset bs bs -> r) -> r
forall {k} (as :: [k]) (cs :: [k]) r.
Subset as cs -> (forall (bs :: [k]). Subset bs cs -> r) -> r
subsetComplement Subset as bs
s (Subset (b : bs) cs -> r
forall (bs :: [k]). Subset bs cs -> r
f (Subset (b : bs) cs -> r)
-> (Subset bs bs -> Subset (b : bs) cs) -> Subset bs bs -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subset bs bs -> Subset (b : bs) cs
Subset bs bs -> Subset (b : bs) (b : bs)
forall {k} (bs :: [k]) (b :: [k]) (a :: k).
Subset bs b -> Subset (a : bs) (a : b)
SubsetYes)
  SubsetYes Subset as bs
s -> \forall (bs :: [k]). Subset bs cs -> r
f -> Subset as bs -> (forall (bs :: [k]). Subset bs bs -> r) -> r
forall {k} (as :: [k]) (cs :: [k]) r.
Subset as cs -> (forall (bs :: [k]). Subset bs cs -> r) -> r
subsetComplement Subset as bs
s (Subset bs cs -> r
forall (bs :: [k]). Subset bs cs -> r
f (Subset bs cs -> r)
-> (Subset bs bs -> Subset bs cs) -> Subset bs bs -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subset bs bs -> Subset bs cs
Subset bs bs -> Subset bs (a : bs)
forall {k} (as :: [k]) (bs :: [k]) (b :: k).
Subset as bs -> Subset as (b : bs)
SubsetNo)

deriving instance Show (Subset as bs)

-- | A type-level predicate that a given list is a "superset" of @as@, in
-- correct order
--
-- @since 0.1.2.0
type IsSubset as = TyPred (Subset as)

instance Auto (IsSubset '[]) '[] where
  auto :: IsSubset '[] @@ '[]
auto = IsSubset '[] @@ '[]
Subset '[] '[]
forall {k}. Subset '[] '[]
SubsetNil

instance {-# OVERLAPPING #-} Auto (IsSubset as) bs => Auto (IsSubset as) (b ': bs) where
  auto :: IsSubset as @@ (b : bs)
auto = Subset as bs -> Subset as (b : bs)
forall {k} (as :: [k]) (bs :: [k]) (b :: k).
Subset as bs -> Subset as (b : bs)
SubsetNo (forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsSubset as) @bs)

instance {-# OVERLAPPING #-} Auto (IsSubset as) bs => Auto (IsSubset (a ': as)) (a ': bs) where
  auto :: IsSubset (a : as) @@ (a : bs)
auto = Subset as bs -> Subset (a : as) (a : bs)
forall {k} (bs :: [k]) (b :: [k]) (a :: k).
Subset bs b -> Subset (a : bs) (a : b)
SubsetYes (forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsSubset as) @bs)

instance (SDecide k, SingI (as :: [k])) => Decidable (IsSubset as) where
  decide :: Decide (IsSubset as)
decide = case forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as of
    Sing as
SList as
SNil -> \case
      Sing a
SList a
SNil -> Subset '[] '[] -> Decision (Subset '[] '[])
forall a. a -> Decision a
Proved Subset '[] '[]
forall {k}. Subset '[] '[]
SubsetNil
      Sing n1
_ `SCons` Sing n2
ys -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: [k] ~> *). Decidable p => Decide p
decide @(IsSubset '[]) Sing n2
ys of
        Proved IsSubset '[] @@ n2
s -> (IsSubset as @@ a) -> Decision (IsSubset as @@ a)
forall a. a -> Decision a
Proved ((IsSubset as @@ a) -> Decision (IsSubset as @@ a))
-> (IsSubset as @@ a) -> Decision (IsSubset as @@ a)
forall a b. (a -> b) -> a -> b
$ Subset '[] n2 -> Subset '[] (n1 : n2)
forall {k} (as :: [k]) (bs :: [k]) (b :: k).
Subset as bs -> Subset as (b : bs)
SubsetNo IsSubset '[] @@ n2
Subset '[] n2
s
        Disproved Refuted (IsSubset '[] @@ n2)
v -> Refuted (IsSubset as @@ a) -> Decision (IsSubset as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsSubset as @@ a) -> Decision (IsSubset as @@ a))
-> Refuted (IsSubset as @@ a) -> Decision (IsSubset as @@ a)
forall a b. (a -> b) -> a -> b
$ \case
          SubsetNo Subset '[] bs
s -> Refuted (IsSubset '[] @@ n2)
v IsSubset '[] @@ n2
Subset '[] bs
s
    Sing n1
x `SCons` (Sing n2
Sing :: Sing as') -> \case
      Sing a
SList a
SNil -> Refuted (IsSubset as @@ a) -> Decision (IsSubset as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsSubset as @@ a) -> Decision (IsSubset as @@ a))
-> Refuted (IsSubset as @@ a) -> Decision (IsSubset as @@ a)
forall a b. (a -> b) -> a -> b
$ \case {}
      Sing n1
y `SCons` Sing n2
ys -> case Sing n1
x Sing n1 -> Sing n1 -> Decision (n1 :~: n1)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
y of
        Proved n1 :~: n1
Refl -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: [k] ~> *). Decidable p => Decide p
decide @(IsSubset as') Sing n2
ys of
          Proved IsSubset n2 @@ n2
s -> (IsSubset as @@ a) -> Decision (IsSubset as @@ a)
forall a. a -> Decision a
Proved ((IsSubset as @@ a) -> Decision (IsSubset as @@ a))
-> (IsSubset as @@ a) -> Decision (IsSubset as @@ a)
forall a b. (a -> b) -> a -> b
$ Subset n2 n2 -> Subset (n1 : n2) (n1 : n2)
forall {k} (bs :: [k]) (b :: [k]) (a :: k).
Subset bs b -> Subset (a : bs) (a : b)
SubsetYes IsSubset n2 @@ n2
Subset n2 n2
s
          Disproved Refuted (IsSubset n2 @@ n2)
v -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: [k] ~> *). Decidable p => Decide p
decide @(IsSubset as) Sing n2
ys of
            Proved IsSubset as @@ n2
s -> (IsSubset as @@ a) -> Decision (IsSubset as @@ a)
forall a. a -> Decision a
Proved ((IsSubset as @@ a) -> Decision (IsSubset as @@ a))
-> (IsSubset as @@ a) -> Decision (IsSubset as @@ a)
forall a b. (a -> b) -> a -> b
$ Subset (n1 : n2) n2 -> Subset (n1 : n2) (n1 : n2)
forall {k} (as :: [k]) (bs :: [k]) (b :: k).
Subset as bs -> Subset as (b : bs)
SubsetNo IsSubset as @@ n2
Subset (n1 : n2) n2
s
            Disproved Refuted (IsSubset as @@ n2)
u -> Refuted (IsSubset as @@ a) -> Decision (IsSubset as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsSubset as @@ a) -> Decision (IsSubset as @@ a))
-> Refuted (IsSubset as @@ a) -> Decision (IsSubset as @@ a)
forall a b. (a -> b) -> a -> b
$ \case
              SubsetNo Subset (n1 : n2) bs
s -> Refuted (IsSubset as @@ n2)
u IsSubset as @@ n2
Subset (n1 : n2) bs
s
              SubsetYes Subset as bs
s -> Refuted (IsSubset n2 @@ n2)
v IsSubset n2 @@ n2
Subset as bs
s
        Disproved Refuted (n1 :~: n1)
v -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: [k] ~> *). Decidable p => Decide p
decide @(IsSubset as) Sing n2
ys of
          Proved IsSubset as @@ n2
s -> (IsSubset as @@ a) -> Decision (IsSubset as @@ a)
forall a. a -> Decision a
Proved ((IsSubset as @@ a) -> Decision (IsSubset as @@ a))
-> (IsSubset as @@ a) -> Decision (IsSubset as @@ a)
forall a b. (a -> b) -> a -> b
$ Subset (n1 : n2) n2 -> Subset (n1 : n2) (n1 : n2)
forall {k} (as :: [k]) (bs :: [k]) (b :: k).
Subset as bs -> Subset as (b : bs)
SubsetNo IsSubset as @@ n2
Subset (n1 : n2) n2
s
          Disproved Refuted (IsSubset as @@ n2)
u -> Refuted (IsSubset as @@ a) -> Decision (IsSubset as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsSubset as @@ a) -> Decision (IsSubset as @@ a))
-> Refuted (IsSubset as @@ a) -> Decision (IsSubset as @@ a)
forall a b. (a -> b) -> a -> b
$ \case
            SubsetNo Subset (n1 : n2) bs
s -> Refuted (IsSubset as @@ n2)
u IsSubset as @@ n2
Subset (n1 : n2) bs
s
            SubsetYes Subset as bs
_ -> Refuted (n1 :~: n1)
v n1 :~: n1
n1 :~: n1
forall {k} (a :: k). a :~: a
Refl

-- | Automatically generate an 'Subset' if @as@ and @bs@ are known
-- statically.
autoSubset :: forall as bs. Auto (IsSubset as) bs => Subset as bs
autoSubset :: forall {k} (as :: [k]) (bs :: [k]).
Auto (IsSubset as) bs =>
Subset as bs
autoSubset = forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsSubset as) @bs

-- | A lens into a subset of a record, indicated by a 'Subset'.
subsetRec :: Subset as bs -> Lens' (Rec f bs) (Rec f as)
subsetRec :: forall {u} (as :: [u]) (bs :: [u]) (f :: u -> *).
Subset as bs -> Lens' (Rec f bs) (Rec f as)
subsetRec = \case
  Subset as bs
SubsetNil -> (Rec f as -> f (Rec f as)) -> Rec f as -> f (Rec f as)
(Rec f as -> f (Rec f as)) -> Rec f bs -> f (Rec f bs)
forall a. a -> a
id
  SubsetNo Subset as bs
s -> \Rec f as -> f (Rec f as)
f -> \case
    f r
x :& Rec f rs
xs -> (f r
x f r -> Rec f bs -> Rec f (r : bs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) (Rec f bs -> Rec f bs) -> f (Rec f bs) -> f (Rec f bs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Subset as bs -> Lens' (Rec f bs) (Rec f as)
forall {u} (as :: [u]) (bs :: [u]) (f :: u -> *).
Subset as bs -> Lens' (Rec f bs) (Rec f as)
subsetRec Subset as bs
s Rec f as -> f (Rec f as)
f Rec f bs
Rec f rs
xs
  SubsetYes Subset as bs
s -> \Rec f as -> f (Rec f as)
f -> \case
    f r
x :& Rec f rs
xs ->
      ((f a, Rec f rs) -> Rec f bs) -> f (f a, Rec f rs) -> f (Rec f bs)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f a -> Rec f rs -> Rec f bs) -> (f a, Rec f rs) -> Rec f bs
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry f a -> Rec f rs -> Rec f bs
f a -> Rec f rs -> Rec f (a : rs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
(:&))
        (f (f a, Rec f rs) -> f (Rec f bs))
-> (Rec f rs -> f (f a, Rec f rs)) -> Rec f rs -> f (Rec f bs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f ((,) (f a)) (Rec f rs) -> f (f a, Rec f rs)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose
        (Compose f ((,) (f a)) (Rec f rs) -> f (f a, Rec f rs))
-> (Rec f rs -> Compose f ((,) (f a)) (Rec f rs))
-> Rec f rs
-> f (f a, Rec f rs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subset as rs -> Lens' (Rec f rs) (Rec f as)
forall {u} (as :: [u]) (bs :: [u]) (f :: u -> *).
Subset as bs -> Lens' (Rec f bs) (Rec f as)
subsetRec Subset as bs
Subset as rs
s (f (f a, Rec f as) -> Compose f ((,) (f a)) (Rec f as)
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (f a, Rec f as) -> Compose f ((,) (f a)) (Rec f as))
-> (Rec f as -> f (f a, Rec f as))
-> Rec f as
-> Compose f ((,) (f a)) (Rec f as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rec f as -> (f a, Rec f as)) -> f (Rec f as) -> f (f a, Rec f as)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(f r
y :& Rec f rs
ys) -> (f a
f r
y, Rec f as
Rec f rs
ys)) (f (Rec f as) -> f (f a, Rec f as))
-> (Rec f as -> f (Rec f as)) -> Rec f as -> f (f a, Rec f as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec f as -> f (Rec f as)
f (Rec f as -> f (Rec f as))
-> (Rec f as -> Rec f as) -> Rec f as -> f (Rec f as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f r
x f r -> Rec f as -> Rec f (r : as)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&))
        (Rec f rs -> f (Rec f bs)) -> Rec f rs -> f (Rec f bs)
forall a b. (a -> b) -> a -> b
$ Rec f rs
xs

-- | Take a subset out of a 'Rec'.  An alias for @'view' ('subsetRec' s)@.
getSubset ::
  Subset as bs ->
  Rec f bs ->
  Rec f as
getSubset :: forall {u} (as :: [u]) (bs :: [u]) (f :: u -> *).
Subset as bs -> Rec f bs -> Rec f as
getSubset = Getting (Rec f as) (Rec f bs) (Rec f as) -> Rec f bs -> Rec f as
forall a s. Getting a s a -> s -> a
view (Getting (Rec f as) (Rec f bs) (Rec f as) -> Rec f bs -> Rec f as)
-> (Subset as bs -> Getting (Rec f as) (Rec f bs) (Rec f as))
-> Subset as bs
-> Rec f bs
-> Rec f as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subset as bs -> Getting (Rec f as) (Rec f bs) (Rec f as)
Subset as bs -> Lens' (Rec f bs) (Rec f as)
forall {u} (as :: [u]) (bs :: [u]) (f :: u -> *).
Subset as bs -> Lens' (Rec f bs) (Rec f as)
subsetRec

-- | Get all of the indices of all the items in a 'Subset'.
subsetIxes ::
  Subset as bs ->
  Rec (Index bs) as
subsetIxes :: forall {u} (as :: [u]) (bs :: [u]).
Subset as bs -> Rec (Index bs) as
subsetIxes Subset as bs
s = Subset as bs -> Rec (Index bs) bs -> Rec (Index bs) as
forall {u} (as :: [u]) (bs :: [u]) (f :: u -> *).
Subset as bs -> Rec f bs -> Rec f as
getSubset Subset as bs
s (Rec (Index bs) bs -> Rec (Index bs) as)
-> (Shape [] bs -> Rec (Index bs) bs)
-> Shape [] bs
-> Rec (Index bs) as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: u). Elem [] bs a -> Proxy a -> Index bs a)
-> Shape [] bs -> Prod [] (Index bs) bs
forall {k} (f :: * -> *) (as :: f k) (g :: k -> *) (h :: k -> *).
FProd f =>
(forall (a :: k). Elem f as a -> g a -> h a)
-> Prod f g as -> Prod f h as
imapProd Index bs a -> Proxy a -> Index bs a
Elem [] bs a -> Proxy a -> Index bs a
forall (a :: u). Elem [] bs a -> Proxy a -> Index bs a
forall a b. a -> b -> a
const (Shape [] bs -> Rec (Index bs) as)
-> Shape [] bs -> Rec (Index bs) as
forall a b. (a -> b) -> a -> b
$ Shape [] bs
sp
  where
    (Shape [] as
_, Shape [] bs
sp) = Subset as bs -> (Shape [] as, Shape [] bs)
forall {k} (as :: [k]) (bs :: [k]).
Subset as bs -> (Shape [] as, Shape [] bs)
subsetShapes Subset as bs
s

-- | Get the 'Shape's associated with a 'Subset'.
subsetShapes ::
  Subset as bs ->
  (Shape [] as, Shape [] bs)
subsetShapes :: forall {k} (as :: [k]) (bs :: [k]).
Subset as bs -> (Shape [] as, Shape [] bs)
subsetShapes = \case
  Subset as bs
SubsetNil -> (Rec Proxy '[]
Shape [] as
forall {u} (a :: u -> *). Rec a '[]
RNil, Rec Proxy '[]
Shape [] bs
forall {u} (a :: u -> *). Rec a '[]
RNil)
  SubsetNo Subset as bs
s -> (Rec Proxy bs -> Shape [] bs)
-> (Shape [] as, Rec Proxy bs) -> (Shape [] as, Shape [] bs)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Proxy b
forall {k} (t :: k). Proxy t
Proxy Proxy b -> Rec Proxy bs -> Rec Proxy (b : bs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) ((Shape [] as, Rec Proxy bs) -> (Shape [] as, Shape [] bs))
-> (Shape [] as, Rec Proxy bs) -> (Shape [] as, Shape [] bs)
forall a b. (a -> b) -> a -> b
$ Subset as bs -> (Shape [] as, Shape [] bs)
forall {k} (as :: [k]) (bs :: [k]).
Subset as bs -> (Shape [] as, Shape [] bs)
subsetShapes Subset as bs
s
  SubsetYes Subset as bs
s -> (Rec Proxy as -> Shape [] as)
-> (Rec Proxy bs -> Shape [] bs)
-> (Rec Proxy as, Rec Proxy bs)
-> (Shape [] as, Shape [] bs)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (Proxy a
forall {k} (t :: k). Proxy t
Proxy Proxy a -> Rec Proxy as -> Rec Proxy (a : as)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) (Proxy a
forall {k} (t :: k). Proxy t
Proxy Proxy a -> Rec Proxy bs -> Rec Proxy (a : bs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) ((Rec Proxy as, Rec Proxy bs) -> (Shape [] as, Shape [] bs))
-> (Rec Proxy as, Rec Proxy bs) -> (Shape [] as, Shape [] bs)
forall a b. (a -> b) -> a -> b
$ Subset as bs -> (Shape [] as, Shape [] bs)
forall {k} (as :: [k]) (bs :: [k]).
Subset as bs -> (Shape [] as, Shape [] bs)
subsetShapes Subset as bs
s

-- | Because @as@ is a subset of @bs@, an index into @as@ should also be an
-- index into @bs@.  This performs that transformation.
--
-- This is like a version of 'injectIndexL' or 'injectIndexR', for
-- 'Subset'.
weakenSubsetIndex ::
  Subset as bs ->
  Index as a ->
  Index bs a
weakenSubsetIndex :: forall {k} (as :: [k]) (bs :: [k]) (a :: k).
Subset as bs -> Index as a -> Index bs a
weakenSubsetIndex = \case
  Subset as bs
SubsetNil -> \case {}
  SubsetNo Subset as bs
s -> Index bs a -> Index bs a
Index bs a -> Index (b : bs) a
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS (Index bs a -> Index bs a)
-> (Index as a -> Index bs a) -> Index as a -> Index bs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subset as bs -> Index as a -> Index bs a
forall {k} (as :: [k]) (bs :: [k]) (a :: k).
Subset as bs -> Index as a -> Index bs a
weakenSubsetIndex Subset as bs
s
  SubsetYes Subset as bs
s -> \case
    Index as a
IZ -> Index bs a
Index (a : bs) a
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
    IS Index bs a
i -> Index bs a -> Index (a : bs) a
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS (Index bs a -> Index (a : bs) a) -> Index bs a -> Index (a : bs) a
forall a b. (a -> b) -> a -> b
$ Subset as bs -> Index as a -> Index bs a
forall {k} (as :: [k]) (bs :: [k]) (a :: k).
Subset as bs -> Index as a -> Index bs a
weakenSubsetIndex Subset as bs
s Index as a
Index bs a
i

-- | Because @as@ is a subset of @bs@, we can /sometimes/ transform an
-- index into @bs@ into an index into @as@.  This performs that
-- transformation.  If it succeeds, it means that the index in @bs@ also
-- exists in @as@; otherwise, it means that the index in @bs@ was excluded
-- from @as@.
--
-- Note that if the index into @a@ was excluded from @as@, it doesn't
-- necessarily mean that there is no @a@ in @bs@ --- @bs@ could contain
-- a duplicate that was included into @as@.  This converts into an index to
-- the exact same item (positionlly) in the list, if it is possible.
--
-- This is like a version of 'unweaveIndex', but for 'Subset'.
strengthenSubsetIndex ::
  Subset as bs ->
  Index bs a ->
  Maybe (Index as a)
strengthenSubsetIndex :: forall {k} (as :: [k]) (bs :: [k]) (a :: k).
Subset as bs -> Index bs a -> Maybe (Index as a)
strengthenSubsetIndex = \case
  Subset as bs
SubsetNil -> \case {}
  SubsetNo Subset as bs
s -> \case
    Index bs a
IZ -> Maybe (Index as a)
forall a. Maybe a
Nothing
    IS Index bs a
i -> Subset as bs -> Index bs a -> Maybe (Index as a)
forall {k} (as :: [k]) (bs :: [k]) (a :: k).
Subset as bs -> Index bs a -> Maybe (Index as a)
strengthenSubsetIndex Subset as bs
s Index bs a
Index bs a
i
  SubsetYes Subset as bs
s -> \case
    Index bs a
IZ -> Index as a -> Maybe (Index as a)
forall a. a -> Maybe a
Just Index as a
Index (a : as) a
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
    IS Index bs a
i -> Index as a -> Index as a
Index as a -> Index (a : as) a
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS (Index as a -> Index as a)
-> Maybe (Index as a) -> Maybe (Index as a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Subset as bs -> Index bs a -> Maybe (Index as a)
forall {k} (as :: [k]) (bs :: [k]) (a :: k).
Subset as bs -> Index bs a -> Maybe (Index as a)
strengthenSubsetIndex Subset as bs
s Index bs a
Index bs a
i