Safe Haskell	Safe
Language	Haskell2010

Abstract.DPO

Contents

Application
- Conditions
- Transformation
Manipulation

Description

Provides definitions for the Double-Pushout approach to High-Level Rewriting Systems.

Synopsis

Documentation

data Production m Source #

A Double-Pushout production.

Consists of two morphisms left : K -> L and right : K -> R, as well as a set of nacs L -> Ni.

Instances

Eq m => Eq (Production m) Source #
Methods (==) :: Production m -> Production m -> Bool # (/=) :: Production m -> Production m -> Bool #
Read m => Read (Production m) Source #
Methods readsPrec :: Int -> ReadS (Production m) # readList :: ReadS [Production m] # readPrec :: ReadPrec (Production m) # readListPrec :: ReadPrec [Production m] #
Show m => Show (Production m) Source #
Methods showsPrec :: Int -> Production m -> ShowS # show :: Production m -> String # showList :: [Production m] -> ShowS #
(Morphism m, Valid m, Eq (Obj m)) => Valid (Production m) Source #
Methods isValid :: Production m -> Bool Source # validate :: Production m -> ValidationResult Source #

buildProduction :: m -> m -> [m] -> Production m Source #

Construct a production from the morphism l : K -> L, the morphism r : K -> R, and the nacs L -> Ni, respectively.

Note: this doesn't check that the production is valid.

getLHS :: Production m -> m Source #

Returns the morphism K -> L of the given production

getRHS :: Production m -> m Source #

Returns the morphism K -> R of the given production

getNACs :: Production m -> [m] Source #

Returns the set of nacs L -> Ni of the given production

data Derivation m Source #

Constructors

Derivation
Fields production :: Production m match :: m comatch :: m gluing :: m dToG :: m dToH :: m

Instances

Eq m => Eq (Derivation m) Source #
Methods (==) :: Derivation m -> Derivation m -> Bool # (/=) :: Derivation m -> Derivation m -> Bool #
Read m => Read (Derivation m) Source #
Methods readsPrec :: Int -> ReadS (Derivation m) # readList :: ReadS [Derivation m] # readPrec :: ReadPrec (Derivation m) # readListPrec :: ReadPrec [Derivation m] #
Show m => Show (Derivation m) Source #
Methods showsPrec :: Int -> Derivation m -> ShowS # show :: Derivation m -> String # showList :: [Derivation m] -> ShowS #

generateDerivation :: DPO m => MorphismsConfig -> m -> Production m -> Maybe (Derivation m) Source #

Given a match m and a production p, it returns Just d, where d is the corresponding Derivation if m satisfies the rewriting conditions, or Nothing.

data Process m Source #

Constructors

Process
Fields productions :: [Production m] coreObject :: Obj m

Instances

(Eq m, Eq (Obj m)) => Eq (Process m) Source #
Methods (==) :: Process m -> Process m -> Bool # (/=) :: Process m -> Process m -> Bool #
(Show m, Show (Obj m)) => Show (Process m) Source #
Methods showsPrec :: Int -> Process m -> ShowS # show :: Process m -> String # showList :: [Process m] -> ShowS #

class DPO m => GenerateProcess m where Source #

Minimal complete definition

restrictMorphisms, restrictMorphism, typing, productionTyping

Methods

restrictMorphisms :: (m, m) -> (m, m) Source #

Given a pair of morhisms with common codomain, it returns a new pair with morphism also with a a new codomain that does not contain the elements that were orphans in both original morphisms

restrictMorphism :: m -> m Source #

Given a morhism, it returns a morphism with a new codomain that is equal to the image of the original morphism

typing :: (Derivation m, (m, m, m)) -> Production m Source #

Given a Derivation d and a tuple (p,q,r) of Morphisms p : G -> C, q : D -> C and r : H -> C, it returns a new Production corresponding to the production in d but typed over C

productionTyping :: (Production m, (m, m, m)) -> Production m Source #

Given a Production p and a tuple (r,s,t) of Morphisms r : G -> C, s : D -> C and t : H -> C, it returns a new Production corresponding to the production in p but typed over C

calculateProcess :: [Derivation m] -> Process m Source #

Given a list of Derivation containing a sequential derivation, returns its corresponding Process

calculateRulesColimit :: RuleSequence m -> [NamedRuleWithMatches m] Source #

generateGraphProcess :: RuleSequence m -> [(String, Production m)] Source #

data MorphismsConfig Source #

Constructors

MorphismsConfig
Fields matchRestriction :: MatchRestriction nacSatisfaction :: NacSatisfaction

data MatchRestriction Source #

Flag indicating what restrictions are required or assumed of matches.

Constructors

MonoMatches
AnyMatches

Instances

Eq MatchRestriction Source #
Methods (==) :: MatchRestriction -> MatchRestriction -> Bool # (/=) :: MatchRestriction -> MatchRestriction -> Bool #
Show MatchRestriction Source #
Methods showsPrec :: Int -> MatchRestriction -> ShowS # show :: MatchRestriction -> String # showList :: [MatchRestriction] -> ShowS #

matchRestrictionToMorphismType :: MatchRestriction -> MorphismType Source #

Converts a match restriction to the corresponding MorphismType

data NacSatisfaction Source #

Flag indicating the semantics of NAC satisfaction.

Constructors

MonomorphicNAC
PartiallyMonomorphicNAC

Instances

Eq NacSatisfaction Source #
Methods (==) :: NacSatisfaction -> NacSatisfaction -> Bool # (/=) :: NacSatisfaction -> NacSatisfaction -> Bool #
Show NacSatisfaction Source #
Methods showsPrec :: Int -> NacSatisfaction -> ShowS # show :: NacSatisfaction -> String # showList :: [NacSatisfaction] -> ShowS #

Application

Conditions

In order to apply a production with a particular match, some application conditions must be satisfied: the gluing condition and the negative application conditions (NACs). This section provides functions that test if such conditions are met.

class (AdhesiveHLR m, FindMorphism m) => DPO m where Source #

Class for morphisms whose category is Adhesive-HLR, and which can be used for double-pushout transformations.

Minimal complete definition

invertProduction, shiftNacOverProduction, isPartiallyMonomorphic

Methods

invertProduction :: MorphismsConfig -> Production m -> Production m Source #

Inverts a production, adjusting the NACs accordingly. Needs information of nac injective satisfaction (in second order) and matches injective.

shiftNacOverProduction :: MorphismsConfig -> Production m -> m -> [m] Source #

Given a production L ←l- K -r→ R and a NAC morphism n : L -> N, obtain a set of NACs n'i : R -> N'i that is equivalent to the original NAC.

isPartiallyMonomorphic :: m -> m -> Bool Source #

Check if the second morphism is monomorphic outside the image of the first morphism.

satisfiesGluingConditions :: DPO m => MorphismsConfig -> Production m -> m -> Bool Source #

Verifies if the gluing conditions for a production p are satisfied by a match m

satisfiesNACs :: DPO m => MorphismsConfig -> Production m -> m -> Bool Source #

True if the given match satisfies all NACs of the given production.

satisfiesRewritingConditions :: DPO m => MorphismsConfig -> Production m -> m -> Bool Source #

True if the given match satisfies the gluing condition and NACs of the given production.

satisfyRewritingConditions :: DPO m => MorphismsConfig -> (Production m, m) -> (Production m, m) -> Bool Source #

Check gluing conditions and the NACs satisfaction for a pair of matches inj only indicates if the match is injective, this function does not checks it

Transformation

Given a production and a match for its left side, it may be possible to apply the production and obtain a transformation of the matched graph. This section provides functions that calculate such transformations.

findAllMatches :: DPO m => MorphismsConfig -> Production m -> Obj m -> [m] Source #

Obtain all matches from the production into the given object, even if they aren't applicable.

When given MonoMatches, only obtains monomorphic matches.

findApplicableMatches :: DPO m => MorphismsConfig -> Production m -> Obj m -> [m] Source #

Obtain the matches from the production into the given object that satisfiy the NACs and gluing conditions.

When given MonoMatches, only obtains monomorphic matches.

calculateDPO :: AdhesiveHLR m => m -> Production m -> (m, m, m, m) Source #

Given a match and a production, calculates the double-pushout diagram for the corresponding transformation.

Given match m : L -> G and the production L ←l- K -r→ R such that satisfiesRewritingConditions _ _ p m == True, returns k, n, f and g (respectively) such that the following two squares are pushouts.

      l        r
   L◀──────K──────▶R
   │       │       │
 m │       │ k     │ n
   ▼       ▼       ▼
   G◀──────D──────▶H
        f     g

Note: this doesn't test whether the match is for the actual production, nor if the match satisfies all application conditions.

calculateComatch :: AdhesiveHLR m => m -> Production m -> m Source #

Given a match and a production, calculate the calculateComatch for the corresponding transformation.

Given match m : L -> G and the production p = L ←l- K -r→ R such that satisfiesRewritingConditions _ _ p m == True, returns n such that the following two squares are pushouts.

      l        r
   L◀──────K──────▶R
   │       │       │
 m │       │       │ n
   ▼       ▼       ▼
   G◀──────D──────▶H

Note: this doesn't test whether the match is for the actual production, nor if the match satisfies all application conditions.

rewrite :: AdhesiveHLR m => m -> Production m -> Obj m Source #

Given a match and a production, obtain the rewritten object.

rewrite match production is equivalent to codomain (calculateComatch match production)

Manipulation

invertProductionWithoutNacs :: Production m -> Production m Source #

Discards the NACs of a production and inverts it.

nacDownwardShift :: EpiPairs m => MorphismsConfig -> m -> m -> [m] Source #

Given a morphism m : L -> L' and a NAC n : L -> N, obtains an equivalent set of NACs n'i : L' -> N'i that is equivalent to the original NAC.