Safe Haskell	None
Language	Haskell2010

Generics.MRSOP.GDiff

Description

This module has been taken from arianvp/generics-mrsop-diff, it essentially isolates Arian's fixes over GDiff and adapts them to work over newer versions of generics-mrsop.

Synopsis

data Cof (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Atom kon -> [Atom kon] -> * where
- ConstrI :: (IsNat c, IsNat n) => Constr (Lkup n codes) c -> ListPrf (Lkup c (Lkup n codes)) -> Cof ki codes (I n) (Lkup c (Lkup n codes))
- ConstrK :: ki k -> Cof ki codes (K k) '[]
cofIdx :: forall ki codes xs n. IsNat n => Cof ki codes (I n) xs -> SNat n
cofWitnessI :: Cof ki codes (I n) t -> Proxy n
cofHeq :: (EqHO ki, TestEquality ki) => Cof ki codes a t1 -> Cof ki codes b t2 -> Maybe (a :~: b, t1 :~: t2)
data ES (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [Atom kon] -> [Atom kon] -> * where
- ES0 :: ES ki codes '[] '[]
- Ins :: Int -> Cof ki codes a t -> ES ki codes i (t :++: j) -> ES ki codes i (a ': j)
- Del :: Int -> Cof ki codes a t -> ES ki codes (t :++: i) j -> ES ki codes (a ': i) j
- Cpy :: Int -> Cof ki codes a t -> ES ki codes (t :++: i) (t :++: j) -> ES ki codes (a ': i) (a ': j)
apply :: forall ki fam codes ty1 ty2 ix1 ix2. (Family ki fam codes, ix1 ~ Idx ty1 fam, ix2 ~ Idx ty2 fam, Lkup ix1 fam ~ ty1, Lkup ix2 fam ~ ty2, IsNat ix1, IsNat ix2, EqHO ki, TestEquality ki) => ES ki codes '[I ix1] '[I ix2] -> ty1 -> Maybe ty2
apply' :: (IsNat ix1, IsNat ix2, EqHO ki) => ES ki codes '[I ix1] '[I ix2] -> Fix ki codes ix1 -> Maybe (Fix ki codes ix2)
applyES :: EqHO ki => ES ki codes xs ys -> PoA ki (Fix ki codes) xs -> Maybe (PoA ki (Fix ki codes) ys)
diff :: forall fam ki codes ix1 ix2 ty1 ty2. (Family ki fam codes, ix1 ~ Idx ty1 fam, ix2 ~ Idx ty2 fam, Lkup ix1 fam ~ ty1, Lkup ix2 fam ~ ty2, IsNat ix1, IsNat ix2, EqHO ki, TestEquality ki) => ty1 -> ty2 -> ES ki codes '[I ix1] '[I ix2]
diff' :: (EqHO ki, IsNat ix1, IsNat ix2, TestEquality ki) => Fix ki codes ix1 -> Fix ki codes ix2 -> ES ki codes '[I ix1] '[I ix2]
cost :: ES ki codes txs tys -> Int

Documentation

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

A Cof represents a leaf of the flattened representation of our tree. Hence, it will be either a constructor of a particular datatype or an opaque value.

Constructors

ConstrI :: (IsNat c, IsNat n) => Constr (Lkup n codes) c -> ListPrf (Lkup c (Lkup n codes)) -> Cof ki codes (I n) (Lkup c (Lkup n codes))	A constructor tells us the type of its arguments and which type in the family it constructs
ConstrK :: ki k -> Cof ki codes (K k) '[]	Requires no arguments to complete

cofIdx :: forall ki codes xs n. IsNat n => Cof ki codes (I n) xs -> SNat n Source #

Extracts an SNat from a Cof

cofWitnessI :: Cof ki codes (I n) t -> Proxy n Source #

Extracts a proxy from a Cof

cofHeq :: (EqHO ki, TestEquality ki) => Cof ki codes a t1 -> Cof ki codes b t2 -> Maybe (a :~: b, t1 :~: t2) Source #

Values of type Cof support heterogeneous equality checking.

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

An edit script will insert, delete or copy Cofs. We keep the cost of the edit script annotated in the constructor

Constructors

ES0 :: ES ki codes '[] '[]
Ins :: Int -> Cof ki codes a t -> ES ki codes i (t :++: j) -> ES ki codes i (a ': j)
Del :: Int -> Cof ki codes a t -> ES ki codes (t :++: i) j -> ES ki codes (a ': i) j
Cpy :: Int -> Cof ki codes a t -> ES ki codes (t :++: i) (t :++: j) -> ES ki codes (a ': i) (a ': j)

Instances

(HasDatatypeInfo ki fam codes, ShowHO ki) => Show (ES ki codes xs ys) Source #
Instance details Defined in Generics.MRSOP.GDiff Methods showsPrec :: Int -> ES ki codes xs ys -> ShowS # show :: ES ki codes xs ys -> String # showList :: [ES ki codes xs ys] -> ShowS #

apply Source #

Arguments

:: (Family ki fam codes, ix1 ~ Idx ty1 fam, ix2 ~ Idx ty2 fam, Lkup ix1 fam ~ ty1, Lkup ix2 fam ~ ty2, IsNat ix1, IsNat ix2, EqHO ki, TestEquality ki)
=> ES ki codes '[I ix1] '[I ix2]
-> ty1
-> Maybe ty2

apply' Source #

Arguments

:: (IsNat ix1, IsNat ix2, EqHO ki)
=> ES ki codes '[I ix1] '[I ix2]
-> Fix ki codes ix1
-> Maybe (Fix ki codes ix2)

applyES Source #

Arguments

:: EqHO ki
=> ES ki codes xs ys
-> PoA ki (Fix ki codes) xs
-> Maybe (PoA ki (Fix ki codes) ys)

diff Source #

Arguments

:: (Family ki fam codes, ix1 ~ Idx ty1 fam, ix2 ~ Idx ty2 fam, Lkup ix1 fam ~ ty1, Lkup ix2 fam ~ ty2, IsNat ix1, IsNat ix2, EqHO ki, TestEquality ki)
=> ty1
-> ty2
-> ES ki codes '[I ix1] '[I ix2]

diff' Source #

Arguments

:: (EqHO ki, IsNat ix1, IsNat ix2, TestEquality ki)
=> Fix ki codes ix1
-> Fix ki codes ix2
-> ES ki codes '[I ix1] '[I ix2]

cost :: ES ki codes txs tys -> Int Source #

Extracts the cost of an edit script