{-# LANGUAGE EmptyCase             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeInType            #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE TypeSynonymInstances  #-}
{-# 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           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         ((%~))
import qualified Control.Category          as C

-- | 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 = 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 = 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 {k} (a :: k). SingI a => Sing a
sing @bs of
      Sing bs
SList bs
SNil -> forall a. Refuted a -> Decision a
Disproved 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 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 {k} (a :: k). SingI a => Sing a
sing @as forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n2
ys of
          Proved as :~: n2
Refl -> forall a. a -> Decision a
Proved forall {a} (as :: [a]) (x :: a). Insert as (x : as) x
InsZ
          Disproved Refuted (as :~: n2)
v -> case forall {k} (a :: k). SingI a => Sing a
sing @as of
            Sing as
SList as
SNil -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case
              IsInsert as bs @@ a
Insert '[] (a : n2) a
InsZ -> Refuted (as :~: n2)
v forall {k} (a :: k). a :~: a
Refl
            Sing n1
x `SCons` (Sing n2
Sing :: Sing as') -> case Sing n1
x forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
y of
              Proved n1 :~: a
Refl -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
decide @(IsInsert as' bs') Sing a
z of
                Proved IsInsert n2 n2 @@ a
i -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ 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
i
                Disproved Refuted (IsInsert n2 n2 @@ a)
u -> forall a. Refuted a -> Decision a
Disproved 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 forall {a} (as :: [a]) (x :: a). Insert as (x : as) x
InsZ
                  InsS Insert as bs a
i -> Refuted (IsInsert n2 n2 @@ a)
u Insert as bs a
i
              Disproved Refuted (n1 :~: a)
u -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case
                IsInsert as bs @@ a
Insert (n1 : n2) (a : n2) a
InsZ   -> Refuted (as :~: n2)
v forall {k} (a :: k). a :~: a
Refl
                InsS Insert as bs a
_ -> Refuted (n1 :~: a)
u forall {k} (a :: k). a :~: a
Refl
        Disproved Refuted (n1 :~: a)
v -> case forall {k} (a :: k). SingI a => Sing a
sing @as of
          Sing as
SList as
SNil -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case
            IsInsert as bs @@ a
Insert '[] (n1 : n2) a
InsZ -> Refuted (n1 :~: a)
v forall {k} (a :: k). a :~: a
Refl
          Sing n1
x `SCons` (Sing n2
Sing :: Sing as') -> case Sing n1
x 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
decide @(IsInsert as' bs') Sing a
z of
              Proved IsInsert n2 n2 @@ a
i -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ 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
i
              Disproved Refuted (IsInsert n2 n2 @@ a)
u -> forall a. Refuted a -> Decision a
Disproved 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 forall {a} (as :: [a]) (x :: a). Insert as (x : as) x
InsZ
                InsS Insert as bs a
i -> Refuted (IsInsert n2 n2 @@ a)
u Insert as bs a
i
            Disproved Refuted (n1 :~: n1)
u -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case
              IsInsert as bs @@ a
Insert (n1 : n2) (n1 : n2) a
InsZ   -> Refuted (n1 :~: a)
v forall {k} (a :: k). a :~: a
Refl
              InsS Insert as bs a
_ -> Refuted (n1 :~: n1)
u 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 -> forall a. Refuted a -> Decision a
Disproved 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 {k} (a :: k). SingI a => Sing a
sing @as forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n2
ys of
        Proved as :~: n2
Refl -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ Sing n1
y forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: forall {a} (as :: [a]) (x :: a). Insert as (x : as) x
InsZ
        Disproved Refuted (as :~: n2)
v -> case forall {k} (a :: k). SingI a => Sing a
sing @as of
          Sing as
SList as
SNil -> forall a. Refuted a -> Decision a
Disproved 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 forall {k} (a :: k). a :~: a
Refl
          Sing n1
x `SCons` (Sing n2
Sing :: Sing as') -> case Sing n1
x 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
decide @(Found (InsertedInto as')) Sing n2
ys of
              Proved (Sing fst
z :&: TyPP (Insert n2) n2 @@ fst
i) -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ Sing fst
z forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: 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
i
              Disproved Refuted (Found (InsertedInto n2) @@ n2)
u      -> forall a. Refuted a -> Decision a
Disproved 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 forall a b. (a -> b) -> a -> b
$ Sing fst
z forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: forall {a} (as :: [a]) (x :: a). Insert as (x : as) x
InsZ
                InsS Insert as bs fst
i' -> Refuted (Found (InsertedInto n2) @@ n2)
u forall a b. (a -> b) -> a -> b
$ Sing fst
z forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: Insert as bs fst
i'
            Disproved Refuted (n1 :~: n1)
u -> forall a. Refuted a -> Decision a
Disproved 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 forall {k} (a :: k). a :~: a
Refl
              InsS Insert as bs fst
_ -> Refuted (n1 :~: n1)
u 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   -> forall {k} (x :: k) (as :: [k]). Delete (x : as) as x
DelZ
    InsS Insert as bs x
i -> forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k).
Delete i x x -> Delete (y : i) (y : x) x
DelS (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 = 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 = 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 = forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Insert as bs x -> Delete bs as x
insToDel forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Delete as bs x -> Insert bs as x
delToIns forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). 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) =
        forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (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
sing @IdSym0) forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Insert as bs x -> Delete bs as x
insToDel)
                    (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
sing @IdSym0) forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Delete as bs x -> Insert bs as x
delToIns)
      forall a b. (a -> b) -> a -> b
$ forall {k1} (p :: k1 ~> *). Decidable p => Decide p
decide @(Found (InsertedInto bs)) (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   -> forall {a} (as :: [a]) (x :: a). Insert as (x : as) x
InsZ
    DelS Delete as bs x
d -> forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k).
Insert i x x -> Insert (y : i) (y : x) x
InsS (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 = 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 = 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 = 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   -> forall {a} (x :: a) (i :: [a]) (y :: a).
Substitute (x : i) (y : i) x y
SubZ
    SubS Substitute as bs x y
s -> 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} (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 -> forall (cs :: [k]). Delete as cs x -> Insert cs bs y -> r
f forall {k} (x :: k) (as :: [k]). Delete (x : as) as x
DelZ 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 -> 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 a b. (a -> b) -> a -> b
$ \Delete as cs x
d Insert cs bs y
i -> forall (cs :: [k]). Delete as cs x -> Insert cs bs y -> r
f (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) (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
xs
    EIns Insert bs cs x
i Edit bs bs
ys -> 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 (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 -> 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 (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 -> 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 (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 = 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 = 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      -> forall k (a :: [k]). Edit a a
ENil
    EIns Insert bs bs x
i Edit as bs
ys -> forall {k} (i :: [k]) (cs :: [k]) (x :: k) (as :: [k]).
Delete i cs x -> Edit as i -> Edit as cs
EDel (forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Insert as bs x -> Delete bs as x
insToDel Insert bs bs x
i) forall k (a :: [k]). Edit a a
ENil forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Edit as bs -> Edit bs cs -> Edit as cs
`compEdit` 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 -> forall {k} (i :: [k]) (cs :: [k]) (x :: k) (as :: [k]).
Insert i cs x -> Edit as i -> Edit as cs
EIns (forall {k} (as :: [k]) (bs :: [k]) (x :: k).
Delete as bs x -> Insert bs as x
delToIns Delete bs bs x
d) forall k (a :: [k]). Edit a a
ENil forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Edit as bs -> Edit bs cs -> Edit as cs
`compEdit` 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 -> forall {k} (i :: [k]) (cs :: [k]) (x :: k) (y :: k) (as :: [k]).
Substitute i cs x y -> Edit as i -> Edit as cs
ESub (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) forall k (a :: [k]). Edit a a
ENil forall {k} (as :: [k]) (bs :: [k]) (cs :: [k]).
Edit as bs -> Edit bs cs -> Edit as cs
`compEdit` 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   -> 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 forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& 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 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 r
x, 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) = 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 rs
xs
                 in  (f x
y, f r
x 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 rs
xs
    DelS Delete as bs x
d -> \case
      f r
x :& Rec f rs
xs -> f r
x forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& 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 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)) = 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 -> (forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec f rs
xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> f (f y)
f f r
x
      SubS Substitute as bs x y
s -> \case
        f r
x :& Rec f rs
xs -> (f r
x forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 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 = forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over (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   -> 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   -> forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
      IS Index bs y
i -> forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS (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 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   -> forall {k} (bs :: [k]) (x :: k). DeletedIx bs x x
GotDeleted
      IS Index bs y
i -> forall {k} (bs :: [k]) (y :: k) (x :: k).
Index bs y -> DeletedIx bs x y
NotDeleted Index bs y
i
    DelS Delete as bs x
del -> \case
      Index as y
IZ   -> forall {k} (bs :: [k]) (y :: k) (x :: k).
Index bs y -> DeletedIx bs x y
NotDeleted forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
      IS Index bs y
i -> case 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 bs y
i of
        DeletedIx bs x y
GotDeleted   -> forall {k} (bs :: [k]) (x :: k). DeletedIx bs x x
GotDeleted
        NotDeleted Index bs y
j -> forall {k} (bs :: [k]) (y :: k) (x :: k).
Index bs y -> DeletedIx bs x y
NotDeleted (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 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   -> forall a. Maybe a
Nothing
    NotDeleted Index bs y
j -> 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   -> forall {k} (bs :: [k]) (y :: k) (z :: k).
Index bs y -> SubstitutedIx bs z y z
GotSubbed forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
      IS Index bs z
i -> forall {k} (bs :: [k]) (z :: k) (x :: k) (y :: k).
Index bs z -> SubstitutedIx bs x y z
NotSubbed (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   -> forall {k} (bs :: [k]) (z :: k) (x :: k) (y :: k).
Index bs z -> SubstitutedIx bs x y z
NotSubbed forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
      IS Index bs z
i -> case 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 bs z
i of
        GotSubbed Index bs y
j -> forall {k} (bs :: [k]) (y :: k) (z :: k).
Index bs y -> SubstitutedIx bs z y z
GotSubbed (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 -> forall {k} (bs :: [k]) (z :: k) (x :: k) (y :: k).
Index bs z -> SubstitutedIx bs x y z
NotSubbed (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 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 -> forall a b. a -> Either a b
Left  Index bs y
j
    NotSubbed Index bs z
j -> 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 -> forall (bs :: [k]). Delete as bs x -> r
f 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 -> forall {k} (as :: [k]) (x :: k) r.
Index as x -> (forall (bs :: [k]). Delete as bs x -> r) -> r
withDelete Index bs x
i (forall (bs :: [k]). Delete as bs x -> r
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> forall (bs :: [k]). Insert as bs y -> r
f 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 -> 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 (forall (bs :: [k]). Insert as bs y -> r
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> forall (bs :: [k]). Insert as bs y -> r
f (forall {k} (i :: [k]) (x :: [k]) (x :: k) (y :: k).
Insert i x x -> Insert (y : i) (y : x) x
InsS 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 -> 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 (forall (bs :: [k]). Insert as bs y -> r
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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     -> 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   -> forall {k} (a :: k) (as1 :: [k]). SIndex (a : as1) a 'IZ
SIZ
      SIS SIndex bs y i
i -> forall {k} (bs :: [k]) (a :: k) (i :: Index bs a) (b1 :: k).
SIndex bs a i -> SIndex (b1 : bs) a ('IS i)
SIS (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 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   -> forall {k} (bs :: [k]) (x :: k). SDeletedIx bs x x 'GotDeleted
SGotDeleted
      SIS SIndex bs y i
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
i
    SDelS SDelete as bs x del
del -> \case
      SIndex as y i
SIZ   -> forall {k} (bs :: [k]) (y :: k) (i :: Index bs y) (x :: k).
SIndex bs y i -> SDeletedIx bs x y ('NotDeleted i)
SNotDeleted forall {k} (a :: k) (as1 :: [k]). SIndex (a : as1) a 'IZ
SIZ
      SIS SIndex bs y i
i -> case 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 bs y i
i of
        SDeletedIx bs x y (DeleteIndex as bs x y del i)
SGotDeleted   -> forall {k} (bs :: [k]) (x :: k). SDeletedIx bs x x 'GotDeleted
SGotDeleted
        SNotDeleted SIndex bs y i
j -> forall {k} (bs :: [k]) (y :: k) (i :: Index bs y) (x :: k).
SIndex bs y i -> SDeletedIx bs x y ('NotDeleted i)
SNotDeleted (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   -> forall {k} (bs :: [k]) (y :: k) (i :: Index bs y) (z :: k).
SIndex bs y i -> SSubstitutedIx bs z y z ('GotSubbed i)
SGotSubbed forall {k} (a :: k) (as1 :: [k]). SIndex (a : as1) a 'IZ
SIZ
      SIS SIndex bs z i
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 (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   -> 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 forall {k} (a :: k) (as1 :: [k]). SIndex (a : as1) a 'IZ
SIZ
      SIS SIndex bs z i
i -> case 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 bs z i
i of
        SGotSubbed SIndex bs y i
j -> forall {k} (bs :: [k]) (y :: k) (i :: Index bs y) (z :: k).
SIndex bs y i -> SSubstitutedIx bs z y z ('GotSubbed i)
SGotSubbed (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 -> 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 (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)