| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Abstract.AdhesiveHLR
- class Eq m => Morphism m where
- data AtomicConstraint m = AtomicConstraint {}
- buildNamedAtomicConstraint :: String -> m -> Bool -> AtomicConstraint m
- satisfiesAtomicConstraint :: FindMorphism m => Obj m -> AtomicConstraint m -> Bool
- satisfiesAllAtomicConstraints :: FindMorphism m => Obj m -> [AtomicConstraint m] -> Bool
- data Constraint m
- = Atomic {
- atomic :: AtomicConstraint m
- | And {
- lc :: Constraint m
- rc :: Constraint m
- | Or {
- lc :: Constraint m
- rc :: Constraint m
- | Not {
- nc :: Constraint m
- = Atomic {
- satisfiesConstraint :: FindMorphism m => Obj m -> Constraint m -> Bool
- satisfiesAllConstraints :: FindMorphism m => Obj m -> [Constraint m] -> Bool
- class Morphism m => EpiPairs m where
- class Cocomplete m => AdhesiveHLR m where
- data MatchRestriction
- matchRestrictionToMorphismType :: MatchRestriction -> MorphismType
- data NacSatisfaction
- data MorphismsConfig = MorphismsConfig {}
Documentation
class Eq m => Morphism m where Source #
Minimal complete definition
compose, domain, codomain, id, isMonomorphism, isEpimorphism, isIsomorphism
Methods
compose :: m -> m -> m Source #
Apply the first argument first (compose f g = g . f)
codomain :: m -> Obj m Source #
isMonomorphism :: m -> Bool Source #
isEpimorphism :: m -> Bool Source #
isIsomorphism :: m -> Bool Source #
Instances
| Morphism (GraphMorphism a b) Source # | |
| Morphism (TypedGraphMorphism a b) Source # | |
| Morphism (RuleMorphism a b) Source # | |
data AtomicConstraint m Source #
Instances
| Show m => Show (AtomicConstraint m) Source # | |
| Valid m => Valid (AtomicConstraint m) Source # | |
buildNamedAtomicConstraint :: String -> m -> Bool -> AtomicConstraint m Source #
satisfiesAtomicConstraint :: FindMorphism m => Obj m -> AtomicConstraint m -> Bool Source #
Given an object G and a AtomicConstraint a : P -> C, check whether G satisfies the AtomicConstraint a
satisfiesAllAtomicConstraints :: FindMorphism m => Obj m -> [AtomicConstraint m] -> Bool Source #
Given an object G and a list of AtomicConstraints a : P -> C, check whether G satisfies the all them
data Constraint m Source #
Constructors
| Atomic | |
Fields
| |
| And | |
Fields
| |
| Or | |
Fields
| |
| Not | |
Fields
| |
Instances
| Show m => Show (Constraint m) Source # | |
| Valid m => Valid (Constraint m) Source # | |
satisfiesConstraint :: FindMorphism m => Obj m -> Constraint m -> Bool Source #
Given an object G and a Constraint c (a Boolean formula over atomic constraints), check whether G satisfies c
satisfiesAllConstraints :: FindMorphism m => Obj m -> [Constraint m] -> Bool Source #
Given an object G and a list of Constraints (Boolean formulas over atomic constraints), check whether G satisfies the all them
class Morphism m => EpiPairs m where Source #
Minimal complete definition
createJointlyEpimorphicPairs, createAllSubobjects, createJointlyEpimorphicPairsFromNAC, calculateCommutativeSquaresAlongMonomorphism
Methods
createJointlyEpimorphicPairs :: Bool -> Obj m -> Obj m -> [(m, m)] Source #
Create all jointly epimorphic pairs of morphisms from the given objects.
If the first argument is true, only pairs of monomorphisms are created. Otherwise, pairs of arbitrary morphisms are created.
createAllSubobjects :: Bool -> Obj m -> [m] Source #
Create all subobjects from the given object.
If the first argument is true, only identity morphism is created. Otherwise, arbitrary (epimorphic) morphisms are created.
createJointlyEpimorphicPairsFromNAC :: MorphismsConfig -> Obj m -> m -> [(m, m)] Source #
Create a special case of jointly epimorphic pairs, where the second morphism is a Nac. The pairs generated are dependent of the NAC config.
FIXME: nacs don't belong in this module
calculateCommutativeSquares :: Bool -> m -> m -> [(m, m)] Source #
calculateCommutativeSquaresAlongMonomorphism :: (m, Bool) -> (m, Bool) -> [(m, m)] Source #
class Cocomplete m => AdhesiveHLR m where Source #
Type class for morphisms whose category Adhesive and suitable for High-Level Replacement Systems.
Mainly provides categorical operations that AdhesiveHLR categories are guaranteed to have.
Minimal complete definition
calculateInitialPushout, hasPushoutComplement, calculatePushoutComplement, calculatePullback
Methods
calculateInitialPushout :: m -> (m, m, m) Source #
Calculate the initial pushout of the given morphism.
Given the morphism f : A -> A', returns the morphisms b : B -> A, f' : B -> C and c: C -> A' such that the following square is the initial pushout of f.
f'
B──────▶C
│ │
b │ │ c
▼ ▼
A──────▶A'
f
calculatePushout :: m -> m -> (m, m) Source #
Calculate the pushout between the two given morphisms.
Given the morphisms f : A -> B and g : A -> C, respectively, returns the pair of morphisms f' : C -> D and g': B -> D such that the following square is a pushout.
g
A──────▶C
│ │
f │ │ f'
▼ ▼
B──────▶D
g'
hasPushoutComplement :: (MorphismType, m) -> (MorphismType, m) -> Bool Source #
Checks if the given sequential morphisms have a pushout complement, assuming they satsify the given restriction.
Given the morphisms g : B -> C and f : A -> B, respectively, tests if there exists a pair of morphisms f' : A -> X and g' : X -> B such that the following square is a pushout. Since the category is Adhesive, such a pair is unique.
f
A──────▶B
│ │
g' │ │ g
▼ ▼
X──────▶C
f'
If the types of the morphisms are known, they should be given. The implementation of this operation may then use them for more efficient calculation.
calculatePushoutComplement :: m -> m -> (m, m) Source #
Calculate the pushout complement for two sequential morphisms, assumes it exists.
In order to test if the pushout complement exists, use hasPushoutComplement.
Given the morphisms g : B -> C and f : A -> B, respectively, returns the pair of morphisms f' : A -> X and g' : X -> B such that the following square is a pushout. Since the category is Adhesive, such a pair is unique.
f
A──────▶B
│ │
g' │ │ g
▼ ▼
X──────▶C
f'
calculatePullback :: m -> m -> (m, m) Source #
Calculate the pullback between the two given morphisms.
Given two morphisms f : A -> C and g : B -> C, respectively, returns the pair of morphisms f' : X -> B and g': X -> A such that the following square is a pullback.
g'
X──────▶A
│ │
f' │ │ f
▼ ▼
B──────▶C
g
data MatchRestriction Source #
Flag indicating what restrictions are required or assumed of matches.
Constructors
| MonoMatches | |
| AnyMatches |
Instances
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
data MorphismsConfig Source #
Constructors
| MorphismsConfig | |