{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      : Data.Type.List.Edit
-- Copyright   : (c) Justin Le 2023
-- License     : BSD3
--
-- Maintainer  : justin@jle.im
-- Stability   : experimental
-- Portability : non-portable
--
-- Witnesses regarding single-item edits of lists.
module Data.Type.List.Edit (
  -- * Simple edits
  Insert (..),
  autoInsert,
  Delete (..),
  autoDelete,
  insToDel,
  delToIns,
  Substitute (..),
  autoSubstitute,
  flipSub,
  subToDelIns,

  -- ** Predicates
  IsInsert,
  InsertedInto,
  IsDelete,
  DeletedFrom,
  IsSubstitute,

  -- ** Singletons
  SInsert (..),
  SDelete (..),
  SSubstitute (..),

  -- * Compound edits
  Edit (..),
  compEdit,
  flipEdit,

  -- * Rec
  insertRec,
  deleteRec,
  deleteGetRec,
  recLens,
  substituteRec,

  -- * Index

  -- ** Manipulating indices
  insertIndex,
  DeletedIx (..),
  deleteIndex,
  deleteIndex_,
  SubstitutedIx (..),
  substituteIndex,
  substituteIndex_,

  -- ** Converting from indices
  withDelete,
  withInsert,
  withInsertAfter,

  -- * Type-Level
  InsertIndex,
  sInsertIndex,
  SDeletedIx (..),
  DeleteIndex,
  sDeleteIndex,
  SSubstitutedIx (..),
  SubstituteIndex,
  sSubstituteIndex,

  -- ** Defunctionalization Symbols
  InsertIndexSym0,
  InsertIndexSym,
  DeleteIndexSym0,
  DeleteIndexSym,
  SubstituteIndexSym0,
  SubstituteIndexSym,
) where

import qualified Control.Category as C
import Data.Function.Singletons (IdSym0)
import Data.Kind
import Data.List.Singletons (SList (..))
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 Lens.Micro hiding ((%~))

-- | An @'Insert' as bs x@ is a witness that you can insert @x@ into some
-- position in list @as@ to produce list @bs@.  It is essentially 'Delete'
-- flipped.
--
-- Some examples:
--
-- @
-- InsZ                   :: Insert '[1,2,3] '[4,1,2,3] 4
-- InsS InsZ              :: Insert '[1,2,3] '[1,4,2,3] 4
-- InsS (InsS InsZ)       :: Insert '[1,2,3] '[1,2,4,3] 4
-- InsS (InsS (InsS InsZ) :: Insert '[1,2,3] '[1,2,3,4] 4
-- @
--
-- @bs@ will always be exactly one item longer than @as@.
data Insert :: [k] -> [k] -> k -> Type where
  InsZ :: Insert as (x ': as) x
  InsS :: Insert as bs x -> Insert (a ': as) (a ': bs) x

deriving instance Show (Insert as bs x)

-- | A type-level predicate that a given value can be used as an insertion
-- to change @as@ to @bs@.
--
-- @since 0.1.2.0
type IsInsert as bs = TyPred (Insert as bs)

-- | Prefers the "earlier" insert if there is ambiguity
instance Auto (IsInsert as (x ': as)) x where
  auto :: IsInsert as (x : as) @@ x
auto = IsInsert as (x : as) @@ x
Insert as (x : as) x
forall {a} (as :: [a]) (x :: a). Insert as (x : as) x
InsZ

instance {-# INCOHERENT #-} Auto (IsInsert as bs) x => Auto (IsInsert (a ': as) (a ': bs)) x where
  auto :: IsInsert (a : as) (a : bs) @@ x
auto = Insert as bs x -> Insert (a : as) (a : bs) x
forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k).
Insert i x x -> Insert (y : i) (y : x) x
InsS (forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsInsert as bs) @x)

instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsInsert as bs) where
  decide :: Decide (IsInsert as bs)
decide Sing a
z = case forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @bs of
    Sing bs
SList bs
SNil -> Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a))
-> Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case {}
    Sing n1
y `SCons` (ys :: Sing n2
ys@Sing n2
Sing :: Sing bs') -> case Sing n1
y Sing n1 -> Sing a -> Decision (n1 :~: 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
z of
      Proved n1 :~: a
Refl -> case forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as Sing as -> Sing n2 -> Decision (as :~: n2)
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 n2
ys of
        Proved as :~: n2
Refl -> Insert as (a : as) a -> Decision (Insert as (a : as) a)
forall a. a -> Decision a
Proved Insert as (a : as) a
forall {a} (as :: [a]) (x :: a). Insert as (x : as) x
InsZ
        Disproved Refuted (as :~: n2)
v -> case forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as of
          Sing as
SList as
SNil -> Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a))
-> Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
            IsInsert as bs @@ a
Insert '[] (a : n2) a
InsZ -> Refuted (as :~: n2)
v as :~: as
as :~: n2
forall {k} (a :: k). a :~: a
Refl
          Sing n1
x `SCons` (Sing n2
Sing :: Sing as') -> case Sing n1
x Sing n1 -> Sing a -> Decision (n1 :~: 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
Sing n1
y of
            Proved n1 :~: a
Refl -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k ~> *). Decidable p => Decide p
decide @(IsInsert as' bs') Sing a
z of
              Proved IsInsert n2 n2 @@ a
i -> (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a. a -> Decision a
Proved ((IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a))
-> (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a b. (a -> b) -> a -> b
$ Insert n2 n2 a -> Insert (a : n2) (a : n2) a
forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k).
Insert i x x -> Insert (y : i) (y : x) x
InsS IsInsert n2 n2 @@ a
Insert n2 n2 a
i
              Disproved Refuted (IsInsert n2 n2 @@ a)
u -> Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a))
-> Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
                IsInsert as bs @@ a
Insert (a : n2) (a : n2) a
InsZ -> Refuted (IsInsert n2 n2 @@ a)
u IsInsert n2 n2 @@ a
Insert n2 (a : n2) a
forall {a} (as :: [a]) (x :: a). Insert as (x : as) x
InsZ
                InsS Insert as bs a
i -> Refuted (IsInsert n2 n2 @@ a)
u IsInsert n2 n2 @@ a
Insert as bs a
i
            Disproved Refuted (n1 :~: a)
u -> Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a))
-> Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
              IsInsert as bs @@ a
Insert (n1 : n2) (a : n2) a
InsZ -> Refuted (as :~: n2)
v as :~: as
as :~: n2
forall {k} (a :: k). a :~: a
Refl
              InsS Insert as bs a
_ -> Refuted (n1 :~: a)
u n1 :~: a
n1 :~: n1
forall {k} (a :: k). a :~: a
Refl
      Disproved Refuted (n1 :~: a)
v -> case forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as of
        Sing as
SList as
SNil -> Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a))
-> Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
          IsInsert as bs @@ a
Insert '[] (n1 : n2) a
InsZ -> Refuted (n1 :~: a)
v n1 :~: a
n1 :~: n1
forall {k} (a :: k). a :~: a
Refl
        Sing n1
x `SCons` (Sing n2
Sing :: Sing as') -> 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 @(IsInsert as' bs') Sing a
z of
            Proved IsInsert n2 n2 @@ a
i -> (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a. a -> Decision a
Proved ((IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a))
-> (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a b. (a -> b) -> a -> b
$ Insert n2 n2 a -> Insert (n1 : n2) (n1 : n2) a
forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k).
Insert i x x -> Insert (y : i) (y : x) x
InsS IsInsert n2 n2 @@ a
Insert n2 n2 a
i
            Disproved Refuted (IsInsert n2 n2 @@ a)
u -> Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a))
-> Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
              IsInsert as bs @@ a
Insert (n1 : n2) (n1 : n2) a
InsZ -> Refuted (IsInsert n2 n2 @@ a)
u IsInsert n2 n2 @@ a
Insert n2 (a : n2) a
forall {a} (as :: [a]) (x :: a). Insert as (x : as) x
InsZ
              InsS Insert as bs a
i -> Refuted (IsInsert n2 n2 @@ a)
u IsInsert n2 n2 @@ a
Insert as bs a
i
          Disproved Refuted (n1 :~: n1)
u -> Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a))
-> Refuted (IsInsert as bs @@ a) -> Decision (IsInsert as bs @@ a)
forall a b. (a -> b) -> a -> b
$ \case
            IsInsert as bs @@ a
Insert (n1 : n2) (n1 : n2) a
InsZ -> Refuted (n1 :~: a)
v n1 :~: a
n1 :~: n1
forall {k} (a :: k). a :~: a
Refl
            InsS Insert as bs a
_ -> Refuted (n1 :~: n1)
u n1 :~: n1
n1 :~: n1
forall {k} (a :: k). a :~: a
Refl

-- | If @bs@ satisfies @'InsertedInto' as@, it means that there exists some
-- element @x@ such that @'IsInsert' as bs \@\@ x@: you can get @bs@ by
-- inserting @x@ into @as@ somewhere.
--
-- In other words, @'InsertedInto' as@ is satisfied by @bs@ if you can turn
-- @as@ into @bs@ by inserting one individual item.
--
-- You can find this element (if it exists) using 'search', or the
-- 'Decidable' instance of @'Found' ('InsertedInto' as)@:
--
-- @
-- 'searchTC' :: SingI as => Sing bs -> 'Decision' ('Σ' k ('IsInsert' as bs))
-- @
--
-- This will find you the single element you need to insert into @as@ to
-- get @bs@, if it exists.
--
-- @since 0.1.2.0
type InsertedInto (as :: [k]) = (TyPP (Insert as) :: ParamPred [k] k)

instance (SDecide k, SingI (as :: [k])) => Decidable (Found (InsertedInto as)) where
  decide :: Decide (Found (InsertedInto as))
decide = \case
    Sing a
SList a
SNil -> Refuted (Found (InsertedInto as) @@ a)
-> Decision (Found (InsertedInto as) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (Found (InsertedInto as) @@ a)
 -> Decision (Found (InsertedInto as) @@ a))
-> Refuted (Found (InsertedInto as) @@ a)
-> Decision (Found (InsertedInto as) @@ a)
forall a b. (a -> b) -> a -> b
$ \(Sing fst
_ :&: TyPP (Insert as) '[] @@ fst
i) -> case TyPP (Insert as) '[] @@ fst
i of {}
    Sing n1
y `SCons` Sing n2
ys -> case forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as Sing as -> Sing n2 -> Decision (as :~: n2)
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 n2
ys of
      Proved as :~: n2
Refl -> (Found (InsertedInto as) @@ a)
-> Decision (Found (InsertedInto as) @@ a)
forall a. a -> Decision a
Proved ((Found (InsertedInto as) @@ a)
 -> Decision (Found (InsertedInto as) @@ a))
-> (Found (InsertedInto as) @@ a)
-> Decision (Found (InsertedInto as) @@ a)
forall a b. (a -> b) -> a -> b
$ Sing n1
y Sing n1
-> (TyPP (Insert as) (n1 : as) @@ n1)
-> Sigma k (TyPP (Insert as) (n1 : as))
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: TyPP (Insert as) (n1 : as) @@ n1
Insert as (n1 : as) n1
forall {a} (as :: [a]) (x :: a). Insert as (x : as) x
InsZ
      Disproved Refuted (as :~: n2)
v -> case forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as of
        Sing as
SList as
SNil -> Refuted (Found (InsertedInto as) @@ a)
-> Decision (Found (InsertedInto as) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (Found (InsertedInto as) @@ a)
 -> Decision (Found (InsertedInto as) @@ a))
-> Refuted (Found (InsertedInto as) @@ a)
-> Decision (Found (InsertedInto as) @@ a)
forall a b. (a -> b) -> a -> b
$ \(Sing fst
_ :&: TyPP (Insert '[]) (n1 : n2) @@ fst
i) -> case TyPP (Insert '[]) (n1 : n2) @@ fst
i of
          TyPP (Insert '[]) (n1 : n2) @@ fst
Insert '[] (n1 : n2) fst
InsZ -> Refuted (as :~: n2)
v as :~: as
as :~: n2
forall {k} (a :: k). a :~: a
Refl
        Sing n1
x `SCons` (Sing n2
Sing :: Sing as') -> 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 @(Found (InsertedInto as')) Sing n2
ys of
            Proved (Sing fst
z :&: TyPP (Insert n2) n2 @@ fst
i) -> (Found (InsertedInto as) @@ a)
-> Decision (Found (InsertedInto as) @@ a)
forall a. a -> Decision a
Proved ((Found (InsertedInto as) @@ a)
 -> Decision (Found (InsertedInto as) @@ a))
-> (Found (InsertedInto as) @@ a)
-> Decision (Found (InsertedInto as) @@ a)
forall a b. (a -> b) -> a -> b
$ Sing fst
z Sing fst
-> (TyPP (Insert (n1 : n2)) (n1 : n2) @@ fst)
-> Sigma k (TyPP (Insert (n1 : n2)) (n1 : n2))
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: Insert n2 n2 fst -> Insert (n1 : n2) (n1 : n2) fst
forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k).
Insert i x x -> Insert (y : i) (y : x) x
InsS TyPP (Insert n2) n2 @@ fst
Insert n2 n2 fst
i
            Disproved Refuted (Found (InsertedInto n2) @@ n2)
u -> Refuted (Found (InsertedInto as) @@ a)
-> Decision (Found (InsertedInto as) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (Found (InsertedInto as) @@ a)
 -> Decision (Found (InsertedInto as) @@ a))
-> Refuted (Found (InsertedInto as) @@ a)
-> Decision (Found (InsertedInto as) @@ a)
forall a b. (a -> b) -> a -> b
$ \(Sing fst
z :&: TyPP (Insert (n1 : n2)) (n1 : n2) @@ fst
i) -> case TyPP (Insert (n1 : n2)) (n1 : n2) @@ fst
i of
              TyPP (Insert (n1 : n2)) (n1 : n2) @@ fst
Insert (n1 : n2) (n1 : n2) fst
InsZ -> Refuted (Found (InsertedInto n2) @@ n2)
u Refuted (Found (InsertedInto n2) @@ n2)
-> Refuted (Found (InsertedInto n2) @@ n2)
forall a b. (a -> b) -> a -> b
$ Sing n1
Sing fst
z Sing n1
-> (TyPP (Insert n2) (n1 : n2) @@ n1)
-> Sigma k (TyPP (Insert n2) (n1 : n2))
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: TyPP (Insert n2) (n1 : n2) @@ n1
Insert n2 (n1 : n2) n1
forall {a} (as :: [a]) (x :: a). Insert as (x : as) x
InsZ
              InsS Insert as bs fst
i' -> Refuted (Found (InsertedInto n2) @@ n2)
u Refuted (Found (InsertedInto n2) @@ n2)
-> Refuted (Found (InsertedInto n2) @@ n2)
forall a b. (a -> b) -> a -> b
$ Sing fst
z Sing fst
-> (TyPP (Insert n2) n2 @@ fst) -> Sigma k (TyPP (Insert n2) n2)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: TyPP (Insert n2) n2 @@ fst
Insert as bs fst
i'
          Disproved Refuted (n1 :~: n1)
u -> Refuted (Found (InsertedInto as) @@ a)
-> Decision (Found (InsertedInto as) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (Found (InsertedInto as) @@ a)
 -> Decision (Found (InsertedInto as) @@ a))
-> Refuted (Found (InsertedInto as) @@ a)
-> Decision (Found (InsertedInto as) @@ a)
forall a b. (a -> b) -> a -> b
$ \(Sing fst
_ :&: TyPP (Insert (n1 : n2)) (n1 : n2) @@ fst
i) -> case TyPP (Insert (n1 : n2)) (n1 : n2) @@ fst
i of
            TyPP (Insert (n1 : n2)) (n1 : n2) @@ fst
Insert (n1 : n2) (n1 : n2) fst
InsZ -> Refuted (as :~: n2)
v as :~: as
as :~: n2
forall {k} (a :: k). a :~: a
Refl
            InsS Insert as bs fst
_ -> Refuted (n1 :~: n1)
u n1 :~: n1
n1 :~: n1
forall {k} (a :: k). a :~: a
Refl

-- | Automatically generate an 'Insert' if @as@, @bs@ and @x@ are known
-- statically.
--
-- Prefers the earlier insertion if there is an ambiguity.
--
-- @
-- InsS InsZ        :: Insert '[1,2] '[1,2,2] 2
-- InsS (InsS InsZ) :: Insert '[1,2] '[1,2,2] 2
-- autoInsert @'[1,2] @'[1,2,2] @2 == InsS InsZ
-- @
--
-- @since 0.1.2.0
autoInsert :: forall as bs x. Auto (IsInsert as bs) x => Insert as bs x
autoInsert :: forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Auto (IsInsert as bs) x =>
Insert as bs x
autoInsert = forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsInsert as bs) @x

-- | Kind-indexed singleton for 'Insert'.
data SInsert (as :: [k]) (bs :: [k]) (x :: k) :: Insert as bs x -> Type where
  SInsZ :: SInsert as (x ': as) x 'InsZ
  SInsS :: SInsert as bs x ins -> SInsert (a ': as) (a ': bs) x ('InsS ins)

deriving instance Show (SInsert as bs x del)

-- | Flip an insertion.
insToDel :: Insert as bs x -> Delete bs as x
insToDel :: forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Insert as bs x -> Delete bs as x
insToDel = \case
  Insert as bs x
InsZ -> Delete bs as x
Delete (x : as) as x
forall {k} (x :: k) (as :: [k]). Delete (x : as) as x
DelZ
  InsS Insert as bs x
i -> Delete bs as x -> Delete (a : bs) (a : as) x
forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k).
Delete i x x -> Delete (y : i) (y : x) x
DelS (Insert as bs x -> Delete bs as x
forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Insert as bs x -> Delete bs as x
insToDel Insert as bs x
i)

-- | A @'Delete' as bs x@ is a witness that you can delete item @x@ from
-- @as@ to produce the list @bs@.  It is essentially 'Insert' flipped.
--
-- Some examples:
--
-- @
-- DelZ             :: Delete '[1,2,3] '[2,3] 1
-- DelS DelZ        :: Delete '[1,2,3] '[2,3] 2
-- DelS (DelS DelZ) :: Delete '[1,2,3] '[1,2] 3
-- @
--
-- @bs@ will always be exactly one item shorter than @as@.
data Delete :: [k] -> [k] -> k -> Type where
  DelZ :: Delete (x ': as) as x
  DelS :: Delete as bs x -> Delete (a ': as) (a ': bs) x

deriving instance Show (Delete as bs x)

-- | A type-level predicate that a given value can be used as a deletion
-- to change @as@ to @bs@.
--
-- @since 0.1.2.0
type IsDelete as bs = TyPred (Delete as bs)

-- | Prefers the "earlier" delete if there is ambiguity
instance Auto (IsDelete (x ': as) as) x where
  auto :: IsDelete (x : as) as @@ x
auto = IsDelete (x : as) as @@ x
Delete (x : as) as x
forall {k} (x :: k) (as :: [k]). Delete (x : as) as x
DelZ

instance {-# INCOHERENT #-} Auto (IsDelete as bs) x => Auto (IsDelete (a ': as) (a ': bs)) x where
  auto :: IsDelete (a : as) (a : bs) @@ x
auto = Delete as bs x -> Delete (a : as) (a : bs) x
forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k).
Delete i x x -> Delete (y : i) (y : x) x
DelS (forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsDelete as bs) @x)

instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsDelete as bs) where
  decide :: Decide (IsDelete as bs)
decide = (Insert bs as a -> Delete as bs a)
-> (Delete as bs a -> Insert bs as a)
-> Decision (Insert bs as a)
-> Decision (Delete as bs a)
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision Insert bs as a -> Delete as bs a
forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Insert as bs x -> Delete bs as x
insToDel Delete as bs a -> Insert bs as a
forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Delete as bs x -> Insert bs as x
delToIns (Decision (Insert bs as a) -> Decision (Delete as bs a))
-> (Sing a -> Decision (Insert bs as a))
-> Sing a
-> Decision (Delete as bs a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k ~> *). Decidable p => Decide p
decide @(IsInsert bs as)

-- | If @bs@ satisfies @'DeletedFrom' as@, it means that there exists some
-- element @x@ such that @'IsDelete' as bs \@\@ x@: you can get @bs@ by
-- deleting @x@ from @as@ somewhere.
--
-- In other words, @'DeletedFrom' as@ is satisfied by @bs@ if you can turn
-- @as@ into @bs@ by deleting one individual item.
--
-- You can find this element (if it exists) using 'search', or the
-- 'Decidable' instance of @'Found' ('DeletedFrom' as)@.
--
-- @
-- 'searchTC' :: SingI as => Sing bs -> 'Decision' ('Σ' k ('IsDelete' as bs))
-- @
--
-- This will find you the single element you need to delete from @as@ to
-- get @bs@, if it exists.
--
-- @since 0.1.2.0
type DeletedFrom (as :: [k]) = (TyPP (Delete as) :: ParamPred [k] k)

instance (SDecide k, SingI (as :: [k])) => Decidable (Found (DeletedFrom as)) where
  decide :: Decide (Found (DeletedFrom as))
decide (Sing a
Sing :: Sing bs) =
    (Sigma k (TyPP (Insert a) as) -> Found (DeletedFrom as) @@ a)
-> ((Found (DeletedFrom as) @@ a) -> Sigma k (TyPP (Insert a) as))
-> Decision (Sigma k (TyPP (Insert a) as))
-> Decision (Found (DeletedFrom as) @@ a)
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision
      (Sing IdSym0
-> (forall (x :: k).
    (TyPP (Insert a) as @@ x) -> TyPP (Delete as) a @@ (IdSym0 @@ x))
-> Sigma k (TyPP (Insert a) as)
-> Sigma k (TyPP (Delete as) a)
forall a b (f :: a ~> b) (p :: a ~> *) (q :: b ~> *).
Sing f
-> (forall (x :: a). (p @@ x) -> q @@ (f @@ x))
-> Sigma a p
-> Sigma b q
mapSigma (forall {k} (a :: k). SingI a => Sing a
forall (a :: TyFun k k -> *). SingI a => Sing a
sing @IdSym0) Apply (TyPP (Insert a) as) x
-> Apply (TyPP (Delete as) a) (Apply IdSym0 x)
Insert a as x -> Delete as a x
forall (x :: k).
(TyPP (Insert a) as @@ x) -> TyPP (Delete as) a @@ (IdSym0 @@ x)
forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Insert as bs x -> Delete bs as x
insToDel)
      (Sing IdSym0
-> (forall (x :: k).
    (TyPP (Delete as) a @@ x) -> TyPP (Insert a) as @@ (IdSym0 @@ x))
-> Sigma k (TyPP (Delete as) a)
-> Sigma k (TyPP (Insert a) as)
forall a b (f :: a ~> b) (p :: a ~> *) (q :: b ~> *).
Sing f
-> (forall (x :: a). (p @@ x) -> q @@ (f @@ x))
-> Sigma a p
-> Sigma b q
mapSigma (forall {k} (a :: k). SingI a => Sing a
forall (a :: TyFun k k -> *). SingI a => Sing a
sing @IdSym0) Apply (TyPP (Delete as) a) x
-> Apply (TyPP (Insert a) as) (Apply IdSym0 x)
Delete as a x -> Insert a as x
forall (x :: k).
(TyPP (Delete as) a @@ x) -> TyPP (Insert a) as @@ (IdSym0 @@ x)
forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Delete as bs x -> Insert bs as x
delToIns)
      (Decision (Sigma k (TyPP (Insert a) as))
 -> Decision (Found (DeletedFrom as) @@ a))
-> Decision (Sigma k (TyPP (Insert a) as))
-> Decision (Found (DeletedFrom as) @@ a)
forall a b. (a -> b) -> a -> b
$ forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: [k] ~> *). Decidable p => Decide p
decide @(Found (InsertedInto bs)) (forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as)

-- | Automatically generate an 'Delete' if @as@, @bs@ and @x@ are known
-- statically.
--
-- Prefers the earlier deletion if there is an ambiguity.
--
-- @
-- DelS DelZ        :: Delete '[1,2,2] '[1,2] 2
-- DelS (DelS DelZ) :: Delete '[1,2,2] '[1,2] 2
-- autoDelete @'[1,2,2] @'[1,2] @2 == DelS DelZ
-- @
--
-- @since 0.1.2.0
autoDelete :: forall as bs x. Auto (IsDelete as bs) x => Delete as bs x
autoDelete :: forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Auto (IsDelete as bs) x =>
Delete as bs x
autoDelete = forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsDelete as bs) @x

-- | Kind-indexed singleton for 'Delete'.
data SDelete (as :: [k]) (bs :: [k]) (x :: k) :: Delete as bs x -> Type where
  SDelZ :: SDelete (x ': as) as x 'DelZ
  SDelS :: SDelete as bs x del -> SDelete (a ': as) (a ': bs) x ('DelS del)

deriving instance Show (SDelete as bs x del)

-- | Flip a deletion.
delToIns :: Delete as bs x -> Insert bs as x
delToIns :: forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Delete as bs x -> Insert bs as x
delToIns = \case
  Delete as bs x
DelZ -> Insert bs as x
Insert bs (x : bs) x
forall {a} (as :: [a]) (x :: a). Insert as (x : as) x
InsZ
  DelS Delete as bs x
d -> Insert bs as x -> Insert (a : bs) (a : as) x
forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k).
Insert i x x -> Insert (y : i) (y : x) x
InsS (Delete as bs x -> Insert bs as x
forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Delete as bs x -> Insert bs as x
delToIns Delete as bs x
d)

-- | A @'Substitute' as bs x y@ is a witness that you can replace item @x@ in
-- @as@ with item @y@ to produce @bs@.
--
-- Some examples:
--
-- @
-- SubZ             :: Substitute '[1,2,3] '[4,2,3] 1 4
-- SubS SubZ        :: Substitute '[1,2,3] '[1,4,3] 2 4
-- SubS (SubS SubZ) :: Substitute '[1,2,3] '[1,2,4] 3 4
-- @
data Substitute :: [k] -> [k] -> k -> k -> Type where
  SubZ :: Substitute (x ': as) (y ': as) x y
  SubS :: Substitute as bs x y -> Substitute (c ': as) (c ': bs) x y

deriving instance Show (Substitute as bs x y)

-- | A type-level predicate that a given value can be used as
-- a substitution of @x@ to change @as@ to @bs@.
--
-- @since 0.1.2.0
type IsSubstitute as bs x = TyPred (Substitute as bs x)

instance Auto (IsSubstitute (x ': as) (y ': as) x) y where
  auto :: IsSubstitute (x : as) (y : as) x @@ y
auto = IsSubstitute (x : as) (y : as) x @@ y
Substitute (x : as) (y : as) x y
forall {a} (x :: a) (i :: [a]) (y :: a).
Substitute (x : i) (y : i) x y
SubZ

-- | Prefers the earlier subsitution if there is ambiguity.
instance Auto (IsSubstitute as bs x) y => Auto (IsSubstitute (c ': as) (c ': bs) x) y where
  auto :: IsSubstitute (c : as) (c : bs) x @@ y
auto = Substitute as bs x y -> Substitute (c : as) (c : bs) x y
forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k) (y :: k).
Substitute i x x y -> Substitute (y : i) (y : x) x y
SubS (forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsSubstitute as bs x) @y)

instance {-# INCOHERENT #-} Auto (IsSubstitute (x ': as) (x ': as) x) x where
  auto :: IsSubstitute (x : as) (x : as) x @@ x
auto = IsSubstitute (x : as) (x : as) x @@ x
Substitute (x : as) (x : as) x x
forall {a} (x :: a) (i :: [a]) (y :: a).
Substitute (x : i) (y : i) x y
SubZ

-- | Automatically generate an 'Substitute' if @as@, @bs@, @x@, and @y@ are
-- known statically.
--
-- Prefers the "earlier" substitution if there is an ambiguity
--
-- @
-- SubZ      :: Substitute '[1,1] '[1,1] 1 1
-- SubS SubZ :: Substitute '[1,1] '[1,1] 1 1
-- autoSubstitute @'[1,1] @'[1,1] @1 @1 == SubZ
-- @
--
-- @since 0.1.2.0
autoSubstitute :: forall as bs x y. Auto (IsSubstitute as bs x) y => Substitute as bs x y
autoSubstitute :: forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k).
Auto (IsSubstitute as bs x) y =>
Substitute as bs x y
autoSubstitute = forall k (p :: Predicate k) (a :: k). Auto p a => p @@ a
auto @_ @(IsSubstitute as bs x) @y

-- | Kind-indexed singleton for 'Substitute'.
data SSubstitute (as :: [k]) (bs :: [k]) (x :: k) (y :: k) :: Substitute as bs x y -> Type where
  SSubZ :: SSubstitute (x ': as) (y ': as) x y 'SubZ
  SSubS ::
    SSubstitute as bs x y sub ->
    SSubstitute (c ': as) (c ': bs) x y ('SubS sub)

-- | Flip a substitution
flipSub :: Substitute as bs x y -> Substitute bs as y x
flipSub :: forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k).
Substitute as bs x y -> Substitute bs as y x
flipSub = \case
  Substitute as bs x y
SubZ -> Substitute bs as y x
Substitute (y : as) (x : as) y x
forall {a} (x :: a) (i :: [a]) (y :: a).
Substitute (x : i) (y : i) x y
SubZ
  SubS Substitute as bs x y
s -> Substitute bs as y x -> Substitute (c : bs) (c : as) y x
forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k) (y :: k).
Substitute i x x y -> Substitute (y : i) (y : x) x y
SubS (Substitute as bs x y -> Substitute bs as y x
forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k).
Substitute as bs x y -> Substitute bs as y x
flipSub Substitute as bs x y
s)

-- | Decompose a 'Substitute' into a 'Delete' followed by an 'Insert'.
subToDelIns ::
  Substitute as bs x y ->
  (forall cs. Delete as cs x -> Insert cs bs y -> r) ->
  r
subToDelIns :: forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k) r.
Substitute as bs x y
-> (forall (cs :: [k]). Delete as cs x -> Insert cs bs y -> r) -> r
subToDelIns = \case
  Substitute as bs x y
SubZ -> \forall (cs :: [k]). Delete as cs x -> Insert cs bs y -> r
f -> Delete as as x -> Insert as bs y -> r
forall (cs :: [k]). Delete as cs x -> Insert cs bs y -> r
f Delete as as x
Delete (x : as) as x
forall {k} (x :: k) (as :: [k]). Delete (x : as) as x
DelZ Insert as bs y
Insert as (y : as) y
forall {a} (as :: [a]) (x :: a). Insert as (x : as) x
InsZ
  SubS Substitute as bs x y
s -> \forall (cs :: [k]). Delete as cs x -> Insert cs bs y -> r
f -> Substitute as bs x y
-> (forall {cs :: [k]}. Delete as cs x -> Insert cs bs y -> r) -> r
forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k) r.
Substitute as bs x y
-> (forall (cs :: [k]). Delete as cs x -> Insert cs bs y -> r) -> r
subToDelIns Substitute as bs x y
s ((forall {cs :: [k]}. Delete as cs x -> Insert cs bs y -> r) -> r)
-> (forall {cs :: [k]}. Delete as cs x -> Insert cs bs y -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Delete as cs x
d Insert cs bs y
i -> Delete as (c : cs) x -> Insert (c : cs) bs y -> r
forall (cs :: [k]). Delete as cs x -> Insert cs bs y -> r
f (Delete as cs x -> Delete (c : as) (c : cs) x
forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k).
Delete i x x -> Delete (y : i) (y : x) x
DelS Delete as cs x
d) (Insert cs bs y -> Insert (c : cs) (c : bs) y
forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k).
Insert i x x -> Insert (y : i) (y : x) x
InsS Insert cs bs y
i)

-- | An @'Edit' as bs@ is a reversible edit script transforming @as@ into
-- @bs@ through successive insertions, deletions, and substitutions.
--
-- TODO: implement Wagner-Fischer or something similar to minimize find
-- a minimal edit distance
data Edit :: [k] -> [k] -> Type where
  ENil :: Edit as as
  EIns :: Insert bs cs x -> Edit as bs -> Edit as cs
  EDel :: Delete bs cs x -> Edit as bs -> Edit as cs
  ESub :: Substitute bs cs x y -> Edit as bs -> Edit as cs

deriving instance Show (Edit as bs)

-- | Compose two 'Edit's
compEdit :: Edit as bs -> Edit bs cs -> Edit as cs
compEdit :: forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Edit as bs -> Edit bs cs -> Edit as cs
compEdit Edit as bs
xs = \case
  Edit bs cs
ENil -> Edit as bs
Edit as cs
xs
  EIns Insert bs cs x
i Edit bs bs
ys -> Insert bs cs x -> Edit as bs -> Edit as cs
forall {k} (i :: [k]) (cs :: [k]) (x :: k) (as :: [k]).
Insert i cs x -> Edit as i -> Edit as cs
EIns Insert bs cs x
i (Edit as bs -> Edit bs bs -> Edit as bs
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Edit as bs -> Edit bs cs -> Edit as cs
compEdit Edit as bs
xs Edit bs bs
ys)
  EDel Delete bs cs x
d Edit bs bs
ys -> Delete bs cs x -> Edit as bs -> Edit as cs
forall {k} (i :: [k]) (cs :: [k]) (x :: k) (as :: [k]).
Delete i cs x -> Edit as i -> Edit as cs
EDel Delete bs cs x
d (Edit as bs -> Edit bs bs -> Edit as bs
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Edit as bs -> Edit bs cs -> Edit as cs
compEdit Edit as bs
xs Edit bs bs
ys)
  ESub Substitute bs cs x y
s Edit bs bs
ys -> Substitute bs cs x y -> Edit as bs -> Edit as cs
forall {k} (i :: [k]) (cs :: [k]) (x :: k) (y :: k) (as :: [k]).
Substitute i cs x y -> Edit as i -> Edit as cs
ESub Substitute bs cs x y
s (Edit as bs -> Edit bs bs -> Edit as bs
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Edit as bs -> Edit bs cs -> Edit as cs
compEdit Edit as bs
xs Edit bs bs
ys)

-- | 'Edit' composition
instance C.Category Edit where
  id :: forall (a :: [k]). Edit a a
id = Edit a a
forall k (a :: [k]). Edit a a
ENil
  Edit b c
xs . :: forall (b :: [k]) (c :: [k]) (a :: [k]).
Edit b c -> Edit a b -> Edit a c
. Edit a b
ys = Edit a b -> Edit b c -> Edit a c
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Edit as bs -> Edit bs cs -> Edit as cs
compEdit Edit a b
ys Edit b c
xs

-- | Reverse an 'Edit' script.  O(n^2).  Please do not use ever in any
-- circumstance.
--
-- TODO: Make O(n) using diff lists.
flipEdit :: Edit as bs -> Edit bs as
flipEdit :: forall {k} (as :: [k]) (bs :: [k]). Edit as bs -> Edit bs as
flipEdit = \case
  Edit as bs
ENil -> Edit bs as
Edit bs bs
forall k (a :: [k]). Edit a a
ENil
  EIns Insert bs bs x
i Edit as bs
ys -> Delete bs bs x -> Edit bs bs -> Edit bs bs
forall {k} (i :: [k]) (cs :: [k]) (x :: k) (as :: [k]).
Delete i cs x -> Edit as i -> Edit as cs
EDel (Insert bs bs x -> Delete bs bs x
forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Insert as bs x -> Delete bs as x
insToDel Insert bs bs x
i) Edit bs bs
forall k (a :: [k]). Edit a a
ENil Edit bs bs -> Edit bs as -> Edit bs as
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Edit as bs -> Edit bs cs -> Edit as cs
`compEdit` Edit as bs -> Edit bs as
forall {k} (as :: [k]) (bs :: [k]). Edit as bs -> Edit bs as
flipEdit Edit as bs
ys
  EDel Delete bs bs x
d Edit as bs
ys -> Insert bs bs x -> Edit bs bs -> Edit bs bs
forall {k} (i :: [k]) (cs :: [k]) (x :: k) (as :: [k]).
Insert i cs x -> Edit as i -> Edit as cs
EIns (Delete bs bs x -> Insert bs bs x
forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Delete as bs x -> Insert bs as x
delToIns Delete bs bs x
d) Edit bs bs
forall k (a :: [k]). Edit a a
ENil Edit bs bs -> Edit bs as -> Edit bs as
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Edit as bs -> Edit bs cs -> Edit as cs
`compEdit` Edit as bs -> Edit bs as
forall {k} (as :: [k]) (bs :: [k]). Edit as bs -> Edit bs as
flipEdit Edit as bs
ys
  ESub Substitute bs bs x y
s Edit as bs
ys -> Substitute bs bs y x -> Edit bs bs -> Edit bs bs
forall {k} (i :: [k]) (cs :: [k]) (x :: k) (y :: k) (as :: [k]).
Substitute i cs x y -> Edit as i -> Edit as cs
ESub (Substitute bs bs x y -> Substitute bs bs y x
forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k).
Substitute as bs x y -> Substitute bs as y x
flipSub Substitute bs bs x y
s) Edit bs bs
forall k (a :: [k]). Edit a a
ENil Edit bs bs -> Edit bs as -> Edit bs as
forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Edit as bs -> Edit bs cs -> Edit as cs
`compEdit` Edit as bs -> Edit bs as
forall {k} (as :: [k]) (bs :: [k]). Edit as bs -> Edit bs as
flipEdit Edit as bs
ys

-- | Insert a value into a 'Rec', at a position indicated by the 'Insert'.
insertRec :: Insert as bs x -> f x -> Rec f as -> Rec f bs
insertRec :: forall {u} (as :: [u]) (bs :: [u]) (x :: u) (f :: u -> *).
Insert as bs x -> f x -> Rec f as -> Rec f bs
insertRec = \case
  Insert as bs x
InsZ -> f x -> Rec f as -> Rec f bs
f x -> Rec f as -> Rec f (x : as)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
(:&)
  InsS Insert as bs x
i -> \f x
x -> \case
    f r
y :& Rec f rs
ys -> f r
y 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)
:& Insert as bs x -> f x -> Rec f as -> Rec f bs
forall {u} (as :: [u]) (bs :: [u]) (x :: u) (f :: u -> *).
Insert as bs x -> f x -> Rec f as -> Rec f bs
insertRec Insert as bs x
i f x
x Rec f as
Rec f rs
ys

-- | Retrieve and delete a value in a 'Rec', at a position indicated by the 'Delete'.
deleteGetRec :: Delete as bs x -> Rec f as -> (f x, Rec f bs)
deleteGetRec :: forall {u} (as :: [u]) (bs :: [u]) (x :: u) (f :: u -> *).
Delete as bs x -> Rec f as -> (f x, Rec f bs)
deleteGetRec = \case
  Delete as bs x
DelZ -> \case
    f r
x :& Rec f rs
xs -> (f x
f r
x, Rec f bs
Rec f rs
xs)
  DelS Delete as bs x
d -> \case
    f r
x :& Rec f rs
xs ->
      let (f x
y, Rec f bs
ys) = Delete as bs x -> Rec f as -> (f x, Rec f bs)
forall {u} (as :: [u]) (bs :: [u]) (x :: u) (f :: u -> *).
Delete as bs x -> Rec f as -> (f x, Rec f bs)
deleteGetRec Delete as bs x
d Rec f as
Rec f rs
xs
       in (f x
y, 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
ys)

-- | Delete a value in a 'Rec', at a position indicated by the 'Delete'.
deleteRec :: Delete as bs x -> Rec f as -> Rec f bs
deleteRec :: forall {u} (as :: [u]) (bs :: [u]) (x :: u) (f :: u -> *).
Delete as bs x -> Rec f as -> Rec f bs
deleteRec = \case
  Delete as bs x
DelZ -> \case
    f r
_ :& Rec f rs
xs -> Rec f bs
Rec f rs
xs
  DelS Delete as bs x
d -> \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)
:& Delete as bs x -> Rec f as -> Rec f bs
forall {u} (as :: [u]) (bs :: [u]) (x :: u) (f :: u -> *).
Delete as bs x -> Rec f as -> Rec f bs
deleteRec Delete as bs x
d Rec f as
Rec f rs
xs

-- | A type-changing lens into a value in a 'Rec', given a 'Substitute'
-- indicating which value.
--
-- For example:
--
-- @
-- recLens (SubS SubZ)
--      :: Lens (Rec f '[a,b,c,d]) (Rec f '[a,e,c,d])
--              (f b)              (f e)
-- @
--
-- The number of 'SubS' in the index essentially indicates the index to
-- edit at.
--
-- This is similar to 'Data.Vinyl.Lens.rlensC' from /vinyl/, but is built
-- explicitly and inductively, instead of using typeclass magic.
recLens ::
  forall as bs x y f.
  () =>
  Substitute as bs x y ->
  Lens (Rec f as) (Rec f bs) (f x) (f y)
recLens :: forall {u} (as :: [u]) (bs :: [u]) (x :: u) (y :: u) (f :: u -> *).
Substitute as bs x y -> Lens (Rec f as) (Rec f bs) (f x) (f y)
recLens Substitute as bs x y
s0 (f x -> f (f y)
f :: f x -> g (f y)) = Substitute as bs x y -> Rec f as -> f (Rec f bs)
forall (cs :: [u]) (ds :: [u]).
Substitute cs ds x y -> Rec f cs -> f (Rec f ds)
go Substitute as bs x y
s0
  where
    go ::
      Substitute cs ds x y ->
      Rec f cs ->
      g (Rec f ds)
    go :: forall (cs :: [u]) (ds :: [u]).
Substitute cs ds x y -> Rec f cs -> f (Rec f ds)
go = \case
      Substitute cs ds x y
SubZ -> \case
        f r
x :& Rec f rs
xs -> (f y -> Rec f rs -> Rec f (y : rs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec f rs
xs) (f y -> Rec f ds) -> f (f y) -> f (Rec f ds)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> f (f y)
f f x
f r
x
      SubS Substitute as bs x y
s -> \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 ds) -> f (Rec f bs) -> f (Rec f ds)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Substitute as bs x y -> Rec f as -> f (Rec f bs)
forall (cs :: [u]) (ds :: [u]).
Substitute cs ds x y -> Rec f cs -> f (Rec f ds)
go Substitute as bs x y
s Rec f as
Rec f rs
xs

-- | Substitute a value in a 'Rec' at a given position, indicated by the
-- 'Substitute'.  This is essentially a specialized version of 'recLens'.
substituteRec ::
  Substitute as bs x y ->
  (f x -> f y) ->
  Rec f as ->
  Rec f bs
substituteRec :: forall {u} (as :: [u]) (bs :: [u]) (x :: u) (y :: u) (f :: u -> *).
Substitute as bs x y -> (f x -> f y) -> Rec f as -> Rec f bs
substituteRec Substitute as bs x y
s = ASetter (Rec f as) (Rec f bs) (f x) (f y)
-> (f x -> f y) -> Rec f as -> Rec f bs
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over (Substitute as bs x y -> Lens (Rec f as) (Rec f bs) (f x) (f y)
forall {u} (as :: [u]) (bs :: [u]) (x :: u) (y :: u) (f :: u -> *).
Substitute as bs x y -> Lens (Rec f as) (Rec f bs) (f x) (f y)
recLens Substitute as bs x y
s)

-- | If you add an item to @as@ to create @bs@, you also need to shift an
-- @'Index' as y@ to @Index bs y@.  This shifts the 'Index' in @as@ to
-- become an 'Index' in @bs@, but makes sure that the index points to the
-- same original value.
insertIndex :: Insert as bs x -> Index as y -> Index bs y
insertIndex :: forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k).
Insert as bs x -> Index as y -> Index bs y
insertIndex = \case
  Insert as bs x
InsZ -> Index as y -> Index bs y
Index as y -> Index (x : as) y
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS
  InsS Insert as bs x
ins -> \case
    Index as y
IZ -> Index bs y
Index (y : bs) y
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
    IS Index bs y
i -> Index bs y -> Index (a : bs) y
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS (Insert as bs x -> Index as y -> Index bs y
forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k).
Insert as bs x -> Index as y -> Index bs y
insertIndex Insert as bs x
ins Index as y
Index bs y
i)

-- | Used as the return type of 'deleteIndex'.  An @'DeletedIx' bs x y@ is
-- like a @'Maybe' ('Index' bs y)@, except the 'Nothing' case witnesses
-- that @x ~ y@.
data DeletedIx :: [k] -> k -> k -> Type where
  GotDeleted :: DeletedIx bs x x
  NotDeleted :: Index bs y -> DeletedIx bs x y

deriving instance Show (DeletedIx bs x y)

-- | If you delete an item in @as@ to create @bs@, you also need to move
-- @'Index' as y@ into @Index bs y@.  This transforms the 'Index' in @as@
-- to become an 'Index' in @bs@, making sure the index points to the same
-- original value.
--
-- However, there is a possibility that the deleted item is the item that
-- the index was originally pointing to.  If this is the case, this
-- function returns 'GotDeleted', a witness that @x ~ y@.  Otherwise, it
-- returns 'NotDeleted' with the unshifted index.
deleteIndex :: Delete as bs x -> Index as y -> DeletedIx bs x y
deleteIndex :: forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k).
Delete as bs x -> Index as y -> DeletedIx bs x y
deleteIndex = \case
  Delete as bs x
DelZ -> \case
    Index as y
IZ -> DeletedIx bs x x
DeletedIx bs x y
forall {k} (bs :: [k]) (x :: k). DeletedIx bs x x
GotDeleted
    IS Index bs y
i -> Index bs y -> DeletedIx bs x y
forall {k} (bs :: [k]) (y :: k) (x :: k).
Index bs y -> DeletedIx bs x y
NotDeleted Index bs y
Index bs y
i
  DelS Delete as bs x
del -> \case
    Index as y
IZ -> Index bs y -> DeletedIx bs x y
forall {k} (bs :: [k]) (y :: k) (x :: k).
Index bs y -> DeletedIx bs x y
NotDeleted Index bs y
Index (y : bs) y
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
    IS Index bs y
i -> case Delete as bs x -> Index as y -> DeletedIx bs x y
forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k).
Delete as bs x -> Index as y -> DeletedIx bs x y
deleteIndex Delete as bs x
del Index as y
Index bs y
i of
      DeletedIx bs x y
GotDeleted -> DeletedIx bs x x
DeletedIx bs x y
forall {k} (bs :: [k]) (x :: k). DeletedIx bs x x
GotDeleted
      NotDeleted Index bs y
j -> Index bs y -> DeletedIx bs x y
forall {k} (bs :: [k]) (y :: k) (x :: k).
Index bs y -> DeletedIx bs x y
NotDeleted (Index bs y -> Index (a : bs) y
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS Index bs y
j)

-- | A version of 'deleteIndex' returning a simple 'Maybe'.  This can be
-- used if you don't care about witnessing that @x ~ y@ in the case that
-- the index is the item that is deleted.
deleteIndex_ :: Delete as bs x -> Index as y -> Maybe (Index bs y)
deleteIndex_ :: forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k).
Delete as bs x -> Index as y -> Maybe (Index bs y)
deleteIndex_ Delete as bs x
del Index as y
i = case Delete as bs x -> Index as y -> DeletedIx bs x y
forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k).
Delete as bs x -> Index as y -> DeletedIx bs x y
deleteIndex Delete as bs x
del Index as y
i of
  DeletedIx bs x y
GotDeleted -> Maybe (Index bs y)
forall a. Maybe a
Nothing
  NotDeleted Index bs y
j -> Index bs y -> Maybe (Index bs y)
forall a. a -> Maybe a
Just Index bs y
j

-- | Used as the return type of 'substituteIndex'.  An @'SubstitutedIx' bs x y z@ is
-- like an @'Either' ('Index' bs y) ('Index' bs z)@, except the 'Left' case
-- witnesses that @x ~ z@.
data SubstitutedIx :: [k] -> k -> k -> k -> Type where
  GotSubbed :: Index bs y -> SubstitutedIx bs z y z
  NotSubbed :: Index bs z -> SubstitutedIx bs x y z

-- | If you substitute an item in @as@ to create @bs@, you also need to
-- reshift @'Index' as z@ into @'Index' bs z@.  This reshifts the 'Index'
-- in @as@ to become an 'Index' in @bs@, making sure the index points to
-- the same original value.
--
-- However, there is a possibility that the substituted item is the item
-- that the index was originally pointing to.  If this is the case, this
-- function returns 'GotSubbed', a witness that @x ~ z@.  Otherwise, it
-- returns 'NotSubbed'.  Both contain the updated index.
substituteIndex ::
  Substitute as bs x y ->
  Index as z ->
  SubstitutedIx bs x y z
substituteIndex :: forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k) (z :: k).
Substitute as bs x y -> Index as z -> SubstitutedIx bs x y z
substituteIndex = \case
  Substitute as bs x y
SubZ -> \case
    Index as z
IZ -> Index bs y -> SubstitutedIx bs x y x
forall {k} (bs :: [k]) (y :: k) (z :: k).
Index bs y -> SubstitutedIx bs z y z
GotSubbed Index bs y
Index (y : as) y
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
    IS Index bs z
i -> Index bs z -> SubstitutedIx bs x y z
forall {k} (bs :: [k]) (z :: k) (x :: k) (y :: k).
Index bs z -> SubstitutedIx bs x y z
NotSubbed (Index bs z -> Index (y : bs) z
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS Index bs z
i)
  SubS Substitute as bs x y
s -> \case
    Index as z
IZ -> Index bs z -> SubstitutedIx bs x y z
forall {k} (bs :: [k]) (z :: k) (x :: k) (y :: k).
Index bs z -> SubstitutedIx bs x y z
NotSubbed Index bs z
Index (z : bs) z
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
    IS Index bs z
i -> case Substitute as bs x y -> Index as z -> SubstitutedIx bs x y z
forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k) (z :: k).
Substitute as bs x y -> Index as z -> SubstitutedIx bs x y z
substituteIndex Substitute as bs x y
s Index as z
Index bs z
i of
      GotSubbed Index bs y
j -> Index bs y -> SubstitutedIx bs x y x
forall {k} (bs :: [k]) (y :: k) (z :: k).
Index bs y -> SubstitutedIx bs z y z
GotSubbed (Index bs y -> Index (c : bs) y
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS Index bs y
j)
      NotSubbed Index bs z
j -> Index bs z -> SubstitutedIx bs x y z
forall {k} (bs :: [k]) (z :: k) (x :: k) (y :: k).
Index bs z -> SubstitutedIx bs x y z
NotSubbed (Index bs z -> Index (c : bs) z
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS Index bs z
j)

-- | A version of 'substituteIndex' returning a simple 'Either'.  This can be
-- the case if you don't care about witnessing @x ~ z@ in the case that the
-- index is the item that was substituted.
substituteIndex_ ::
  Substitute as bs x y ->
  Index as z ->
  Either (Index bs y) (Index bs z)
substituteIndex_ :: forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k) (z :: k).
Substitute as bs x y
-> Index as z -> Either (Index bs y) (Index bs z)
substituteIndex_ Substitute as bs x y
sub Index as z
i = case Substitute as bs x y -> Index as z -> SubstitutedIx bs x y z
forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k) (z :: k).
Substitute as bs x y -> Index as z -> SubstitutedIx bs x y z
substituteIndex Substitute as bs x y
sub Index as z
i of
  GotSubbed Index bs y
j -> Index bs y -> Either (Index bs y) (Index bs z)
forall a b. a -> Either a b
Left Index bs y
j
  NotSubbed Index bs z
j -> Index bs z -> Either (Index bs y) (Index bs z)
forall a b. b -> Either a b
Right Index bs z
j

-- | Given an 'Index' pointing to an element, create a 'Delete'
-- corresponding to the given item.  The type of the resulting list is
-- existentially quantified, is guaranteed to be just exactly the original
-- list minus the specified element.
withDelete ::
  Index as x ->
  (forall bs. Delete as bs x -> r) ->
  r
withDelete :: forall {k} (as :: [k]) (x :: k) r.
Index as x -> (forall (bs :: [k]). Delete as bs x -> r) -> r
withDelete = \case
  Index as x
IZ -> \forall (bs :: [k]). Delete as bs x -> r
f -> Delete as as x -> r
forall (bs :: [k]). Delete as bs x -> r
f Delete as as x
Delete (x : as) as x
forall {k} (x :: k) (as :: [k]). Delete (x : as) as x
DelZ
  IS Index bs x
i -> \forall (bs :: [k]). Delete as bs x -> r
f -> Index bs x -> (forall (bs :: [k]). Delete bs bs x -> r) -> r
forall {k} (as :: [k]) (x :: k) r.
Index as x -> (forall (bs :: [k]). Delete as bs x -> r) -> r
withDelete Index bs x
i (Delete as (b1 : bs) x -> r
forall (bs :: [k]). Delete as bs x -> r
f (Delete as (b1 : bs) x -> r)
-> (Delete bs bs x -> Delete as (b1 : bs) x) -> Delete bs bs x -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Delete bs bs x -> Delete as (b1 : bs) x
Delete bs bs x -> Delete (b1 : bs) (b1 : bs) x
forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k).
Delete i x x -> Delete (y : i) (y : x) x
DelS)

-- | Given an 'Index' pointing to an element, create an 'Insert' placing an
-- item /directly before/ the given element.  The type is existentailly
-- quantified.
withInsert ::
  Index as x ->
  (forall bs. Insert as bs y -> r) ->
  r
withInsert :: forall {k} (as :: [k]) (x :: k) (y :: k) r.
Index as x -> (forall (bs :: [k]). Insert as bs y -> r) -> r
withInsert = \case
  Index as x
IZ -> \forall (bs :: [k]). Insert as bs y -> r
f -> Insert as (y : as) y -> r
forall (bs :: [k]). Insert as bs y -> r
f Insert as (y : as) y
forall {a} (as :: [a]) (x :: a). Insert as (x : as) x
InsZ
  IS Index bs x
i -> \forall (bs :: [k]). Insert as bs y -> r
f -> Index bs x -> (forall (bs :: [k]). Insert bs bs y -> r) -> r
forall {k} (as :: [k]) (x :: k) (y :: k) r.
Index as x -> (forall (bs :: [k]). Insert as bs y -> r) -> r
withInsert Index bs x
i (Insert as (b1 : bs) y -> r
forall (bs :: [k]). Insert as bs y -> r
f (Insert as (b1 : bs) y -> r)
-> (Insert bs bs y -> Insert as (b1 : bs) y) -> Insert bs bs y -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Insert bs bs y -> Insert as (b1 : bs) y
Insert bs bs y -> Insert (b1 : bs) (b1 : bs) y
forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k).
Insert i x x -> Insert (y : i) (y : x) x
InsS)

-- | Given an 'Index' pointing to an element, create an 'Insert' placing an
-- item /directly after/ the given element.  The type is existentailly
-- quantified.
withInsertAfter ::
  Index as x ->
  (forall bs. Insert as bs y -> r) ->
  r
withInsertAfter :: forall {k} (as :: [k]) (x :: k) (y :: k) r.
Index as x -> (forall (bs :: [k]). Insert as bs y -> r) -> r
withInsertAfter = \case
  Index as x
IZ -> \forall (bs :: [k]). Insert as bs y -> r
f -> Insert as (x : y : as) y -> r
forall (bs :: [k]). Insert as bs y -> r
f (Insert as (y : as) y -> Insert (x : as) (x : y : as) y
forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k).
Insert i x x -> Insert (y : i) (y : x) x
InsS Insert as (y : as) y
forall {a} (as :: [a]) (x :: a). Insert as (x : as) x
InsZ)
  IS Index bs x
i -> \forall (bs :: [k]). Insert as bs y -> r
f -> Index bs x -> (forall (bs :: [k]). Insert bs bs y -> r) -> r
forall {k} (as :: [k]) (x :: k) (y :: k) r.
Index as x -> (forall (bs :: [k]). Insert as bs y -> r) -> r
withInsertAfter Index bs x
i (Insert as (b1 : bs) y -> r
forall (bs :: [k]). Insert as bs y -> r
f (Insert as (b1 : bs) y -> r)
-> (Insert bs bs y -> Insert as (b1 : bs) y) -> Insert bs bs y -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Insert bs bs y -> Insert as (b1 : bs) y
Insert bs bs y -> Insert (b1 : bs) (b1 : bs) y
forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k).
Insert i x x -> Insert (y : i) (y : x) x
InsS)

-- | Type-level version of 'insertIndex'.  Because of how GADTs and type
-- families interact, the type-level lists and kinds of the insertion and
-- index must be provided.
type family
  InsertIndex (as :: [k]) (bs :: [k]) (x :: k) (y :: k) (ins :: Insert as bs x) (i :: Index as y) ::
    Index bs y
  where
  InsertIndex as (x ': as) x y 'InsZ i = 'IS i
  InsertIndex (y ': as) (y ': bs) x y ('InsS ins) 'IZ = 'IZ
  InsertIndex (a ': as) (a ': bs) x y ('InsS ins) ('IS i) = 'IS (InsertIndex as bs x y ins i)

-- | Defunctionalization symbol for 'InsertIndex', expecting only the kind
-- variables.
data InsertIndexSym0 as bs x y :: Insert as bs x ~> Index as y ~> Index bs y

-- | Defunctionalization symbol for 'InsertIndex', expecting the 'Insert'
-- along with the kind variables.
data InsertIndexSym as bs x y :: Insert as bs x -> Index as y ~> Index bs y

type instance Apply (InsertIndexSym0 as bs x y) ins = InsertIndexSym as bs x y ins
type instance Apply (InsertIndexSym as bs x y ins) i = InsertIndex as bs x y ins i

-- | Singleton witness for 'InsertIndex'.
sInsertIndex ::
  SInsert as bs x ins ->
  SIndex as y i ->
  SIndex bs y (InsertIndex as bs x y ins i)
sInsertIndex :: forall {k} (as :: [k]) (bs :: [k]) (x :: k) (ins :: Insert as bs x)
       (y :: k) (i :: Index as y).
SInsert as bs x ins
-> SIndex as y i -> SIndex bs y (InsertIndex as bs x y ins i)
sInsertIndex = \case
  SInsert as bs x ins
SInsZ -> SIndex as y i -> SIndex bs y (InsertIndex as bs x y ins i)
SIndex as y i -> SIndex (x : as) y ('IS i)
forall {k} (bs :: [k]) (a :: k) (i :: Index bs a) (b1 :: k).
SIndex bs a i -> SIndex (b1 : bs) a ('IS i)
SIS
  SInsS SInsert as bs x ins
ins -> \case
    SIndex as y i
SIZ -> SIndex bs y (InsertIndex as bs x y ins i)
SIndex (y : bs) y 'IZ
forall {k} (a :: k) (as1 :: [k]). SIndex (a : as1) a 'IZ
SIZ
    SIS SIndex bs y i
i -> SIndex bs y (InsertIndex as bs x y ins i)
-> SIndex (a : bs) y ('IS (InsertIndex as bs x y ins i))
forall {k} (bs :: [k]) (a :: k) (i :: Index bs a) (b1 :: k).
SIndex bs a i -> SIndex (b1 : bs) a ('IS i)
SIS (SInsert as bs x ins
-> SIndex as y i -> SIndex bs y (InsertIndex as bs x y ins i)
forall {k} (as :: [k]) (bs :: [k]) (x :: k) (ins :: Insert as bs x)
       (y :: k) (i :: Index as y).
SInsert as bs x ins
-> SIndex as y i -> SIndex bs y (InsertIndex as bs x y ins i)
sInsertIndex SInsert as bs x ins
ins SIndex as y i
SIndex bs y i
i)

-- | Helper type family for the implementation of 'DeleteIndex', to get
-- around the lack of case statements at the type level.
type family
  SuccDeletedIx (b :: k) (bs :: [k]) (x :: k) (y :: k) (del :: DeletedIx bs x y) ::
    DeletedIx (b ': bs) x y
  where
  SuccDeletedIx b bs x x 'GotDeleted = 'GotDeleted
  SuccDeletedIx b bs x y ('NotDeleted i) = 'NotDeleted ('IS i)

-- | Type-level version of 'deleteIndex'.  Because of how GADTs and type
-- families interact, the type-level lists and kinds of the insertion and
-- index must be provided.
type family
  DeleteIndex (as :: [k]) (bs :: [k]) (x :: k) (y :: k) (del :: Delete as bs x) (i :: Index as y) ::
    DeletedIx bs x y
  where
  DeleteIndex (x ': bs) bs x x 'DelZ 'IZ = 'GotDeleted
  DeleteIndex (x ': bs) bs x y 'DelZ ('IS i) = 'NotDeleted i
  DeleteIndex (y ': as) (y ': bs) x y ('DelS del) 'IZ = 'NotDeleted 'IZ
  DeleteIndex (b ': as) (b ': bs) x y ('DelS del) ('IS i) =
    SuccDeletedIx b bs x y (DeleteIndex as bs x y del i)

-- | Defunctionalization symbol for 'DeleteIndex', expecting only the kind
-- variables.
data DeleteIndexSym0 as bs x y :: Delete as bs x ~> Index as y ~> DeletedIx bs x y

-- | Defunctionalization symbol for 'DeleteIndex', expecting the 'Delete'
-- along with the kind variables.
data DeleteIndexSym as bs x y :: Delete as bs x -> Index as y ~> DeletedIx bs x y

type instance Apply (DeleteIndexSym0 as bs x y) del = DeleteIndexSym as bs x y del
type instance Apply (DeleteIndexSym as bs x y del) i = DeleteIndex as bs x y del i

-- | Kind-indexed singleton for 'DeletedIx'.
data SDeletedIx (bs :: [k]) (x :: k) (y :: k) :: DeletedIx bs x y -> Type where
  SGotDeleted :: SDeletedIx bs x x 'GotDeleted
  SNotDeleted :: SIndex bs y i -> SDeletedIx bs x y ('NotDeleted i)

-- | Singleton witness for 'DeleteIndex'.
sDeleteIndex ::
  SDelete as bs x del ->
  SIndex as y i ->
  SDeletedIx bs x y (DeleteIndex as bs x y del i)
sDeleteIndex :: forall {k} (as :: [k]) (bs :: [k]) (x :: k) (del :: Delete as bs x)
       (y :: k) (i :: Index as y).
SDelete as bs x del
-> SIndex as y i -> SDeletedIx bs x y (DeleteIndex as bs x y del i)
sDeleteIndex = \case
  SDelete as bs x del
SDelZ -> \case
    SIndex as y i
SIZ -> SDeletedIx bs x x 'GotDeleted
SDeletedIx bs x y (DeleteIndex as bs x y del i)
forall {k} (bs :: [k]) (x :: k). SDeletedIx bs x x 'GotDeleted
SGotDeleted
    SIS SIndex bs y i
i -> SIndex bs y i -> SDeletedIx bs x y ('NotDeleted i)
forall {k} (bs :: [k]) (y :: k) (i :: Index bs y) (x :: k).
SIndex bs y i -> SDeletedIx bs x y ('NotDeleted i)
SNotDeleted SIndex bs y i
SIndex bs y i
i
  SDelS SDelete as bs x del
del -> \case
    SIndex as y i
SIZ -> SIndex bs y 'IZ -> SDeletedIx bs x y ('NotDeleted 'IZ)
forall {k} (bs :: [k]) (y :: k) (i :: Index bs y) (x :: k).
SIndex bs y i -> SDeletedIx bs x y ('NotDeleted i)
SNotDeleted SIndex bs y 'IZ
SIndex (y : bs) y 'IZ
forall {k} (a :: k) (as1 :: [k]). SIndex (a : as1) a 'IZ
SIZ
    SIS SIndex bs y i
i -> case SDelete as bs x del
-> SIndex as y i -> SDeletedIx bs x y (DeleteIndex as bs x y del i)
forall {k} (as :: [k]) (bs :: [k]) (x :: k) (del :: Delete as bs x)
       (y :: k) (i :: Index as y).
SDelete as bs x del
-> SIndex as y i -> SDeletedIx bs x y (DeleteIndex as bs x y del i)
sDeleteIndex SDelete as bs x del
del SIndex as y i
SIndex bs y i
i of
      SDeletedIx bs x y (DeleteIndex as bs x y del i)
SGotDeleted -> SDeletedIx bs x x 'GotDeleted
SDeletedIx bs x y (DeleteIndex as bs x y del i)
forall {k} (bs :: [k]) (x :: k). SDeletedIx bs x x 'GotDeleted
SGotDeleted
      SNotDeleted SIndex bs y i
j -> SIndex bs y ('IS i) -> SDeletedIx bs x y ('NotDeleted ('IS i))
forall {k} (bs :: [k]) (y :: k) (i :: Index bs y) (x :: k).
SIndex bs y i -> SDeletedIx bs x y ('NotDeleted i)
SNotDeleted (SIndex bs y i -> SIndex (a : bs) y ('IS i)
forall {k} (bs :: [k]) (a :: k) (i :: Index bs a) (b1 :: k).
SIndex bs a i -> SIndex (b1 : bs) a ('IS i)
SIS SIndex bs y i
j)

-- | Helper type family for the implementation of 'SubstituteIndex', to get
-- around the lack of case statements at the type level.
type family
  SuccSubstitutedIx (b :: k) (bs :: [k]) (x :: k) (y :: k) (z :: k) (s :: SubstitutedIx bs x y z) ::
    SubstitutedIx (b ': bs) x y z
  where
  SuccSubstitutedIx b bs x y x ('GotSubbed i) = 'GotSubbed ('IS i)
  SuccSubstitutedIx b bs x y z ('NotSubbed i) = 'NotSubbed ('IS i)

-- | Type-level version of 'substituteIndex'.  Because of how GADTs and
-- type families interact, the type-level lists and kinds of the insertion
-- and index must be provided.
type family
  SubstituteIndex
    (as :: [k])
    (bs :: [k])
    (x :: k)
    (y :: k)
    (z :: k)
    (s :: Substitute as bs x y)
    (i :: Index as z) ::
    SubstitutedIx bs x y z
  where
  SubstituteIndex (z ': as) (y ': as) z y z 'SubZ 'IZ = 'GotSubbed 'IZ
  SubstituteIndex (x ': as) (y ': as) x y z 'SubZ ('IS i) = 'NotSubbed ('IS i)
  SubstituteIndex (z ': as) (z ': bs) x y z ('SubS s) 'IZ = 'NotSubbed 'IZ
  SubstituteIndex (b ': as) (b ': bs) x y z ('SubS s) ('IS i) =
    SuccSubstitutedIx b bs x y z (SubstituteIndex as bs x y z s i)

-- | Defunctionalization symbol for 'SubstituteIndex', expecting only the kind
-- variables.
data SubstituteIndexSym0 as bs x y z :: Substitute as bs x y ~> Index as z ~> SubstitutedIx bs x y z

-- | Defunctionalization symbol for 'SubstituteIndex', expecting the 'Substitute'
-- along with the kind variables.
data SubstituteIndexSym as bs x y z :: Substitute as bs x y -> Index as z ~> SubstitutedIx bs x y z

type instance Apply (SubstituteIndexSym0 as bs x y z) s = SubstituteIndexSym as bs x y z s
type instance Apply (SubstituteIndexSym as bs x y z s) i = SubstituteIndex as bs x y z s i

-- | Kind-indexed singleton for 'SubstitutedIx'.
data SSubstitutedIx (bs :: [k]) (x :: k) (y :: k) (z :: k) :: SubstitutedIx bs x y z -> Type where
  SGotSubbed :: SIndex bs y i -> SSubstitutedIx bs z y z ('GotSubbed i)
  SNotSubbed :: SIndex bs z i -> SSubstitutedIx bs x y z ('NotSubbed i)

-- | Singleton witness for 'SubstituteIndex'.
sSubstituteIndex ::
  SSubstitute as bs x y s ->
  SIndex as z i ->
  SSubstitutedIx bs x y z (SubstituteIndex as bs x y z s i)
sSubstituteIndex :: forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k)
       (s :: Substitute as bs x y) (z :: k) (i :: Index as z).
SSubstitute as bs x y s
-> SIndex as z i
-> SSubstitutedIx bs x y z (SubstituteIndex as bs x y z s i)
sSubstituteIndex = \case
  SSubstitute as bs x y s
SSubZ -> \case
    SIndex as z i
SIZ -> SIndex bs y 'IZ -> SSubstitutedIx bs x y x ('GotSubbed 'IZ)
forall {k} (bs :: [k]) (y :: k) (i :: Index bs y) (z :: k).
SIndex bs y i -> SSubstitutedIx bs z y z ('GotSubbed i)
SGotSubbed SIndex bs y 'IZ
SIndex (y : as) y 'IZ
forall {k} (a :: k) (as1 :: [k]). SIndex (a : as1) a 'IZ
SIZ
    SIS SIndex bs z i
i -> SIndex bs z ('IS i) -> SSubstitutedIx bs x y z ('NotSubbed ('IS i))
forall {k} (bs :: [k]) (z :: k) (i :: Index bs z) (x :: k)
       (y :: k).
SIndex bs z i -> SSubstitutedIx bs x y z ('NotSubbed i)
SNotSubbed (SIndex bs z i -> SIndex (y : bs) z ('IS i)
forall {k} (bs :: [k]) (a :: k) (i :: Index bs a) (b1 :: k).
SIndex bs a i -> SIndex (b1 : bs) a ('IS i)
SIS SIndex bs z i
i)
  SSubS SSubstitute as bs x y sub
s -> \case
    SIndex as z i
SIZ -> SIndex bs z 'IZ -> SSubstitutedIx bs x y z ('NotSubbed 'IZ)
forall {k} (bs :: [k]) (z :: k) (i :: Index bs z) (x :: k)
       (y :: k).
SIndex bs z i -> SSubstitutedIx bs x y z ('NotSubbed i)
SNotSubbed SIndex bs z 'IZ
SIndex (z : bs) z 'IZ
forall {k} (a :: k) (as1 :: [k]). SIndex (a : as1) a 'IZ
SIZ
    SIS SIndex bs z i
i -> case SSubstitute as bs x y sub
-> SIndex as z i
-> SSubstitutedIx bs x y z (SubstituteIndex as bs x y z sub i)
forall {k} (as :: [k]) (bs :: [k]) (x :: k) (y :: k)
       (s :: Substitute as bs x y) (z :: k) (i :: Index as z).
SSubstitute as bs x y s
-> SIndex as z i
-> SSubstitutedIx bs x y z (SubstituteIndex as bs x y z s i)
sSubstituteIndex SSubstitute as bs x y sub
s SIndex as z i
SIndex bs z i
i of
      SGotSubbed SIndex bs y i
j -> SIndex bs y ('IS i) -> SSubstitutedIx bs x y x ('GotSubbed ('IS i))
forall {k} (bs :: [k]) (y :: k) (i :: Index bs y) (z :: k).
SIndex bs y i -> SSubstitutedIx bs z y z ('GotSubbed i)
SGotSubbed (SIndex bs y i -> SIndex (c : bs) y ('IS i)
forall {k} (bs :: [k]) (a :: k) (i :: Index bs a) (b1 :: k).
SIndex bs a i -> SIndex (b1 : bs) a ('IS i)
SIS SIndex bs y i
j)
      SNotSubbed SIndex bs z i
j -> SIndex bs z ('IS i) -> SSubstitutedIx bs x y z ('NotSubbed ('IS i))
forall {k} (bs :: [k]) (z :: k) (i :: Index bs z) (x :: k)
       (y :: k).
SIndex bs z i -> SSubstitutedIx bs x y z ('NotSubbed i)
SNotSubbed (SIndex bs z i -> SIndex (c : bs) z ('IS i)
forall {k} (bs :: [k]) (a :: k) (i :: Index bs a) (b1 :: k).
SIndex bs a i -> SIndex (b1 : bs) a ('IS i)
SIS SIndex bs z i
j)