Merge branch layers refactoring - Partial #25

.stylish-haskell.yaml

@@ -20,8 +20,8 @@ steps:
   # line.
   - simple_align:
       cases: false
-      top_level_patterns: false
-      records: false
+      top_level_patterns: true
+      records: true
 
   # Import cleanup
   - imports:

src/CLI/ApplySndOrderRules.hs

@@ -4,8 +4,8 @@ module ApplySndOrderRules
   , execute
   ) where
 
-import           Abstract.AdhesiveHLR
-import           Abstract.DPO
+import           Category.AdhesiveHLR
+import           Category.DPO
 import           Control.Monad            (when)
 import           Graph.Graph              (Graph)
 import qualified SndOrder.Rule            as SO

src/CLI/ConcurrentRules.hs

@@ -7,8 +7,8 @@ module ConcurrentRules
 import           Data.Monoid              ((<>))
 import           GlobalOptions
 
-import           Abstract.AdhesiveHLR
-import           Abstract.DPO
+import           Category.AdhesiveHLR
+import           Category.DPO
 import           Analysis.ConcurrentRules
 import           Control.Monad
 import           Options.Applicative

src/CLI/CriticalPairAnalysis.hs

@@ -4,8 +4,8 @@ module CriticalPairAnalysis
   , execute
   ) where
 
-import           Abstract.AdhesiveHLR                  (EpiPairs)
-import           Abstract.DPO
+import           Category.AdhesiveHLR                  (EpiPairs)
+import           Category.DPO
 import           Analysis.CriticalPairs
 import           Analysis.CriticalSequence
 import           Analysis.EssentialCriticalPairs
@@ -154,8 +154,8 @@ printEvoConflicts = map printOneEvo
                        show (printConf (True,True) (thd e)) ++ ")"
     printConf str evos = countElement str (map cpe evos)
 
-printAnalysis :: (EpiPairs m, DPO m) =>
-  Bool -> AnalysisType -> MorphismsConfig -> [Production m] -> IO ()
+printAnalysis :: (EpiPairs morph, DPO morph) =>
+  Bool -> AnalysisType -> MorphismsConfig -> [Production morph] -> IO ()
 printAnalysis essential action dpoConf rules =
   let essentialConfMatrix = analysisMatrix dpoConf rules
         findAllEssentialDeleteUse findAllEssentialProduceDangling findAllEssentialProduceForbid
@@ -181,10 +181,10 @@ printAnalysis essential action dpoConf rules =
 
 -- Receives functions and theirs names,
 -- and returns they applicated to the rules
-analysisMatrix :: MorphismsConfig -> [Production m]
-  -> (MorphismsConfig -> Production m -> Production m -> [cps])
-  -> (MorphismsConfig -> Production m -> Production m -> [cps])
-  -> (MorphismsConfig -> Production m -> Production m -> [cps])
+analysisMatrix :: MorphismsConfig -> [Production morph]
+  -> (MorphismsConfig -> Production morph -> Production morph -> [cps])
+  -> (MorphismsConfig -> Production morph -> Production morph -> [cps])
+  -> (MorphismsConfig -> Production morph -> Production morph -> [cps])
   -> String -> String -> String -> String
   -> [String]
 analysisMatrix dpoConf rules f1 f2 f3 n1 n2 n3 n4 =

src/CLI/GlobalOptions.hs

@@ -7,7 +7,7 @@ module GlobalOptions
   , useConstraints
   ) where
 
-import           Abstract.AdhesiveHLR (MatchRestriction (..), MorphismsConfig (..),
+import           Category.AdhesiveHLR (MatchRestriction (..), MorphismsConfig (..),
                                        NacSatisfaction (..))
 import           Data.Monoid          ((<>))
 import           Options.Applicative

src/CLI/ModelChecker.hs

@@ -4,9 +4,9 @@ import           Data.Monoid              ((<>))
 import           GlobalOptions
 import           Options.Applicative
 
-import           Abstract.DPO             as DPO hiding (NamedProduction)
-import           Abstract.DPO.StateSpace  as StateSpace
-import           Abstract.Morphism
+import           Category.DPO             as DPO hiding (NamedProduction)
+import           Category.DPO.StateSpace  as StateSpace
+import           Category.FinitaryCategory
 import           Abstract.Valid
 import qualified Image.Dot                as Dot
 import qualified Logic.Ctl                as Logic

src/CLI/ParallelIndependence.hs

@@ -4,7 +4,7 @@ module ParallelIndependence
   , execute
   ) where
 
-import           Abstract.DPO
+import           Category.DPO
 import           Analysis.ParallelIndependent
 import           Control.Monad                (unless, when)
 import           Data.Matrix                  hiding ((<|>))

src/CLI/Processes.hs

@@ -12,8 +12,8 @@ import           Data.Set                         (toList)
 import           GlobalOptions
 import           Options.Applicative
 
-import           Abstract.DPO
-import           Abstract.DPO.Process        hiding (productions)
+import           Category.DPO
+import           Category.DPO.Process        hiding (productions)
 import           Abstract.Valid
 import           Analysis.Processes
 import           TypedGraph.DPO.GraphProcess
@@ -86,7 +86,7 @@ execute globalOpts opts = do
           ++ show rulesOrdering ++ "\n}\n"
           ++ "Element Ordering: {"
           ++ show elementsOrdering ++"\n}\n\n"
-          ++ "Set of Abstract Restrictions: {\n"
+          ++ "Set of Category Restrictions: {\n"
           ++ restrictionToString (restrictRelation completeOgg) ++ "\n}"
 
     putStrLn "Tesing Serialization: "

src/library/Analysis/ConcurrentRules.hs

@@ -5,19 +5,20 @@ module Analysis.ConcurrentRules
   maxConcurrentRules
 ) where
 
-import           Abstract.AdhesiveHLR
 import           Abstract.Cardinality
-import qualified Abstract.Cocomplete       as C
-import           Abstract.DPO
 import           Abstract.Valid
 import           Analysis.CriticalSequence (findTriggeredCriticalSequences,
                                             getCriticalSequenceComatches)
+import           Category.AdhesiveHLR
+import qualified Category.Cocomplete       as C
+import           Category.DPO
 import           Data.Maybe                (mapMaybe)
 
 data CRDependencies = AllOverlapings | OnlyDependency
 
 -- | Generates the Concurrent Rules for a given list of Productions following the order of the elements in the list.
-allConcurrentRules :: (DPO m, EpiPairs m, Eq (Obj m), Valid m) => CRDependencies -> MorphismsConfig -> [Constraint m] -> [Production m] -> [Production m]
+allConcurrentRules :: (DPO morph, EpiPairs morph, Eq (Obj morph), Valid morph) => CRDependencies -> MorphismsConfig
+                    -> [Constraint morph] -> [Production morph] -> [Production morph]
 allConcurrentRules _ _ _ [] = []
 allConcurrentRules _ _ _ [x] = [x]
 allConcurrentRules dep conf constraints (x:xs) = concatMap (crs x) (allCRs xs)
@@ -27,8 +28,8 @@ allConcurrentRules dep conf constraints (x:xs) = concatMap (crs x) (allCRs xs)
 
 -- | Generates the Concurrent Rules with the least disjoint EpiPairs (EpiPairs with the least cardinality) for a given list of Productions
 -- (following the order of the elements in the list).
-maxConcurrentRules :: (DPO m, EpiPairs m, Eq (Obj m), Valid m, Cardinality (Obj m)) => CRDependencies -> MorphismsConfig ->
-  [Constraint m] -> [Production m] -> [Production m]
+maxConcurrentRules :: (DPO morph, EpiPairs morph, Eq (Obj morph), Valid morph, Cardinality (Obj morph))
+                  => CRDependencies -> MorphismsConfig -> [Constraint morph] -> [Production morph] -> [Production morph]
 maxConcurrentRules _ _ _ [] = []
 maxConcurrentRules _ _ _ [r] = [r]
 maxConcurrentRules dep conf constraints (r:rs) = concat $ concatRule r (maxConcurrentRules dep conf constraints rs)
@@ -37,13 +38,13 @@ maxConcurrentRules dep conf constraints (r:rs) = concat $ concatRule r (maxConcu
       [] -> []
       xs -> map (maxConcurrentRuleForLastPairs dep conf constraints rule) xs
 
-concurrentRules :: (DPO m, EpiPairs m) => CRDependencies -> MorphismsConfig -> [Constraint m] -> Production m -> Production m -> [Production m]
+concurrentRules :: (DPO morph, EpiPairs morph) => CRDependencies -> MorphismsConfig -> [Constraint morph] -> Production morph -> Production morph -> [Production morph]
 concurrentRules dep conf constraints c n =
   let epiPairs = epiPairsForConcurrentRule dep conf constraints c n
   in mapMaybe (concurrentRuleForPair conf constraints c n) epiPairs
 
-maxConcurrentRuleForLastPairs :: (DPO m, EpiPairs m, Cardinality (Obj m)) => CRDependencies -> MorphismsConfig -> [Constraint m] ->
-  Production m -> Production m -> [Production m]
+maxConcurrentRuleForLastPairs :: (DPO morph, EpiPairs morph, Cardinality (Obj morph)) => CRDependencies -> MorphismsConfig -> [Constraint morph] ->
+  Production morph -> Production morph -> [Production morph]
 maxConcurrentRuleForLastPairs dep conf constraints c n =
   let epiPairs = epiPairsForConcurrentRule dep conf constraints c n
       maxPair = last (epiPairsForConcurrentRule dep conf constraints c n)
@@ -54,8 +55,8 @@ maxConcurrentRuleForLastPairs dep conf constraints c n =
         else mapMaybe (concurrentRuleForPair conf constraints c n) maxPairs
   in maxRule
 
-epiPairsForConcurrentRule :: (DPO m, EpiPairs m)
-  => CRDependencies -> MorphismsConfig -> [Constraint m] -> Production m -> Production m -> [(m, m)]
+epiPairsForConcurrentRule :: (DPO morph, EpiPairs morph)
+  => CRDependencies -> MorphismsConfig -> [Constraint morph] -> Production morph -> Production morph -> [(morph,morph)]
 -- it only considers triggered dependencies because is the most intuitive and natural behaviour expected until now.
 epiPairsForConcurrentRule OnlyDependency conf constraints c n =
   let dependencies = map getCriticalSequenceComatches (findTriggeredCriticalSequences conf c n)
@@ -69,7 +70,7 @@ epiPairsForConcurrentRule AllOverlapings conf constraints c n =
         satisfiesGluingConditions conf (invertProductionWithoutNacs c) lp && satisfiesRewritingConditions conf n rp
   in filter isValidPair allPairs
 
-concurrentRuleForPair :: (DPO m, EpiPairs m) => MorphismsConfig -> [Constraint m] -> Production m -> Production m -> (m, m) -> Maybe (Production m)
+concurrentRuleForPair :: (DPO morph, EpiPairs morph) => MorphismsConfig -> [Constraint morph] -> Production morph -> Production morph -> (morph,morph) -> Maybe (Production morph)
 concurrentRuleForPair conf constraints c n pair = if invalidSides then Nothing else Just (buildProduction l r (dmc ++ lp))
   where
     pocC = calculatePushoutComplement (fst pair) (getRHS c)

src/library/Analysis/CriticalPairs.hs

@@ -17,10 +17,10 @@ module Analysis.CriticalPairs
    findAllDeleteUseAndProduceDangling
    ) where
 
-import           Abstract.AdhesiveHLR       as RW
-import           Abstract.DPO               as RW hiding (calculateComatch)
 import           Analysis.DiagramAlgorithms
 import           Analysis.EpimorphicPairs
+import           Category.AdhesiveHLR       as RW
+import           Category.DPO               as RW hiding (calculateComatch)
 import           Data.Maybe                 (mapMaybe)
 
 -- | Data representing the type of a 'CriticalPair'
@@ -31,8 +31,8 @@ data CriticalPairType =
   | ProduceDangling
   deriving(Eq,Show)
 
-type NamedRule m = (String, Production m)
-type NamedCriticalPairs m = (String,String,[CriticalPair m])
+type NamedRule morph = (String, Production morph)
+type NamedCriticalPairs morph = (String,String,[CriticalPair morph])
 
 -- | A Critical Pair is defined as two matches (m1,m2) from the left
 -- side of their productions to a same graph.
@@ -63,41 +63,41 @@ type NamedCriticalPairs m = (String,String,[CriticalPair m])
 --
 -- q21 (nacMatch) :: from N2 to P1
 
-data CriticalPair m = CriticalPair {
-    matches   :: (m, m),
-    comatches :: Maybe (m, m),
-    nacMatch  :: Maybe (m, Int), --if it is a ProduceForbid, here is the index of the nac
+data CriticalPair morph = CriticalPair {
+    matches   :: (morph,morph),
+    comatches :: Maybe (morph,morph),
+    nacMatch  :: Maybe (morph, Int), --if it is a ProduceForbid, here is the index of the nac
     cpType    :: CriticalPairType
     } deriving (Eq,Show)
 
 -- | Returns the matches (m1,m2)
-getCriticalPairMatches :: CriticalPair m -> (m, m)
+getCriticalPairMatches :: CriticalPair morph -> (morph,morph)
 getCriticalPairMatches = matches
 
 -- | Returns the comatches (m1',m2')
-getCriticalPairComatches :: CriticalPair m -> Maybe (m, m)
+getCriticalPairComatches :: CriticalPair morph -> Maybe (morph,morph)
 getCriticalPairComatches = comatches
 
 -- | Returns the type of a Critical Pair
-getCriticalPairType :: CriticalPair m -> CriticalPairType
+getCriticalPairType :: CriticalPair morph -> CriticalPairType
 getCriticalPairType = cpType
 
 -- | Returns the nac match of a 'CriticalPair'
-getNacMatchOfCriticalPair :: CriticalPair m -> Maybe m
+getNacMatchOfCriticalPair :: CriticalPair morph -> Maybe morph
 getNacMatchOfCriticalPair criticalPair =
   case nacMatch criticalPair of
     Just (nac,_) -> Just nac
     Nothing      -> Nothing
 
 -- | Returns the nac index of a 'CriticalPair'
-getNacIndexOfCriticalPair :: CriticalPair m -> Maybe Int
+getNacIndexOfCriticalPair :: CriticalPair morph -> Maybe Int
 getNacIndexOfCriticalPair criticalPair =
   case nacMatch criticalPair of
     Just (_,idx) -> Just idx
     Nothing      -> Nothing
 
 -- | Returns the Critical Pairs with rule names
-namedCriticalPairs :: (EpiPairs m, DPO m) => MorphismsConfig -> [NamedRule m] -> [NamedCriticalPairs m]
+namedCriticalPairs :: (EpiPairs morph, DPO morph) => MorphismsConfig -> [NamedRule morph] -> [NamedCriticalPairs morph]
 namedCriticalPairs conf namedRules =
   map (uncurry getCPs) [(a,b) | a <- namedRules, b <- namedRules]
     where
@@ -106,14 +106,14 @@ namedCriticalPairs conf namedRules =
 
 -- TODO: Use this as an auxiliary function to optimize the search for critical pairs
 -- | Returns a list of morphisms from left side of rules to all valid overlapping pairs
-findPotentialCriticalPairs :: (DPO m, EpiPairs m) => MorphismsConfig -> Production m -> Production m -> [(m, m)]
+findPotentialCriticalPairs :: (DPO morph, EpiPairs morph) => MorphismsConfig -> Production morph -> Production morph -> [(morph,morph)]
 findPotentialCriticalPairs conf p1 p2 = satisfyingPairs
   where
     pairs = createJointlyEpimorphicPairsFromCodomains (matchRestriction conf) (getLHS p1) (getLHS p2)
     satisfyingPairs = filter (\(m1,m2) -> satisfyRewritingConditions conf (p1,m1) (p2,m2)) pairs
 
 -- | Finds all Critical Pairs between two given Productions
-findCriticalPairs :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> [CriticalPair m]
+findCriticalPairs :: (EpiPairs morph, DPO morph) => MorphismsConfig -> Production morph -> Production morph -> [CriticalPair morph]
 findCriticalPairs conf p1 p2 =
   findAllDeleteUseAndProduceDangling conf p1 p2 ++ findAllProduceForbid conf p1 p2
 
@@ -123,7 +123,7 @@ findCriticalPairs conf p1 p2 =
 
 -- | All DeleteUse caused by the derivation of @p1@ before @p2@.
 -- It occurs when @p1@ deletes something used by @p2@.
-findAllDeleteUse :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> [CriticalPair m]
+findAllDeleteUse :: (EpiPairs morph, DPO morph) => MorphismsConfig -> Production morph -> Production morph -> [CriticalPair morph]
 findAllDeleteUse conf p1 p2 =
   map (\m -> CriticalPair m Nothing Nothing DeleteUse) deleteUsePairs
   where
@@ -134,7 +134,7 @@ findAllDeleteUse conf p1 p2 =
 
 -- | All ProduceDangling caused by the derivation of @p1@ before @p2@.
 -- It occurs when @p1@ creates something that unable @p2@.
-findAllProduceDangling :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> [CriticalPair m]
+findAllProduceDangling :: (EpiPairs morph, DPO morph) => MorphismsConfig -> Production morph -> Production morph -> [CriticalPair morph]
 findAllProduceDangling conf p1 p2 =
   map (\m -> CriticalPair m Nothing Nothing ProduceDangling) produceDanglingPairs
   where
@@ -145,7 +145,7 @@ findAllProduceDangling conf p1 p2 =
 
 -- | Tests DeleteUse and ProduceDangling for the same pairs,
 -- more efficient than deal separately.
-findAllDeleteUseAndProduceDangling :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> [CriticalPair m]
+findAllDeleteUseAndProduceDangling :: (EpiPairs morph, DPO morph) => MorphismsConfig -> Production morph -> Production morph -> [CriticalPair morph]
 findAllDeleteUseAndProduceDangling conf p1 p2 =
   map categorizeConflict conflicts
   where
@@ -161,13 +161,13 @@ findAllDeleteUseAndProduceDangling conf p1 p2 =
 --
 -- Rule @p1@ causes a produce-forbid conflict with @p2@ if some
 -- NAC in @p2@ fails to be satisfied after the aplication of @p1@.
-findAllProduceForbid :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> [CriticalPair m]
+findAllProduceForbid :: (EpiPairs morph, DPO morph) => MorphismsConfig -> Production morph -> Production morph -> [CriticalPair morph]
 findAllProduceForbid conf p1 p2 =
   concatMap (findProduceForbidForNAC conf p1 p2) (zip (getNACs p2) [0..])
 
 -- | Check ProduceForbid for a NAC @n@ in @p2@.
-findProduceForbidForNAC :: (EpiPairs m, DPO m) => MorphismsConfig -> Production m -> Production m -> (m, Int) -> [CriticalPair m]
+findProduceForbidForNAC :: (EpiPairs morph, DPO morph) => MorphismsConfig -> Production morph -> Production morph -> (morph, Int) -> [CriticalPair morph]
 findProduceForbidForNAC conf p1 p2 nac =
   map
-    (\(m,m',nac) -> CriticalPair m (Just m') (Just nac) ProduceForbid)
+    (\(morph,morph',nac) -> CriticalPair morph (Just morph') (Just nac) ProduceForbid)
     (produceForbidOneNac conf p1 p2 nac)