Generics.MRSOP.STDiff.Compute

Annotating Trees

First we use gdiff to annotate the source and destination forests before translating them to a Almu The idea being that the information comming from gdiff is sufficient to know which constructors are copies and which have been modified.

data Ann

Annotations to be placed throughout the tree.

Constructors

Modify

Copy

Instances

Show Ann

Defined in Generics.MRSOP.STDiff.Compute

Methods

showsPrec :: Int -> Ann -> ShowS

show :: Ann -> String

showList :: [Ann] -> ShowS

injCofAnn :: Cof ki codes a t -> Const ann ix -> PoA ki (AnnFix ki codes (Const ann)) t -> NA ki (AnnFix ki codes (Const ann)) a

Adds an annotated constructor to a product of atoms.

insCofAnn :: Cof ki codes a t -> Const ann ix -> PoA ki (AnnFix ki codes (Const ann)) (t :++: as) -> PoA ki (AnnFix ki codes (Const ann)) (a ': as)

Inserts an annotated constructor at the head of a product of atoms.

annSrc

Arguments

:: (EqHO ki, IsNat ix)

=> Fix ki codes ix

-> ES ki codes '[I ix] ys

-> AnnFix ki codes (Const Ann) ix

Annotates the source of an edit script.

annDest

Arguments

:: (EqHO ki, IsNat ix)

=> Fix ki codes ix

-> ES ki codes xs '[I ix]

-> AnnFix ki codes (Const Ann) ix

Annotates the destination of an edit script.

Differencing Annotated Trees

Once we have annotated the trees on the source and destination of the edit script, we can easily diff them in the stdiff style.

Stiff Patches

We call a patch stiff if it has no copies. It is trivial to produce sauch a patch given two elements. We simply delete the entire source and insert the entire destination.

stiffAlmu

Arguments

:: (TestEquality ki, EqHO ki)

=> Fix ki codes ix

-> Fix ki codes iy

-> Almu ki codes ix iy

stiffSpine

Arguments

:: (TestEquality ki, EqHO ki)

=> Rep ki (Fix ki codes) xs

-> Rep ki (Fix ki codes) ys

-> Spine ki codes xs ys

stiffAt

Arguments

:: (TestEquality ki, EqHO ki)

=> NA ki (Fix ki codes) x

-> NA ki (Fix ki codes) x

-> At ki codes x

stiffAl

Arguments

:: (TestEquality ki, EqHO ki)

=> PoA ki (Fix ki codes) xs

-> PoA ki (Fix ki codes) ys

-> Al ki codes xs ys

Copy Counting

In order to decide which path to follow from the roof to the leaves whenver we are faced with a choice, we will pre-compute the amount of copies present in each subtree.

copiesAlgebra

Arguments

:: Const Ann ix

-> Rep ki (Const Int) xs

-> Const Int ix

Algebra for counting copies.

countCopies

Arguments

:: IsNat ix

=> AnnFix ki codes (Const Ann) ix

-> AnnFix ki codes (Const Int :*: Const Ann) ix

Annotates the tree with how many copies are underneath each node (inclusive with self)

copies Copy = 1 + copies children
copies Modify = copies children

hasCopies :: AnnFix ki codes (Const Int :*: chi) ix -> Bool

Returns whether or not a subtree constains any copies.

myGetAnn :: (Const Int :*: Const Ann) x -> Ann

Easily retrieves annotations

myGetAnnAt :: NA ki (AnnFix ki codes (Const Int :*: Const Ann)) (I x) -> Ann

myGetCopies :: (Const Int :*: Const Ann) x -> Int

Easily retrieves annotations

myForgetAnn :: NA ki (AnnFix ki codes (Const Int :*: Const Ann)) at -> NA ki (Fix ki codes) at

Computing the Patch

Given trees annotated with information about each of their constructors and how many of those are supposed to be copied, we can finally deterministically translate two tress into a patch.

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

Constructors

CtxIns :: InsOrDel ki codes (Almu ki codes)

CtxDel :: InsOrDel ki codes (AlmuMin ki codes)

diffCtx :: forall ki codes p ix xs. (EqHO ki, TestEquality ki, IsNat ix) => InsOrDel ki codes p -> AnnFix ki codes (Const Int :*: Const Ann) ix -> PoA ki (AnnFix ki codes (Const Int :*: Const Ann)) xs -> Ctx ki codes p ix xs

Finds the element in the PoA ... xs with the most copies and diff the given AnnFix.

PRECONDITION: The PoA .. xs must contain at least one tree with a copy. Always guard this call with hasCopies

diffAlmu

Arguments

:: (EqHO ki, IsNat ix, IsNat iy, TestEquality ki)

=> AnnFix ki codes (Const Int :*: Const Ann) ix

-> AnnFix ki codes (Const Int :*: Const Ann) iy

-> Almu ki codes ix iy

Takes two annotated trees, and produces a patch

diffSpine

Arguments

:: (TestEquality ki, EqHO ki, IsNat ix, IsNat iy)

=> SNat ix

We need these to identify the mutrec family

-> SNat iy

-> Rep ki (AnnFix ki codes (Const Int :*: Const Ann)) (Lkup ix codes)

-> Rep ki (AnnFix ki codes (Const Int :*: Const Ann)) (Lkup iy codes)

-> Spine ki codes (Lkup ix codes) (Lkup iy codes)

Takes two annotated Reps, and produces a patch

diffAl

Arguments

:: (EqHO ki, TestEquality ki)

=> PoA ki (AnnFix ki codes (Const Int :*: Const Ann)) xs

-> PoA ki (AnnFix ki codes (Const Int :*: Const Ann)) ys

-> Al ki codes xs ys

diffAt

Arguments

:: (EqHO ki, TestEquality ki)

=> NA ki (AnnFix ki codes (Const Int :*: Const Ann)) a

-> NA ki (AnnFix ki codes (Const Int :*: Const Ann)) a

-> At ki codes a

diff

Arguments

:: (EqHO ki, TestEquality ki, IsNat ix)

=> Fix ki codes ix

-> Fix ki codes ix

-> Almu ki codes ix ix

The interface function which witnesses thecomplete pipeline. its implementation is straightforward:

diff x y = let es = GDiff.diff' x y
               ax = countCopies $ annSrc  x es
               ay = countCopies $ annDest y es
            in diffAlmu ax ay