Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data Conflict :: (kon -> *) -> [[[Atom kon]]] -> Atom kon -> * where
- type PatchC ki codes ix = Holes ki codes (Sum (Conflict ki codes) (CChange ki codes)) (I ix)
- noConflicts :: PatchC ki codes ix -> Maybe (Patch ki codes ix)
- getConflicts :: ShowHO ki => PatchC ki codes ix -> [String]
- (//) :: (Applicable ki codes (Holes2 ki codes), EqHO ki, ShowHO ki, HasDatatypeInfo ki fam codes) => Patch ki codes ix -> Patch ki codes ix -> PatchC ki codes ix
- reconcile :: forall ki codes fam at. (Applicable ki codes (Holes2 ki codes), EqHO ki, ShowHO ki, HasDatatypeInfo ki fam codes) => RawPatch ki codes at -> RawPatch ki codes at -> Holes ki codes (Sum (Conflict ki codes) (CChange ki codes)) at
- data ProcessOutcome ki codes
- = ReturnNominator
- | InstDenominator (Subst ki codes (Holes2 ki codes))
- | CantReconcile String
- rawCpy :: Map Int Int -> Holes2 ki codes at -> Bool
- simpleCopy :: Holes2 ki codes at -> Bool
- isLocalIns :: Holes2 ki codes at -> Bool
- arityMap :: Holes ki codes (MetaVarIK ki) at -> Map Int Int
- process :: (Applicable ki codes (Holes2 ki codes), EqHO ki, ShowHO ki) => HolesHoles2 ki codes at -> HolesHoles2 ki codes at -> ProcessOutcome ki codes
Merging Treefixes
After merging two patches, we might end up with a conflict. That is, two changes that can't be reconciled.
data Conflict :: (kon -> *) -> [[[Atom kon]]] -> Atom kon -> * where Source #
Hence, a conflict is simply two changes together.
Instances
(HasDatatypeInfo ki fam codes, RendererHO ki) => Show (Holes ki codes (Sum (Conflict ki codes) (CChange ki codes)) at) Source # | |
type PatchC ki codes ix = Holes ki codes (Sum (Conflict ki codes) (CChange ki codes)) (I ix) Source #
A PatchC
is a patch with potential conflicts inside
getConflicts :: ShowHO ki => PatchC ki codes ix -> [String] Source #
Returns the labels of the conflicts ina a patch.
(//) :: (Applicable ki codes (Holes2 ki codes), EqHO ki, ShowHO ki, HasDatatypeInfo ki fam codes) => Patch ki codes ix -> Patch ki codes ix -> PatchC ki codes ix Source #
A merge of p
over q
, denoted p // q
, is the adaptation
of p
so that it could be applied to an element in the
image of q
.
reconcile :: forall ki codes fam at. (Applicable ki codes (Holes2 ki codes), EqHO ki, ShowHO ki, HasDatatypeInfo ki fam codes) => RawPatch ki codes at -> RawPatch ki codes at -> Holes ki codes (Sum (Conflict ki codes) (CChange ki codes)) at Source #
The reconcile
function will try to reconcile disagreeing
patches.
Precondition: before calling reconcile p q
, make sure
p
and q
are different.
data ProcessOutcome ki codes Source #
ReturnNominator | |
InstDenominator (Subst ki codes (Holes2 ki codes)) | |
CantReconcile String |
rawCpy :: Map Int Int -> Holes2 ki codes at -> Bool Source #
Checks whether a variable is a rawCpy, note that we need a map that checks occurences of this variable.
simpleCopy :: Holes2 ki codes at -> Bool Source #
isLocalIns :: Holes2 ki codes at -> Bool Source #
process :: (Applicable ki codes (Holes2 ki codes), EqHO ki, ShowHO ki) => HolesHoles2 ki codes at -> HolesHoles2 ki codes at -> ProcessOutcome ki codes Source #
This will process two changes, represented as a spine and
inner changes, into a potential merged patch. The result of process sp sq
is supposed to instruct how to construct a patch that
can be applied to the image sq
.
We do so by traversing the places where both sp
and sq
differ.
While we perform this traversal we instantiate a valuation of
potential substitutions, which might be needed in case we
need to adapt sp
to sq
. After we are done, we know whether
we need to adapt sp
, return sp
as is, or there is a conflict.