Generics.MRSOP.GDiff

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.

Documentation

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

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

Extracts an SNat from a Cof

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

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)

Values of type Cof support heterogeneous equality checking.

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

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)

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

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'

Arguments

:: (IsNat ix1, IsNat ix2, EqHO ki)

=> ES ki codes '[I ix1] '[I ix2]

-> Fix ki codes ix1

-> Maybe (Fix ki codes ix2)

applyES

Arguments

:: EqHO ki

=> ES ki codes xs ys

-> PoA ki (Fix ki codes) xs

-> Maybe (PoA ki (Fix ki codes) ys)

diff

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'

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

Extracts the cost of an edit script