Safe Haskell	None
Language	Haskell2010

Generics.MRSOP.STDiff.Types

Contents

Functorial Changes
Fixpoint Changes

Synopsis

data TrivialK (ki :: kon -> *) :: kon -> * where
- Trivial :: ki kon -> ki kon -> TrivialK ki kon
data At (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Atom kon -> * where
- AtSet :: TrivialK ki kon -> At ki codes (K kon)
- AtFix :: IsNat ix => Almu ki codes ix ix -> At ki codes (I ix)
data Al (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [Atom kon] -> [Atom kon] -> * where
- A0 :: Al ki codes '[] '[]
- AX :: At ki codes x -> Al ki codes xs ys -> Al ki codes (x ': xs) (x ': ys)
- ADel :: NA ki (Fix ki codes) x -> Al ki codes xs ys -> Al ki codes (x ': xs) ys
- AIns :: NA ki (Fix ki codes) x -> Al ki codes xs ys -> Al ki codes xs (x ': ys)
data Spine (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [[Atom kon]] -> [[Atom kon]] -> * where
- Scp :: Spine ki codes s1 s1
- SCns :: Constr s1 c1 -> NP (At ki codes) (Lkup c1 s1) -> Spine ki codes s1 s1
- SChg :: Constr s1 c1 -> Constr s2 c2 -> Al ki codes (Lkup c1 s1) (Lkup c2 s2) -> Spine ki codes s1 s2
data Ctx (ki :: kon -> *) (codes :: [[[Atom kon]]]) (p :: Nat -> Nat -> *) (ix :: Nat) :: [Atom kon] -> * where
- H :: IsNat iy => p ix iy -> PoA ki (Fix ki codes) xs -> Ctx ki codes p ix (I iy ': xs)
- T :: NA ki (Fix ki codes) a -> Ctx ki codes p ix xs -> Ctx ki codes p ix (a ': xs)
type InsCtx ki codes ix xs = Ctx ki codes (Almu ki codes) ix xs
type DelCtx ki codes ix xs = Ctx ki codes (AlmuMin ki codes) ix xs
newtype AlmuMin ki codes ix iy = AlmuMin {
- unAlmuMin :: Almu ki codes iy ix
}
data Almu (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Nat -> Nat -> * where
- Spn :: Spine ki codes (Lkup ix codes) (Lkup iy codes) -> Almu ki codes ix iy
- Ins :: Constr (Lkup iy codes) c -> InsCtx ki codes ix (Lkup c (Lkup iy codes)) -> Almu ki codes ix iy
- Del :: IsNat iy => Constr (Lkup ix codes) c -> DelCtx ki codes iy (Lkup c (Lkup ix codes)) -> Almu ki codes ix iy

Functorial Changes

Represents changes on the first layer of two values of mutually recursive families. For a more in-depth explanation of the datatypes and their meaning we refer the interested reader to the relevant literature:

Miraldo, Dagand and Swierstra, TyDe 2017 pdf
van Putten, MSc thesis https://dspace.library.uu.nl/handle/1874/380853

data TrivialK (ki :: kon -> *) :: kon -> * where Source #

Represents a change between two opaque values. When they are equal represents a copy.

Constructors

Trivial :: ki kon -> ki kon -> TrivialK ki kon

data At (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Atom kon -> * where Source #

Represents a change between two atoms, where an atom is either a recursive or an opaque value.

Constructors

AtSet :: TrivialK ki kon -> At ki codes (K kon)
AtFix :: IsNat ix => Almu ki codes ix ix -> At ki codes (I ix)

data Al (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [Atom kon] -> [Atom kon] -> * where Source #

Represents an alignment between two product of atoms.

Constructors

A0 :: Al ki codes '[] '[]
AX :: At ki codes x -> Al ki codes xs ys -> Al ki codes (x ': xs) (x ': ys)
ADel :: NA ki (Fix ki codes) x -> Al ki codes xs ys -> Al ki codes (x ': xs) ys
AIns :: NA ki (Fix ki codes) x -> Al ki codes xs ys -> Al ki codes xs (x ': ys)

data Spine (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [[Atom kon]] -> [[Atom kon]] -> * where Source #

Represents a change at the coproduct structure.

Constructors

Scp :: Spine ki codes s1 s1
SCns :: Constr s1 c1 -> NP (At ki codes) (Lkup c1 s1) -> Spine ki codes s1 s1
SChg :: Constr s1 c1 -> Constr s2 c2 -> Al ki codes (Lkup c1 s1) (Lkup c2 s2) -> Spine ki codes s1 s2

Fixpoint Changes

The next datatypes represent a sequence of Spine, Al and At assembled coupled with operators to describe changes in the recursive structure such as inserting and deleting constructors.

data Ctx (ki :: kon -> *) (codes :: [[[Atom kon]]]) (p :: Nat -> Nat -> *) (ix :: Nat) :: [Atom kon] -> * where Source #

Represents a one-hole context over a NP (NA ki (fix ki codes)) xs where the hole is in a distinguished element indexed by 'I ix and is filled with applying p to the relevant indexes.

Constructors

H :: IsNat iy => p ix iy -> PoA ki (Fix ki codes) xs -> Ctx ki codes p ix (I iy ': xs)
T :: NA ki (Fix ki codes) a -> Ctx ki codes p ix xs -> Ctx ki codes p ix (a ': xs)

type InsCtx ki codes ix xs = Ctx ki codes (Almu ki codes) ix xs Source #

Simple synonym for contexts.

type DelCtx ki codes ix xs = Ctx ki codes (AlmuMin ki codes) ix xs Source #

A deletion context needs to swap the indexes in the hole, hence we use a newtype for that.

newtype AlmuMin ki codes ix iy Source #

The newtype used to swap the indexes to |Almu|.

Constructors

AlmuMin
Fields unAlmuMin :: Almu ki codes iy ix

data Almu (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Nat -> Nat -> * where Source #

Represent recursive spines.

Constructors

Spn :: Spine ki codes (Lkup ix codes) (Lkup iy codes) -> Almu ki codes ix iy
Ins :: Constr (Lkup iy codes) c -> InsCtx ki codes ix (Lkup c (Lkup iy codes)) -> Almu ki codes ix iy
Del :: IsNat iy => Constr (Lkup ix codes) c -> DelCtx ki codes iy (Lkup c (Lkup ix codes)) -> Almu ki codes ix iy