{-# 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 (
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 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
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 = 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
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
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 -> 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)
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 = 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)
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)
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 -> 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)
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 = 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 = 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
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 -> 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)
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)
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
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)
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
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
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
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)
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
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
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)
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)
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 -> 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)
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
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 -> 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)
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
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)
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)
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 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 -> 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)
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 -> 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)
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 -> 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)