From 43775f9f8ecbdc9e1c2009e843037f293474423c Mon Sep 17 00:00:00 2001
From: "Jonas S. Bezerra" <jsbezerra@inf.ufrgs.br>
Date: Fri, 4 Nov 2022 14:48:30 +0000
Subject: [PATCH 01/12] chore: bump stack lts resolver from 10.5 to 19.3 (ghc
 8.2.2 -> 9.0.2)

---
 .gitignore                     |  5 +++--
 src/library/Base/Valid.hs      |  2 ++
 src/library/Data/DList.hs      |  2 ++
 src/library/GrLang/Compiler.hs |  2 +-
 src/repl/GrLang.hs             |  8 +++++---
 stack.yaml                     |  4 ++--
 stack.yaml.lock                | 26 ++++++++++++++++++++++++++
 verigraph.cabal                | 21 ++++++++++-----------
 8 files changed, 51 insertions(+), 19 deletions(-)
 create mode 100644 stack.yaml.lock

diff --git a/.gitignore b/.gitignore
index 8e9a568a..648e015f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,6 +3,7 @@ doc/
 org/
 tmp/
 .stack-work/
+dist-newstyle/
 *.hp
 *.prof
 *.xsl
@@ -29,7 +30,7 @@ images/.directory
 
 
 # Editor/IDE stuff
-TAGS
-*#
 .vscode/
 .idea/
+.fleet/
+verigraph.code-workspace
diff --git a/src/library/Base/Valid.hs b/src/library/Base/Valid.hs
index fd2bb80f..b74f74ab 100644
--- a/src/library/Base/Valid.hs
+++ b/src/library/Base/Valid.hs
@@ -44,6 +44,8 @@ data ValidationResult
   deriving (Eq, Show)
 
 
+instance Semigroup ValidationResult
+
 instance Monoid ValidationResult where
 
   mempty = IsValid
diff --git a/src/library/Data/DList.hs b/src/library/Data/DList.hs
index 8b3619aa..7a6ae618 100644
--- a/src/library/Data/DList.hs
+++ b/src/library/Data/DList.hs
@@ -29,6 +29,8 @@ import           Prelude hiding (null)
 -- difference lists, allowing /O(1)/ checks if the list is empty.
 newtype DList a = DList { unDList :: Maybe ([a] -> [a]) }
 
+instance Semigroup (DList a)
+
 instance Monoid (DList a) where
   mempty = empty
 
diff --git a/src/library/GrLang/Compiler.hs b/src/library/GrLang/Compiler.hs
index ce8edc69..fbd81a08 100644
--- a/src/library/GrLang/Compiler.hs
+++ b/src/library/GrLang/Compiler.hs
@@ -171,7 +171,7 @@ createEdge edgeType src tgt loc Nothing = do
   return newId
 
 
-compileMorphism' :: MonadGrLang m => Maybe Location -> Located Text -> Located Text -> [MorphismDeclaration] -> ExceptT Error m GrMorphism
+compileMorphism' :: (MonadGrLang m) => Maybe Location -> Located Text -> Located Text -> [MorphismDeclaration] -> ExceptT Error m GrMorphism
 compileMorphism' loc domName codName decls = do
   [domain, codomain] <- mapMCollectErrors getGraph [(domName, "domain"), (codName, "codomain")]
   compileMorphism loc domain codomain decls
diff --git a/src/repl/GrLang.hs b/src/repl/GrLang.hs
index 59ba5c8c..4b6fe9dc 100644
--- a/src/repl/GrLang.hs
+++ b/src/repl/GrLang.hs
@@ -344,11 +344,13 @@ initGrLang globalState = do
           freeGrLang idx
       )
     , ("toDot", haskellFn2 globalState $ \idx name -> do
-          VGraph graph <- lookupGrLangValue idx
-          return . show $ Dot.typedGraph grLangNamingContext (pretty $ Text.decodeUtf8 name) graph
+          graph <- lookupGrLangValue idx
+          case graph of
+            VGraph graph -> return . show $ Dot.typedGraph grLangNamingContext (pretty $ Text.decodeUtf8 name) graph
+            _ -> error "Pattern match failed"
       )
     , ("compileFile", haskellFn1 globalState $ \path ->
-          GrLang.compileFile path
+        GrLang.compileFile path
       )
     , ("readGGX", haskellFn1 globalState $ \fileName -> do
           (grammar, _, _) <- liftIO $ GGX.readGrammar fileName False morphConf
diff --git a/stack.yaml b/stack.yaml
index 442fd6a1..a289d7f2 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -3,9 +3,9 @@ extra-package-dbs: []
 packages:
 - '.'
 extra-deps:
-- combinat-0.2.8.2
+- combinat-0.2.10.0
 - hslua-0.9.4
-resolver: lts-10.5
+resolver: lts-19.31
 
 ghc-options:
   '$everything': -threaded
\ No newline at end of file
diff --git a/stack.yaml.lock b/stack.yaml.lock
new file mode 100644
index 00000000..693d6634
--- /dev/null
+++ b/stack.yaml.lock
@@ -0,0 +1,26 @@
+# This file was autogenerated by Stack.
+# You should not edit this file by hand.
+# For more information, please see the documentation at:
+#   https://docs.haskellstack.org/en/stable/lock_files
+
+packages:
+- completed:
+    hackage: combinat-0.2.10.0@sha256:adc1dbb532b048e419374e9e89dc4f92c47758300ffe8534a54849266706e53b,5318
+    pantry-tree:
+      sha256: 3633e40972d9b3bc12ae75fdeadff558d5bf8293f592245db8bfdbff8c9e22be
+      size: 4964
+  original:
+    hackage: combinat-0.2.10.0
+- completed:
+    hackage: hslua-0.9.4@sha256:92ededc7d83003554084767def4fc5bfaf0b585f9b93d09e612868344a18bb86,7915
+    pantry-tree:
+      sha256: 200b4b2794bdc906efbcc0d8344e4966c640fb3623c8a1d0e5920320e57ebab2
+      size: 5517
+  original:
+    hackage: hslua-0.9.4
+snapshots:
+- completed:
+    sha256: e5f56f619132209b826084cacd6374d7f0344cc88a9d1d305878190e4204ae1f
+    size: 619205
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/19/31.yaml
+  original: lts-19.31
diff --git a/verigraph.cabal b/verigraph.cabal
index b345d91f..a564212b 100644
--- a/verigraph.cabal
+++ b/verigraph.cabal
@@ -1,5 +1,6 @@
+cabal-version:       3.4
 name:                verigraph
-version:             1.1.0
+version:             1.2.0
 synopsis:            Software specification and verification tool based on graph rewriting.
 -- description:
 license:             Apache-2.0
@@ -11,25 +12,24 @@ category:            Data
 build-type:          Simple
 -- extra-source-files:
 data-files:          src/repl/lua/*.lua
-cabal-version:       >=1.22
 
 library
   default-language:    Haskell2010
   hs-source-dirs:      src/library/
   ghc-options:         -O -Wall -fno-warn-name-shadowing -fno-warn-unused-do-bind -fno-warn-orphans
   other-extensions:    TypeFamilies, MultiParamTypeClasses, FlexibleContexts
-  build-depends:       base >=4.8 && <4.11,
-                       containers >=0.4 && <0.6,
+  build-depends:       base >= 4.15,
+                       containers >= 0.6,
                        directory >= 1.3 && <2,
                        filepath >= 1.4 && <2,
                        hxt >=9.3.1.15 && <9.4,
                        mtl >=2.2 && <2.3,
                        parallel >= 3.2,
                        parsec >=3.1 && <3.2,
-                       prettyprinter >=1.1 && <1.2,
-                       QuickCheck >=2.8 && <2.11,
+                       prettyprinter >=1.7,
+                       QuickCheck == 2.14.2,
                        semigroups >= 0.18,
-                       set-monad >= 0.2 && <0.3,
+                       set-monad >= 0.3,
                        split >= 0.2,
                        text >=1.2 && <1.3
   exposed-modules:     Abstract.Category.Adhesive
@@ -136,7 +136,7 @@ executable verigraph
                        filepath,
                        hxt,
                        matrix >= 0.3,
-                       optparse-applicative>=0.12 && < 0.15,
+                       optparse-applicative>=0.16,
                        parallel >= 3.2,
                        prettyprinter,
                        split >= 0.2
@@ -157,7 +157,7 @@ executable verigraph-mcheck
   build-depends:       base, verigraph,
                        containers,
                        hxt,
-                       optparse-applicative>=0.12 && < 0.15,
+                       optparse-applicative>=0.16,
                        prettyprinter
   other-modules:       GlobalOptions
 
@@ -174,7 +174,7 @@ executable verigraph-repl
                        haskeline >=0.7 && <1.0,
                        hslua >=0.9.4 && <1.0,
                        mtl,
-                       optparse-applicative>=0.12 && < 0.15,
+                       optparse-applicative >= 0.16,
                        prettyprinter,
                        text
   autogen-modules:     Paths_verigraph
@@ -182,7 +182,6 @@ executable verigraph-repl
                        Paths_verigraph
                        Util.Lua
 
-
 test-suite HSpecTests
   default-language:    Haskell2010
   hs-source-dirs:      tests/

From 6f99584843c0d22a58f4788dcb6007279318e505 Mon Sep 17 00:00:00 2001
From: "Jonas S. Bezerra" <jsbezerra@inf.ufrgs.br>
Date: Tue, 8 Nov 2022 18:10:12 +0000
Subject: [PATCH 02/12] solve deprecation warnings

---
 src/library/Abstract/Category.hs     | 5 +++--
 src/library/Image/Dot/Prettyprint.hs | 2 +-
 src/library/Image/Dot/StateSpace.hs  | 4 ++--
 3 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/library/Abstract/Category.hs b/src/library/Abstract/Category.hs
index b81ed3ef..3e45372b 100644
--- a/src/library/Abstract/Category.hs
+++ b/src/library/Abstract/Category.hs
@@ -12,6 +12,7 @@ module Abstract.Category
   , Cospan
   ) where
 
+import Data.Kind (Type)
 
 {- | Type class for representing categories in Verigraph.
 
@@ -20,7 +21,7 @@ there is an associated type of objects @Obj morph@.
 -}
 class (Eq morph) => Category morph where
   -- | Data type that represents objects of the category
-  type Obj morph :: *
+  type Obj morph :: Type
 
   -- | Morphism composition operator.
   --
@@ -36,7 +37,7 @@ class (Eq morph) => Category morph where
   codomain :: morph -> Obj morph
 
   -- | Data type defining the different classes of morphism for this category.
-  data MorphismClass morph :: *
+  data MorphismClass morph :: Type
   -- | Class containing all morphisms of the category.
   anyMorphism :: MorphismClass morph
   -- | Class containing all monomorphisms of the category.
diff --git a/src/library/Image/Dot/Prettyprint.hs b/src/library/Image/Dot/Prettyprint.hs
index f9c50783..b2e05d5d 100644
--- a/src/library/Image/Dot/Prettyprint.hs
+++ b/src/library/Image/Dot/Prettyprint.hs
@@ -13,7 +13,7 @@
 module Image.Dot.Prettyprint
   (graph, digraph, node, undirEdge, dirEdge, attrList, subgraph, anonSubgraph) where
 
-import           Data.Text.Prettyprint.Doc
+import           Prettyprinter
 
 -- | Pretty prints a (undirected) graph with the given name and list of statements.
 graph :: Doc ann -> [Doc ann] -> Doc ann
diff --git a/src/library/Image/Dot/StateSpace.hs b/src/library/Image/Dot/StateSpace.hs
index 9a7d70eb..fa9ae87a 100644
--- a/src/library/Image/Dot/StateSpace.hs
+++ b/src/library/Image/Dot/StateSpace.hs
@@ -10,8 +10,8 @@ module Image.Dot.StateSpace (stateSpace) where
 
 import qualified Data.IntMap                       as IntMap
 import qualified Data.Set                          as Set
-import           Data.Text.Prettyprint.Doc         (Doc, Pretty (..))
-import qualified Data.Text.Prettyprint.Doc         as PP
+import           Prettyprinter                     (Doc, Pretty (..))
+import qualified Prettyprinter                     as PP
 
 import           Abstract.Rewriting.DPO.StateSpace
 import qualified Image.Dot.Prettyprint             as Dot

From cbd1d7e273cb9a137c1813975e4fffe7c35983b6 Mon Sep 17 00:00:00 2001
From: "Jonas S. Bezerra" <jsbezerra@inf.ufrgs.br>
Date: Tue, 8 Nov 2022 18:10:54 +0000
Subject: [PATCH 03/12] update combinat dependency

---
 stack.yaml      | 1 +
 stack.yaml.lock | 7 +++++++
 verigraph.cabal | 2 +-
 3 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/stack.yaml b/stack.yaml
index a289d7f2..bf1946d2 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -5,6 +5,7 @@ packages:
 extra-deps:
 - combinat-0.2.10.0
 - hslua-0.9.4
+- compact-word-vectors-0.2.0.2
 resolver: lts-19.31
 
 ghc-options:
diff --git a/stack.yaml.lock b/stack.yaml.lock
index 693d6634..3a6091bb 100644
--- a/stack.yaml.lock
+++ b/stack.yaml.lock
@@ -18,6 +18,13 @@ packages:
       size: 5517
   original:
     hackage: hslua-0.9.4
+- completed:
+    hackage: compact-word-vectors-0.2.0.2@sha256:49cf00f224000f149306e7043c228fa33e3dba87f10589e8326388c3278ba594,2709
+    pantry-tree:
+      sha256: 5713337589ee024f627123b448f8bf6ddf33e457c72daabc84a12f4ce7d8ddb0
+      size: 744
+  original:
+    hackage: compact-word-vectors-0.2.0.2
 snapshots:
 - completed:
     sha256: e5f56f619132209b826084cacd6374d7f0344cc88a9d1d305878190e4204ae1f
diff --git a/verigraph.cabal b/verigraph.cabal
index a564212b..f9c30abb 100644
--- a/verigraph.cabal
+++ b/verigraph.cabal
@@ -191,7 +191,7 @@ test-suite HSpecTests
   build-depends:       base, verigraph,
                        call-stack,
                        containers,
-                       combinat >= 0.2.8,
+                       combinat >= 0.2.10,
                        directory,
                        deepseq,
                        filepath,

From 1604d1fd84de3fd96f9b2e7779c1ffa78647685d Mon Sep 17 00:00:00 2001
From: "Jonas S. Bezerra" <jsbezerra@inf.ufrgs.br>
Date: Tue, 8 Nov 2022 21:21:39 +0000
Subject: [PATCH 04/12] explicit MonadFail in function sigantures

---
 src/library/GrLang/Compiler.hs | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/library/GrLang/Compiler.hs b/src/library/GrLang/Compiler.hs
index fbd81a08..16b48160 100644
--- a/src/library/GrLang/Compiler.hs
+++ b/src/library/GrLang/Compiler.hs
@@ -39,14 +39,14 @@ import           Rewriting.DPO.TypedGraph       (Production (..))
 import qualified Util.Map                       as Map
 import           Util.Monad
 
-compileFile :: (MonadIO m, MonadGrLang m) => FilePath -> ExceptT Error m ()
+compileFile :: (MonadIO m, MonadGrLang m, MonadFail m) => FilePath -> ExceptT Error m ()
 compileFile path = importIfNeeded_ path $
   loadModule (A Nothing path) >>= compile
 
-compile :: (MonadIO m, MonadGrLang m) => [TopLevelDeclaration] -> ExceptT Error m ()
+compile :: (MonadIO m, MonadGrLang m, MonadFail m) => [TopLevelDeclaration] -> ExceptT Error m ()
 compile = mapMCollectErrors_ compileDecl
 
-compileDecl :: (MonadIO m, MonadGrLang m) => TopLevelDeclaration -> ExceptT Error m ()
+compileDecl :: (MonadIO m, MonadGrLang m, MonadFail m) => TopLevelDeclaration -> ExceptT Error m ()
 compileDecl (DeclNodeType n) = addNodeType n
 compileDecl (DeclEdgeType e s t) = addEdgeType e s t
 compileDecl (DeclGraph name graphDecls) =
@@ -171,7 +171,7 @@ createEdge edgeType src tgt loc Nothing = do
   return newId
 
 
-compileMorphism' :: (MonadGrLang m) => Maybe Location -> Located Text -> Located Text -> [MorphismDeclaration] -> ExceptT Error m GrMorphism
+compileMorphism' :: (MonadGrLang m, MonadFail m) => Maybe Location -> Located Text -> Located Text -> [MorphismDeclaration] -> ExceptT Error m GrMorphism
 compileMorphism' loc domName codName decls = do
   [domain, codomain] <- mapMCollectErrors getGraph [(domName, "domain"), (codName, "codomain")]
   compileMorphism loc domain codomain decls
@@ -183,7 +183,7 @@ compileMorphism' loc domName codName decls = do
         (VMorph _) -> throwError loc . PP.fillSep . PP.words $ "Cannot use a morphism as " <> descr <> "."
         (VRule _) -> throwError loc . PP.fillSep . PP.words $ "Cannot use a rule as " <> descr <> "."
 
-compileMorphism :: MonadGrLang m => Maybe Location -> GrGraph -> GrGraph -> [MorphismDeclaration] -> ExceptT Error m GrMorphism
+compileMorphism :: (MonadGrLang m, MonadFail m) => Maybe Location -> GrGraph -> GrGraph -> [MorphismDeclaration] -> ExceptT Error m GrMorphism
 compileMorphism loc domain codomain decls = do
   let domElems = namedElementsOf domain
       codElems = namedElementsOf codomain
@@ -244,7 +244,7 @@ maybeLeft = either Just (const Nothing)
 maybeRight :: Either a b -> Maybe b
 maybeRight = either (const Nothing) Just
 
-compileRule :: MonadGrLang m => [RuleDeclaration] -> ExceptT Error m GrRule
+compileRule :: (MonadGrLang m, MonadFail m) => [RuleDeclaration] -> ExceptT Error m GrRule
 compileRule decls = do
   -- Compile the LHS graph from match declarations
   lhsState <- evalGraphT emptyGraphState $ mapMCollectErrors_ compileMatch decls >> get
@@ -346,7 +346,7 @@ compileCreate _                  = return ()
 --
 -- NOTE: when nodes are joined, any incident edges will become invalid, so they have to be corrected
 -- after calling this function.
-compileJoin :: MonadGrLang m => RuleDeclaration -> GraphT m (Either [(NodeId, NodeId)] [(EdgeId, EdgeId)])
+compileJoin :: (MonadGrLang m, MonadFail m) => RuleDeclaration -> GraphT m (Either [(NodeId, NodeId)] [(EdgeId, EdgeId)])
 compileJoin (DeclJoin joined newName) = do
   elems <- getJoinableElems joined
   case elems of

From 2e53c7d3f10b31f61854bf3f2c005b26ea6883a9 Mon Sep 17 00:00:00 2001
From: "Jonas S. Bezerra" <jsbezerra@inf.ufrgs.br>
Date: Tue, 8 Nov 2022 21:53:32 +0000
Subject: [PATCH 05/12] Revert "explicit MonadFail in function sigantures"

This reverts commit f0a155fcc1c88353991b582550bcd448b8198356.
---
 src/library/GrLang/Compiler.hs | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/library/GrLang/Compiler.hs b/src/library/GrLang/Compiler.hs
index 16b48160..fbd81a08 100644
--- a/src/library/GrLang/Compiler.hs
+++ b/src/library/GrLang/Compiler.hs
@@ -39,14 +39,14 @@ import           Rewriting.DPO.TypedGraph       (Production (..))
 import qualified Util.Map                       as Map
 import           Util.Monad
 
-compileFile :: (MonadIO m, MonadGrLang m, MonadFail m) => FilePath -> ExceptT Error m ()
+compileFile :: (MonadIO m, MonadGrLang m) => FilePath -> ExceptT Error m ()
 compileFile path = importIfNeeded_ path $
   loadModule (A Nothing path) >>= compile
 
-compile :: (MonadIO m, MonadGrLang m, MonadFail m) => [TopLevelDeclaration] -> ExceptT Error m ()
+compile :: (MonadIO m, MonadGrLang m) => [TopLevelDeclaration] -> ExceptT Error m ()
 compile = mapMCollectErrors_ compileDecl
 
-compileDecl :: (MonadIO m, MonadGrLang m, MonadFail m) => TopLevelDeclaration -> ExceptT Error m ()
+compileDecl :: (MonadIO m, MonadGrLang m) => TopLevelDeclaration -> ExceptT Error m ()
 compileDecl (DeclNodeType n) = addNodeType n
 compileDecl (DeclEdgeType e s t) = addEdgeType e s t
 compileDecl (DeclGraph name graphDecls) =
@@ -171,7 +171,7 @@ createEdge edgeType src tgt loc Nothing = do
   return newId
 
 
-compileMorphism' :: (MonadGrLang m, MonadFail m) => Maybe Location -> Located Text -> Located Text -> [MorphismDeclaration] -> ExceptT Error m GrMorphism
+compileMorphism' :: (MonadGrLang m) => Maybe Location -> Located Text -> Located Text -> [MorphismDeclaration] -> ExceptT Error m GrMorphism
 compileMorphism' loc domName codName decls = do
   [domain, codomain] <- mapMCollectErrors getGraph [(domName, "domain"), (codName, "codomain")]
   compileMorphism loc domain codomain decls
@@ -183,7 +183,7 @@ compileMorphism' loc domName codName decls = do
         (VMorph _) -> throwError loc . PP.fillSep . PP.words $ "Cannot use a morphism as " <> descr <> "."
         (VRule _) -> throwError loc . PP.fillSep . PP.words $ "Cannot use a rule as " <> descr <> "."
 
-compileMorphism :: (MonadGrLang m, MonadFail m) => Maybe Location -> GrGraph -> GrGraph -> [MorphismDeclaration] -> ExceptT Error m GrMorphism
+compileMorphism :: MonadGrLang m => Maybe Location -> GrGraph -> GrGraph -> [MorphismDeclaration] -> ExceptT Error m GrMorphism
 compileMorphism loc domain codomain decls = do
   let domElems = namedElementsOf domain
       codElems = namedElementsOf codomain
@@ -244,7 +244,7 @@ maybeLeft = either Just (const Nothing)
 maybeRight :: Either a b -> Maybe b
 maybeRight = either (const Nothing) Just
 
-compileRule :: (MonadGrLang m, MonadFail m) => [RuleDeclaration] -> ExceptT Error m GrRule
+compileRule :: MonadGrLang m => [RuleDeclaration] -> ExceptT Error m GrRule
 compileRule decls = do
   -- Compile the LHS graph from match declarations
   lhsState <- evalGraphT emptyGraphState $ mapMCollectErrors_ compileMatch decls >> get
@@ -346,7 +346,7 @@ compileCreate _                  = return ()
 --
 -- NOTE: when nodes are joined, any incident edges will become invalid, so they have to be corrected
 -- after calling this function.
-compileJoin :: (MonadGrLang m, MonadFail m) => RuleDeclaration -> GraphT m (Either [(NodeId, NodeId)] [(EdgeId, EdgeId)])
+compileJoin :: MonadGrLang m => RuleDeclaration -> GraphT m (Either [(NodeId, NodeId)] [(EdgeId, EdgeId)])
 compileJoin (DeclJoin joined newName) = do
   elems <- getJoinableElems joined
   case elems of

From 5c667136fc314a46cf0262d19274f8a1e229ee1d Mon Sep 17 00:00:00 2001
From: "Jonas S. Bezerra" <jsbezerra@inf.ufrgs.br>
Date: Tue, 8 Nov 2022 23:18:04 +0000
Subject: [PATCH 06/12] desugarize pattern matching

---
 src/CLI/CriticalPairAnalysis.hs |   1 -
 src/library/GrLang/Compiler.hs  |   3 +-
 src/repl/GrLang.hs              | 165 ++++++++++++++++++++------------
 3 files changed, 108 insertions(+), 61 deletions(-)

diff --git a/src/CLI/CriticalPairAnalysis.hs b/src/CLI/CriticalPairAnalysis.hs
index c094d389..7a76e68e 100644
--- a/src/CLI/CriticalPairAnalysis.hs
+++ b/src/CLI/CriticalPairAnalysis.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE TupleSections #-}
 module CriticalPairAnalysis
   ( Options
   , options
diff --git a/src/library/GrLang/Compiler.hs b/src/library/GrLang/Compiler.hs
index fbd81a08..39f6d143 100644
--- a/src/library/GrLang/Compiler.hs
+++ b/src/library/GrLang/Compiler.hs
@@ -173,7 +173,8 @@ createEdge edgeType src tgt loc Nothing = do
 
 compileMorphism' :: (MonadGrLang m) => Maybe Location -> Located Text -> Located Text -> [MorphismDeclaration] -> ExceptT Error m GrMorphism
 compileMorphism' loc domName codName decls = do
-  [domain, codomain] <- mapMCollectErrors getGraph [(domName, "domain"), (codName, "codomain")]
+  errors <- mapMCollectErrors getGraph [(domName, "domain"), (codName, "codomain")]
+  let [domain, codomain] = errors
   compileMorphism loc domain codomain decls
   where
     getGraph (name, descr) = do
diff --git a/src/repl/GrLang.hs b/src/repl/GrLang.hs
index 4b6fe9dc..37f3e393 100644
--- a/src/repl/GrLang.hs
+++ b/src/repl/GrLang.hs
@@ -180,8 +180,9 @@ instance MonadGrLang (ReaderT GrLangState Lua) where
   addNodeType (A loc name) = do
     existingType <- lift $ lookupNodeType name
     GrLang.addNew loc "Node type" name (nodeLocation <$> existingType) $ do
-      newId:_ <- TypeGraph.newNodes <$> get typeGraph
-      let metadata = Metadata (Just name) loc
+      newNodes <- TypeGraph.newNodes <$> get typeGraph
+      let newId:_ = newNodes
+          metadata = Metadata (Just name) loc
       modify typeGraph $ TypeGraph.insertNodeWithPayload newId (Just metadata)
       modify nodeTypes $ Map.insert name newId
 
@@ -190,8 +191,9 @@ instance MonadGrLang (ReaderT GrLangState Lua) where
     tgtType <- GrLang.getNodeType tgtName
     existingType <- lift $ lookupEdgeType name srcType tgtType
     GrLang.addNew loc "Edge type" (showEdgeType name srcType tgtType) (edgeLocation <$> existingType) $ do
-      newId:_ <- TypeGraph.newEdges <$> get typeGraph
-      let metadata = Metadata (Just name) loc
+      newEdges <- TypeGraph.newEdges <$> get typeGraph
+      let newId:_ = newEdges
+          metadata = Metadata (Just name) loc
           (Node srcId _, Node tgtId _) = (srcType, tgtType)
       modify typeGraph $ TypeGraph.insertEdgeWithPayload newId srcId tgtId (Just metadata)
       modify edgeTypes $ Map.insert (name, srcId, tgtId) newId
@@ -395,47 +397,59 @@ initGrLang globalState = do
           allocateGrLang (VGraph graph)
       )
     , ("identity", haskellFn1 globalState $ \idx -> do
-          VGraph graph <- lookupGrLangValue idx
+          value <- lookupGrLangValue idx
+          let VGraph graph = value
           allocateGrLang (VMorph $ identity graph)
       )
     , ("isInitial", haskellFn1 globalState $ \idx -> do
-          VGraph graph <- lookupGrLangValue idx
+          value <- lookupGrLangValue idx
+          let VGraph graph = value
           return (isInitial (Proxy @GrMorphism) graph)
       )
     , ("calculateCoproduct", haskellFn2 globalState $ \idG idH -> do
-          VGraph g <- lookupGrLangValue idG
-          VGraph h <- lookupGrLangValue idH
-          let (jG, jH) = calculateCoproduct g h
+          valueG <- lookupGrLangValue idG
+          valueH <- lookupGrLangValue idH
+          let VGraph g = valueG
+              VGraph h = valueH
+              (jG, jH) = calculateCoproduct g h
           returnVals [VGraph (codomain jG), VMorph jG, VMorph jH]
       )
     , ("calculateProduct", haskellFn2 globalState $ \idG idH -> do
-          VGraph g <- lookupGrLangValue idG
-          VGraph h <- lookupGrLangValue idH
-          let (pG, pH) = calculateProduct g h
+          valueG <- lookupGrLangValue idG
+          valueH <- lookupGrLangValue idH
+          let VGraph g = valueG
+              VGraph h = valueH
+              (pG, pH) = calculateProduct g h
           returnVals [VGraph (domain pG), VMorph pG, VMorph pH]
       )
     , ("findMorphisms", haskellFn3 globalState $ \kindStr idG idH -> do
-          VGraph g <- lookupGrLangValue idG
-          VGraph h <- lookupGrLangValue idH
+          valueG <- lookupGrLangValue idG
+          valueH <- lookupGrLangValue idH
+          let VGraph g = valueG
+              VGraph h = valueH
           cls <- morphClassFromString kindStr
           withMemSpace iterLists .
             allocateMemSpace . map (\f -> [VMorph f]) $ findMorphisms cls g h
       )
     , ("findAllSubobjectsOf", haskellFn1 globalState $ \idx -> do
-          VGraph g <- lookupGrLangValue idx
+          value <- lookupGrLangValue idx
+          let VGraph g = value
           withMemSpace iterLists .
             allocateMemSpace . map (\f -> [VGraph (domain f), VMorph f]) $
               findAllSubobjectsOf g
       )
     , ("findAllQuotientsOf", haskellFn1 globalState $ \idx -> do
-          VGraph g <- lookupGrLangValue idx
+          value <- lookupGrLangValue idx
+          let VGraph g = value
           withMemSpace iterLists .
             allocateMemSpace . map (\f -> [VGraph (codomain f), VMorph f]) $
               findAllQuotientsOf g
       )
     , ("findJointSurjections", haskellFn4 globalState $ \idG kindStrG idH kindStrH -> do
-          VGraph g <- lookupGrLangValue idG
-          VGraph h <- lookupGrLangValue idH
+          valueG <- lookupGrLangValue idG
+          valueH <- lookupGrLangValue idH
+          let VGraph g = valueG
+              VGraph h = valueH
           clsG <- morphClassFromString kindStrG
           clsH <- morphClassFromString kindStrH
           withMemSpace iterLists .
@@ -446,83 +460,109 @@ initGrLang globalState = do
 
   setNative "Morphism"
     [ ("parse", haskellFn3 globalState $ \domIdx codIdx string -> do
-          VGraph dom <- lookupGrLangValue domIdx
-          VGraph cod <- lookupGrLangValue codIdx
+          valueDom <- lookupGrLangValue domIdx
+          valueCod <- lookupGrLangValue codIdx
+          let VGraph dom = valueDom
+              VGraph cod = valueCod
           morphism <- GrLang.compileMorphism Nothing dom cod =<< GrLang.parseMorphism "<repl>" (string :: String)
           allocateGrLang (VMorph morphism)
       )
     , ("compose", haskellFn2 globalState $ \idF idG -> do
-          VMorph f <- lookupGrLangValue idF
-          VMorph g <- lookupGrLangValue idG
+          valueF <- lookupGrLangValue idF
+          valueG <- lookupGrLangValue idG
+          let VMorph f = valueF
+              VMorph g = valueG
           allocateGrLang (VMorph $ f <&> g)
       )
     , ("isMonic", haskellFn1 globalState $ \idx -> do
-          VMorph f <- lookupGrLangValue idx
+          value <- lookupGrLangValue idx
+          let VMorph f = value
           return (isMonic f)
       )
     , ("isEpic", haskellFn1 globalState $ \idx -> do
-          VMorph f <- lookupGrLangValue idx
+          value <- lookupGrLangValue idx
+          let VMorph f = value
           return (isEpic f)
       )
     , ("isIsomorphism", haskellFn1 globalState $ \idx -> do
-          VMorph f <- lookupGrLangValue idx
+          value <- lookupGrLangValue idx
+          let VMorph f = value
           return (isIsomorphism f)
       )
     , ("calculatePullback", haskellFn2 globalState $ \idF idG -> do
-          VMorph f <- lookupGrLangValue idF
-          VMorph g <- lookupGrLangValue idG
-          let (f', g') = calculatePullback f g
+          valueF <- lookupGrLangValue idF
+          valueG <- lookupGrLangValue idG
+          let VMorph f = valueF
+              VMorph g = valueG
+              (f', g') = calculatePullback f g
           returnVals [VGraph (domain f'), VMorph f', VMorph g']
       )
     , ("calculatePushout", haskellFn2 globalState $ \idF idG -> do
-          VMorph f <- lookupGrLangValue idF
-          VMorph g <- lookupGrLangValue idG
-          let (f', g') = calculatePushout f g
+          valueF <- lookupGrLangValue idF
+          valueG <- lookupGrLangValue idG
+          let VMorph f = valueF
+              VMorph g = valueG
+              (f', g') = calculatePushout f g
           returnVals [VGraph (codomain f'), VMorph f', VMorph g']
       )
     , ("calculateEqualizer", haskellFn2 globalState $ \idF idG -> do
-          VMorph f <- lookupGrLangValue idF
-          VMorph g <- lookupGrLangValue idG
-          let e = calculateEqualizer f g
+          valueF <- lookupGrLangValue idF
+          valueG <- lookupGrLangValue idG
+          let VMorph f = valueF
+              VMorph g = valueG
+              e = calculateEqualizer f g
           returnVals [VGraph (domain e), VMorph e]
       )
     , ("calculateCoequalizer", haskellFn2 globalState $ \idF idG -> do
-          VMorph f <- lookupGrLangValue idF
-          VMorph g <- lookupGrLangValue idG
-          let e = calculateCoequalizer f g
+          valueF <- lookupGrLangValue idF
+          valueG <- lookupGrLangValue idG
+          let VMorph f = valueF
+              VMorph g = valueG
+              e = calculateCoequalizer f g
           returnVals [VGraph (codomain e), VMorph e]
       )
     , ("hasPushoutComplementAlongM", haskellFn2 globalState $ \idF idG -> do
-          VMorph f <- lookupGrLangValue idF
-          VMorph g <- lookupGrLangValue idG
+          valueF <- lookupGrLangValue idF
+          valueG <- lookupGrLangValue idG
+          let VMorph f = valueF
+              VMorph g = valueG
           return (hasPushoutComplementAlongM f g)
       )
     , ("calculatePushoutComplementAlongM", haskellFn2 globalState $ \idF idG -> do
-          VMorph f <- lookupGrLangValue idF
-          VMorph g <- lookupGrLangValue idG
-          let (g', f') = calculatePushoutComplementAlongM f g
+          valueF <- lookupGrLangValue idF
+          valueG <- lookupGrLangValue idG
+          let VMorph f = valueF
+              VMorph g = valueG
+              (g', f') = calculatePushoutComplementAlongM f g
           returnVals [VGraph (codomain g'), VMorph g', VMorph f']
       )
     , ("calculateInitialPushout", haskellFn1 globalState $ \idx -> do
-          VMorph f <- lookupGrLangValue idx
-          let (b, f', c) = calculateMInitialPushout f
+          valueF <- lookupGrLangValue idx
+          let VMorph f = valueF
+              (b, f', c) = calculateMInitialPushout f
           returnVals [VGraph (domain b), VGraph (domain c), VMorph b, VMorph f', VMorph c]
       )
     , ("subobjectIntersection", haskellFn2 globalState $ \idA idB -> do
-          VMorph a <- lookupGrLangValue idA
-          VMorph b <- lookupGrLangValue idB
-          let c = subobjectIntersection a b
+          valueA <- lookupGrLangValue idA
+          valueB <- lookupGrLangValue idB
+          let VMorph a = valueA
+              VMorph b = valueB
+              c = subobjectIntersection a b
           returnVals [VGraph (domain c), VMorph c]
       )
     , ("subobjectUnion", haskellFn2 globalState $ \idA idB -> do
-          VMorph a <- lookupGrLangValue idA
-          VMorph b <- lookupGrLangValue idB
-          let c = subobjectUnion a b
+          valueA <- lookupGrLangValue idA
+          valueB <- lookupGrLangValue idB
+          let VMorph a = valueA
+              VMorph b = valueB
+              c = subobjectUnion a b
           returnVals [VGraph (domain c), VMorph c]
       )
     , ("findJointSurjectionSquares", haskellFn4 globalState $ \kindStrF idF kindStrG idG -> do
-        VMorph f <- lookupGrLangValue idF
-        VMorph g <- lookupGrLangValue idG
+        valueF <- lookupGrLangValue idF
+        valueG <- lookupGrLangValue idG
+        let VMorph f = valueF
+            VMorph g = valueG
         clsF <- morphClassFromString kindStrF
         clsG <- morphClassFromString kindStrG
         withMemSpace iterLists .
@@ -533,8 +573,10 @@ initGrLang globalState = do
 
   setNative "Cospan"
     [ ("findCospanCommuters", haskellFn3 globalState $ \kindStr idF idG -> do
-        VMorph f <- lookupGrLangValue idF
-        VMorph g <- lookupGrLangValue idG
+        valueF <- lookupGrLangValue idF
+        valueG <- lookupGrLangValue idG
+        let VMorph f = valueF
+            VMorph g = valueG
         cls <- morphClassFromString kindStr
         withMemSpace iterLists .
           allocateMemSpace . map (\h -> [VMorph h]) $ findCospanCommuters cls f g
@@ -547,23 +589,28 @@ initGrLang globalState = do
           allocateGrLang (VRule rule)
       )
     , ("getLeftObject", haskellFn1 globalState $ \idRule -> do
-          VRule rule <- lookupGrLangValue idRule
+          ruleValue <- lookupGrLangValue idRule
+          let VRule rule = ruleValue
           allocateGrLang (VGraph $ leftObject rule)
       )
     , ("getRightObject", haskellFn1 globalState $ \idRule -> do
-          VRule rule <- lookupGrLangValue idRule
+          ruleValue <- lookupGrLangValue idRule
+          let VRule rule = ruleValue
           allocateGrLang (VGraph $ rightObject rule)
       )
     , ("getInterface", haskellFn1 globalState $ \idRule -> do
-          VRule rule <- lookupGrLangValue idRule
+          ruleValue <- lookupGrLangValue idRule
+          let VRule rule = ruleValue
           allocateGrLang (VGraph $ interfaceObject rule)
       )
     , ("getLeftMorphism", haskellFn1 globalState $ \idRule -> do
-          VRule rule <- lookupGrLangValue idRule
+          ruleValue <- lookupGrLangValue idRule
+          let VRule rule = ruleValue
           allocateGrLang (VMorph $ leftMorphism rule)
       )
     , ("getRightMorphism", haskellFn1 globalState $ \idRule -> do
-          VRule rule <- lookupGrLangValue idRule
+          ruleValue <- lookupGrLangValue idRule
+          let VRule rule = ruleValue
           allocateGrLang (VMorph $ rightMorphism rule)
       )
     ]

From b38355839dbb554627eb6878f250b87b8557b639 Mon Sep 17 00:00:00 2001
From: "Jonas S. Bezerra" <jsbezerra@inf.ufrgs.br>
Date: Tue, 8 Nov 2022 23:43:15 +0000
Subject: [PATCH 07/12] fix tests

---
 .../ReplIntegrationSpec/read-ggx.stdout       | 76 ++++++-------------
 1 file changed, 22 insertions(+), 54 deletions(-)

diff --git a/tests/GrLang/ReplIntegrationSpec/read-ggx.stdout b/tests/GrLang/ReplIntegrationSpec/read-ggx.stdout
index 2eaf8c19..853855c0 100644
--- a/tests/GrLang/ReplIntegrationSpec/read-ggx.stdout
+++ b/tests/GrLang/ReplIntegrationSpec/read-ggx.stdout
@@ -16,16 +16,13 @@ Rules:
 add_floor	rule  {
   match {
     floor_1 floor : floor
-    floor_1 - next_up : next_up
-        -> floor
+    floor_1 - next_up : next_up -> floor
   }
   delete next_up
   create {
     floor : floor
-    floor_2 - next_up_1 : next_up
-        -> floor
-    floor - next_up : next_up
-        -> floor_1
+    floor_2 - next_up_1 : next_up -> floor
+    floor - next_up : next_up -> floor_1
   }
 }
 call_request	rule  {
@@ -44,17 +41,12 @@ call_request	rule  {
 initial_higher	rule  {
   match {
     floor_1 floor : floor
-    floor - next_up : next_up
-        -> floor_1
+    floor - next_up : next_up -> floor_1
   }
   forbid {
-    floor_1 -
-        higher_than : higher_than
-        -> floor
+    floor_1 - higher_than : higher_than -> floor
   }
-  create floor_1 -
-      higher_than : higher_than
-      -> floor
+  create floor_1 - higher_than : higher_than -> floor
 }
 move_down	rule  {
   match {
@@ -63,21 +55,16 @@ move_down	rule  {
     elevator : elevator
     floor_2 floor_1 floor : floor
     elevator - on : on -> floor_2
-    floor_2 -
-        higher_than : higher_than
-        -> floor
-    floor_1 - next_up : next_up
-        -> floor_2
+    floor_2 - higher_than : higher_than -> floor
+    floor_1 - next_up : next_up -> floor_2
     floor - holds : holds -> request
   }
   forbid {
     request : request
-    floor_2 - holds : holds
-        -> request
+    floor_2 - holds : holds -> request
   }
   delete on
-  create elevator - on : on
-      -> floor_1
+  create elevator - on : on -> floor_1
 }
 move_up	rule  {
   match {
@@ -86,19 +73,14 @@ move_up	rule  {
     elevator : elevator
     floor_2 floor_1 floor : floor
     elevator - on : on -> floor_2
-    floor_2 - next_up : next_up
-        -> floor_1
-    floor -
-        higher_than : higher_than
-        -> floor_2
+    floor_2 - next_up : next_up -> floor_1
+    floor - higher_than : higher_than -> floor_2
     floor - holds : holds -> request
   }
   forbid {
     request_1 : request
-    floor_2 - holds_1 : holds
-        -> request_1
-    request_1 - stop : stop
-        -> request_1
+    floor_2 - holds_1 : holds -> request_1
+    request_1 - stop : stop -> request_1
   }
   delete on
   create {
@@ -121,8 +103,7 @@ process_stop_up	rule  {
     floor - holds : holds -> request
     request - call : call -> request
   }
-  delete request
-  with matched edges
+  delete request with matched edges
 }
 set-direction_down	rule  {
   match {
@@ -131,23 +112,18 @@ set-direction_down	rule  {
     elevator : elevator
     floor_1 floor : floor
     elevator - on : on -> floor_1
-    floor_1 -
-        higher_than : higher_than
-        -> floor
+    floor_1 - higher_than : higher_than -> floor
     floor - holds : holds -> request
   }
   forbid {
     request : request
     floor : floor
-    floor -
-        higher_than : higher_than
-        -> floor_2
+    floor - higher_than : higher_than -> floor_2
     floor - holds : holds -> request
   }
   forbid {
     request : request
-    floor_1 - holds : holds
-        -> request
+    floor_1 - holds : holds -> request
     request - stop : stop -> request
   }
   delete up
@@ -169,19 +145,11 @@ stop_request	rule  {
 transitive_higher	rule  {
   match {
     floor_2 floor_1 floor : floor
-    floor_2 -
-        higher_than_1 : higher_than
-        -> floor_1
-    floor_1 -
-        higher_than : higher_than
-        -> floor
+    floor_2 - higher_than_1 : higher_than -> floor_1
+    floor_1 - higher_than : higher_than -> floor
   }
   forbid {
-    floor_2 -
-        higher_than : higher_than
-        -> floor
+    floor_2 - higher_than : higher_than -> floor
   }
-  create floor_2 -
-      higher_than : higher_than
-      -> floor
+  create floor_2 - higher_than : higher_than -> floor
 }

From 9fd485d11b16b345f933b30885214d155505a530 Mon Sep 17 00:00:00 2001
From: "Jonas S. Bezerra" <jsbezerra@inf.ufrgs.br>
Date: Wed, 9 Nov 2022 00:38:29 +0000
Subject: [PATCH 08/12] fix tests

---
 tests/Analysis/CriticalPairsSpec.hs          | 120 +++++----
 tests/Analysis/CriticalSequenceSpec.hs       | 242 +++++++++++--------
 tests/Analysis/EssentialCriticalPairsSpec.hs |  34 +--
 3 files changed, 224 insertions(+), 172 deletions(-)

diff --git a/tests/Analysis/CriticalPairsSpec.hs b/tests/Analysis/CriticalPairsSpec.hs
index 72e983f9..c591a668 100644
--- a/tests/Analysis/CriticalPairsSpec.hs
+++ b/tests/Analysis/CriticalPairsSpec.hs
@@ -27,47 +27,55 @@ cpaTest = do
 
       it "delete-use" $
         testCase findAllDeleteUse rules $
-          "( 2 0 0 0 0 0 0 0 )\n"++
-          "( 0 3 0 0 0 0 0 0 )\n"++
-          "( 0 2 6 0 0 0 0 0 )\n"++
-          "( 0 0 0 1 0 0 0 0 )\n"++
-          "( 0 0 1 0 4 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"
+          "┌                 ┐\n\
+          \│ 2 0 0 0 0 0 0 0 │\n\
+          \│ 0 3 0 0 0 0 0 0 │\n\
+          \│ 0 2 6 0 0 0 0 0 │\n\
+          \│ 0 0 0 1 0 0 0 0 │\n\
+          \│ 0 0 1 0 4 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \└                 ┘"
 
       it "produce-dangling" $
         testCase findAllProduceDangling rules $
-          "( 0 0 0 0 0 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"++
-          "( 0 0 0 0 1 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"
+          "┌                 ┐\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \│ 0 0 0 0 1 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \└                 ┘"
 
       it "delete-use and produce-dangling" $
         testCase findAllDeleteUseAndProduceDangling rules $
-          "( 2 0 0 0 0 0 0 0 )\n"++
-          "( 0 3 0 0 0 0 0 0 )\n"++
-          "( 0 2 6 0 1 0 0 0 )\n"++
-          "( 0 0 0 1 0 0 0 0 )\n"++
-          "( 0 0 1 0 4 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"
+          "┌                 ┐\n\
+          \│ 2 0 0 0 0 0 0 0 │\n\
+          \│ 0 3 0 0 0 0 0 0 │\n\
+          \│ 0 2 6 0 1 0 0 0 │\n\
+          \│ 0 0 0 1 0 0 0 0 │\n\
+          \│ 0 0 1 0 4 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \└                 ┘"
 
       it "produce-forbid" $
         testCase findAllProduceForbid rules $
-          "( 0 0 0 0 0 0 0 0 )\n"++
-          "( 2 0 0 0 0 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"++
-          "( 0 0 0 0 0 0 0 0 )\n"++
-          "( 0 0 0 0 0 1 0 0 )\n"
+          "┌                 ┐\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \│ 2 0 0 0 0 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \│ 0 0 0 0 0 0 0 0 │\n\
+          \│ 0 0 0 0 0 1 0 0 │\n\
+          \└                 ┘"
 
     describe "second-order" $ do
       (_,gg2,_) <- runIO $ XML.readGrammar fileName2 False dpoConf
@@ -75,35 +83,43 @@ cpaTest = do
 
       it "delete-use" $
         testCase findAllDeleteUse rules $
-            "( 0 0 0 0 0 )\n"++
-            "( 0 0 0 0 0 )\n"++
-            "( 0 0 5 0 0 )\n"++
-            "( 0 0 0 3 0 )\n"++
-            "( 0 0 0 0 3 )\n"
+            "┌           ┐\n\
+            \│ 0 0 0 0 0 │\n\
+            \│ 0 0 0 0 0 │\n\
+            \│ 0 0 5 0 0 │\n\
+            \│ 0 0 0 3 0 │\n\
+            \│ 0 0 0 0 3 │\n\
+            \└           ┘"
 
       it "produce-dangling" $
         testCase findAllProduceDangling rules $
-            "( 0 0 0 0 0 )\n"++
-            "( 0 0 0 0 0 )\n"++
-            "( 0 0 0 0 0 )\n"++
-            "( 0 0 0 0 0 )\n"++
-            "( 0 0 0 0 0 )\n"
+            "┌           ┐\n\
+            \│ 0 0 0 0 0 │\n\
+            \│ 0 0 0 0 0 │\n\
+            \│ 0 0 0 0 0 │\n\
+            \│ 0 0 0 0 0 │\n\
+            \│ 0 0 0 0 0 │\n\
+            \└           ┘"
 
       it "delete-use and produce-dangling" $
         testCase findAllDeleteUseAndProduceDangling rules $
-            "( 0 0 0 0 0 )\n"++
-            "( 0 0 0 0 0 )\n"++
-            "( 0 0 5 0 0 )\n"++
-            "( 0 0 0 3 0 )\n"++
-            "( 0 0 0 0 3 )\n"
+            "┌           ┐\n\
+            \│ 0 0 0 0 0 │\n\
+            \│ 0 0 0 0 0 │\n\
+            \│ 0 0 5 0 0 │\n\
+            \│ 0 0 0 3 0 │\n\
+            \│ 0 0 0 0 3 │\n\
+            \└           ┘"
 
       it "produce-forbid" $
         testCase findAllProduceForbid rules $
-            "( 0 0 0 0 0 )\n"++
-            "( 0 0 0 0 0 )\n"++
-            "( 0 0 0 0 0 )\n"++
-            "( 0 0 0 0 0 )\n"++
-            "( 0 0 0 0 0 )\n"
+            "┌           ┐\n\
+            \│ 0 0 0 0 0 │\n\
+            \│ 0 0 0 0 0 │\n\
+            \│ 0 0 0 0 0 │\n\
+            \│ 0 0 0 0 0 │\n\
+            \│ 0 0 0 0 0 │\n\
+            \└           ┘"
 
 pairwise :: (a -> a -> [b]) -> [a] -> Matrix Int
 pairwise f items =
diff --git a/tests/Analysis/CriticalSequenceSpec.hs b/tests/Analysis/CriticalSequenceSpec.hs
index 8eeb3a87..bd1e053b 100644
--- a/tests/Analysis/CriticalSequenceSpec.hs
+++ b/tests/Analysis/CriticalSequenceSpec.hs
@@ -14,7 +14,7 @@ fileName2 = "tests/grammars/secondOrderMatchTest.ggx"
 
 dpoConf :: Category morph => MorphismsConfig morph
 dpoConf = MorphismsConfig anyMorphism
-testCase findDependencies rules expected = expected `shouldBe` show (pairwise (findDependencies dpoConf []) rules)
+testCase findDependencies rules expected = show (pairwise (findDependencies dpoConf []) rules) `shouldBe` expected
 
 spec :: Spec
 spec = context "Critical Sequences Test" csaTest
@@ -36,128 +36,160 @@ csaTest = do
 testTeseRodrigoDependencies rules =
   do
     testCase findAllProduceUse rules $
-        "( 0 1 0 0 0 0 0 0 )\n"++
-        "( 0 0 3 0 0 0 0 0 )\n"++
-        "( 0 0 0 1 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 1 0 2 0 0 0 )\n"
+        "┌                 ┐\n\
+        \│ 0 1 0 0 0 0 0 0 │\n\
+        \│ 0 0 3 0 0 0 0 0 │\n\
+        \│ 0 0 0 1 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 1 0 2 0 0 0 │\n\
+        \└                 ┘"
     testCase findAllDeleteForbid rules $
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"
+        "┌                 ┐\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \└                 ┘"
     testCase findAllRemoveDangling rules $
-        "( 0 0 0 0 1 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"
+        "┌                 ┐\n\
+        \│ 0 0 0 0 1 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \└                 ┘"
     testCase findAllDeliverDelete rules $
-        "( 0 0 0 0 1 0 0 0 )\n"++
-        "( 0 0 3 0 0 0 0 0 )\n"++
-        "( 0 0 0 1 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 1 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 1 0 0 0 )\n"
+        "┌                 ┐\n\
+        \│ 0 0 0 0 1 0 0 0 │\n\
+        \│ 0 0 3 0 0 0 0 0 │\n\
+        \│ 0 0 0 1 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 1 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 1 0 0 0 │\n\
+        \└                 ┘"
     testCase findAllDeliverDangling rules $
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 1 0 0 0 0 0 )\n"
+        "┌                 ┐\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 1 0 0 0 0 0 │\n\
+        \└                 ┘"
     testCase findAllForbidProduce rules $
-        "( 0 3 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 1 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"
+        "┌                 ┐\n\
+        \│ 0 3 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 1 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \└                 ┘"
     testCase findAllProduceUseAndRemoveDangling rules $
-        "( 0 1 0 0 1 0 0 0 )\n"++
-        "( 0 0 3 0 0 0 0 0 )\n"++
-        "( 0 0 0 1 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 1 0 2 0 0 0 )\n"
+        "┌                 ┐\n\
+        \│ 0 1 0 0 1 0 0 0 │\n\
+        \│ 0 0 3 0 0 0 0 0 │\n\
+        \│ 0 0 0 1 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 1 0 2 0 0 0 │\n\
+        \└                 ┘"
     testCase findAllDeliverDeleteAndDeliverDangling rules $
-        "( 0 0 0 0 1 0 0 0 )\n"++
-        "( 0 0 3 0 0 0 0 0 )\n"++
-        "( 0 0 0 1 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 1 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 0 0 0 )\n"++
-        "( 0 0 1 0 1 0 0 0 )\n"
+        "┌                 ┐\n\
+        \│ 0 0 0 0 1 0 0 0 │\n\
+        \│ 0 0 3 0 0 0 0 0 │\n\
+        \│ 0 0 0 1 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 1 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 0 0 0 │\n\
+        \│ 0 0 1 0 1 0 0 0 │\n\
+        \└                 ┘"
 
 testSndOrderDependencies rules =
   do
     testCase findAllProduceUse rules $
-        "( 0 0 1 0 0 )\n"++
-        "( 0 0 1 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"
+        "┌           ┐\n\
+        \│ 0 0 1 0 0 │\n\
+        \│ 0 0 1 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \└           ┘"
     testCase findAllDeleteForbid rules $
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"
+        "┌           ┐\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \└           ┘"
     testCase findAllRemoveDangling rules $
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"
+        "┌           ┐\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \└           ┘"
     testCase findAllDeliverDelete rules $
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 1 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"
+        "┌           ┐\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 1 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \└           ┘"
     testCase findAllDeliverDangling rules $
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"
+        "┌           ┐\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \└           ┘"
     testCase findAllForbidProduce rules $
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"
+        "┌           ┐\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \└           ┘"
     testCase findAllProduceUseAndRemoveDangling rules $
-        "( 0 0 1 0 0 )\n"++
-        "( 0 0 1 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"
+        "┌           ┐\n\
+        \│ 0 0 1 0 0 │\n\
+        \│ 0 0 1 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \└           ┘"
     testCase findAllDeliverDeleteAndDeliverDangling rules $
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 1 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"++
-        "( 0 0 0 0 0 )\n"
+        "┌           ┐\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 1 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \│ 0 0 0 0 0 │\n\
+        \└           ┘"
 
 pairwise :: (a -> a -> [b]) -> [a] -> Matrix Int
 pairwise f items =
diff --git a/tests/Analysis/EssentialCriticalPairsSpec.hs b/tests/Analysis/EssentialCriticalPairsSpec.hs
index 4a47a96c..6bedf773 100644
--- a/tests/Analysis/EssentialCriticalPairsSpec.hs
+++ b/tests/Analysis/EssentialCriticalPairsSpec.hs
@@ -14,7 +14,7 @@ fileName2 = "tests/grammars/secondOrderMatchTest.ggx"
 
 dpoConf :: Category morph => MorphismsConfig morph
 dpoConf = MorphismsConfig monic
-testCase findEssentialCP rules expected = expected `shouldBe` show (pairwise (findEssentialCP dpoConf) rules)
+testCase findEssentialCP rules expected = show (pairwise (findEssentialCP dpoConf) rules) `shouldBe` expected
 
 spec :: Spec
 spec = context "Essential Critical Pairs Test" ecpaTest
@@ -35,23 +35,27 @@ ecpaTest = do
 
 testSndOrderConflicts rules =
   testCase findAllEssentialDeleteUse rules $
-    "( 0 0 0 0 0 )\n"++
-    "( 0 0 0 0 0 )\n"++
-    "( 0 0 2 0 0 )\n"++
-    "( 0 0 0 1 0 )\n"++
-    "( 0 0 0 0 1 )\n"
+    "┌           ┐\n\
+    \│ 0 0 0 0 0 │\n\
+    \│ 0 0 0 0 0 │\n\
+    \│ 0 0 2 0 0 │\n\
+    \│ 0 0 0 1 0 │\n\
+    \│ 0 0 0 0 1 │\n\
+    \└           ┘"
 
 testElevatorConflicts rules =
   testCase findAllEssentialDeleteUse rules $
-    "( 1 1 0 0 1 0 1 0 0 )\n"++
-    "( 0 0 0 0 0 0 0 0 0 )\n"++
-    "( 0 0 0 0 0 0 0 0 0 )\n"++
-    "( 0 0 0 0 0 0 0 0 0 )\n"++
-    "( 0 0 0 0 1 1 1 0 0 )\n"++
-    "( 0 0 0 0 0 1 1 0 1 )\n"++
-    "( 0 0 0 0 1 0 1 0 0 )\n"++
-    "( 0 0 0 0 0 0 0 0 0 )\n"++
-    "( 0 0 0 0 1 1 1 0 1 )\n"
+    "┌                   ┐\n\
+    \│ 1 1 0 0 1 0 1 0 0 │\n\
+    \│ 0 0 0 0 0 0 0 0 0 │\n\
+    \│ 0 0 0 0 0 0 0 0 0 │\n\
+    \│ 0 0 0 0 0 0 0 0 0 │\n\
+    \│ 0 0 0 0 1 1 1 0 0 │\n\
+    \│ 0 0 0 0 0 1 1 0 1 │\n\
+    \│ 0 0 0 0 1 0 1 0 0 │\n\
+    \│ 0 0 0 0 0 0 0 0 0 │\n\
+    \│ 0 0 0 0 1 1 1 0 1 │\n\
+    \└                   ┘"
 
 pairwise :: (a -> a -> [b]) -> [a] -> Matrix Int
 pairwise f items =

From e992a1d4eacd76180cd4e0b41e8dde88ba9d192a Mon Sep 17 00:00:00 2001
From: "Jonas S. Bezerra" <jonassantosbezerra@outlook.com>
Date: Wed, 9 Nov 2022 01:26:19 +0000
Subject: [PATCH 09/12] resolve import and deprecation warnings

---
 src/CLI/ApplySndOrderRules.hs       | 3 +--
 src/CLI/Cli.hs                      | 1 -
 src/CLI/ConcurrentRules.hs          | 1 -
 src/CLI/CriticalPairAnalysis.hs     | 2 --
 src/CLI/GlobalOptions.hs            | 1 -
 src/CLI/ModelChecker.hs             | 7 +++----
 src/CLI/ParallelIndependence.hs     | 1 -
 src/CLI/Processes.hs                | 1 -
 src/library/Base/Annotation.hs      | 4 ++--
 src/library/Base/Location.hs        | 3 +--
 src/library/Data/Graphs.hs          | 4 ++--
 src/library/GrLang/AST.hs           | 4 ++--
 src/library/GrLang/Compiler.hs      | 8 ++++----
 src/library/GrLang/Monad.hs         | 7 +++----
 src/library/GrLang/Parser.hs        | 4 ++--
 src/library/GrLang/Value.hs         | 3 +--
 src/library/Image/Dot/TypedGraph.hs | 4 ++--
 src/library/Logic/Ctl/Base.hs       | 2 +-
 src/library/Logic/Model.hs          | 4 ++--
 src/repl/GrLang.hs                  | 3 +--
 src/repl/Main.hs                    | 1 -
 tests/GrLang/CompilerSpec.hs        | 2 +-
 tests/GrLang/ParserSpec.hs          | 2 +-
 tests/Logic/Ctl/ParserSpec.hs       | 2 +-
 24 files changed, 30 insertions(+), 44 deletions(-)

diff --git a/src/CLI/ApplySndOrderRules.hs b/src/CLI/ApplySndOrderRules.hs
index 0b06d112..e79eeb91 100644
--- a/src/CLI/ApplySndOrderRules.hs
+++ b/src/CLI/ApplySndOrderRules.hs
@@ -5,8 +5,7 @@ module ApplySndOrderRules
   ) where
 
 import           Control.Monad                           (when)
-import           Data.Monoid                             ((<>))
-import           Data.Text.Prettyprint.Doc               (Pretty (..))
+import           Prettyprinter                          (Pretty (..))
 import           Options.Applicative
 import           System.IO                               (hPrint, stderr)
 
diff --git a/src/CLI/Cli.hs b/src/CLI/Cli.hs
index b43c6124..40a7e8f8 100644
--- a/src/CLI/Cli.hs
+++ b/src/CLI/Cli.hs
@@ -1,6 +1,5 @@
 module Main (main) where
 
-import           Data.Monoid          ((<>))
 import           GlobalOptions
 import           Options.Applicative
 
diff --git a/src/CLI/ConcurrentRules.hs b/src/CLI/ConcurrentRules.hs
index 645614d8..31fcdd70 100644
--- a/src/CLI/ConcurrentRules.hs
+++ b/src/CLI/ConcurrentRules.hs
@@ -5,7 +5,6 @@ module ConcurrentRules
   ) where
 
 import           Control.Monad
-import           Data.Monoid              ((<>))
 import           Options.Applicative
 
 import           Abstract.Constraint
diff --git a/src/CLI/CriticalPairAnalysis.hs b/src/CLI/CriticalPairAnalysis.hs
index 7a76e68e..34beab56 100644
--- a/src/CLI/CriticalPairAnalysis.hs
+++ b/src/CLI/CriticalPairAnalysis.hs
@@ -7,8 +7,6 @@ module CriticalPairAnalysis
 import           Control.Monad                         (when)
 import           Data.Matrix                           (Matrix)
 import qualified Data.Matrix                           as Matrix
-import           Data.Maybe                            (maybe)
-import           Data.Monoid                           ((<>))
 import qualified Data.Set                              as Set
 import           GHC.Conc                              (numCapabilities)
 import           Options.Applicative
diff --git a/src/CLI/GlobalOptions.hs b/src/CLI/GlobalOptions.hs
index 87455030..b139586d 100644
--- a/src/CLI/GlobalOptions.hs
+++ b/src/CLI/GlobalOptions.hs
@@ -5,7 +5,6 @@ module GlobalOptions
   , morphismsConf
   ) where
 
-import           Data.Monoid            ((<>))
 import           Options.Applicative
 
 import           Abstract.Category
diff --git a/src/CLI/ModelChecker.hs b/src/CLI/ModelChecker.hs
index 84120189..091e0432 100644
--- a/src/CLI/ModelChecker.hs
+++ b/src/CLI/ModelChecker.hs
@@ -3,10 +3,9 @@ module Main (main) where
 import           Control.Monad
 import qualified Data.IntMap                           as IntMap
 import qualified Data.List                             as List
-import           Data.Monoid                           ((<>))
-import           Data.Text.Prettyprint.Doc             (Pretty (..))
-import qualified Data.Text.Prettyprint.Doc             as PP
-import           Data.Text.Prettyprint.Doc.Render.Text (renderIO)
+import           Prettyprinter                         (Pretty (..))
+import qualified Prettyprinter                         as PP
+import           Prettyprinter.Render.Text             (renderIO)
 import           Options.Applicative
 import           System.Exit
 import           System.IO
diff --git a/src/CLI/ParallelIndependence.hs b/src/CLI/ParallelIndependence.hs
index ec0ff4b9..a0cbe407 100644
--- a/src/CLI/ParallelIndependence.hs
+++ b/src/CLI/ParallelIndependence.hs
@@ -8,7 +8,6 @@ import           Abstract.Rewriting.DPO
 import           Analysis.ParallelIndependent
 import           Control.Monad                (unless, when)
 import           Data.Matrix                  hiding ((<|>))
-import           Data.Monoid                  ((<>))
 import           GlobalOptions
 import           Options.Applicative
 import           Rewriting.DPO.TypedGraphRule
diff --git a/src/CLI/Processes.hs b/src/CLI/Processes.hs
index f8644845..52028a73 100644
--- a/src/CLI/Processes.hs
+++ b/src/CLI/Processes.hs
@@ -7,7 +7,6 @@ module Processes
 
 import           Control.Monad
 import           Data.Maybe                                               (fromJust, isJust)
-import           Data.Monoid                                              ((<>))
 import           Data.Set                                                 (toList)
 import           GlobalOptions
 import           Options.Applicative
diff --git a/src/library/Base/Annotation.hs b/src/library/Base/Annotation.hs
index d8fd77e5..a2ab5923 100644
--- a/src/library/Base/Annotation.hs
+++ b/src/library/Base/Annotation.hs
@@ -26,8 +26,8 @@ module Base.Annotation
 
 import           Prelude                   hiding (drop)
 
-import           Data.Text.Prettyprint.Doc (Doc, Pretty (..), (<+>))
-import qualified Data.Text.Prettyprint.Doc as PP
+import           Prettyprinter             (Doc, Pretty (..), (<+>))
+import qualified Prettyprinter             as PP
 
 import           Base.Location
 
diff --git a/src/library/Base/Location.hs b/src/library/Base/Location.hs
index 5e6495de..11a1b650 100644
--- a/src/library/Base/Location.hs
+++ b/src/library/Base/Location.hs
@@ -6,8 +6,7 @@ module Base.Location
   , Position(..)
   ) where
 
-import           Data.Monoid
-import           Data.Text.Prettyprint.Doc (Pretty (..))
+import           Prettyprinter (Pretty (..))
 
 
 -- | Position within a text file.
diff --git a/src/library/Data/Graphs.hs b/src/library/Data/Graphs.hs
index d1b4b14e..412a1840 100644
--- a/src/library/Data/Graphs.hs
+++ b/src/library/Data/Graphs.hs
@@ -84,8 +84,8 @@ module Data.Graphs (
 import           Data.Function             (on)
 import           Data.List
 import           Data.Maybe                (fromMaybe)
-import           Data.Text.Prettyprint.Doc (Pretty (..), (<+>))
-import qualified Data.Text.Prettyprint.Doc as PP
+import           Prettyprinter             (Pretty (..), (<+>))
+import qualified Prettyprinter             as PP
 
 import           Base.Cardinality
 import           Base.Valid
diff --git a/src/library/GrLang/AST.hs b/src/library/GrLang/AST.hs
index f5b460ba..7cdf5488 100644
--- a/src/library/GrLang/AST.hs
+++ b/src/library/GrLang/AST.hs
@@ -9,8 +9,8 @@ module GrLang.AST
   ) where
 
 import           Data.Text                 (Text)
-import           Data.Text.Prettyprint.Doc (Doc, Pretty (..), (<+>), (<>))
-import qualified Data.Text.Prettyprint.Doc as PP
+import           Prettyprinter             (Doc, Pretty (..), (<+>))
+import qualified Prettyprinter             as PP
 
 import           Base.Annotation           (Annotated (..), Located)
 import qualified Base.Annotation           as Ann
diff --git a/src/library/GrLang/Compiler.hs b/src/library/GrLang/Compiler.hs
index 39f6d143..e3bab04f 100644
--- a/src/library/GrLang/Compiler.hs
+++ b/src/library/GrLang/Compiler.hs
@@ -9,7 +9,7 @@ module GrLang.Compiler
   , compileRule
   ) where
 
-import           Control.Monad.Except           (ExceptT (..), mapExceptT)
+import           Control.Monad.Except           (mapExceptT)
 import           Control.Monad.State
 import           Data.Either                    (lefts, rights)
 import           Data.Map                       (Map)
@@ -19,9 +19,9 @@ import qualified Data.Set                       as Set
 import           Data.Text                      (Text)
 import qualified Data.Text                      as Text
 import           Data.Text.Lazy.IO              as Text
-import           Data.Text.Prettyprint.Doc      (Pretty (..), (<>))
-import qualified Data.Text.Prettyprint.Doc      as PP
-import qualified Data.Text.Prettyprint.Doc.Util as PP
+import           Prettyprinter                  (Pretty (..))
+import qualified Prettyprinter                  as PP
+import qualified Prettyprinter.Util             as PP
 import           System.FilePath                (takeDirectory, (</>))
 import           System.IO.Error                (ioeGetErrorString, tryIOError)
 
diff --git a/src/library/GrLang/Monad.hs b/src/library/GrLang/Monad.hs
index 88c5a3ce..4b6ab014 100644
--- a/src/library/GrLang/Monad.hs
+++ b/src/library/GrLang/Monad.hs
@@ -33,13 +33,12 @@ import qualified Data.DList                     as DList
 import           Data.Functor.Identity
 import           Data.Map                       (Map)
 import qualified Data.Map                       as Map
-import           Data.Monoid
 import           Data.Set                       (Set)
 import qualified Data.Set                       as Set
 import           Data.Text                      (Text)
-import           Data.Text.Prettyprint.Doc      (Doc, Pretty (..), (<+>))
-import qualified Data.Text.Prettyprint.Doc      as PP
-import qualified Data.Text.Prettyprint.Doc.Util as PP
+import           Prettyprinter                  (Doc, Pretty (..), (<+>))
+import qualified Prettyprinter                  as PP
+import qualified Prettyprinter.Util             as PP
 
 import           Base.Annotation                (Annotated (..), Located, locatedDoc, locationOf)
 import qualified Base.Annotation                as Ann
diff --git a/src/library/GrLang/Parser.hs b/src/library/GrLang/Parser.hs
index b51585e4..a85f735b 100644
--- a/src/library/GrLang/Parser.hs
+++ b/src/library/GrLang/Parser.hs
@@ -7,8 +7,8 @@ import           Data.Functor              (($>))
 import           Data.Functor.Identity
 import           Data.Text                 (Text)
 import qualified Data.Text                 as Text
-import           Data.Text.Prettyprint.Doc (Pretty (..))
-import qualified Data.Text.Prettyprint.Doc as PP
+import           Prettyprinter             (Pretty (..))
+import qualified Prettyprinter             as PP
 import           Text.Parsec
 import           Text.Parsec.Error
 import qualified Text.Parsec.Token         as P
diff --git a/src/library/GrLang/Value.hs b/src/library/GrLang/Value.hs
index e28205b3..745224e1 100644
--- a/src/library/GrLang/Value.hs
+++ b/src/library/GrLang/Value.hs
@@ -49,12 +49,11 @@ import           Data.Function             (on)
 import qualified Data.List                 as List
 import qualified Data.Map                  as Map
 import           Data.Maybe                (fromMaybe, isJust, mapMaybe)
-import           Data.Monoid               ((<>))
 import           Data.Set                  (Set)
 import qualified Data.Set                  as Set
 import           Data.Text                 (Text)
 import qualified Data.Text                 as Text
-import           Data.Text.Prettyprint.Doc (Pretty (..))
+import           Prettyprinter             (Pretty (..))
 
 import           Abstract.Category
 import           Base.Annotation           (Annotated (..))
diff --git a/src/library/Image/Dot/TypedGraph.hs b/src/library/Image/Dot/TypedGraph.hs
index f2e1a6f8..a7cc3533 100644
--- a/src/library/Image/Dot/TypedGraph.hs
+++ b/src/library/Image/Dot/TypedGraph.hs
@@ -15,8 +15,8 @@ module Image.Dot.TypedGraph
   , sndOrderRule
   ) where
 
-import           Data.Text.Prettyprint.Doc    (Doc, Pretty (..), (<+>), (<>))
-import qualified Data.Text.Prettyprint.Doc    as PP
+import           Prettyprinter                (Doc, Pretty (..), (<+>))
+import qualified Prettyprinter                as PP
 
 import           Abstract.Category
 import           Category.TypedGraphRule
diff --git a/src/library/Logic/Ctl/Base.hs b/src/library/Logic/Ctl/Base.hs
index 8a6dffff..aa60bfcc 100755
--- a/src/library/Logic/Ctl/Base.hs
+++ b/src/library/Logic/Ctl/Base.hs
@@ -5,7 +5,7 @@ module Logic.Ctl.Base
   , StateQuantified(..)
   ) where
 
-import           Data.Text.Prettyprint.Doc
+import           Prettyprinter
 
 
 -- | CTL expressions
diff --git a/src/library/Logic/Model.hs b/src/library/Logic/Model.hs
index 6f7c132a..db6cee09 100644
--- a/src/library/Logic/Model.hs
+++ b/src/library/Logic/Model.hs
@@ -34,7 +34,7 @@ module Logic.Model
   ) where
 
 import           Data.Maybe
-
+import           Data.Kind (Type)
 
 -- | A Kripke structure is composed of a list of states and a list of
 -- transitions between such states. States are labeled with the atomic
@@ -132,7 +132,7 @@ precedes ts s1 s2 =
 -- | Type class for elements that have a numeric identifier and a list of associated values.
 class Element e where
   -- | Type of associated values.
-  type Payload e :: *
+  type Payload e :: Type
 
   -- | Obtain the numeric identifier of an element.
   elementId :: e -> Int
diff --git a/src/repl/GrLang.hs b/src/repl/GrLang.hs
index 37f3e393..a1359fb1 100644
--- a/src/repl/GrLang.hs
+++ b/src/repl/GrLang.hs
@@ -15,14 +15,13 @@ import qualified Data.ByteString                as BS
 import           Data.IORef
 import           Data.Map                       (Map)
 import qualified Data.Map                       as Map
-import           Data.Monoid
 import           Data.Proxy
 import           Data.Set                       (Set)
 import qualified Data.Set                       as Set
 import           Data.Text                      (Text)
 import qualified Data.Text                      as Text
 import qualified Data.Text.Encoding             as Text
-import           Data.Text.Prettyprint.Doc      (Pretty (..))
+import           Prettyprinter                  (Pretty (..))
 import           Foreign.Lua                    (FromLuaStack, Lua, ToHaskellFunction)
 import qualified Foreign.Lua                    as Lua
 import qualified Foreign.Lua.Util               as Lua
diff --git a/src/repl/Main.hs b/src/repl/Main.hs
index bd604d80..ff3bf4c9 100644
--- a/src/repl/Main.hs
+++ b/src/repl/Main.hs
@@ -5,7 +5,6 @@ import           Control.Monad
 import           Control.Monad.Trans
 import qualified Data.ByteString          as ByteString
 import qualified Data.ByteString          as BS
-import           Data.Monoid              ((<>))
 import           Foreign.Lua              (Lua, runLua)
 import qualified Foreign.Lua              as Lua
 import           Options.Applicative
diff --git a/tests/GrLang/CompilerSpec.hs b/tests/GrLang/CompilerSpec.hs
index fe8a5089..5b1b41b0 100644
--- a/tests/GrLang/CompilerSpec.hs
+++ b/tests/GrLang/CompilerSpec.hs
@@ -13,7 +13,7 @@ import           Data.Map                       (Map)
 import qualified Data.Map                       as Map
 import           Data.String
 import           Data.Text                      (Text)
-import           Data.Text.Prettyprint.Doc      (Pretty (..))
+import           Prettyprinter                  (Pretty (..))
 import           System.FilePath
 import           Test.Hspec
 import           Test.HUnit
diff --git a/tests/GrLang/ParserSpec.hs b/tests/GrLang/ParserSpec.hs
index 97588218..7bf79ad8 100644
--- a/tests/GrLang/ParserSpec.hs
+++ b/tests/GrLang/ParserSpec.hs
@@ -7,7 +7,7 @@ import           Control.Monad.Except      (runExceptT)
 import           Data.Functor.Identity
 import           Data.String               (IsString (..))
 import           Data.Text                 ()
-import           Data.Text.Prettyprint.Doc (Pretty (..), vsep)
+import           Prettyprinter             (Pretty (..), vsep)
 import           Test.Hspec
 import           Test.Hspec.QuickCheck     (modifyMaxSize, modifyMaxSuccess)
 import           Test.QuickCheck
diff --git a/tests/Logic/Ctl/ParserSpec.hs b/tests/Logic/Ctl/ParserSpec.hs
index 8de7569e..ea576dfd 100644
--- a/tests/Logic/Ctl/ParserSpec.hs
+++ b/tests/Logic/Ctl/ParserSpec.hs
@@ -4,7 +4,7 @@ module Logic.Ctl.ParserSpec where
 import           Test.Hspec
 import qualified Test.HUnit              as HUnit
 import           Test.QuickCheck
-import           Data.Text.Prettyprint.Doc (Pretty(..))
+import           Prettyprinter           (Pretty(..))
 
 import           Logic.Ctl
 import           Logic.Ctl.TestUtils     ()

From f8d884ced3aeb70a409aaa4211858596e79d92be Mon Sep 17 00:00:00 2001
From: "Jonas S. Bezerra" <jonassantosbezerra@outlook.com>
Date: Wed, 9 Nov 2022 01:37:48 +0000
Subject: [PATCH 10/12] resolve import and unused binding warnings

---
 src/library/Category/TypedGraph/Finitary.hs |  1 -
 src/library/Data/TypedGraph.hs              |  4 ++--
 src/library/Rewriting/DPO/TypedGraph.hs     | 11 +++++------
 src/repl/GrLang.hs                          |  1 -
 4 files changed, 7 insertions(+), 10 deletions(-)

diff --git a/src/library/Category/TypedGraph/Finitary.hs b/src/library/Category/TypedGraph/Finitary.hs
index 4cd906f2..57615f61 100644
--- a/src/library/Category/TypedGraph/Finitary.hs
+++ b/src/library/Category/TypedGraph/Finitary.hs
@@ -8,7 +8,6 @@ import           Abstract.Category
 import           Abstract.Category.Finitary
 import           Category.TypedGraph.Category                    
 import           Category.Graph                     ()
-import           Data.Graphs                        (Node(..), Edge(..))
 import qualified Data.Graphs                        as Graph
 import qualified Data.Graphs.Morphism               as Untyped
 import           Data.TypedGraph
diff --git a/src/library/Data/TypedGraph.hs b/src/library/Data/TypedGraph.hs
index 80220b7e..d4da2544 100644
--- a/src/library/Data/TypedGraph.hs
+++ b/src/library/Data/TypedGraph.hs
@@ -298,7 +298,7 @@ removeNodeAndIncidentEdges :: NodeId -> TypedGraph n e -> TypedGraph n e
 removeNodeAndIncidentEdges nodeId g@(GraphMorphism dom cod nodeMap edgeMap) =
   case lookupNodeInContext nodeId g of
     Nothing -> g
-    Just (_,_,nodeCtx) ->
+    Just _ ->
       let
         dom' = Graph.removeNodeAndIncidentEdges nodeId dom
         notRemoved e = isJust (Graph.lookupEdge e dom')
@@ -308,5 +308,5 @@ removeNodeAndIncidentEdges nodeId g@(GraphMorphism dom cod nodeMap edgeMap) =
 
 -- | Remove the given edge from the graph. /O(e)/.
 removeEdge :: EdgeId -> TypedGraph n e -> TypedGraph n e
-removeEdge e g@(GraphMorphism dom cod nodeMap edgeMap) =
+removeEdge e (GraphMorphism dom cod nodeMap edgeMap) =
   GraphMorphism (Graph.removeEdge e dom) cod nodeMap (Relation.removeFromDomain e edgeMap)
diff --git a/src/library/Rewriting/DPO/TypedGraph.hs b/src/library/Rewriting/DPO/TypedGraph.hs
index 03f6f8f6..212009ae 100644
--- a/src/library/Rewriting/DPO/TypedGraph.hs
+++ b/src/library/Rewriting/DPO/TypedGraph.hs
@@ -26,12 +26,11 @@ import           Abstract.Category
 import           Abstract.Rewriting.DPO             as DPO
 import           Category.TypedGraph.Category       (toMorphismType, MorphismType(..))
 import           Category.TypedGraph                
-import           Category.TypedGraph.Adhesive       (isDeleted)
-import  Data.Graphs                        (Graph)
-import qualified Data.Graphs                        as G
-import qualified Data.Graphs.Morphism               as GM
-import           Data.TypedGraph                    as GM
-import           Data.TypedGraph.Morphism           as TGM
+import           Category.TypedGraph.Adhesive            (isDeleted)
+import           Data.Graphs                             (Graph)
+import qualified Data.Graphs                             as G
+import           Data.TypedGraph                         as GM
+import           Data.TypedGraph.Morphism                as TGM
 import           Data.TypedGraph.Partition               (generateGraphPartitions)
 import           Data.TypedGraph.Partition.ToVerigraph   (mountTypedGraphMorphisms)
 import           Data.TypedGraph.Partition.FromVerigraph (createSatisfyingNacsDisjointUnion)
diff --git a/src/repl/GrLang.hs b/src/repl/GrLang.hs
index a1359fb1..c0349dbe 100644
--- a/src/repl/GrLang.hs
+++ b/src/repl/GrLang.hs
@@ -9,7 +9,6 @@ import           Control.Monad
 import           Control.Monad.Except           (ExceptT (..), runExceptT)
 import qualified Control.Monad.Except           as ExceptT
 import           Control.Monad.Reader
-import           Control.Monad.Trans            (lift)
 import           Data.Array.IO
 import qualified Data.ByteString                as BS
 import           Data.IORef

From 391bc281ee8a1540a13bc5be7f420a5e80d325b1 Mon Sep 17 00:00:00 2001
From: "Jonas S. Bezerra" <jonassantosbezerra@outlook.com>
Date: Wed, 9 Nov 2022 01:49:20 +0000
Subject: [PATCH 11/12] identation

---
 src/CLI/ApplySndOrderRules.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/CLI/ApplySndOrderRules.hs b/src/CLI/ApplySndOrderRules.hs
index e79eeb91..a3619719 100644
--- a/src/CLI/ApplySndOrderRules.hs
+++ b/src/CLI/ApplySndOrderRules.hs
@@ -5,7 +5,7 @@ module ApplySndOrderRules
   ) where
 
 import           Control.Monad                           (when)
-import           Prettyprinter                          (Pretty (..))
+import           Prettyprinter                           (Pretty (..))
 import           Options.Applicative
 import           System.IO                               (hPrint, stderr)
 

From 62df9342254f3da718ab845e454102712d702246 Mon Sep 17 00:00:00 2001
From: "Jonas S. Bezerra" <jonassantosbezerra@outlook.com>
Date: Wed, 9 Nov 2022 14:16:54 +0000
Subject: [PATCH 12/12] upper bound constraints

---
 verigraph.cabal | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/verigraph.cabal b/verigraph.cabal
index f9c30abb..6db7091f 100644
--- a/verigraph.cabal
+++ b/verigraph.cabal
@@ -18,18 +18,18 @@ library
   hs-source-dirs:      src/library/
   ghc-options:         -O -Wall -fno-warn-name-shadowing -fno-warn-unused-do-bind -fno-warn-orphans
   other-extensions:    TypeFamilies, MultiParamTypeClasses, FlexibleContexts
-  build-depends:       base >= 4.15,
-                       containers >= 0.6,
+  build-depends:       base >= 4.15 && <4.16,
+                       containers >= 0.6 && <0.7,
                        directory >= 1.3 && <2,
                        filepath >= 1.4 && <2,
                        hxt >=9.3.1.15 && <9.4,
                        mtl >=2.2 && <2.3,
                        parallel >= 3.2,
                        parsec >=3.1 && <3.2,
-                       prettyprinter >=1.7,
-                       QuickCheck == 2.14.2,
+                       prettyprinter >=1.7 && <1.8,
+                       QuickCheck >= 2.14 && <2.15,
                        semigroups >= 0.18,
-                       set-monad >= 0.3,
+                       set-monad >= 0.3 && <0.4,
                        split >= 0.2,
                        text >=1.2 && <1.3
   exposed-modules:     Abstract.Category.Adhesive
@@ -136,7 +136,7 @@ executable verigraph
                        filepath,
                        hxt,
                        matrix >= 0.3,
-                       optparse-applicative>=0.16,
+                       optparse-applicative>=0.16 && <0.17,
                        parallel >= 3.2,
                        prettyprinter,
                        split >= 0.2
@@ -157,7 +157,7 @@ executable verigraph-mcheck
   build-depends:       base, verigraph,
                        containers,
                        hxt,
-                       optparse-applicative>=0.16,
+                       optparse-applicative>=0.16 && <0.17,
                        prettyprinter
   other-modules:       GlobalOptions
 
@@ -174,7 +174,7 @@ executable verigraph-repl
                        haskeline >=0.7 && <1.0,
                        hslua >=0.9.4 && <1.0,
                        mtl,
-                       optparse-applicative >= 0.16,
+                       optparse-applicative >= 0.16 && <0.17,
                        prettyprinter,
                        text
   autogen-modules:     Paths_verigraph
@@ -191,7 +191,7 @@ test-suite HSpecTests
   build-depends:       base, verigraph,
                        call-stack,
                        containers,
-                       combinat >= 0.2.10,
+                       combinat >= 0.2 && <0.3,
                        directory,
                        deepseq,
                        filepath,