{-# 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.Kind
import Data.Singletons
import Data.Singletons.Decide
import Data.Singletons.Prelude
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 = InsZ
instance {-# INCOHERENT #-} Auto (IsInsert as bs) x => Auto (IsInsert (a ': as) (a ': bs)) x where
auto = InsS (auto @_ @(IsInsert as bs) @x)
instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsInsert as bs) where
decide z = case sing @bs of
SNil -> Disproved $ \case {}
y `SCons` (ys@Sing :: Sing bs') -> case y %~ z of
Proved Refl -> case sing @as %~ ys of
Proved Refl -> Proved InsZ
Disproved v -> case sing @as of
SNil -> Disproved $ \case
InsZ -> v Refl
x `SCons` (Sing :: Sing as') -> case x %~ y of
Proved Refl -> case decide @(IsInsert as' bs') z of
Proved i -> Proved $ InsS i
Disproved u -> Disproved $ \case
InsZ -> u InsZ
InsS i -> u i
Disproved u -> Disproved $ \case
InsZ -> v Refl
InsS _ -> u Refl
Disproved v -> case sing @as of
SNil -> Disproved $ \case
InsZ -> v Refl
x `SCons` (Sing :: Sing as') -> case x %~ y of
Proved Refl -> case decide @(IsInsert as' bs') z of
Proved i -> Proved $ InsS i
Disproved u -> Disproved $ \case
InsZ -> u InsZ
InsS i -> u i
Disproved u -> Disproved $ \case
InsZ -> v Refl
InsS _ -> u Refl
type InsertedInto (as :: [k]) = (TyPP (Insert as) :: ParamPred [k] k)
instance (SDecide k, SingI (as :: [k])) => Decidable (Found (InsertedInto as)) where
decide = \case
SNil -> Disproved $ \(_ :&: i) -> case i of {}
y `SCons` ys -> case sing @as %~ ys of
Proved Refl -> Proved $ y :&: InsZ
Disproved v -> case sing @as of
SNil -> Disproved $ \(_ :&: i) -> case i of
InsZ -> v Refl
x `SCons` (Sing :: Sing as') -> case x %~ y of
Proved Refl -> case decide @(Found (InsertedInto as')) ys of
Proved (z :&: i) -> Proved $ z :&: InsS i
Disproved u -> Disproved $ \(z :&: i) -> case i of
InsZ -> u $ z :&: InsZ
InsS i' -> u $ z :&: i'
Disproved u -> Disproved $ \(_ :&: i) -> case i of
InsZ -> v Refl
InsS _ -> u Refl
autoInsert :: forall as bs x. Auto (IsInsert as bs) x => Insert as bs x
autoInsert = auto @_ @(IsInsert as bs) @x
data SInsert as bs x :: 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 = \case
InsZ -> DelZ
InsS i -> DelS (insToDel 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 = DelZ
instance {-# INCOHERENT #-} Auto (IsDelete as bs) x => Auto (IsDelete (a ': as) (a ': bs)) x where
auto = DelS (auto @_ @(IsDelete as bs) @x)
instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsDelete as bs) where
decide = mapDecision insToDel delToIns . 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 (Sing :: Sing bs) =
mapDecision (mapSigma (sing @IdSym0) insToDel)
(mapSigma (sing @IdSym0) delToIns)
$ decide @(Found (InsertedInto bs)) (sing @as)
autoDelete :: forall as bs x. Auto (IsDelete as bs) x => Delete as bs x
autoDelete = auto @_ @(IsDelete as bs) @x
data SDelete as bs x :: 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 = \case
DelZ -> InsZ
DelS d -> InsS (delToIns 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 = SubZ
instance Auto (IsSubstitute as bs x) y => Auto (IsSubstitute (c ': as) (c ': bs) x) y where
auto = SubS (auto @_ @(IsSubstitute as bs x) @y)
instance {-# INCOHERENT #-} Auto (IsSubstitute (x ': as) (x ': as) x) x where
auto = SubZ
autoSubstitute :: forall as bs x y. Auto (IsSubstitute as bs x) y => Substitute as bs x y
autoSubstitute = auto @_ @(IsSubstitute as bs x) @y
data SSubstitute as bs x y :: 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 = \case
SubZ -> SubZ
SubS s -> SubS (flipSub s)
subToDelIns
:: Substitute as bs x y
-> (forall cs. Delete as cs x -> Insert cs bs y -> r)
-> r
subToDelIns = \case
SubZ -> \f -> f DelZ InsZ
SubS s -> \f -> subToDelIns s $ \d i -> f (DelS d) (InsS 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 xs = \case
ENil -> xs
EIns i ys -> EIns i (compEdit xs ys)
EDel d ys -> EDel d (compEdit xs ys)
ESub s ys -> ESub s (compEdit xs ys)
instance C.Category Edit where
id = ENil
xs . ys = compEdit ys xs
flipEdit :: Edit as bs -> Edit bs as
flipEdit = \case
ENil -> ENil
EIns i ys -> EDel (insToDel i) ENil `compEdit` flipEdit ys
EDel d ys -> EIns (delToIns d) ENil `compEdit` flipEdit ys
ESub s ys -> ESub (flipSub s) ENil `compEdit` flipEdit ys
insertRec :: Insert as bs x -> f x -> Rec f as -> Rec f bs
insertRec = \case
InsZ -> (:&)
InsS i -> \x -> \case
y :& ys -> y :& insertRec i x ys
deleteGetRec :: Delete as bs x -> Rec f as -> (f x, Rec f bs)
deleteGetRec = \case
DelZ -> \case
x :& xs -> (x, xs)
DelS d -> \case
x :& xs -> let (y, ys) = deleteGetRec d xs
in (y, x :& ys)
deleteRec :: Delete as bs x -> Rec f as -> Rec f bs
deleteRec = \case
DelZ -> \case
_ :& xs -> xs
DelS d -> \case
x :& xs -> x :& deleteRec d 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 s0 (f :: f x -> g (f y)) = go s0
where
go :: Substitute cs ds x y
-> Rec f cs
-> g (Rec f ds)
go = \case
SubZ -> \case
x :& xs -> (:& xs) <$> f x
SubS s -> \case
x :& xs -> (x :&) <$> go s xs
substituteRec
:: Substitute as bs x y
-> (f x -> f y)
-> Rec f as
-> Rec f bs
substituteRec s = over (recLens s)
insertIndex :: Insert as bs x -> Index as y -> Index bs y
insertIndex = \case
InsZ -> IS
InsS ins -> \case
IZ -> IZ
IS i -> IS (insertIndex ins 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 = \case
DelZ -> \case
IZ -> GotDeleted
IS i -> NotDeleted i
DelS del -> \case
IZ -> NotDeleted IZ
IS i -> case deleteIndex del i of
GotDeleted -> GotDeleted
NotDeleted j -> NotDeleted (IS j)
deleteIndex_ :: Delete as bs x -> Index as y -> Maybe (Index bs y)
deleteIndex_ del i = case deleteIndex del i of
GotDeleted -> Nothing
NotDeleted j -> Just 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 = \case
SubZ -> \case
IZ -> GotSubbed IZ
IS i -> NotSubbed (IS i)
SubS s -> \case
IZ -> NotSubbed IZ
IS i -> case substituteIndex s i of
GotSubbed j -> GotSubbed (IS j)
NotSubbed j -> NotSubbed (IS j)
substituteIndex_
:: Substitute as bs x y
-> Index as z
-> Either (Index bs y) (Index bs z)
substituteIndex_ sub i = case substituteIndex sub i of
GotSubbed j -> Left j
NotSubbed j -> Right j
withDelete
:: Index as x
-> (forall bs. Delete as bs x -> r)
-> r
withDelete = \case
IZ -> \f -> f DelZ
IS i -> \f -> withDelete i (f . DelS)
withInsert
:: Index as x
-> (forall bs. Insert as bs y -> r)
-> r
withInsert = \case
IZ -> \f -> f InsZ
IS i -> \f -> withInsert i (f . InsS)
withInsertAfter
:: Index as x
-> (forall bs. Insert as bs y -> r)
-> r
withInsertAfter = \case
IZ -> \f -> f (InsS InsZ)
IS i -> \f -> withInsertAfter i (f . InsS)
type family InsertIndex as bs x y (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 = \case
SInsZ -> SIS
SInsS ins -> \case
SIZ -> SIZ
SIS i -> SIS (sInsertIndex ins i)
type family SuccDeletedIx b bs x y (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 bs x y (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 x y :: 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 = \case
SDelZ -> \case
SIZ -> SGotDeleted
SIS i -> SNotDeleted i
SDelS del -> \case
SIZ -> SNotDeleted SIZ
SIS i -> case sDeleteIndex del i of
SGotDeleted -> SGotDeleted
SNotDeleted j -> SNotDeleted (SIS j)
type family SuccSubstitutedIx b bs x y z (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 bs x y z (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 x y z :: 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 = \case
SSubZ -> \case
SIZ -> SGotSubbed SIZ
SIS i -> SNotSubbed (SIS i)
SSubS s -> \case
SIZ -> SNotSubbed SIZ
SIS i -> case sSubstituteIndex s i of
SGotSubbed j -> SGotSubbed (SIS j)
SNotSubbed j -> SNotSubbed (SIS j)