Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data CChange ki codes at where
- cmatch :: Holes ki codes (MetaVarIK ki) at -> Holes ki codes (MetaVarIK ki) at -> CChange ki codes at
- 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)
- 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
- changeEq :: EqHO ki => CChange ki codes at -> CChange ki codes at -> Bool
- changeCopy :: MetaVarIK ki at -> CChange ki codes at
- isCpy :: EqHO ki => CChange ki codes at -> Bool
- makeCopyFrom :: CChange ki codes at -> CChange ki codes at
- cWithDisjNamesFrom :: CChange ki codes at -> CChange ki codes at -> CChange ki codes at
- distrCChange :: Holes ki codes (CChange ki codes) at -> CChange ki codes at
- data OChange ki codes at where
- change :: Holes ki codes (MetaVarIK ki) at -> Holes ki codes (MetaVarIK ki) at -> Sum (OChange ki codes) (CChange ki codes) at
- 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
Documentation
data CChange ki codes at where Source #
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.
Instances
HasIKProjInj (ki :: kon -> Type) (CChange ki codes :: Atom kon -> Type) Source # | |
TestEquality ki => TestEquality (CChange ki codes :: Atom kon -> Type) Source # | |
Defined in Data.HDiff.Change | |
(HasDatatypeInfo ki fam codes, RendererHO ki) => Show (CChange ki codes at) Source # | |
(HasDatatypeInfo ki fam codes, RendererHO ki) => Show (Holes ki codes (Sum (Conflict ki codes) (CChange ki codes)) at) Source # | |
(HasDatatypeInfo ki fam codes, RendererHO ki) => Show (Holes ki codes (CChange ki codes) at) Source # | |
cmatch :: Holes ki codes (MetaVarIK ki) at -> Holes ki codes (MetaVarIK ki) at -> CChange ki codes at Source #
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) Source #
type Domain ki codes = Holes ki codes (MetaVarIK ki) Source #
A Domain
is just a deletion context. Type-synonym helps us
identify what's what on the algorithms below.
unCMatch :: CChange ki codes at -> (Holes ki codes (MetaVarIK ki) :*: Holes ki codes (MetaVarIK ki)) at Source #
changeEq :: EqHO ki => CChange ki codes at -> CChange ki codes at -> Bool Source #
Alpha-equality for CChange
changeCopy :: MetaVarIK ki at -> CChange ki codes at Source #
Issues a copy, this is a closed change analogous to > x -> x
makeCopyFrom :: CChange ki codes at -> CChange ki codes at Source #
cWithDisjNamesFrom :: CChange ki codes at -> CChange ki codes at -> CChange ki codes at Source #
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 Source #
A Utx with closed changes distributes over a closed change
change :: Holes ki codes (MetaVarIK ki) at -> Holes ki codes (MetaVarIK ki) at -> Sum (OChange ki codes) (CChange ki codes) at Source #
Given two treefixes, constructs and classifies a change from them.
type HolesHoles2 ki codes = Holes ki codes (Holes2 ki codes) Source #
utx2distr :: HolesHoles2 ki codes at -> Holes2 ki codes at Source #
utx22change :: HolesHoles2 ki codes at -> Maybe (CChange ki codes at) Source #
change2holes2 :: EqHO ki => CChange ki codes at -> HolesHoles2 ki codes at Source #
Orphan instances
HasIKProjInj (ki :: kon -> Type) (Holes2 ki codes :: Atom kon -> Type) Source # | |
TestEquality f => TestEquality (f :*: g :: k -> Type) Source # | |