{-# 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 (
Insert (..),
autoInsert,
Delete (..),
autoDelete,
insToDel,
delToIns,
Substitute (..),
autoSubstitute,
flipSub,
subToDelIns,
IsInsert,
InsertedInto,
IsDelete,
DeletedFrom,
IsSubstitute,
SInsert (..),
SDelete (..),
SSubstitute (..),
Edit (..),
compEdit,
flipEdit,
insertRec,
deleteRec,
deleteGetRec,
recLens,
substituteRec,
insertIndex,
DeletedIx (..),
deleteIndex,
deleteIndex_,
SubstitutedIx (..),
substituteIndex,
substituteIndex_,
withDelete,
withInsert,
withInsertAfter,
InsertIndex,
sInsertIndex,
SDeletedIx (..),
DeleteIndex,
sDeleteIndex,
SSubstitutedIx (..),
SubstituteIndex,
sSubstituteIndex,
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 ((%~))
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)
type IsInsert as bs = TyPred (Insert as bs)
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
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
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
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)
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)
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)
type IsDelete as bs = TyPred (Delete as bs)
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)
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)
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
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)
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)
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)
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
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
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
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)
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)
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)
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)
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)
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
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
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
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)
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
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
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)
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)
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)
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)
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
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
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)
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
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)
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)
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 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)
data InsertIndexSym0 as bs x y :: Insert as bs x ~> Index as y ~> Index bs y
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
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)
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 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)
data DeleteIndexSym0 as bs x y :: Delete as bs x ~> Index as y ~> DeletedIx bs x y
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
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)
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)
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 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)
data SubstituteIndexSym0 as bs x y z :: Substitute as bs x y ~> Index as z ~> SubstitutedIx bs x y z
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
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)
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)