Generics.MRSOP.STDiff

Documentation

module Generics.MRSOP.STDiff.Types

apply :: forall ki codes ix iy. (IsNat ix, IsNat iy, EqHO ki) => Almu ki codes ix iy -> Fix ki codes ix -> Maybe (Fix ki codes iy)

Applies a patch to an element

merge :: forall ki codes ix. (EqHO ki, IsNat ix) => Almu ki codes ix ix -> Almu ki codes ix ix -> Maybe (Almu ki codes ix ix)

Merges two patches in the stdiff style. Satisfies the following postcondition:

if merge p q == Just pq && merge q p == Just qp
then apply pq . q == apply qp . p

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