Data.HDiff.Change

Documentation

data CChange ki codes at where

A CChange, or, closed change, consists in a declaration of metavariables and two contexts. The precondition is that every variable declared occurs at least once in ctxDel and that every variable that occurs in ctxIns is declared.

Constructors

CMatch

Fields

• :: { cCtxVars :: Set (Exists (MetaVarIK ki))
•    , cCtxDel :: Holes ki codes (MetaVarIK ki) at
•    , cCtxIns :: Holes ki codes (MetaVarIK ki) at
•    } -> CChange ki codes at

Instances

HasIKProjInj (ki :: kon -> Type) (CChange ki codes :: Atom kon -> Type)

Defined in Data.HDiff.Change

Methods

konInj :: ki k -> CChange ki codes (K k)

varProj :: Proxy ki -> CChange ki codes x -> Maybe (IsI x)

TestEquality ki => TestEquality (CChange ki codes :: Atom kon -> Type)

Defined in Data.HDiff.Change

Methods

testEquality :: CChange ki codes a -> CChange ki codes b -> Maybe (a :~: b)

(HasDatatypeInfo ki fam codes, RendererHO ki) => Show (CChange ki codes at)

Defined in Data.HDiff.Patch.Show

Methods

showsPrec :: Int -> CChange ki codes at -> ShowS

show :: CChange ki codes at -> String

showList :: [CChange ki codes at] -> ShowS

(HasDatatypeInfo ki fam codes, RendererHO ki) => Show (Holes ki codes (Sum (Conflict ki codes) (CChange ki codes)) at)

Defined in Data.HDiff.Patch.Show

Methods

showsPrec :: Int -> Holes ki codes (Sum (Conflict ki codes) (CChange ki codes)) at -> ShowS

show :: Holes ki codes (Sum (Conflict ki codes) (CChange ki codes)) at -> String

showList :: [Holes ki codes (Sum (Conflict ki codes) (CChange ki codes)) at] -> ShowS

(HasDatatypeInfo ki fam codes, RendererHO ki) => Show (Holes ki codes (CChange ki codes) at)

Defined in Data.HDiff.Patch.Show

Methods

showsPrec :: Int -> Holes ki codes (CChange ki codes) at -> ShowS

show :: Holes ki codes (CChange ki codes) at -> String

showList :: [Holes ki codes (CChange ki codes) at] -> ShowS

cmatch :: Holes ki codes (MetaVarIK ki) at -> Holes ki codes (MetaVarIK ki) at -> CChange ki codes at

smart constructor for CChange. Enforces the invariant

cmatch' :: Holes ki codes (MetaVarIK ki) at -> Holes ki codes (MetaVarIK ki) at -> Maybe (CChange ki codes at)

type Domain ki codes = Holes ki codes (MetaVarIK ki)

A Domain is just a deletion context. Type-synonym helps us identify what's what on the algorithms below.

domain :: CChange ki codes at -> Domain ki codes at

unCMatch :: CChange ki codes at -> (Holes ki codes (MetaVarIK ki) :*: Holes ki codes (MetaVarIK ki)) at

cMaxVar :: CChange ki codes at -> Int

Returns the maximum variable in a change

changeEq :: EqHO ki => CChange ki codes at -> CChange ki codes at -> Bool

Alpha-equality for CChange

changeCopy :: MetaVarIK ki at -> CChange ki codes at

Issues a copy, this is a closed change analogous to > x -> x

isCpy :: EqHO ki => CChange ki codes at -> Bool

Checks whetehr a change is a copy.

makeCopyFrom :: CChange ki codes at -> CChange ki codes at

cWithDisjNamesFrom :: CChange ki codes at -> CChange ki codes at -> CChange ki codes at

Renames all changes within a Holes so that their variable names will not clash.

distrCChange :: Holes ki codes (CChange ki codes) at -> CChange ki codes at

A Utx with closed changes distributes over a closed change

data OChange ki codes at where

A OChange, or, open change, is analogous to a CChange, but has a list of free variables. These are the ones that appear in oCtxIns but not in oCtxDel

Constructors

OMatch

Fields

• :: { oCtxVDel :: Set (Exists (MetaVarIK ki))
•    , oCtxVIns :: Set (Exists (MetaVarIK ki))
•    , oCtxDel :: Holes ki codes (MetaVarIK ki) at
•    , oCtxIns :: Holes ki codes (MetaVarIK ki) at
•    } -> OChange ki codes at

change :: Holes ki codes (MetaVarIK ki) at -> Holes ki codes (MetaVarIK ki) at -> Sum (OChange ki codes) (CChange ki codes) at

Given two treefixes, constructs and classifies a change from them.

type Holes2 ki codes = Holes ki codes (MetaVarIK ki) :*: Holes ki codes (MetaVarIK ki)

type HolesHoles2 ki codes = Holes ki codes (Holes2 ki codes)

fst' :: (f :*: g) x -> f x

snd' :: (f :*: g) x -> g x

scDel :: HolesHoles2 ki codes at -> Holes ki codes (MetaVarIK ki) at

scIns :: HolesHoles2 ki codes at -> Holes ki codes (MetaVarIK ki) at

utx2distr :: HolesHoles2 ki codes at -> Holes2 ki codes at

utx22change :: HolesHoles2 ki codes at -> Maybe (CChange ki codes at)

change2holes2 :: EqHO ki => CChange ki codes at -> HolesHoles2 ki codes at

Orphan instances

HasIKProjInj (ki :: kon -> Type) (Holes2 ki codes :: Atom kon -> Type)

Methods

konInj :: ki k -> Holes2 ki codes (K k)

varProj :: Proxy ki -> Holes2 ki codes x -> Maybe (IsI x)

TestEquality f => TestEquality (f :*: g :: k -> Type)

Methods

testEquality :: (f :*: g) a -> (f :*: g) b -> Maybe (a :~: b)