Data.HDiff.Patch

Patches

type RawPatch ki codes = Holes ki codes (CChange ki codes)

Instead of keeping unecessary information, a RawPatch will factor out the common prefix before the actual changes.

type Patch ki codes ix = Holes ki codes (CChange ki codes) (I ix)

A Patch is a RawPatch instantiated to I atoms.

Patch Alpha Equivalence

patchEq :: EqHO ki => RawPatch ki codes at -> RawPatch ki codes at -> Bool

patchIsCpy :: EqHO ki => RawPatch ki codes at -> Bool

Functionality over a Patch

patchMaxVar :: RawPatch ki codes at -> Int

withFreshNamesFrom :: RawPatch ki codes at -> RawPatch ki codes at -> RawPatch ki codes at

Calling p withFreshNamesFrom q will return an alpha equivalent version of p that has no name clasehs with q.

patchCost :: RawPatch ki codes at -> Int

Computes the cost of a Patch. This is in the sense of edit-scripts where it counts how many constructors are being inserted and deleted.

Applying a Patch

Patch application really is trivial. Say we are applying a patch p against an element x, first we match x with the ctxDel p; upon a succesfull match we record, in a Valuation, which tree fell in which hole. Then, we use the same valuation to inject those trees into ctxIns p.

The only slight trick is that we need to wrap our trees in existentials inside our valuation.

apply :: (TestEquality ki, EqHO ki, ShowHO ki, IsNat ix) => Patch ki codes ix -> Fix ki codes ix -> Either String (Fix ki codes ix)

Applying a patch is trivial, we simply project the deletion treefix and inject the valuation into the insertion.

Specializing a Patch

composes :: (ShowHO ki, EqHO ki, TestEquality ki) => RawPatch ki codes at -> RawPatch ki codes at -> Bool

The predicate composes qr pq checks whether qr is immediatly applicable to the codomain of pq.

applicableTo :: (ShowHO ki, EqHO ki, TestEquality ki) => Holes ki codes (MetaVarIK ki) ix -> Holes ki codes (MetaVarIK ki) ix -> Bool

substInsert' :: (ShowHO ki, EqHO ki, TestEquality ki) => String -> Subst ki codes (MetaVarIK ki) -> MetaVarIK ki ix -> Holes ki codes (MetaVarIK ki) ix -> Except (ApplicationErr ki codes (MetaVarIK ki)) (Subst ki codes (MetaVarIK ki))