| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.HDiff.Patch
Contents
Synopsis
- type RawPatch ki codes = Holes ki codes (CChange ki codes)
- type Patch ki codes ix = Holes ki codes (CChange ki codes) (I ix)
- patchEq :: EqHO ki => RawPatch ki codes at -> RawPatch ki codes at -> Bool
- patchIsCpy :: EqHO ki => RawPatch ki codes at -> Bool
- patchMaxVar :: RawPatch ki codes at -> Int
- withFreshNamesFrom :: RawPatch ki codes at -> RawPatch ki codes at -> RawPatch ki codes at
- patchCost :: RawPatch ki codes at -> Int
- apply :: (TestEquality ki, EqHO ki, ShowHO ki, IsNat ix) => Patch ki codes ix -> Fix ki codes ix -> Either String (Fix ki codes ix)
- composes :: (ShowHO ki, EqHO ki, TestEquality ki) => RawPatch ki codes at -> RawPatch ki codes at -> Bool
- 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))
Patches
type RawPatch ki codes = Holes ki codes (CChange ki codes) Source #
Instead of keeping unecessary information, a RawPatch will
factor out the common prefix before the actual changes.
Patch Alpha Equivalence
Functionality over a Patch
patchMaxVar :: RawPatch ki codes at -> Int Source #
withFreshNamesFrom :: RawPatch ki codes at -> RawPatch ki codes at -> RawPatch ki codes at Source #
Calling p will return an alpha equivalent
version of withFreshNamesFrom qp that has no name clasehs with q.
patchCost :: RawPatch ki codes at -> Int Source #
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) Source #
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 Source #
The predicate composes qr pq checks whether qr is immediatly applicable
to the codomain of pq.