{-# LANGUAGE FlexibleInstances #-}
{- |
Module      :  ./CASL/Amalgamability.hs
Description :  Amalgamability analysis for CASL.
Copyright   :  (c) Maciek Makowski, Warsaw University 2004-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Amalgamability analysis for CASL.

  Follows the algorithm outlined in MFCS 2001 (LNCS 2136, pp. 451-463,
  Springer 2001) paper.
-}

module CASL.Amalgamability
  ( CASLDiag
  , ensuresAmalgamability
  ) where


import CASL.AS_Basic_CASL
import CASL.Morphism
import CASL.Sign

import Common.Amalgamate
import Common.Doc
import Common.DocUtils
import Common.Id
import Common.Result

import Data.Graph.Inductive.Graph
import Data.List
import Data.Maybe

import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Graph as Tree
import qualified Common.Lib.Rel as Rel

import qualified Data.Map as Map
import qualified Data.Set as Set

-- Miscellaneous types
type CASLDiag = Tree.Gr CASLSign (Int, CASLMor)
type DiagSort = (Node, SORT)
type DiagOp = (Node, (Id, OpType))
type DiagPred = (Node, (Id, PredType))
type DiagEmb = (Node, SORT, SORT)
type DiagEmbWord = [DiagEmb]
-- | equivalence classes are represented as lists of elements
type EquivClass a = [a]
-- | equivalence relations are represented as lists of equivalence classes
type EquivRel a = [EquivClass a]
-- | or, sometimes, as lists of pairs (element, equiv. class tag)
type EquivRelTagged a b = [(a, b)]

-- Pretty instance (for diagnostic output)
instance (Pretty a, Pretty b) => Pretty (Tree.Gr a (Int, b)) where
    pretty :: Gr a (Int, b) -> Doc
pretty diag :: Gr a (Int, b)
diag =
        String -> Doc
text "nodes:"
        Doc -> Doc -> Doc
<+> [LNode a] -> Doc
forall a. Pretty a => a -> Doc
pretty (Gr a (Int, b) -> [LNode a]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr a (Int, b)
diag)
        Doc -> Doc -> Doc
$+$ String -> Doc
text "edges:"
        Doc -> Doc -> Doc
<+> [b] -> Doc
forall a. Pretty a => a -> Doc
pretty (((Int, Int, (Int, b)) -> b) -> [(Int, Int, (Int, b))] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, _, label :: (Int, b)
label) -> (Int, b) -> b
forall a b. (a, b) -> b
snd (Int, b)
label) ([(Int, Int, (Int, b))] -> [b]) -> [(Int, Int, (Int, b))] -> [b]
forall a b. (a -> b) -> a -> b
$ Gr a (Int, b) -> [(Int, Int, (Int, b))]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges Gr a (Int, b)
diag)

-- | find in Map
findInMap :: Ord k => k -> Map.Map k a -> a
findInMap :: k -> Map k a -> a
findInMap k :: k
k = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe (String -> a
forall a. HasCallStack => String -> a
error "Amalgamability.findInMap") (Maybe a -> a) -> (Map k a -> Maybe a) -> Map k a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                k -> Map k a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k

{- | Compute the Sorts set -- a disjoint union of all the sorts
in the diagram. -}
sorts :: CASLDiag        -- ^ the diagram to get the sorts from
      -> [DiagSort]
sorts :: CASLDiag -> [DiagSort]
sorts diag :: CASLDiag
diag =
    let mkNodeSortPair :: a -> b -> (a, b)
mkNodeSortPair n :: a
n srt :: b
srt = (a
n, b
srt)
        appendSorts :: [(a, SORT)] -> (a, Sign f e) -> [(a, SORT)]
appendSorts sl :: [(a, SORT)]
sl (n :: a
n, sig :: Sign f e
sig) =
            [(a, SORT)]
sl [(a, SORT)] -> [(a, SORT)] -> [(a, SORT)]
forall a. [a] -> [a] -> [a]
++ (SORT -> (a, SORT)) -> [SORT] -> [(a, SORT)]
forall a b. (a -> b) -> [a] -> [b]
map (a -> SORT -> (a, SORT)
forall a b. a -> b -> (a, b)
mkNodeSortPair a
n) (Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> [SORT]) -> Set SORT -> [SORT]
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
sig)
    in ([DiagSort] -> (Int, Sign () ()) -> [DiagSort])
-> [DiagSort] -> [(Int, Sign () ())] -> [DiagSort]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [DiagSort] -> (Int, Sign () ()) -> [DiagSort]
forall a f e. [(a, SORT)] -> (a, Sign f e) -> [(a, SORT)]
appendSorts [] (CASLDiag -> [(Int, Sign () ())]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes CASLDiag
diag)


{- | Compute the Ops set -- a disjoint union of all the operation symbols
in the diagram. -}
ops :: CASLDiag        -- ^ the diagram to get the ops from
    -> [DiagOp]
ops :: CASLDiag -> [DiagOp]
ops diag :: CASLDiag
diag =
    let mkNodeOp :: a -> a -> b -> [(a, (a, b))] -> [(a, (a, b))]
mkNodeOp n :: a
n opId :: a
opId opType :: b
opType ol :: [(a, (a, b))]
ol = [(a, (a, b))]
ol [(a, (a, b))] -> [(a, (a, b))] -> [(a, (a, b))]
forall a. [a] -> [a] -> [a]
++ [(a
n, (a
opId, b
opType))]
        mkNodeOps :: a -> a -> Set b -> [(a, (a, b))] -> [(a, (a, b))]
mkNodeOps n :: a
n opId :: a
opId opTypes :: Set b
opTypes ol :: [(a, (a, b))]
ol =
            [(a, (a, b))]
ol [(a, (a, b))] -> [(a, (a, b))] -> [(a, (a, b))]
forall a. [a] -> [a] -> [a]
++ (b -> [(a, (a, b))] -> [(a, (a, b))])
-> [(a, (a, b))] -> Set b -> [(a, (a, b))]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (a -> a -> b -> [(a, (a, b))] -> [(a, (a, b))]
forall a a b. a -> a -> b -> [(a, (a, b))] -> [(a, (a, b))]
mkNodeOp a
n a
opId) [] Set b
opTypes
        appendOps :: [(a, (SORT, OpType))] -> (a, Sign f e) -> [(a, (SORT, OpType))]
appendOps ol :: [(a, (SORT, OpType))]
ol (n :: a
n, Sign { opMap :: forall f e. Sign f e -> OpMap
opMap = OpMap
m }) =
            [(a, (SORT, OpType))]
ol [(a, (SORT, OpType))]
-> [(a, (SORT, OpType))] -> [(a, (SORT, OpType))]
forall a. [a] -> [a] -> [a]
++ (SORT
 -> Set OpType -> [(a, (SORT, OpType))] -> [(a, (SORT, OpType))])
-> [(a, (SORT, OpType))]
-> Map SORT (Set OpType)
-> [(a, (SORT, OpType))]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (a
-> SORT
-> Set OpType
-> [(a, (SORT, OpType))]
-> [(a, (SORT, OpType))]
forall a a b. a -> a -> Set b -> [(a, (a, b))] -> [(a, (a, b))]
mkNodeOps a
n) [] (OpMap -> Map SORT (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap OpMap
m)
    in ([DiagOp] -> (Int, Sign () ()) -> [DiagOp])
-> [DiagOp] -> [(Int, Sign () ())] -> [DiagOp]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [DiagOp] -> (Int, Sign () ()) -> [DiagOp]
forall a f e.
[(a, (SORT, OpType))] -> (a, Sign f e) -> [(a, (SORT, OpType))]
appendOps [] (CASLDiag -> [(Int, Sign () ())]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes CASLDiag
diag)


{- | Compute the Preds set -- a disjoint union of all the predicate symbols
in the diagram. -}
preds :: CASLDiag        -- ^ the diagram to get the preds from
      -> [DiagPred]
preds :: CASLDiag -> [DiagPred]
preds diag :: CASLDiag
diag =
    let mkNodePred :: a -> a -> b -> [(a, (a, b))] -> [(a, (a, b))]
mkNodePred n :: a
n predId :: a
predId predType :: b
predType pl :: [(a, (a, b))]
pl = [(a, (a, b))]
pl [(a, (a, b))] -> [(a, (a, b))] -> [(a, (a, b))]
forall a. [a] -> [a] -> [a]
++ [(a
n, (a
predId, b
predType))]
        mkNodePreds :: a -> a -> Set b -> [(a, (a, b))] -> [(a, (a, b))]
mkNodePreds n :: a
n predId :: a
predId predTypes :: Set b
predTypes pl :: [(a, (a, b))]
pl =
            [(a, (a, b))]
pl [(a, (a, b))] -> [(a, (a, b))] -> [(a, (a, b))]
forall a. [a] -> [a] -> [a]
++ (b -> [(a, (a, b))] -> [(a, (a, b))])
-> [(a, (a, b))] -> Set b -> [(a, (a, b))]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (a -> a -> b -> [(a, (a, b))] -> [(a, (a, b))]
forall a a b. a -> a -> b -> [(a, (a, b))] -> [(a, (a, b))]
mkNodePred a
n a
predId) [] Set b
predTypes
        appendPreds :: [(a, (SORT, PredType))] -> (a, Sign f e) -> [(a, (SORT, PredType))]
appendPreds pl :: [(a, (SORT, PredType))]
pl (n :: a
n, Sign { predMap :: forall f e. Sign f e -> PredMap
predMap = PredMap
m }) =
            [(a, (SORT, PredType))]
pl [(a, (SORT, PredType))]
-> [(a, (SORT, PredType))] -> [(a, (SORT, PredType))]
forall a. [a] -> [a] -> [a]
++ (SORT
 -> Set PredType
 -> [(a, (SORT, PredType))]
 -> [(a, (SORT, PredType))])
-> [(a, (SORT, PredType))]
-> Map SORT (Set PredType)
-> [(a, (SORT, PredType))]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (a
-> SORT
-> Set PredType
-> [(a, (SORT, PredType))]
-> [(a, (SORT, PredType))]
forall a a b. a -> a -> Set b -> [(a, (a, b))] -> [(a, (a, b))]
mkNodePreds a
n) [] (PredMap -> Map SORT (Set PredType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap PredMap
m)
    in ([DiagPred] -> (Int, Sign () ()) -> [DiagPred])
-> [DiagPred] -> [(Int, Sign () ())] -> [DiagPred]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [DiagPred] -> (Int, Sign () ()) -> [DiagPred]
forall a f e.
[(a, (SORT, PredType))] -> (a, Sign f e) -> [(a, (SORT, PredType))]
appendPreds [] (CASLDiag -> [(Int, Sign () ())]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes CASLDiag
diag)


{- | Convert the relation representation from list of pairs
(val, equiv. class tag) to a list of equivalence classes. -}
taggedValsToEquivClasses :: Ord b
                         => EquivRelTagged a b -- ^ a list of (value,tag) pairs
                         -> EquivRel a
taggedValsToEquivClasses :: EquivRelTagged a b -> EquivRel a
taggedValsToEquivClasses [] = []
taggedValsToEquivClasses rel' :: EquivRelTagged a b
rel' =
    let {- prepMap: create a map with all the equivalence class tags mapped to
        empty lists -}
        prepMap :: [(a, b)] -> Map b [a]
prepMap =
            (Map b [a] -> (a, b) -> Map b [a])
-> Map b [a] -> [(a, b)] -> Map b [a]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m :: Map b [a]
m k :: (a, b)
k -> b -> [a] -> Map b [a] -> Map b [a]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ((a, b) -> b
forall a b. (a, b) -> b
snd (a, b)
k) [] Map b [a]
m) Map b [a]
forall k a. Map k a
Map.empty
        -- conv: perform actual conversion
        convert :: [(a, b)] -> Map b [a] -> [[a]]
convert [] m :: Map b [a]
m = ((b, [a]) -> [a]) -> [(b, [a])] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map (b, [a]) -> [a]
forall a b. (a, b) -> b
snd (Map b [a] -> [(b, [a])]
forall k a. Map k a -> [(k, a)]
Map.toList Map b [a]
m)
        convert ((ds :: a
ds, ect :: b
ect) : dsps :: [(a, b)]
dsps) m :: Map b [a]
m =
            let m' :: Map b [a]
m' = ([a] -> Maybe [a]) -> b -> Map b [a] -> Map b [a]
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update (\ ec :: [a]
ec -> [a] -> Maybe [a]
forall a. a -> Maybe a
Just (a
ds a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ec)) b
ect Map b [a]
m
            in [(a, b)] -> Map b [a] -> [[a]]
convert [(a, b)]
dsps Map b [a]
m'
    in EquivRelTagged a b -> Map b [a] -> EquivRel a
forall b a. Ord b => [(a, b)] -> Map b [a] -> [[a]]
convert EquivRelTagged a b
rel' (EquivRelTagged a b -> Map b [a]
forall a a. [(a, b)] -> Map b [a]
prepMap EquivRelTagged a b
rel')


{- | Convert the relation representation from list of
equivalence classes to list of (value, tag) pairs. -}
equivClassesToTaggedVals :: Ord a
                         => EquivRel a
                         -> EquivRelTagged a a
equivClassesToTaggedVals :: EquivRel a -> EquivRelTagged a a
equivClassesToTaggedVals rel :: EquivRel a
rel =
    let eqClToList :: [a] -> [(a, a)]
eqClToList [] = []
        eqClToList eqcl :: [a]
eqcl@(ft :: a
ft : _) = (a -> (a, a)) -> [a] -> [(a, a)]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: a
x -> (a
x, a
ft)) [a]
eqcl
    in (EquivRelTagged a a -> [a] -> EquivRelTagged a a)
-> EquivRelTagged a a -> EquivRel a -> EquivRelTagged a a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ vtl :: EquivRelTagged a a
vtl eqcl :: [a]
eqcl -> EquivRelTagged a a
vtl EquivRelTagged a a -> EquivRelTagged a a -> EquivRelTagged a a
forall a. [a] -> [a] -> [a]
++ [a] -> EquivRelTagged a a
forall a. [a] -> [(a, a)]
eqClToList [a]
eqcl) [] EquivRel a
rel

{- the old, n^3 version of mergeEquivClassesBy:
-- | Merge the equivalence classes for elements fulfilling given condition.
mergeEquivClassesBy :: Eq b
                    => (a -> a -> Bool)
                   -- ^ the condition stating when two elements are in relation
                    -> EquivRelTagged a b -- ^ the input relation
                    -> EquivRelTagged a b
-- ^ returns the input relation with equivalence classes merged according to
-- the condition.
mergeEquivClassesBy cond rel =
 -- Starting with the first element in the list an element (elem, tag) is taken
    -- and cond is subsequently applied to it and all the elements
    -- following it in the list. Whenever an element (elem', tag')
    -- that is in relation with the chosen one is found, all the equivalence
    -- class tags in the list that are equal to tag' are updated to tag.

    let merge rel pos | pos >= length rel = rel
        merge rel pos | otherwise =
            let mergeWith cmpl _ [] = cmpl
                mergeWith cmpl vtp@(elem, ec) toCmpl@((elem', ec') : _) =
                    let (cmpl', toCmpl') = if ec /= ec' && (cond elem elem')
                                             then let upd (elem'', ec'') =
                                                        if ec'' == ec'
                                                           then (elem'', ec)
                                                           else (elem'', ec'')
                                                  in (map upd cmpl,
                                                      map upd toCmpl)
                                             else (cmpl, toCmpl)
                    in mergeWith (cmpl' ++ [head toCmpl']) vtp (tail toCmpl')
                (cmpl, (vtp : vtps)) = splitAt pos rel
                rel' = mergeWith (cmpl ++ [vtp]) vtp vtps
            in merge rel' (pos + 1)
    in merge rel 0
-}

data TagEqcl a b = Eqcl [a] | TagRef b
                   deriving Int -> TagEqcl a b -> ShowS
[TagEqcl a b] -> ShowS
TagEqcl a b -> String
(Int -> TagEqcl a b -> ShowS)
-> (TagEqcl a b -> String)
-> ([TagEqcl a b] -> ShowS)
-> Show (TagEqcl a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> TagEqcl a b -> ShowS
forall a b. (Show a, Show b) => [TagEqcl a b] -> ShowS
forall a b. (Show a, Show b) => TagEqcl a b -> String
showList :: [TagEqcl a b] -> ShowS
$cshowList :: forall a b. (Show a, Show b) => [TagEqcl a b] -> ShowS
show :: TagEqcl a b -> String
$cshow :: forall a b. (Show a, Show b) => TagEqcl a b -> String
showsPrec :: Int -> TagEqcl a b -> ShowS
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> TagEqcl a b -> ShowS
Show

-- | Merge the equivalence classes for elements fulfilling given condition.
mergeEquivClassesBy :: (Ord b)
                    => (a -> a -> Bool)
                  -- ^ the condition stating when two elements are in relation
                    -> EquivRelTagged a b -- ^ the input relation
                    -> EquivRelTagged a b
{- ^ returns the input relation with equivalence classes merged according to
the condition. -}
mergeEquivClassesBy :: (a -> a -> Bool) -> EquivRelTagged a b -> EquivRelTagged a b
mergeEquivClassesBy cond :: a -> a -> Bool
cond rel :: EquivRelTagged a b
rel =
    {- Starting with the first element in the list an element (elem,
    tag) is taken and cond is subsequently applied to it and all the
    elements following it in the list. Whenever an element (elem',
    tag') that is in relation with the chosen one is found, the
    equivalence classes in tagMap for tag and tag' are merged: tag in
    tagMap points to the merged equivalence class and tag' in tagMap
    is a reference to tag. -}
    let -- create the initial map mapping tags to equivalence classes
        initialTagMap :: Map b (TagEqcl a b)
initialTagMap =
            let insEl :: Map k [a] -> (a, k) -> Map k [a]
insEl tagMap :: Map k [a]
tagMap (val :: a
val, tag :: k
tag) =
                    ([a] -> [a] -> [a]) -> k -> [a] -> Map k [a] -> Map k [a]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++) k
tag [a
val] Map k [a]
tagMap
            in ([a] -> TagEqcl a b) -> Map b [a] -> Map b (TagEqcl a b)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map [a] -> TagEqcl a b
forall a b. [a] -> TagEqcl a b
Eqcl (Map b [a] -> Map b (TagEqcl a b))
-> Map b [a] -> Map b (TagEqcl a b)
forall a b. (a -> b) -> a -> b
$ (Map b [a] -> (a, b) -> Map b [a])
-> Map b [a] -> EquivRelTagged a b -> Map b [a]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map b [a] -> (a, b) -> Map b [a]
forall k a. Ord k => Map k [a] -> (a, k) -> Map k [a]
insEl Map b [a]
forall k a. Map k a
Map.empty EquivRelTagged a b
rel

        -- merge equivalence classes tagged with t1 and t2
        mergeInMap :: Map a (TagEqcl a a) -> a -> a -> Map a (TagEqcl a a)
mergeInMap inTagMap :: Map a (TagEqcl a a)
inTagMap t1 :: a
t1 t2 :: a
t2 =
            let {- find the tag and equivalence class that corresponds
                to the given tag performing path compression while
                traversing the referneces. -}
                findEqcl :: b -> Map b (TagEqcl a b) -> (b, [a], Map b (TagEqcl a b))
findEqcl t :: b
t tagMap :: Map b (TagEqcl a b)
tagMap =
                    case b -> Map b (TagEqcl a b) -> TagEqcl a b
forall k a. Ord k => k -> Map k a -> a
findInMap b
t Map b (TagEqcl a b)
tagMap of
                    Eqcl eqcl :: [a]
eqcl -> (b
t, [a]
eqcl, Map b (TagEqcl a b)
tagMap)
                    TagRef t' :: b
t' -> let
                        (rt :: b
rt, eqcl :: [a]
eqcl, tagMap' :: Map b (TagEqcl a b)
tagMap') = b -> Map b (TagEqcl a b) -> (b, [a], Map b (TagEqcl a b))
findEqcl b
t' Map b (TagEqcl a b)
tagMap
                        tagMap'' :: Map b (TagEqcl a b)
tagMap'' = if b
rt b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
t' then Map b (TagEqcl a b)
tagMap' else
                              (TagEqcl a b -> Maybe (TagEqcl a b))
-> b -> Map b (TagEqcl a b) -> Map b (TagEqcl a b)
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update (\ _ -> TagEqcl a b -> Maybe (TagEqcl a b)
forall a. a -> Maybe a
Just (b -> TagEqcl a b
forall a b. b -> TagEqcl a b
TagRef b
rt)) b
t Map b (TagEqcl a b)
tagMap'
                        in (b
rt, [a]
eqcl, Map b (TagEqcl a b)
tagMap'')
                (rt1 :: a
rt1, eqcl1 :: [a]
eqcl1, tagMap1 :: Map a (TagEqcl a a)
tagMap1) = a -> Map a (TagEqcl a a) -> (a, [a], Map a (TagEqcl a a))
forall b a.
Ord b =>
b -> Map b (TagEqcl a b) -> (b, [a], Map b (TagEqcl a b))
findEqcl a
t1 Map a (TagEqcl a a)
inTagMap
                (rt2 :: a
rt2, eqcl2 :: [a]
eqcl2, tagMap2 :: Map a (TagEqcl a a)
tagMap2) = a -> Map a (TagEqcl a a) -> (a, [a], Map a (TagEqcl a a))
forall b a.
Ord b =>
b -> Map b (TagEqcl a b) -> (b, [a], Map b (TagEqcl a b))
findEqcl a
t2 Map a (TagEqcl a a)
tagMap1
            in if a
rt1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
rt2 then Map a (TagEqcl a a)
tagMap2
                  else let (nrt1 :: a
nrt1, nrt2 :: a
nrt2) = if a
rt1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
rt2 then (a
rt2, a
rt1)
                                          else (a
rt1, a
rt2)
                           tagMap3 :: Map a (TagEqcl a a)
tagMap3 = (TagEqcl a a -> Maybe (TagEqcl a a))
-> a -> Map a (TagEqcl a a) -> Map a (TagEqcl a a)
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update
                             (\ _ -> TagEqcl a a -> Maybe (TagEqcl a a)
forall a. a -> Maybe a
Just ([a] -> TagEqcl a a
forall a b. [a] -> TagEqcl a b
Eqcl ([a]
eqcl1 [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
eqcl2))) a
nrt1 Map a (TagEqcl a a)
tagMap2
                           tagMap4 :: Map a (TagEqcl a a)
tagMap4 = (TagEqcl a a -> Maybe (TagEqcl a a))
-> a -> Map a (TagEqcl a a) -> Map a (TagEqcl a a)
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update
                             (\ _ -> TagEqcl a a -> Maybe (TagEqcl a a)
forall a. a -> Maybe a
Just (a -> TagEqcl a a
forall a b. b -> TagEqcl a b
TagRef a
nrt1)) a
nrt2 Map a (TagEqcl a a)
tagMap3
                       in Map a (TagEqcl a a)
tagMap4

        {- iterate through the relation merging equivalence classes of
        appropriate elements -}
        merge :: Map b (TagEqcl a b) -> [(a, b)] -> Int -> Map b (TagEqcl a b)
merge tagMap' :: Map b (TagEqcl a b)
tagMap' rel' :: [(a, b)]
rel' pos :: Int
pos | Int
pos Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [(a, b)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(a, b)]
rel' = Map b (TagEqcl a b)
tagMap'
        merge tagMap' :: Map b (TagEqcl a b)
tagMap' rel' :: [(a, b)]
rel' pos :: Int
pos =
            let mergeWith :: Map b (TagEqcl a b) -> (a, b) -> [(a, b)] -> Map b (TagEqcl a b)
mergeWith tagMap :: Map b (TagEqcl a b)
tagMap _ [] = Map b (TagEqcl a b)
tagMap
                mergeWith tagMap :: Map b (TagEqcl a b)
tagMap vtp :: (a, b)
vtp@(elem1 :: a
elem1, ec :: b
ec) toCmpl :: [(a, b)]
toCmpl@((elem2 :: a
elem2, ec' :: b
ec') : _) =
                    let tagMap1 :: Map b (TagEqcl a b)
tagMap1 = if b
ec b -> b -> Bool
forall a. Eq a => a -> a -> Bool
/= b
ec' Bool -> Bool -> Bool
&& a -> a -> Bool
cond a
elem1 a
elem2
                                     then Map b (TagEqcl a b) -> b -> b -> Map b (TagEqcl a b)
forall a a.
Ord a =>
Map a (TagEqcl a a) -> a -> a -> Map a (TagEqcl a a)
mergeInMap Map b (TagEqcl a b)
tagMap b
ec b
ec'
                                     else Map b (TagEqcl a b)
tagMap
                    in Map b (TagEqcl a b) -> (a, b) -> [(a, b)] -> Map b (TagEqcl a b)
mergeWith Map b (TagEqcl a b)
tagMap1 (a, b)
vtp ([(a, b)] -> [(a, b)]
forall a. [a] -> [a]
tail [(a, b)]
toCmpl)
                (_, vtp' :: (a, b)
vtp' : vtps :: [(a, b)]
vtps) = Int -> [(a, b)] -> ([(a, b)], [(a, b)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
pos [(a, b)]
rel'
                tagMap'' :: Map b (TagEqcl a b)
tagMap'' = Map b (TagEqcl a b) -> (a, b) -> [(a, b)] -> Map b (TagEqcl a b)
forall b a.
Ord b =>
Map b (TagEqcl a b) -> (a, b) -> [(a, b)] -> Map b (TagEqcl a b)
mergeWith Map b (TagEqcl a b)
tagMap' (a, b)
vtp' [(a, b)]
vtps
            in Map b (TagEqcl a b) -> [(a, b)] -> Int -> Map b (TagEqcl a b)
merge Map b (TagEqcl a b)
tagMap'' [(a, b)]
rel' (Int
pos Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)

        -- append given equivalence class to the list of (value, tag) pairs
        tagMapToRel :: [(a, b)] -> (b, TagEqcl a b) -> [(a, b)]
tagMapToRel rel' :: [(a, b)]
rel' (_, TagRef _) = [(a, b)]
rel'
        tagMapToRel rel' :: [(a, b)]
rel' (tag :: b
tag, Eqcl eqcl :: [a]
eqcl) =
            ([(a, b)] -> a -> [(a, b)]) -> [(a, b)] -> [a] -> [(a, b)]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ l :: [(a, b)]
l v :: a
v -> (a
v, b
tag) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)]
l) [(a, b)]
rel' [a]
eqcl

        myTagMap :: Map b (TagEqcl a b)
myTagMap = Map b (TagEqcl a b)
-> EquivRelTagged a b -> Int -> Map b (TagEqcl a b)
forall b a.
Ord b =>
Map b (TagEqcl a b) -> [(a, b)] -> Int -> Map b (TagEqcl a b)
merge Map b (TagEqcl a b)
forall b. Map b (TagEqcl a b)
initialTagMap EquivRelTagged a b
rel 0

    in (EquivRelTagged a b -> (b, TagEqcl a b) -> EquivRelTagged a b)
-> EquivRelTagged a b -> [(b, TagEqcl a b)] -> EquivRelTagged a b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl EquivRelTagged a b -> (b, TagEqcl a b) -> EquivRelTagged a b
forall a b b. [(a, b)] -> (b, TagEqcl a b) -> [(a, b)]
tagMapToRel [] (Map b (TagEqcl a b) -> [(b, TagEqcl a b)]
forall k a. Map k a -> [(k, a)]
Map.toList Map b (TagEqcl a b)
myTagMap)

-- | Merge the equivalence classes for given tags.
mergeEquivClasses :: Eq b
                  => EquivRelTagged a b
                  -> b                -- ^ tag 1
                  -> b                -- ^ tag 2
                  -> EquivRelTagged a b
mergeEquivClasses :: EquivRelTagged a b -> b -> b -> EquivRelTagged a b
mergeEquivClasses rel :: EquivRelTagged a b
rel tag1 :: b
tag1 tag2 :: b
tag2 | b
tag1 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
tag2 = EquivRelTagged a b
rel
                                | Bool
otherwise =
    let upd :: (a, b) -> (a, b)
upd (el :: a
el, tag :: b
tag) | b
tag b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
tag2 = (a
el, b
tag1)
                      | Bool
otherwise = (a
el, b
tag)
    in ((a, b) -> (a, b)) -> EquivRelTagged a b -> EquivRelTagged a b
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> (a, b)
forall a. (a, b) -> (a, b)
upd EquivRelTagged a b
rel


{- | Return true if there is an edge between srcNode and targetNode
and the morphism with which it's labelled maps srcSort to targetSort -}
isMorphSort :: CASLDiag
            -> DiagSort
            -> DiagSort
            -> Bool
isMorphSort :: CASLDiag -> DiagSort -> DiagSort -> Bool
isMorphSort diag :: CASLDiag
diag (srcNode :: Int
srcNode, srcSort :: SORT
srcSort) (targetNode :: Int
targetNode, targetSort :: SORT
targetSort) =
    let checkEdges :: [(Int, Int, (a, Morphism f e m))] -> Bool
checkEdges [] = Bool
False
        checkEdges ((sn :: Int
sn, tn :: Int
tn, (_, Morphism { sort_map :: forall f e m. Morphism f e m -> Sort_map
sort_map = Sort_map
sm })) : edgs :: [(Int, Int, (a, Morphism f e m))]
edgs) =
               Int
sn Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
srcNode Bool -> Bool -> Bool
&&
               Int
tn Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
targetNode Bool -> Bool -> Bool
&&
               Sort_map -> SORT -> SORT
mapSort Sort_map
sm SORT
srcSort SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
targetSort
               Bool -> Bool -> Bool
|| [(Int, Int, (a, Morphism f e m))] -> Bool
checkEdges [(Int, Int, (a, Morphism f e m))]
edgs
    in [(Int, Int, (Int, Morphism () () ()))] -> Bool
forall a f e m. [(Int, Int, (a, Morphism f e m))] -> Bool
checkEdges (CASLDiag -> Int -> [(Int, Int, (Int, Morphism () () ()))]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> [LEdge b]
out CASLDiag
diag Int
srcNode)


{- | Return true if there is an edge between srcNode and targetNode
and the morphism with which it's labelled maps srcOp to targetOp -}
isMorphOp :: CASLDiag
          -> DiagOp
          -> DiagOp
          -> Bool
isMorphOp :: CASLDiag -> DiagOp -> DiagOp -> Bool
isMorphOp diag :: CASLDiag
diag (srcNode :: Int
srcNode, srcOp :: (SORT, OpType)
srcOp) (targetNode :: Int
targetNode, targetOp :: (SORT, OpType)
targetOp) =
    let checkEdges :: [(Int, Int, (a, Morphism f e m))] -> Bool
checkEdges [] = Bool
False
        checkEdges
          ((sn :: Int
sn, tn :: Int
tn, (_, Morphism { sort_map :: forall f e m. Morphism f e m -> Sort_map
sort_map = Sort_map
sm, op_map :: forall f e m. Morphism f e m -> Op_map
op_map = Op_map
fm })) : edgs :: [(Int, Int, (a, Morphism f e m))]
edgs) =
               Int
sn Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
srcNode Bool -> Bool -> Bool
&&
               Int
tn Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
targetNode Bool -> Bool -> Bool
&&
               Sort_map -> Op_map -> (SORT, OpType) -> (SORT, OpType)
mapOpSym Sort_map
sm Op_map
fm (SORT, OpType)
srcOp (SORT, OpType) -> (SORT, OpType) -> Bool
forall a. Eq a => a -> a -> Bool
== (SORT, OpType)
targetOp
               Bool -> Bool -> Bool
|| [(Int, Int, (a, Morphism f e m))] -> Bool
checkEdges [(Int, Int, (a, Morphism f e m))]
edgs
    in [(Int, Int, (Int, Morphism () () ()))] -> Bool
forall a f e m. [(Int, Int, (a, Morphism f e m))] -> Bool
checkEdges (CASLDiag -> Int -> [(Int, Int, (Int, Morphism () () ()))]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> [LEdge b]
out CASLDiag
diag Int
srcNode)


{- | Return true if there is an edge between srcNode and targetNode
and the morphism with which it's labelled maps srcPred to targetPred -}
isMorphPred :: CASLDiag
            -> DiagPred
            -> DiagPred
            -> Bool
isMorphPred :: CASLDiag -> DiagPred -> DiagPred -> Bool
isMorphPred diag :: CASLDiag
diag (srcNode :: Int
srcNode, srcPred :: (SORT, PredType)
srcPred) (targetNode :: Int
targetNode, targetPred :: (SORT, PredType)
targetPred) =
   let checkEdges :: [(Int, Int, (a, Morphism f e m))] -> Bool
checkEdges [] = Bool
False
       checkEdges
         ((sn :: Int
sn, tn :: Int
tn, (_, Morphism { sort_map :: forall f e m. Morphism f e m -> Sort_map
sort_map = Sort_map
sm, pred_map :: forall f e m. Morphism f e m -> Pred_map
pred_map = Pred_map
pm })) : edgs :: [(Int, Int, (a, Morphism f e m))]
edgs) =
               Int
sn Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
srcNode Bool -> Bool -> Bool
&&
               Int
tn Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
targetNode Bool -> Bool -> Bool
&&
               Sort_map -> Pred_map -> (SORT, PredType) -> (SORT, PredType)
mapPredSym Sort_map
sm Pred_map
pm (SORT, PredType)
srcPred (SORT, PredType) -> (SORT, PredType) -> Bool
forall a. Eq a => a -> a -> Bool
== (SORT, PredType)
targetPred
               Bool -> Bool -> Bool
|| [(Int, Int, (a, Morphism f e m))] -> Bool
checkEdges [(Int, Int, (a, Morphism f e m))]
edgs
   in [(Int, Int, (Int, Morphism () () ()))] -> Bool
forall a f e m. [(Int, Int, (a, Morphism f e m))] -> Bool
checkEdges (CASLDiag -> Int -> [(Int, Int, (Int, Morphism () () ()))]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> [LEdge b]
out CASLDiag
diag Int
srcNode)


-- | Compute the simeq relation for given diagram.
simeq :: CASLDiag  -- ^ the diagram for which the relation should be created
      -> EquivRel DiagSort
{- ^ returns the relation represented as a list of equivalence
classes (each represented as a list of diagram ops) -}
simeq :: CASLDiag -> EquivRel DiagSort
simeq diag :: CASLDiag
diag =
    {- During the computations the relation is represented as a list of pairs
    (DiagSort, DiagSort). The first element is a diagram sort and the second
    denotes the equivalence class to which it belongs. All the pairs with
    equal second element denote elements of one equivalence class. -}

    let mergeCond :: DiagSort -> DiagSort -> Bool
mergeCond ds :: DiagSort
ds ds' :: DiagSort
ds' = CASLDiag -> DiagSort -> DiagSort -> Bool
isMorphSort CASLDiag
diag DiagSort
ds DiagSort
ds' Bool -> Bool -> Bool
|| CASLDiag -> DiagSort -> DiagSort -> Bool
isMorphSort CASLDiag
diag DiagSort
ds' DiagSort
ds

        -- compute the relation
        rel :: [(DiagSort, DiagSort)]
rel = (DiagSort -> (DiagSort, DiagSort))
-> [DiagSort] -> [(DiagSort, DiagSort)]
forall a b. (a -> b) -> [a] -> [b]
map (\ ds :: DiagSort
ds -> (DiagSort
ds, DiagSort
ds)) (CASLDiag -> [DiagSort]
sorts CASLDiag
diag)
        rel' :: [(DiagSort, DiagSort)]
rel' = (DiagSort -> DiagSort -> Bool)
-> [(DiagSort, DiagSort)] -> [(DiagSort, DiagSort)]
forall b a.
Ord b =>
(a -> a -> Bool) -> EquivRelTagged a b -> EquivRelTagged a b
mergeEquivClassesBy DiagSort -> DiagSort -> Bool
mergeCond [(DiagSort, DiagSort)]
rel
    in [(DiagSort, DiagSort)] -> EquivRel DiagSort
forall b a. Ord b => EquivRelTagged a b -> EquivRel a
taggedValsToEquivClasses [(DiagSort, DiagSort)]
rel'


-- | Compute the simeq^op relation for given diagram.
simeqOp :: CASLDiag  -- ^ the diagram for which the relation should be created
         -> EquivRel DiagOp
{- ^ returns the relation represented as a list of equivalence
classes (each represented as a list of diagram ops) -}
simeqOp :: CASLDiag -> EquivRel DiagOp
simeqOp diag :: CASLDiag
diag =
    {- During the computations the relation is represented as a list of pairs
    (DiagOp, DiagOp). The first element is a diagram op and the second
    denotes the equivalence class to which it belongs. All the pairs with
    equal second element denote elements of one equivalence class. -}

    let mergeCond :: DiagOp -> DiagOp -> Bool
mergeCond ds :: DiagOp
ds ds' :: DiagOp
ds' = CASLDiag -> DiagOp -> DiagOp -> Bool
isMorphOp CASLDiag
diag DiagOp
ds DiagOp
ds' Bool -> Bool -> Bool
|| CASLDiag -> DiagOp -> DiagOp -> Bool
isMorphOp CASLDiag
diag DiagOp
ds' DiagOp
ds

        -- compute the relation
        rel :: [(DiagOp, DiagOp)]
rel = (DiagOp -> (DiagOp, DiagOp)) -> [DiagOp] -> [(DiagOp, DiagOp)]
forall a b. (a -> b) -> [a] -> [b]
map (\ ds :: DiagOp
ds -> (DiagOp
ds, DiagOp
ds)) (CASLDiag -> [DiagOp]
ops CASLDiag
diag)
        rel' :: [(DiagOp, DiagOp)]
rel' = (DiagOp -> DiagOp -> Bool)
-> [(DiagOp, DiagOp)] -> [(DiagOp, DiagOp)]
forall b a.
Ord b =>
(a -> a -> Bool) -> EquivRelTagged a b -> EquivRelTagged a b
mergeEquivClassesBy DiagOp -> DiagOp -> Bool
mergeCond [(DiagOp, DiagOp)]
rel
    in [(DiagOp, DiagOp)] -> EquivRel DiagOp
forall b a. Ord b => EquivRelTagged a b -> EquivRel a
taggedValsToEquivClasses [(DiagOp, DiagOp)]
rel'


-- | Compute the simeq^pred relation for given diagram.
simeqPred :: CASLDiag
             -- ^ the diagram for which the relation should be created
          -> EquivRel DiagPred
             {- ^ returns the relation represented as a list of equivalence
classes (each represented as a list of diagram preds) -}
simeqPred :: CASLDiag -> EquivRel DiagPred
simeqPred diag :: CASLDiag
diag =
    {- During the computations the relation is represented as a list of pairs
    (DiagPred, DiagPred). The first element is a diagram pred and the second
    denotes the equivalence class to which it belongs. All the pairs with
    equal second element denote elements of one equivalence class. -}

    let mergeCond :: DiagPred -> DiagPred -> Bool
mergeCond ds :: DiagPred
ds ds' :: DiagPred
ds' = CASLDiag -> DiagPred -> DiagPred -> Bool
isMorphPred CASLDiag
diag DiagPred
ds DiagPred
ds' Bool -> Bool -> Bool
|| CASLDiag -> DiagPred -> DiagPred -> Bool
isMorphPred CASLDiag
diag DiagPred
ds' DiagPred
ds

        -- compute the relation
        rel :: [(DiagPred, DiagPred)]
rel = (DiagPred -> (DiagPred, DiagPred))
-> [DiagPred] -> [(DiagPred, DiagPred)]
forall a b. (a -> b) -> [a] -> [b]
map (\ ds :: DiagPred
ds -> (DiagPred
ds, DiagPred
ds)) (CASLDiag -> [DiagPred]
preds CASLDiag
diag)
        rel' :: [(DiagPred, DiagPred)]
rel' = (DiagPred -> DiagPred -> Bool)
-> [(DiagPred, DiagPred)] -> [(DiagPred, DiagPred)]
forall b a.
Ord b =>
(a -> a -> Bool) -> EquivRelTagged a b -> EquivRelTagged a b
mergeEquivClassesBy DiagPred -> DiagPred -> Bool
mergeCond [(DiagPred, DiagPred)]
rel
    in [(DiagPred, DiagPred)] -> EquivRel DiagPred
forall b a. Ord b => EquivRelTagged a b -> EquivRel a
taggedValsToEquivClasses [(DiagPred, DiagPred)]
rel'


-- | Compute the simeq_tau relation for given diagram.
simeqTau :: [(Node, CASLMor)]
          -> EquivRel DiagSort
simeqTau :: [(Int, Morphism () () ())] -> EquivRel DiagSort
simeqTau sink :: [(Int, Morphism () () ())]
sink =
    let {- tagEdge: for given morphism m create a list of pairs
        (a, b) where a is DiagSort from the source signature that
        is mapped by m to b -}
        tagEdge :: (a, Morphism f e m) -> [((a, SORT), SORT)]
tagEdge (sn :: a
sn, Morphism { msource :: forall f e m. Morphism f e m -> Sign f e
msource = Sign f e
src, sort_map :: forall f e m. Morphism f e m -> Sort_map
sort_map = Sort_map
sm }) =
            (SORT -> ((a, SORT), SORT)) -> [SORT] -> [((a, SORT), SORT)]
forall a b. (a -> b) -> [a] -> [b]
map (\ ss :: SORT
ss -> ((a
sn, SORT
ss), Sort_map -> SORT -> SORT
mapSort Sort_map
sm SORT
ss))
                 (Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> [SORT]) -> Set SORT -> [SORT]
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
src)
        rel :: [(DiagSort, SORT)]
rel = ([(DiagSort, SORT)]
 -> (Int, Morphism () () ()) -> [(DiagSort, SORT)])
-> [(DiagSort, SORT)]
-> [(Int, Morphism () () ())]
-> [(DiagSort, SORT)]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ l :: [(DiagSort, SORT)]
l e :: (Int, Morphism () () ())
e -> [(DiagSort, SORT)]
l [(DiagSort, SORT)] -> [(DiagSort, SORT)] -> [(DiagSort, SORT)]
forall a. [a] -> [a] -> [a]
++ (Int, Morphism () () ()) -> [(DiagSort, SORT)]
forall a f e m. (a, Morphism f e m) -> [((a, SORT), SORT)]
tagEdge (Int, Morphism () () ())
e) [] [(Int, Morphism () () ())]
sink
    in [(DiagSort, SORT)] -> EquivRel DiagSort
forall b a. Ord b => EquivRelTagged a b -> EquivRel a
taggedValsToEquivClasses [(DiagSort, SORT)]
rel


-- | Compute the simeq^op_tau relation for given diagram.
simeqOpTau :: [(Node, CASLMor)]
            -> EquivRel DiagOp
simeqOpTau :: [(Int, Morphism () () ())] -> EquivRel DiagOp
simeqOpTau sink :: [(Int, Morphism () () ())]
sink =
    let {- tagEdge: for given morphism m create a list of pairs
        (a, b) where a is DiagOp from the source signature that
        is mapped by m to b -}
        tagEdge :: (a, Morphism f e m) -> [((a, (SORT, OpType)), (SORT, OpType))]
tagEdge (sn :: a
sn, Morphism { msource :: forall f e m. Morphism f e m -> Sign f e
msource = Sign f e
src, sort_map :: forall f e m. Morphism f e m -> Sort_map
sort_map = Sort_map
sm, op_map :: forall f e m. Morphism f e m -> Op_map
op_map = Op_map
fm }) =
            ((SORT, OpType) -> ((a, (SORT, OpType)), (SORT, OpType)))
-> [(SORT, OpType)] -> [((a, (SORT, OpType)), (SORT, OpType))]
forall a b. (a -> b) -> [a] -> [b]
map (\ srcOp :: (SORT, OpType)
srcOp -> ((a
sn, (SORT, OpType)
srcOp), Sort_map -> Op_map -> (SORT, OpType) -> (SORT, OpType)
mapOpSym Sort_map
sm Op_map
fm (SORT, OpType)
srcOp))
                (OpMap -> [(SORT, OpType)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList (OpMap -> [(SORT, OpType)]) -> OpMap -> [(SORT, OpType)]
forall a b. (a -> b) -> a -> b
$ Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
src)
        rel :: [(DiagOp, (SORT, OpType))]
rel = ([(DiagOp, (SORT, OpType))]
 -> (Int, Morphism () () ()) -> [(DiagOp, (SORT, OpType))])
-> [(DiagOp, (SORT, OpType))]
-> [(Int, Morphism () () ())]
-> [(DiagOp, (SORT, OpType))]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ l :: [(DiagOp, (SORT, OpType))]
l e :: (Int, Morphism () () ())
e -> [(DiagOp, (SORT, OpType))]
l [(DiagOp, (SORT, OpType))]
-> [(DiagOp, (SORT, OpType))] -> [(DiagOp, (SORT, OpType))]
forall a. [a] -> [a] -> [a]
++ (Int, Morphism () () ()) -> [(DiagOp, (SORT, OpType))]
forall a f e m.
(a, Morphism f e m) -> [((a, (SORT, OpType)), (SORT, OpType))]
tagEdge (Int, Morphism () () ())
e) [] [(Int, Morphism () () ())]
sink
    in [(DiagOp, (SORT, OpType))] -> EquivRel DiagOp
forall b a. Ord b => EquivRelTagged a b -> EquivRel a
taggedValsToEquivClasses [(DiagOp, (SORT, OpType))]
rel


-- | Compute the simeq^pred_tau relation for given diagram.
simeqPredTau :: [(Node, CASLMor)]
              -> EquivRel DiagPred
simeqPredTau :: [(Int, Morphism () () ())] -> EquivRel DiagPred
simeqPredTau sink :: [(Int, Morphism () () ())]
sink =
    let {- tagEdge: for given morphism m create a list of pairs
        (a, b) where a is DiagPred from the source signature that
        is mapped by m to b -}
        tagEdge :: (a, Morphism f e m) -> [((a, (SORT, PredType)), (SORT, PredType))]
tagEdge (sn :: a
sn, Morphism { msource :: forall f e m. Morphism f e m -> Sign f e
msource = Sign f e
src, sort_map :: forall f e m. Morphism f e m -> Sort_map
sort_map = Sort_map
sm, pred_map :: forall f e m. Morphism f e m -> Pred_map
pred_map = Pred_map
pm }) =
            ((SORT, PredType) -> ((a, (SORT, PredType)), (SORT, PredType)))
-> [(SORT, PredType)]
-> [((a, (SORT, PredType)), (SORT, PredType))]
forall a b. (a -> b) -> [a] -> [b]
map (\ srcPred :: (SORT, PredType)
srcPred -> ((a
sn, (SORT, PredType)
srcPred), Sort_map -> Pred_map -> (SORT, PredType) -> (SORT, PredType)
mapPredSym Sort_map
sm Pred_map
pm (SORT, PredType)
srcPred))
               (PredMap -> [(SORT, PredType)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList (PredMap -> [(SORT, PredType)]) -> PredMap -> [(SORT, PredType)]
forall a b. (a -> b) -> a -> b
$ Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
src)
        rel :: [(DiagPred, (SORT, PredType))]
rel = ([(DiagPred, (SORT, PredType))]
 -> (Int, Morphism () () ()) -> [(DiagPred, (SORT, PredType))])
-> [(DiagPred, (SORT, PredType))]
-> [(Int, Morphism () () ())]
-> [(DiagPred, (SORT, PredType))]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ l :: [(DiagPred, (SORT, PredType))]
l e :: (Int, Morphism () () ())
e -> [(DiagPred, (SORT, PredType))]
l [(DiagPred, (SORT, PredType))]
-> [(DiagPred, (SORT, PredType))] -> [(DiagPred, (SORT, PredType))]
forall a. [a] -> [a] -> [a]
++ (Int, Morphism () () ()) -> [(DiagPred, (SORT, PredType))]
forall a f e m.
(a, Morphism f e m) -> [((a, (SORT, PredType)), (SORT, PredType))]
tagEdge (Int, Morphism () () ())
e) [] [(Int, Morphism () () ())]
sink
    in [(DiagPred, (SORT, PredType))] -> EquivRel DiagPred
forall b a. Ord b => EquivRelTagged a b -> EquivRel a
taggedValsToEquivClasses [(DiagPred, (SORT, PredType))]
rel


{- | Check that one equivalence relation is a subset of another.
The relations are represented as a lists of equivalence classes,
where equivalence classes are lists of elements. -}
subRelation :: Eq a
            => EquivRel a  -- ^ the relation that is supposed to be a subset
            -> EquivRel a  -- ^ the relation that is supposed to be a superset
            -> Maybe (a, a)
{- ^ returns a pair of elements that are in the same equivalence class of the
first relation but are not in the same equivalence class of the second
relation or Nothing the first relation is a subset of the second one. -}
subRelation :: EquivRel a -> EquivRel a -> Maybe (a, a)
subRelation [] _ = Maybe (a, a)
forall a. Maybe a
Nothing
subRelation ([] : eqcls :: EquivRel a
eqcls) sup :: EquivRel a
sup = EquivRel a -> EquivRel a -> Maybe (a, a)
forall a. Eq a => EquivRel a -> EquivRel a -> Maybe (a, a)
subRelation EquivRel a
eqcls EquivRel a
sup
                               -- this should never be the case
subRelation (elts' :: EquivClass a
elts'@(elt' :: a
elt' : _) : eqcls' :: EquivRel a
eqcls') sup :: EquivRel a
sup =
    let findEqCl :: t -> [[t]] -> [t]
findEqCl _ [] = []
        findEqCl elt :: t
elt (eqcl :: [t]
eqcl : eqcls :: [[t]]
eqcls) =
            if t -> [t] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem t
elt [t]
eqcl then [t]
eqcl else t -> [[t]] -> [t]
findEqCl t
elt [[t]]
eqcls
        checkEqCl :: [a] -> t a -> Maybe a
checkEqCl [] _ = Maybe a
forall a. Maybe a
Nothing
        checkEqCl (elt :: a
elt : elts :: [a]
elts) supEqCl :: t a
supEqCl =
            if a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
elt t a
supEqCl
               then [a] -> t a -> Maybe a
checkEqCl [a]
elts t a
supEqCl
               else a -> Maybe a
forall a. a -> Maybe a
Just a
elt
        curFail :: Maybe a
curFail = EquivClass a -> EquivClass a -> Maybe a
forall (t :: * -> *) a. (Foldable t, Eq a) => [a] -> t a -> Maybe a
checkEqCl EquivClass a
elts' (a -> EquivRel a -> EquivClass a
forall t. Eq t => t -> [[t]] -> [t]
findEqCl a
elt' EquivRel a
sup)
    in case Maybe a
curFail of
            Nothing -> EquivRel a -> EquivRel a -> Maybe (a, a)
forall a. Eq a => EquivRel a -> EquivRel a -> Maybe (a, a)
subRelation EquivRel a
eqcls' EquivRel a
sup
            Just elt2 :: a
elt2 -> (a, a) -> Maybe (a, a)
forall a. a -> Maybe a
Just (a
elt', a
elt2)


-- | Compute the set of sort embeddings defined in the diagram.
embs :: CASLDiag
     -> [DiagEmb]
embs :: CASLDiag -> [DiagEmb]
embs diag :: CASLDiag
diag =
    let embs' :: [(a, Sign f e)] -> [(a, SORT, SORT)]
embs' [] = []
        embs' ((n :: a
n, sig :: Sign f e
sig) : lNodes :: [(a, Sign f e)]
lNodes) =
           let ssl :: [(SORT, SORT)]
ssl = Rel SORT -> [(SORT, SORT)]
forall a. Rel a -> [(a, a)]
Rel.toList (Rel SORT -> [(SORT, SORT)])
-> (Rel SORT -> Rel SORT) -> Rel SORT -> [(SORT, SORT)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.irreflex (Rel SORT -> [(SORT, SORT)]) -> Rel SORT -> [(SORT, SORT)]
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
sig in
            ((SORT, SORT) -> (a, SORT, SORT))
-> [(SORT, SORT)] -> [(a, SORT, SORT)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s1 :: SORT
s1, s2 :: SORT
s2) -> (a
n, SORT
s1, SORT
s2)) [(SORT, SORT)]
ssl [(a, SORT, SORT)] -> [(a, SORT, SORT)] -> [(a, SORT, SORT)]
forall a. [a] -> [a] -> [a]
++ [(a, Sign f e)] -> [(a, SORT, SORT)]
embs' [(a, Sign f e)]
lNodes
    in [(Int, Sign () ())] -> [DiagEmb]
forall a f e. [(a, Sign f e)] -> [(a, SORT, SORT)]
embs' (CASLDiag -> [(Int, Sign () ())]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes CASLDiag
diag)


{- | Compute the set of sort embeddings (relations on sorts) defined
in the source nodes of the sink. -}
sinkEmbs :: CASLDiag          -- ^ the diagram
         -> [(Node, CASLMor)] -- ^ the sink
         -> [DiagEmb]
sinkEmbs :: CASLDiag -> [(Int, Morphism () () ())] -> [DiagEmb]
sinkEmbs _ [] = []
sinkEmbs diag :: CASLDiag
diag ((srcNode :: Int
srcNode, _) : edgs :: [(Int, Morphism () () ())]
edgs) =
    let (_, _, sig :: Sign () ()
sig, _) = CASLDiag
-> Int
-> (Adj (Int, Morphism () () ()), Int, Sign () (),
    Adj (Int, Morphism () () ()))
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> Context a b
context CASLDiag
diag Int
srcNode
        ssl :: [(SORT, SORT)]
ssl = Rel SORT -> [(SORT, SORT)]
forall a. Rel a -> [(a, a)]
Rel.toList (Rel SORT -> [(SORT, SORT)])
-> (Rel SORT -> Rel SORT) -> Rel SORT -> [(SORT, SORT)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.irreflex (Rel SORT -> [(SORT, SORT)]) -> Rel SORT -> [(SORT, SORT)]
forall a b. (a -> b) -> a -> b
$ Sign () () -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign () ()
sig
    in ((SORT, SORT) -> DiagEmb) -> [(SORT, SORT)] -> [DiagEmb]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s1 :: SORT
s1, s2 :: SORT
s2) -> (Int
srcNode, SORT
s1, SORT
s2)) [(SORT, SORT)]
ssl
           [DiagEmb] -> [DiagEmb] -> [DiagEmb]
forall a. [a] -> [a] -> [a]
++ CASLDiag -> [(Int, Morphism () () ())] -> [DiagEmb]
sinkEmbs CASLDiag
diag [(Int, Morphism () () ())]
edgs


-- | Check if the two given elements are in the given relation.
inRel :: Eq a
      => EquivRel a -- ^ the relation
      -> a          -- ^ the first element
      -> a          -- ^ the second element
      -> Bool
inRel :: EquivRel a -> a -> a -> Bool
inRel [] _ _ = Bool
False
inRel (eqc :: EquivClass a
eqc : eqcs :: EquivRel a
eqcs) a :: a
a b :: a
b | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b = Bool
True
                       | Bool
otherwise =
    case (a -> Bool) -> EquivClass a -> Maybe a
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a) EquivClass a
eqc of
         Nothing -> EquivRel a -> a -> a -> Bool
forall a. Eq a => EquivRel a -> a -> a -> Bool
inRel EquivRel a
eqcs a
a a
b
         Just _ -> case (a -> Bool) -> EquivClass a -> Maybe a
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b) EquivClass a
eqc of
                        Nothing -> Bool
False
                        Just _ -> Bool
True


{- | Check if two embeddings can occur subsequently in a word
given the simeq relation on sorts. -}
admissible :: EquivRel DiagSort -- ^ the \simeq relation
           -> DiagEmb           -- ^ the first embedding
           -> DiagEmb           -- ^ the second embedding
           -> Bool
admissible :: EquivRel DiagSort -> DiagEmb -> DiagEmb -> Bool
admissible simeq' :: EquivRel DiagSort
simeq' (n1 :: Int
n1, s1 :: SORT
s1, _) (n2 :: Int
n2, _, s2 :: SORT
s2) =
    EquivRel DiagSort -> DiagSort -> DiagSort -> Bool
forall a. Eq a => EquivRel a -> a -> a -> Bool
inRel EquivRel DiagSort
simeq' (Int
n1, SORT
s1) (Int
n2, SORT
s2)


{- | Compute the set of all the loopless, admissible
words over given set of embeddings. Paper section 6 -}
looplessWords :: [DiagEmb]         -- ^ the embeddings
         -> EquivRel DiagSort
            -- ^ the \simeq relation that defines admissibility
         -> [DiagEmbWord]
looplessWords :: [DiagEmb] -> EquivRel DiagSort -> [[DiagEmb]]
looplessWords embs1 :: [DiagEmb]
embs1 simeq1 :: EquivRel DiagSort
simeq1 =
    let {- generate the list of all loopless words over given alphabet
        with given suffix -}
        looplessWords' :: [DiagEmb] -> [DiagEmb] -> Int -> [[DiagEmb]]
looplessWords' suff :: [DiagEmb]
suff@(e :: DiagEmb
e : _) embs2 :: [DiagEmb]
embs2 pos :: Int
pos | Int
pos Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [DiagEmb] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DiagEmb]
embs2 = [[DiagEmb]
suff]
                                              | Bool
otherwise =
            let emb :: DiagEmb
emb = [DiagEmb]
embs2 [DiagEmb] -> Int -> DiagEmb
forall a. [a] -> Int -> a
!! Int
pos
                embs' :: [DiagEmb]
embs' = [DiagEmb]
embs2 [DiagEmb] -> [DiagEmb] -> [DiagEmb]
forall a. Eq a => [a] -> [a] -> [a]
\\ [DiagEmb
emb]
                ws :: [[DiagEmb]]
ws = if EquivRel DiagSort -> DiagEmb -> DiagEmb -> Bool
admissible EquivRel DiagSort
simeq1 DiagEmb
emb DiagEmb
e
                       then [DiagEmb] -> [DiagEmb] -> Int -> [[DiagEmb]]
looplessWords' (DiagEmb
emb DiagEmb -> [DiagEmb] -> [DiagEmb]
forall a. a -> [a] -> [a]
: [DiagEmb]
suff) [DiagEmb]
embs' 0
                       else []
            in [[DiagEmb]]
ws [[DiagEmb]] -> [[DiagEmb]] -> [[DiagEmb]]
forall a. [a] -> [a] -> [a]
++ [DiagEmb] -> [DiagEmb] -> Int -> [[DiagEmb]]
looplessWords' [DiagEmb]
suff [DiagEmb]
embs2 (Int
pos Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
        looplessWords' [] embs2 :: [DiagEmb]
embs2 pos :: Int
pos | Int
pos Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [DiagEmb] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DiagEmb]
embs2 = []
                                    | Bool
otherwise =
            let emb :: DiagEmb
emb = [DiagEmb]
embs2 [DiagEmb] -> Int -> DiagEmb
forall a. [a] -> Int -> a
!! Int
pos
                embs' :: [DiagEmb]
embs' = [DiagEmb]
embs2 [DiagEmb] -> [DiagEmb] -> [DiagEmb]
forall a. Eq a => [a] -> [a] -> [a]
\\ [DiagEmb
emb]
            in [DiagEmb] -> [DiagEmb] -> Int -> [[DiagEmb]]
looplessWords' [DiagEmb
emb] [DiagEmb]
embs' 0 [[DiagEmb]] -> [[DiagEmb]] -> [[DiagEmb]]
forall a. [a] -> [a] -> [a]
++
               [DiagEmb] -> [DiagEmb] -> Int -> [[DiagEmb]]
looplessWords' [] [DiagEmb]
embs2 (Int
pos Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
    in [DiagEmb] -> [DiagEmb] -> Int -> [[DiagEmb]]
looplessWords' [] [DiagEmb]
embs1 0


-- | Return the codomain of an embedding path.
wordCod :: DiagEmbWord
        -> DiagSort
wordCod :: [DiagEmb] -> DiagSort
wordCod ((n :: Int
n, _, s2 :: SORT
s2) : _) = (Int
n, SORT
s2)
wordCod [] = String -> DiagSort
forall a. HasCallStack => String -> a
error "wordCod"


-- | Return the domain of an embedding path.
wordDom :: DiagEmbWord
        -> DiagSort
wordDom :: [DiagEmb] -> DiagSort
wordDom [] = String -> DiagSort
forall a. HasCallStack => String -> a
error "wordDom"
wordDom w :: [DiagEmb]
w = let (n :: Int
n, s1 :: SORT
s1, _) = [DiagEmb] -> DiagEmb
forall a. [a] -> a
last [DiagEmb]
w in (Int
n, SORT
s1)


-- | Find an equivalence class tag for given element.
findTag :: Eq a
        => EquivRelTagged a b
        -> a
        -> Maybe b
findTag :: EquivRelTagged a b -> a -> Maybe b
findTag [] _ = Maybe b
forall a. Maybe a
Nothing
findTag ((w' :: a
w', t :: b
t) : wtps :: EquivRelTagged a b
wtps) w :: a
w =
    if a
w a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
w' then b -> Maybe b
forall a. a -> Maybe a
Just b
t else EquivRelTagged a b -> a -> Maybe b
forall a b. Eq a => EquivRelTagged a b -> a -> Maybe b
findTag EquivRelTagged a b
wtps a
w


-- | Compute the left-cancellable closure of a relation on words.
leftCancellableClosure :: EquivRelTagged DiagEmbWord DiagEmbWord
                       -> EquivRelTagged DiagEmbWord DiagEmbWord
leftCancellableClosure :: EquivRelTagged [DiagEmb] [DiagEmb]
-> EquivRelTagged [DiagEmb] [DiagEmb]
leftCancellableClosure rel1 :: EquivRelTagged [DiagEmb] [DiagEmb]
rel1 =
    let {- checkPrefixes: for each common prefix of two given words
        merge the equivalence classes of the suffixes -}
        checkPrefixes :: [a] -> [a] -> [([a], a)] -> [([a], a)]
checkPrefixes [] _ rel :: [([a], a)]
rel = [([a], a)]
rel
        checkPrefixes _ [] rel :: [([a], a)]
rel = [([a], a)]
rel
        checkPrefixes w1 :: [a]
w1@(l1 :: a
l1 : suf1 :: [a]
suf1) w2 :: [a]
w2@(l2 :: a
l2 : suf2 :: [a]
suf2) rel :: [([a], a)]
rel
          | [a]
w1 [a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
== [a]
w2 = [([a], a)]
rel
          | a
l1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
l2 = [([a], a)]
rel
          | Bool
otherwise =
            let tag1 :: a
tag1 = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe (String -> a
forall a. HasCallStack => String -> a
error "checkPrefixes: tag1")
                       (Maybe a -> a) -> Maybe a -> a
forall a b. (a -> b) -> a -> b
$ [([a], a)] -> [a] -> Maybe a
forall a b. Eq a => EquivRelTagged a b -> a -> Maybe b
findTag [([a], a)]
rel [a]
suf1
                tag2 :: a
tag2 = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe (String -> a
forall a. HasCallStack => String -> a
error "checkPrefixes: tag2")
                       (Maybe a -> a) -> Maybe a -> a
forall a b. (a -> b) -> a -> b
$ [([a], a)] -> [a] -> Maybe a
forall a b. Eq a => EquivRelTagged a b -> a -> Maybe b
findTag [([a], a)]
rel [a]
suf2
                rel' :: [([a], a)]
rel' = if a
tag1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
tag2 then [([a], a)]
rel
                          else let upd :: (a, a) -> (a, a)
upd (w :: a
w, t :: a
t) | a
t a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
tag2 = (a
w, a
tag1)
                                              | Bool
otherwise = (a
w, a
t)
                               in (([a], a) -> ([a], a)) -> [([a], a)] -> [([a], a)]
forall a b. (a -> b) -> [a] -> [b]
map ([a], a) -> ([a], a)
forall a. (a, a) -> (a, a)
upd [([a], a)]
rel
            in [a] -> [a] -> [([a], a)] -> [([a], a)]
checkPrefixes [a]
suf1 [a]
suf2 [([a], a)]
rel'

        -- iterateWord1: for each pair of related words call checkPrefixes
        iterateWord1 :: [([a], b)] -> Int -> [([a], b)]
iterateWord1 rel :: [([a], b)]
rel pos :: Int
pos | Int
pos Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [([a], b)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [([a], b)]
rel = [([a], b)]
rel
                             | Bool
otherwise =
            let iterateWord2 :: ([a], b) -> [([a], b)] -> Int -> [([a], b)]
iterateWord2 wtp1 :: ([a], b)
wtp1@(w1 :: [a]
w1, t1 :: b
t1) rel2 :: [([a], b)]
rel2 pos2 :: Int
pos2
                    | Int
pos2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [([a], b)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [([a], b)]
rel2 = [([a], b)]
rel2
                    | Bool
otherwise =
                    let _wtp2 :: ([a], b)
_wtp2@(w2 :: [a]
w2, t2 :: b
t2) = [([a], b)]
rel2 [([a], b)] -> Int -> ([a], b)
forall a. [a] -> Int -> a
!! Int
pos2
                        rel3 :: [([a], b)]
rel3 = if b
t1 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
t2 then [a] -> [a] -> [([a], b)] -> [([a], b)]
forall a a. (Eq a, Eq a) => [a] -> [a] -> [([a], a)] -> [([a], a)]
checkPrefixes [a]
w1 [a]
w2 [([a], b)]
rel2
                               else [([a], b)]
rel2
                    in ([a], b) -> [([a], b)] -> Int -> [([a], b)]
iterateWord2 ([a], b)
wtp1 [([a], b)]
rel3 (Int
pos2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
                wtp :: ([a], b)
wtp = [([a], b)]
rel [([a], b)] -> Int -> ([a], b)
forall a. [a] -> Int -> a
!! Int
pos
                rel' :: [([a], b)]
rel' = ([a], b) -> [([a], b)] -> Int -> [([a], b)]
forall b a.
(Eq b, Eq a) =>
([a], b) -> [([a], b)] -> Int -> [([a], b)]
iterateWord2 ([a], b)
wtp [([a], b)]
rel 0
            in [([a], b)] -> Int -> [([a], b)]
iterateWord1 [([a], b)]
rel' (Int
pos Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
    in EquivRelTagged [DiagEmb] [DiagEmb]
-> Int -> EquivRelTagged [DiagEmb] [DiagEmb]
forall b a. (Eq b, Eq a) => [([a], b)] -> Int -> [([a], b)]
iterateWord1 EquivRelTagged [DiagEmb] [DiagEmb]
rel1 0

{- | Compute the congruence closure of an equivalence R: two pairs of
elements (1, 3) and (2, 4) are chosen such that 1 R 2 and 3 R 4. It is
then checked that elements 1, 3 and 2, 4 are in relation supplied and
if so equivalence classes for (op 1 3) and (op 1 4) in R are merged.
This function should be applied to the relation until a fixpoint is
reached. -}

congruenceClosure :: (Eq a, Eq b)
                  => (a -> a -> Bool)
                  -- ^ the check to be performed on elements 1, 3 and 2, 4
                  -> (a -> a -> a)
                  -- ^ the operation to be performed on elements 1, 3 and 2, 4
                  -> EquivRelTagged a b
                  -> EquivRelTagged a b
congruenceClosure :: (a -> a -> Bool)
-> (a -> a -> a) -> EquivRelTagged a b -> EquivRelTagged a b
congruenceClosure check :: a -> a -> Bool
check op :: a -> a -> a
op rel :: EquivRelTagged a b
rel =
    let -- iterateWord1
    iterateWord1 :: EquivRelTagged a b -> Int -> EquivRelTagged a b
iterateWord1 rel1 :: EquivRelTagged a b
rel1 pos1 :: Int
pos1 | Int
pos1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= EquivRelTagged a b -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length EquivRelTagged a b
rel1 = EquivRelTagged a b
rel1
                           | Bool
otherwise = let -- iterateWord2
      iterateWord2 :: (a, b) -> EquivRelTagged a b -> Int -> EquivRelTagged a b
iterateWord2 wtp1 :: (a, b)
wtp1@(_, t1 :: b
t1) rel2 :: EquivRelTagged a b
rel2 pos2 :: Int
pos2 | Int
pos2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= EquivRelTagged a b -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length EquivRelTagged a b
rel2 = EquivRelTagged a b
rel2
                                          | Bool
otherwise = let -- iterateWord3
        iterateWord3 :: (a, b) -> (a, b) -> EquivRelTagged a b -> Int -> EquivRelTagged a b
iterateWord3 wtp1' :: (a, b)
wtp1'@(w1' :: a
w1', _) wtp2' :: (a, b)
wtp2' rel3 :: EquivRelTagged a b
rel3 pos3 :: Int
pos3
            | Int
pos3 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= EquivRelTagged a b -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length EquivRelTagged a b
rel3 = EquivRelTagged a b
rel3
            | Bool
otherwise = let -- iterateWord4
          iterateWord4 :: (a, b)
-> (a, b)
-> (a, b)
-> EquivRelTagged a b
-> Int
-> EquivRelTagged a b
iterateWord4 wtp1'' :: (a, b)
wtp1''@(w1 :: a
w1, _) wtp2'' :: (a, b)
wtp2''@(w2 :: a
w2, _) wtp3' :: (a, b)
wtp3'@(w3 :: a
w3, t3 :: b
t3) rel4 :: EquivRelTagged a b
rel4 pos4 :: Int
pos4
              | Int
pos4 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= EquivRelTagged a b -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length EquivRelTagged a b
rel4 = EquivRelTagged a b
rel4
              | Bool
otherwise = let
            (w4 :: a
w4, t4 :: b
t4) = EquivRelTagged a b
rel4 EquivRelTagged a b -> Int -> (a, b)
forall a. [a] -> Int -> a
!! Int
pos4
            rel4' :: EquivRelTagged a b
rel4' = if b
t3 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
/= b
t4 Bool -> Bool -> Bool
|| Bool -> Bool
not (a -> a -> Bool
check a
w2 a
w4) then EquivRelTagged a b
rel4 else let
              mct1 :: Maybe b
mct1 = EquivRelTagged a b -> a -> Maybe b
forall a b. Eq a => EquivRelTagged a b -> a -> Maybe b
findTag EquivRelTagged a b
rel (a -> a -> a
op a
w1 a
w3)
              mct2 :: Maybe b
mct2 = EquivRelTagged a b -> a -> Maybe b
forall a b. Eq a => EquivRelTagged a b -> a -> Maybe b
findTag EquivRelTagged a b
rel (a -> a -> a
op a
w2 a
w4)
              in case (Maybe b
mct1, Maybe b
mct2) of
              (Nothing, _) -> EquivRelTagged a b
rel4 -- w3w1 is not in the domain of rel
              (_, Nothing) -> EquivRelTagged a b
rel4 -- w4w2 is not in the domain of rel
              (Just ct1 :: b
ct1, Just ct2 :: b
ct2) -> EquivRelTagged a b -> b -> b -> EquivRelTagged a b
forall b a.
Eq b =>
EquivRelTagged a b -> b -> b -> EquivRelTagged a b
mergeEquivClasses EquivRelTagged a b
rel4 b
ct1 b
ct2
            in (a, b)
-> (a, b)
-> (a, b)
-> EquivRelTagged a b
-> Int
-> EquivRelTagged a b
iterateWord4 (a, b)
wtp1'' (a, b)
wtp2'' (a, b)
wtp3' EquivRelTagged a b
rel4' (Int
pos4 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
          wtp3 :: (a, b)
wtp3@(w3' :: a
w3', _) = EquivRelTagged a b
rel3 EquivRelTagged a b -> Int -> (a, b)
forall a. [a] -> Int -> a
!! Int
pos3
          rel3' :: EquivRelTagged a b
rel3' = if a -> a -> Bool
check a
w1' a
w3' {- inRel here is usually much more efficient
                                          than findTag rel (w3 ++ w1) -}
                 then (a, b)
-> (a, b)
-> (a, b)
-> EquivRelTagged a b
-> Int
-> EquivRelTagged a b
forall b b.
(a, b)
-> (a, b)
-> (a, b)
-> EquivRelTagged a b
-> Int
-> EquivRelTagged a b
iterateWord4 (a, b)
wtp1' (a, b)
wtp2' (a, b)
wtp3 EquivRelTagged a b
rel3 0 else EquivRelTagged a b
rel3
          in (a, b) -> (a, b) -> EquivRelTagged a b -> Int -> EquivRelTagged a b
iterateWord3 (a, b)
wtp1' (a, b)
wtp2 EquivRelTagged a b
rel3' (Int
pos3 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
        wtp2 :: (a, b)
wtp2@(_, t2 :: b
t2) = EquivRelTagged a b
rel2 EquivRelTagged a b -> Int -> (a, b)
forall a. [a] -> Int -> a
!! Int
pos2
        rel2' :: EquivRelTagged a b
rel2' = if b
t1 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
/= b
t2 then EquivRelTagged a b
rel2 else (a, b) -> (a, b) -> EquivRelTagged a b -> Int -> EquivRelTagged a b
forall b.
(a, b) -> (a, b) -> EquivRelTagged a b -> Int -> EquivRelTagged a b
iterateWord3 (a, b)
wtp1 (a, b)
wtp2 EquivRelTagged a b
rel2 0
        in (a, b) -> EquivRelTagged a b -> Int -> EquivRelTagged a b
iterateWord2 (a, b)
wtp1 EquivRelTagged a b
rel2' (Int
pos2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
      wtp :: (a, b)
wtp = EquivRelTagged a b
rel1 EquivRelTagged a b -> Int -> (a, b)
forall a. [a] -> Int -> a
!! Int
pos1
      rel' :: EquivRelTagged a b
rel' = (a, b) -> EquivRelTagged a b -> Int -> EquivRelTagged a b
iterateWord2 (a, b)
wtp EquivRelTagged a b
rel1 0
      in EquivRelTagged a b -> Int -> EquivRelTagged a b
iterateWord1 EquivRelTagged a b
rel' (Int
pos1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
    in EquivRelTagged a b -> Int -> EquivRelTagged a b
iterateWord1 EquivRelTagged a b
rel 0


-- | Compute the cong_tau relation for given diagram and sink.
congTau :: CASLDiag          -- ^ the diagram
         -> [(Node, CASLMor)] -- ^ the sink
         -> EquivRel DiagSort -- ^ the \simeq_tau relation
         -> EquivRel DiagEmbWord
congTau :: CASLDiag
-> [(Int, Morphism () () ())]
-> EquivRel DiagSort
-> EquivRel [DiagEmb]
congTau diag :: CASLDiag
diag sink :: [(Int, Morphism () () ())]
sink st :: EquivRel DiagSort
st =
    -- domCodSimeq: check that domains and codomains of given words are related
    let domCodSimeq :: [DiagEmb] -> [DiagEmb] -> Bool
domCodSimeq w1 :: [DiagEmb]
w1 w2 :: [DiagEmb]
w2 = EquivRel DiagSort -> DiagSort -> DiagSort -> Bool
forall a. Eq a => EquivRel a -> a -> a -> Bool
inRel EquivRel DiagSort
st ([DiagEmb] -> DiagSort
wordDom [DiagEmb]
w1) ([DiagEmb] -> DiagSort
wordDom [DiagEmb]
w2)
                            Bool -> Bool -> Bool
&& EquivRel DiagSort -> DiagSort -> DiagSort -> Bool
forall a. Eq a => EquivRel a -> a -> a -> Bool
inRel EquivRel DiagSort
st ([DiagEmb] -> DiagSort
wordCod [DiagEmb]
w1) ([DiagEmb] -> DiagSort
wordCod [DiagEmb]
w2)
        embs1 :: [DiagEmb]
embs1 = CASLDiag -> [(Int, Morphism () () ())] -> [DiagEmb]
sinkEmbs CASLDiag
diag [(Int, Morphism () () ())]
sink
        words1 :: [[DiagEmb]]
words1 = [DiagEmb] -> EquivRel DiagSort -> [[DiagEmb]]
looplessWords [DiagEmb]
embs1 EquivRel DiagSort
st
        rel :: EquivRelTagged [DiagEmb] [DiagEmb]
rel = ([DiagEmb] -> ([DiagEmb], [DiagEmb]))
-> [[DiagEmb]] -> EquivRelTagged [DiagEmb] [DiagEmb]
forall a b. (a -> b) -> [a] -> [b]
map (\ w :: [DiagEmb]
w -> ([DiagEmb]
w, [DiagEmb]
w)) [[DiagEmb]]
words1
        rel' :: EquivRelTagged [DiagEmb] [DiagEmb]
rel' = ([DiagEmb] -> [DiagEmb] -> Bool)
-> EquivRelTagged [DiagEmb] [DiagEmb]
-> EquivRelTagged [DiagEmb] [DiagEmb]
forall b a.
Ord b =>
(a -> a -> Bool) -> EquivRelTagged a b -> EquivRelTagged a b
mergeEquivClassesBy [DiagEmb] -> [DiagEmb] -> Bool
domCodSimeq EquivRelTagged [DiagEmb] [DiagEmb]
rel
    in EquivRelTagged [DiagEmb] [DiagEmb] -> EquivRel [DiagEmb]
forall b a. Ord b => EquivRelTagged a b -> EquivRel a
taggedValsToEquivClasses EquivRelTagged [DiagEmb] [DiagEmb]
rel'


{- | Compute the finite representation of cong_0 relation for given diagram.
The representation consists only of equivalence classes that
contain more than one element. -}
cong0 :: CASLDiag
       -> EquivRel DiagSort -- ^ the \simeq relation
       -> EquivRel DiagEmbWord
-- Comp rule is not applied
cong0 :: CASLDiag -> EquivRel DiagSort -> EquivRel [DiagEmb]
cong0 diag :: CASLDiag
diag simeq' :: EquivRel DiagSort
simeq' =
    let -- diagRule: the Diag rule
        diagRule :: [DiagEmb] -> [DiagEmb] -> Bool
diagRule [(n1 :: Int
n1, s11 :: SORT
s11, s12 :: SORT
s12)] [(n2 :: Int
n2, s21 :: SORT
s21, s22 :: SORT
s22)] =
            CASLDiag -> DiagSort -> DiagSort -> Bool
isMorphSort CASLDiag
diag (Int
n1, SORT
s11) (Int
n2, SORT
s21)
                Bool -> Bool -> Bool
&& CASLDiag -> DiagSort -> DiagSort -> Bool
isMorphSort CASLDiag
diag (Int
n1, SORT
s12) (Int
n2, SORT
s22)
            Bool -> Bool -> Bool
|| CASLDiag -> DiagSort -> DiagSort -> Bool
isMorphSort CASLDiag
diag (Int
n2, SORT
s21) (Int
n1, SORT
s11)
                Bool -> Bool -> Bool
&& CASLDiag -> DiagSort -> DiagSort -> Bool
isMorphSort CASLDiag
diag (Int
n2, SORT
s22) (Int
n1, SORT
s12)
        diagRule _ _ = Bool
False

        -- addToRel: add given word to given relation
        addToRel :: EquivRel [DiagEmb] -> [DiagEmb] -> EquivRel [DiagEmb]
addToRel [] _ = []
        addToRel ([] : _) _ = String -> EquivRel [DiagEmb]
forall a. HasCallStack => String -> a
error "addToRel"
        addToRel (eqcl :: [[DiagEmb]]
eqcl@(refw :: [DiagEmb]
refw : _) : eqcls :: EquivRel [DiagEmb]
eqcls) w :: [DiagEmb]
w =
            if [DiagEmb] -> DiagSort
wordDom [DiagEmb]
w DiagSort -> DiagSort -> Bool
forall a. Eq a => a -> a -> Bool
== [DiagEmb] -> DiagSort
wordDom [DiagEmb]
refw Bool -> Bool -> Bool
&& [DiagEmb] -> DiagSort
wordCod [DiagEmb]
w DiagSort -> DiagSort -> Bool
forall a. Eq a => a -> a -> Bool
== [DiagEmb] -> DiagSort
wordCod [DiagEmb]
refw
               then ([DiagEmb]
w [DiagEmb] -> [[DiagEmb]] -> [[DiagEmb]]
forall a. a -> [a] -> [a]
: [[DiagEmb]]
eqcl) [[DiagEmb]] -> EquivRel [DiagEmb] -> EquivRel [DiagEmb]
forall a. a -> [a] -> [a]
: EquivRel [DiagEmb]
eqcls
               else [[DiagEmb]]
eqcl [[DiagEmb]] -> EquivRel [DiagEmb] -> EquivRel [DiagEmb]
forall a. a -> [a] -> [a]
: EquivRel [DiagEmb] -> [DiagEmb] -> EquivRel [DiagEmb]
addToRel EquivRel [DiagEmb]
eqcls [DiagEmb]
w

     -- words2: generate all the admissible 2-letter words over given alphabet
        words2 :: [DiagEmb] -> [DiagEmb] -> [DiagEmb] -> [[DiagEmb]]
words2 _ [] _ = []
        words2 alph :: [DiagEmb]
alph (_ : embs1 :: [DiagEmb]
embs1) [] = [DiagEmb] -> [DiagEmb] -> [DiagEmb] -> [[DiagEmb]]
words2 [DiagEmb]
alph [DiagEmb]
embs1 [DiagEmb]
alph
        words2 alph :: [DiagEmb]
alph embs1 :: [DiagEmb]
embs1@(emb1 :: DiagEmb
emb1 : _) (emb2 :: DiagEmb
emb2 : embs2 :: [DiagEmb]
embs2) =
            let ws :: [[DiagEmb]]
ws = [DiagEmb] -> [DiagEmb] -> [DiagEmb] -> [[DiagEmb]]
words2 [DiagEmb]
alph [DiagEmb]
embs1 [DiagEmb]
embs2
            in if EquivRel DiagSort -> DiagEmb -> DiagEmb -> Bool
admissible EquivRel DiagSort
simeq' DiagEmb
emb1 DiagEmb
emb2
               then [DiagEmb
emb1, DiagEmb
emb2] [DiagEmb] -> [[DiagEmb]] -> [[DiagEmb]]
forall a. a -> [a] -> [a]
: [[DiagEmb]]
ws else [[DiagEmb]]
ws

        -- compute the relation
        em :: [DiagEmb]
em = CASLDiag -> [DiagEmb]
embs CASLDiag
diag
        rel :: EquivRelTagged [DiagEmb] [DiagEmb]
rel = (DiagEmb -> ([DiagEmb], [DiagEmb]))
-> [DiagEmb] -> EquivRelTagged [DiagEmb] [DiagEmb]
forall a b. (a -> b) -> [a] -> [b]
map (\ e :: DiagEmb
e -> ([DiagEmb
e], [DiagEmb
e])) [DiagEmb]
em
        rel' :: EquivRelTagged [DiagEmb] [DiagEmb]
rel' = ([DiagEmb] -> [DiagEmb] -> Bool)
-> EquivRelTagged [DiagEmb] [DiagEmb]
-> EquivRelTagged [DiagEmb] [DiagEmb]
forall b a.
Ord b =>
(a -> a -> Bool) -> EquivRelTagged a b -> EquivRelTagged a b
mergeEquivClassesBy [DiagEmb] -> [DiagEmb] -> Bool
diagRule EquivRelTagged [DiagEmb] [DiagEmb]
rel
        rel'' :: EquivRel [DiagEmb]
rel'' = EquivRelTagged [DiagEmb] [DiagEmb] -> EquivRel [DiagEmb]
forall b a. Ord b => EquivRelTagged a b -> EquivRel a
taggedValsToEquivClasses EquivRelTagged [DiagEmb] [DiagEmb]
rel'
        w2s :: [[DiagEmb]]
w2s = [DiagEmb] -> [DiagEmb] -> [DiagEmb] -> [[DiagEmb]]
words2 [DiagEmb]
em [DiagEmb]
em [DiagEmb]
em
        rel''' :: EquivRel [DiagEmb]
rel''' = (EquivRel [DiagEmb] -> [DiagEmb] -> EquivRel [DiagEmb])
-> EquivRel [DiagEmb] -> [[DiagEmb]] -> EquivRel [DiagEmb]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl EquivRel [DiagEmb] -> [DiagEmb] -> EquivRel [DiagEmb]
addToRel EquivRel [DiagEmb]
rel'' [[DiagEmb]]
w2s
    in EquivRel [DiagEmb]
rel'''


-- | Compute the set Adm_\simeq if it's finite.
finiteAdmSimeq :: [DiagEmb]         -- ^ the embeddings
                -> EquivRel DiagSort
                -- ^ the \simeq relation that defines admissibility
                -> Maybe [DiagEmbWord]
-- ^ returns the computed set or Nothing if it's infinite
finiteAdmSimeq :: [DiagEmb] -> EquivRel DiagSort -> Maybe [[DiagEmb]]
finiteAdmSimeq embs' :: [DiagEmb]
embs' simeq' :: EquivRel DiagSort
simeq' =
    let {- generate the list of the words over given alphabet
        with given suffix -}
        embWords' :: [DiagEmb] -> [DiagEmb] -> Int -> Maybe [[DiagEmb]]
embWords' suff :: [DiagEmb]
suff@(e :: DiagEmb
e : _) embs1 :: [DiagEmb]
embs1 pos :: Int
pos | Int
pos Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [DiagEmb] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DiagEmb]
embs1 = [[DiagEmb]] -> Maybe [[DiagEmb]]
forall a. a -> Maybe a
Just [[DiagEmb]
suff]
                                        | Bool
otherwise =
            let emb :: DiagEmb
emb = [DiagEmb]
embs1 [DiagEmb] -> Int -> DiagEmb
forall a. [a] -> Int -> a
!! Int
pos
                mws1 :: Maybe [[DiagEmb]]
mws1 = if EquivRel DiagSort -> DiagEmb -> DiagEmb -> Bool
admissible EquivRel DiagSort
simeq' DiagEmb
emb DiagEmb
e
                         then if DiagEmb -> [DiagEmb] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem DiagEmb
emb [DiagEmb]
suff
                                then Maybe [[DiagEmb]]
forall a. Maybe a
Nothing
                                else [DiagEmb] -> [DiagEmb] -> Int -> Maybe [[DiagEmb]]
embWords' (DiagEmb
emb DiagEmb -> [DiagEmb] -> [DiagEmb]
forall a. a -> [a] -> [a]
: [DiagEmb]
suff) [DiagEmb]
embs1 0
                         else [[DiagEmb]] -> Maybe [[DiagEmb]]
forall a. a -> Maybe a
Just []
                mws2 :: Maybe [[DiagEmb]]
mws2 = case Maybe [[DiagEmb]]
mws1 of
                            Nothing -> Maybe [[DiagEmb]]
forall a. Maybe a
Nothing
                            Just _ -> [DiagEmb] -> [DiagEmb] -> Int -> Maybe [[DiagEmb]]
embWords' [DiagEmb]
suff [DiagEmb]
embs1 (Int
pos Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
            in case Maybe [[DiagEmb]]
mws1 of
                    Nothing -> Maybe [[DiagEmb]]
forall a. Maybe a
Nothing
                    Just ws1 :: [[DiagEmb]]
ws1 -> case Maybe [[DiagEmb]]
mws2 of
                                     Nothing -> Maybe [[DiagEmb]]
forall a. Maybe a
Nothing
                                     Just ws2 :: [[DiagEmb]]
ws2 -> [[DiagEmb]] -> Maybe [[DiagEmb]]
forall a. a -> Maybe a
Just ([[DiagEmb]]
ws1 [[DiagEmb]] -> [[DiagEmb]] -> [[DiagEmb]]
forall a. [a] -> [a] -> [a]
++ [[DiagEmb]]
ws2)
        embWords' [] embs1 :: [DiagEmb]
embs1 pos :: Int
pos | Int
pos Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [DiagEmb] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DiagEmb]
embs1 = [[DiagEmb]] -> Maybe [[DiagEmb]]
forall a. a -> Maybe a
Just []
        embWords' [] embs1 :: [DiagEmb]
embs1 pos :: Int
pos =
            let emb :: DiagEmb
emb = [DiagEmb]
embs1 [DiagEmb] -> Int -> DiagEmb
forall a. [a] -> Int -> a
!! Int
pos
                mws1 :: Maybe [[DiagEmb]]
mws1 = [DiagEmb] -> [DiagEmb] -> Int -> Maybe [[DiagEmb]]
embWords' [DiagEmb
emb] [DiagEmb]
embs1 0
                mws2 :: Maybe [[DiagEmb]]
mws2 = case Maybe [[DiagEmb]]
mws1 of
                            Nothing -> Maybe [[DiagEmb]]
forall a. Maybe a
Nothing
                            Just _ -> [DiagEmb] -> [DiagEmb] -> Int -> Maybe [[DiagEmb]]
embWords' [] [DiagEmb]
embs1 (Int
pos Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
            in case Maybe [[DiagEmb]]
mws1 of
                    Nothing -> Maybe [[DiagEmb]]
forall a. Maybe a
Nothing
                    Just ws1 :: [[DiagEmb]]
ws1 -> case Maybe [[DiagEmb]]
mws2 of
                                     Nothing -> Maybe [[DiagEmb]]
forall a. Maybe a
Nothing
                                     Just ws2 :: [[DiagEmb]]
ws2 -> [[DiagEmb]] -> Maybe [[DiagEmb]]
forall a. a -> Maybe a
Just ([[DiagEmb]]
ws1 [[DiagEmb]] -> [[DiagEmb]] -> [[DiagEmb]]
forall a. [a] -> [a] -> [a]
++ [[DiagEmb]]
ws2)
    in [DiagEmb] -> [DiagEmb] -> Int -> Maybe [[DiagEmb]]
embWords' [] [DiagEmb]
embs' 0


-- | Check if the colimit is thin.
colimitIsThin :: EquivRel DiagSort    -- ^ the simeq relation
              -> [DiagEmb]            -- ^ the set of diagram embeddings
              -> EquivRel DiagEmbWord -- ^ the cong_0 relation
              -> Bool
colimitIsThin :: EquivRel DiagSort -> [DiagEmb] -> EquivRel [DiagEmb] -> Bool
colimitIsThin simeq' :: EquivRel DiagSort
simeq' embs' :: [DiagEmb]
embs' c0 :: EquivRel [DiagEmb]
c0 =
    let -- sortsC: a list of colimit sorts
        sortsC :: [DiagSort]
sortsC = ([DiagSort] -> [DiagSort] -> [DiagSort])
-> [DiagSort] -> EquivRel DiagSort -> [DiagSort]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ ls :: [DiagSort]
ls eqcl :: [DiagSort]
eqcl -> [DiagSort] -> DiagSort
forall a. [a] -> a
head [DiagSort]
eqcl DiagSort -> [DiagSort] -> [DiagSort]
forall a. a -> [a] -> [a]
: [DiagSort]
ls) [] EquivRel DiagSort
simeq'
        simeqT :: [(DiagSort, DiagSort)]
simeqT = EquivRel DiagSort -> [(DiagSort, DiagSort)]
forall a. Ord a => EquivRel a -> EquivRelTagged a a
equivClassesToTaggedVals EquivRel DiagSort
simeq'

     -- ordMap: map representing the topological order on sorts in the colimit
        ordMap :: Map DiagSort (Set DiagSort)
ordMap =
            let sortClasses' :: Map DiagSort (Set DiagSort)
-> [DiagEmb] -> Map DiagSort (Set DiagSort)
sortClasses' m :: Map DiagSort (Set DiagSort)
m [] = Map DiagSort (Set DiagSort)
m
                sortClasses' m :: Map DiagSort (Set DiagSort)
m ((n :: Int
n, s1 :: SORT
s1, s2 :: SORT
s2) : embs1 :: [DiagEmb]
embs1) =
                    let c1 :: DiagSort
c1 = DiagSort -> Maybe DiagSort -> DiagSort
forall a. a -> Maybe a -> a
fromMaybe (String -> DiagSort
forall a. HasCallStack => String -> a
error "sortClasses:s1")
                             (Maybe DiagSort -> DiagSort) -> Maybe DiagSort -> DiagSort
forall a b. (a -> b) -> a -> b
$ [(DiagSort, DiagSort)] -> DiagSort -> Maybe DiagSort
forall a b. Eq a => EquivRelTagged a b -> a -> Maybe b
findTag [(DiagSort, DiagSort)]
simeqT (Int
n, SORT
s1)
                        c2 :: DiagSort
c2 = DiagSort -> Maybe DiagSort -> DiagSort
forall a. a -> Maybe a -> a
fromMaybe (String -> DiagSort
forall a. HasCallStack => String -> a
error "sortClasses:s2")
                             (Maybe DiagSort -> DiagSort) -> Maybe DiagSort -> DiagSort
forall a b. (a -> b) -> a -> b
$ [(DiagSort, DiagSort)] -> DiagSort -> Maybe DiagSort
forall a b. Eq a => EquivRelTagged a b -> a -> Maybe b
findTag [(DiagSort, DiagSort)]
simeqT (Int
n, SORT
s2)
                    in Map DiagSort (Set DiagSort)
-> [DiagEmb] -> Map DiagSort (Set DiagSort)
sortClasses' ((Set DiagSort -> Maybe (Set DiagSort))
-> DiagSort
-> Map DiagSort (Set DiagSort)
-> Map DiagSort (Set DiagSort)
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update (Set DiagSort -> Maybe (Set DiagSort)
forall a. a -> Maybe a
Just (Set DiagSort -> Maybe (Set DiagSort))
-> (Set DiagSort -> Set DiagSort)
-> Set DiagSort
-> Maybe (Set DiagSort)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DiagSort -> Set DiagSort -> Set DiagSort
forall a. Ord a => a -> Set a -> Set a
Set.insert DiagSort
c2) DiagSort
c1 Map DiagSort (Set DiagSort)
m)
                        [DiagEmb]
embs1
                ordMap' :: Map DiagSort (Set a)
ordMap' = (Map DiagSort (Set a) -> DiagSort -> Map DiagSort (Set a))
-> Map DiagSort (Set a) -> [DiagSort] -> Map DiagSort (Set a)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m :: Map DiagSort (Set a)
m cl :: DiagSort
cl -> DiagSort -> Set a -> Map DiagSort (Set a) -> Map DiagSort (Set a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert DiagSort
cl Set a
forall a. Set a
Set.empty Map DiagSort (Set a)
m)
                                Map DiagSort (Set a)
forall k a. Map k a
Map.empty [DiagSort]
sortsC
            in Map DiagSort (Set DiagSort)
-> [DiagEmb] -> Map DiagSort (Set DiagSort)
sortClasses' Map DiagSort (Set DiagSort)
forall a. Map DiagSort (Set a)
ordMap' [DiagEmb]
embs'

        -- larger: return a list of colimit sorts larger than given sort
        larger :: DiagSort -> [DiagSort]
larger srt :: DiagSort
srt =
            let dl :: [DiagSort]
dl = Set DiagSort -> [DiagSort]
forall a. Set a -> [a]
Set.toList (DiagSort -> Map DiagSort (Set DiagSort) -> Set DiagSort
forall k a. Ord k => k -> Map k a -> a
findInMap DiagSort
srt Map DiagSort (Set DiagSort)
ordMap)
            in DiagSort
srt DiagSort -> [DiagSort] -> [DiagSort]
forall a. a -> [a] -> [a]
: ([DiagSort] -> DiagSort -> [DiagSort])
-> [DiagSort] -> [DiagSort] -> [DiagSort]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ l :: [DiagSort]
l so :: DiagSort
so -> [DiagSort]
l [DiagSort] -> [DiagSort] -> [DiagSort]
forall a. [a] -> [a] -> [a]
++ DiagSort -> [DiagSort]
larger DiagSort
so) [] [DiagSort]
dl

        -- s: the map representing sets S_{\geq s1,s2}
        s :: Map (DiagSort, DiagSort) (Set DiagSort)
s = let compS :: Map (DiagSort, DiagSort) (Set DiagSort)
-> (DiagSort, DiagSort) -> Map (DiagSort, DiagSort) (Set DiagSort)
compS m :: Map (DiagSort, DiagSort) (Set DiagSort)
m (s1 :: DiagSort
s1, s2 :: DiagSort
s2) =
                    let ls1 :: Set DiagSort
ls1 = [DiagSort] -> Set DiagSort
forall a. Ord a => [a] -> Set a
Set.fromList (DiagSort -> [DiagSort]
larger DiagSort
s1)
                        ls2 :: Set DiagSort
ls2 = [DiagSort] -> Set DiagSort
forall a. Ord a => [a] -> Set a
Set.fromList (DiagSort -> [DiagSort]
larger DiagSort
s2)
                    in (DiagSort, DiagSort)
-> Set DiagSort
-> Map (DiagSort, DiagSort) (Set DiagSort)
-> Map (DiagSort, DiagSort) (Set DiagSort)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (DiagSort
s1, DiagSort
s2) (Set DiagSort -> Set DiagSort -> Set DiagSort
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set DiagSort
ls1 Set DiagSort
ls2) Map (DiagSort, DiagSort) (Set DiagSort)
m
            in (Map (DiagSort, DiagSort) (Set DiagSort)
 -> (DiagSort, DiagSort) -> Map (DiagSort, DiagSort) (Set DiagSort))
-> Map (DiagSort, DiagSort) (Set DiagSort)
-> [(DiagSort, DiagSort)]
-> Map (DiagSort, DiagSort) (Set DiagSort)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map (DiagSort, DiagSort) (Set DiagSort)
-> (DiagSort, DiagSort) -> Map (DiagSort, DiagSort) (Set DiagSort)
compS Map (DiagSort, DiagSort) (Set DiagSort)
forall k a. Map k a
Map.empty [(DiagSort
s1, DiagSort
s2) | DiagSort
s1 <- [DiagSort]
sortsC, DiagSort
s2 <- [DiagSort]
sortsC]

        -- b: the map representing sets B_{s1,s2}
        b :: Map (DiagSort, DiagSort) (EquivRel DiagSort)
b = let compB :: Map (DiagSort, DiagSort) (EquivRel DiagSort)
-> (DiagSort, DiagSort)
-> Map (DiagSort, DiagSort) (EquivRel DiagSort)
compB m :: Map (DiagSort, DiagSort) (EquivRel DiagSort)
m sp :: (DiagSort, DiagSort)
sp =
                    let sim' :: DiagSort -> DiagSort -> Bool
sim' s' :: DiagSort
s' s'' :: DiagSort
s'' = Bool -> Bool
not (Set DiagSort -> Bool
forall a. Set a -> Bool
Set.null ((DiagSort, DiagSort)
-> Map (DiagSort, DiagSort) (Set DiagSort) -> Set DiagSort
forall k a. Ord k => k -> Map k a -> a
findInMap (DiagSort
s', DiagSort
s'') Map (DiagSort, DiagSort) (Set DiagSort)
s))
                        rel :: [(DiagSort, DiagSort)]
rel = (DiagSort -> (DiagSort, DiagSort))
-> [DiagSort] -> [(DiagSort, DiagSort)]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: DiagSort
x -> (DiagSort
x, DiagSort
x)) (Set DiagSort -> [DiagSort]
forall a. Set a -> [a]
Set.toList ((DiagSort, DiagSort)
-> Map (DiagSort, DiagSort) (Set DiagSort) -> Set DiagSort
forall k a. Ord k => k -> Map k a -> a
findInMap (DiagSort, DiagSort)
sp Map (DiagSort, DiagSort) (Set DiagSort)
s))
                        rel' :: [(DiagSort, DiagSort)]
rel' = (DiagSort -> DiagSort -> Bool)
-> [(DiagSort, DiagSort)] -> [(DiagSort, DiagSort)]
forall b a.
Ord b =>
(a -> a -> Bool) -> EquivRelTagged a b -> EquivRelTagged a b
mergeEquivClassesBy DiagSort -> DiagSort -> Bool
sim' [(DiagSort, DiagSort)]
rel
                    in (DiagSort, DiagSort)
-> EquivRel DiagSort
-> Map (DiagSort, DiagSort) (EquivRel DiagSort)
-> Map (DiagSort, DiagSort) (EquivRel DiagSort)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (DiagSort, DiagSort)
sp ([(DiagSort, DiagSort)] -> EquivRel DiagSort
forall b a. Ord b => EquivRelTagged a b -> EquivRel a
taggedValsToEquivClasses [(DiagSort, DiagSort)]
rel') Map (DiagSort, DiagSort) (EquivRel DiagSort)
m
            in (Map (DiagSort, DiagSort) (EquivRel DiagSort)
 -> (DiagSort, DiagSort)
 -> Map (DiagSort, DiagSort) (EquivRel DiagSort))
-> Map (DiagSort, DiagSort) (EquivRel DiagSort)
-> [(DiagSort, DiagSort)]
-> Map (DiagSort, DiagSort) (EquivRel DiagSort)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map (DiagSort, DiagSort) (EquivRel DiagSort)
-> (DiagSort, DiagSort)
-> Map (DiagSort, DiagSort) (EquivRel DiagSort)
compB Map (DiagSort, DiagSort) (EquivRel DiagSort)
forall k a. Map k a
Map.empty [(DiagSort
s1, DiagSort
s2) | DiagSort
s1 <- [DiagSort]
sortsC, DiagSort
s2 <- [DiagSort]
sortsC]

        embDomS :: (Int, SORT, c) -> DiagSort
embDomS (n :: Int
n, dom :: SORT
dom, _) = DiagSort -> Maybe DiagSort -> DiagSort
forall a. a -> Maybe a -> a
fromMaybe (String -> DiagSort
forall a. HasCallStack => String -> a
error "embDomS")
                              (Maybe DiagSort -> DiagSort) -> Maybe DiagSort -> DiagSort
forall a b. (a -> b) -> a -> b
$ [(DiagSort, DiagSort)] -> DiagSort -> Maybe DiagSort
forall a b. Eq a => EquivRelTagged a b -> a -> Maybe b
findTag [(DiagSort, DiagSort)]
simeqT (Int
n, SORT
dom)
        embCodS :: (Int, b, SORT) -> DiagSort
embCodS (n :: Int
n, _, cod :: SORT
cod) = DiagSort -> Maybe DiagSort -> DiagSort
forall a. a -> Maybe a -> a
fromMaybe (String -> DiagSort
forall a. HasCallStack => String -> a
error "embCodS")
                               (Maybe DiagSort -> DiagSort) -> Maybe DiagSort -> DiagSort
forall a b. (a -> b) -> a -> b
$ [(DiagSort, DiagSort)] -> DiagSort -> Maybe DiagSort
forall a b. Eq a => EquivRelTagged a b -> a -> Maybe b
findTag [(DiagSort, DiagSort)]
simeqT (Int
n, SORT
cod)
        -- checkAllSorts: check the C = B condition for all colimit sorts
        checkAllSorts :: Map DiagSort (Set DiagSort) -> Bool
checkAllSorts m :: Map DiagSort (Set DiagSort)
m | Map DiagSort (Set DiagSort) -> Bool
forall k a. Map k a -> Bool
Map.null Map DiagSort (Set DiagSort)
m = {- trace "CT: Yes" -} Bool
True
                        | Bool
otherwise =
            let -- checkSort: check if for given colimit sort C = B
          checkSort :: DiagSort -> Bool
checkSort chs :: DiagSort
chs = let
            embsCs :: [DiagEmb]
embsCs = (DiagEmb -> Bool) -> [DiagEmb] -> [DiagEmb]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ e :: DiagEmb
e -> DiagEmb -> DiagSort
forall c. (Int, SORT, c) -> DiagSort
embDomS DiagEmb
e DiagSort -> DiagSort -> Bool
forall a. Eq a => a -> a -> Bool
== DiagSort
chs) [DiagEmb]
embs'
            c :: Map (DiagEmb, DiagEmb) [a]
c = (Map (DiagEmb, DiagEmb) [a]
 -> (DiagEmb, DiagEmb) -> Map (DiagEmb, DiagEmb) [a])
-> Map (DiagEmb, DiagEmb) [a]
-> [(DiagEmb, DiagEmb)]
-> Map (DiagEmb, DiagEmb) [a]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ ma :: Map (DiagEmb, DiagEmb) [a]
ma ep :: (DiagEmb, DiagEmb)
ep -> (DiagEmb, DiagEmb)
-> [a] -> Map (DiagEmb, DiagEmb) [a] -> Map (DiagEmb, DiagEmb) [a]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (DiagEmb, DiagEmb)
ep [] Map (DiagEmb, DiagEmb) [a]
ma) Map (DiagEmb, DiagEmb) [a]
forall k a. Map k a
Map.empty
                [(DiagEmb
d, DiagEmb
e) | DiagEmb
d <- [DiagEmb]
embsCs, DiagEmb
e <- [DiagEmb]
embsCs]
            c' :: Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
c' = let
              updC :: Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
-> ((Int, b, SORT), (Int, b, SORT))
-> Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
updC c1 :: Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
c1 (d :: (Int, b, SORT)
d, e :: (Int, b, SORT)
e) = let
                s1 :: DiagSort
s1 = (Int, b, SORT) -> DiagSort
forall b. (Int, b, SORT) -> DiagSort
embCodS (Int, b, SORT)
d
                s2 :: DiagSort
s2 = (Int, b, SORT) -> DiagSort
forall b. (Int, b, SORT) -> DiagSort
embCodS (Int, b, SORT)
e
                in (EquivRel DiagSort -> Maybe (EquivRel DiagSort))
-> ((Int, b, SORT), (Int, b, SORT))
-> Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
-> Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update (\ _ -> EquivRel DiagSort -> Maybe (EquivRel DiagSort)
forall a. a -> Maybe a
Just ((DiagSort, DiagSort)
-> Map (DiagSort, DiagSort) (EquivRel DiagSort)
-> EquivRel DiagSort
forall k a. Ord k => k -> Map k a -> a
findInMap (DiagSort
s1, DiagSort
s2) Map (DiagSort, DiagSort) (EquivRel DiagSort)
b)) ((Int, b, SORT)
d, (Int, b, SORT)
e) Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
c1
              in (Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
 -> (DiagEmb, DiagEmb)
 -> Map (DiagEmb, DiagEmb) (EquivRel DiagSort))
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
-> [(DiagEmb, DiagEmb)]
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
-> (DiagEmb, DiagEmb) -> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
forall b b.
(Ord b, Ord b) =>
Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
-> ((Int, b, SORT), (Int, b, SORT))
-> Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
updC Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
forall a. Map (DiagEmb, DiagEmb) [a]
c
                     [(DiagEmb
d, DiagEmb
e) | DiagEmb
d <- [DiagEmb]
embsCs, DiagEmb
e <- [DiagEmb]
embsCs, EquivRel [DiagEmb] -> [DiagEmb] -> [DiagEmb] -> Bool
forall a. Eq a => EquivRel a -> a -> a -> Bool
inRel EquivRel [DiagEmb]
c0 [DiagEmb
d] [DiagEmb
e]]
            c'' :: Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
c'' = let
              updC :: Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
-> (DiagEmb, DiagEmb) -> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
updC c1 :: Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
c1 (d :: DiagEmb
d@(n1 :: Int
n1, _, cod1 :: SORT
cod1), e :: DiagEmb
e@(n2 :: Int
n2, _, cod2 :: SORT
cod2)) = let
                s1 :: DiagSort
s1 = DiagEmb -> DiagSort
forall b. (Int, b, SORT) -> DiagSort
embCodS DiagEmb
d
                s2 :: DiagSort
s2 = DiagEmb -> DiagSort
forall b. (Int, b, SORT) -> DiagSort
embCodS DiagEmb
e
                in if Bool -> Bool
not ((DiagEmb -> Bool) -> [DiagEmb] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ (n :: Int
n, dom :: SORT
dom, cod :: SORT
cod) -> (Int
n, SORT
dom) DiagSort -> DiagSort -> Bool
forall a. Eq a => a -> a -> Bool
== (Int
n1, SORT
cod1)
                              Bool -> Bool -> Bool
&& (Int
n, SORT
cod) DiagSort -> DiagSort -> Bool
forall a. Eq a => a -> a -> Bool
== (Int
n2, SORT
cod2)) [DiagEmb]
embs')
                   then Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
forall a. Map (DiagEmb, DiagEmb) [a]
c else let
                   [absCls :: [DiagSort]
absCls] = ([DiagSort] -> Bool) -> EquivRel DiagSort -> EquivRel DiagSort
forall a. (a -> Bool) -> [a] -> [a]
filter (DiagSort -> [DiagSort] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem DiagSort
s2) ((DiagSort, DiagSort)
-> Map (DiagSort, DiagSort) (EquivRel DiagSort)
-> EquivRel DiagSort
forall k a. Ord k => k -> Map k a -> a
findInMap (DiagSort
s1, DiagSort
s2) Map (DiagSort, DiagSort) (EquivRel DiagSort)
b)
                   in (Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
 -> (DiagEmb, DiagEmb)
 -> Map (DiagEmb, DiagEmb) (EquivRel DiagSort))
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
-> [(DiagEmb, DiagEmb)]
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (((DiagEmb, DiagEmb)
 -> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
 -> Map (DiagEmb, DiagEmb) (EquivRel DiagSort))
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
-> (DiagEmb, DiagEmb)
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((DiagEmb, DiagEmb)
  -> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
  -> Map (DiagEmb, DiagEmb) (EquivRel DiagSort))
 -> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
 -> (DiagEmb, DiagEmb)
 -> Map (DiagEmb, DiagEmb) (EquivRel DiagSort))
-> ((DiagEmb, DiagEmb)
    -> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
    -> Map (DiagEmb, DiagEmb) (EquivRel DiagSort))
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
-> (DiagEmb, DiagEmb)
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
forall a b. (a -> b) -> a -> b
$ (EquivRel DiagSort -> Maybe (EquivRel DiagSort))
-> (DiagEmb, DiagEmb)
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update (\ l :: EquivRel DiagSort
l -> EquivRel DiagSort -> Maybe (EquivRel DiagSort)
forall a. a -> Maybe a
Just
                          (EquivRel DiagSort
l EquivRel DiagSort -> EquivRel DiagSort -> EquivRel DiagSort
forall a. [a] -> [a] -> [a]
++ [[DiagSort]
absCls]))) Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
c1 [(DiagEmb
d, DiagEmb
e), (DiagEmb
e, DiagEmb
d)]
              in (Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
 -> (DiagEmb, DiagEmb)
 -> Map (DiagEmb, DiagEmb) (EquivRel DiagSort))
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
-> [(DiagEmb, DiagEmb)]
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
-> (DiagEmb, DiagEmb) -> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
updC Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
c' [(DiagEmb
d, DiagEmb
e) | DiagEmb
d <- [DiagEmb]
embsCs,
                                DiagEmb
e <- [DiagEmb]
embsCs, [DiagEmb] -> DiagSort
wordDom [DiagEmb
d] DiagSort -> DiagSort -> Bool
forall a. Eq a => a -> a -> Bool
== [DiagEmb] -> DiagSort
wordDom [DiagEmb
e]]
            fixUpdRule :: Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
fixUpdRule cFix :: Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
cFix = let
              updC :: Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
-> ((Int, b, SORT), (Int, b, SORT), (Int, b, SORT))
-> Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
updC c1 :: Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
c1 (e1 :: (Int, b, SORT)
e1, e2 :: (Int, b, SORT)
e2, e3 :: (Int, b, SORT)
e3) = let
                updC' :: Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
-> ([a], [a], [a]) -> Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
updC' c2 :: Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
c2 (b12 :: [a]
b12, b23 :: [a]
b23, b13 :: [a]
b13) = let
                  sb12 :: Set a
sb12 = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a]
b12
                  sb23 :: Set a
sb23 = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a]
b23
                  sb13 :: Set a
sb13 = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a]
b13
                  comm :: Set a
comm = Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set a
sb12 (Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set a
sb23 Set a
sb13)
                  in if Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
comm then Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
c2 else let
                    c2' :: Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
c2' = if [a] -> [[a]] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [a]
b13 (((Int, b, SORT), (Int, b, SORT))
-> Map ((Int, b, SORT), (Int, b, SORT)) [[a]] -> [[a]]
forall k a. Ord k => k -> Map k a -> a
findInMap ((Int, b, SORT)
e1, (Int, b, SORT)
e3) Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
c2)
                         then Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
c2
                         else ([[a]] -> Maybe [[a]])
-> ((Int, b, SORT), (Int, b, SORT))
-> Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
-> Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update (\ l :: [[a]]
l -> [[a]] -> Maybe [[a]]
forall a. a -> Maybe a
Just ([[a]]
l [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ [[a]
b13])) ((Int, b, SORT)
e1, (Int, b, SORT)
e3) Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
c2
                    in if [a] -> [[a]] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [a]
b13 (((Int, b, SORT), (Int, b, SORT))
-> Map ((Int, b, SORT), (Int, b, SORT)) [[a]] -> [[a]]
forall k a. Ord k => k -> Map k a -> a
findInMap ((Int, b, SORT)
e1, (Int, b, SORT)
e3) Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
c2')
                       then Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
c2'
                       else ([[a]] -> Maybe [[a]])
-> ((Int, b, SORT), (Int, b, SORT))
-> Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
-> Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update (\ l :: [[a]]
l -> [[a]] -> Maybe [[a]]
forall a. a -> Maybe a
Just ([[a]]
l [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ [[a]
b13])) ((Int, b, SORT)
e3, (Int, b, SORT)
e1) Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
c2'
                s1 :: DiagSort
s1 = (Int, b, SORT) -> DiagSort
forall b. (Int, b, SORT) -> DiagSort
embCodS (Int, b, SORT)
e1
                s3 :: DiagSort
s3 = (Int, b, SORT) -> DiagSort
forall b. (Int, b, SORT) -> DiagSort
embCodS (Int, b, SORT)
e3
                in (Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
 -> ([DiagSort], [DiagSort], [DiagSort])
 -> Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort))
-> Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
-> [([DiagSort], [DiagSort], [DiagSort])]
-> Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
-> ([DiagSort], [DiagSort], [DiagSort])
-> Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
forall a.
Ord a =>
Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
-> ([a], [a], [a]) -> Map ((Int, b, SORT), (Int, b, SORT)) [[a]]
updC' Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
c1 [ ([DiagSort]
b12, [DiagSort]
b23, [DiagSort]
b13)
                                  | [DiagSort]
b12 <- ((Int, b, SORT), (Int, b, SORT))
-> Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
-> EquivRel DiagSort
forall k a. Ord k => k -> Map k a -> a
findInMap ((Int, b, SORT)
e1, (Int, b, SORT)
e2) Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
c1
                                  , [DiagSort]
b23 <- ((Int, b, SORT), (Int, b, SORT))
-> Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
-> EquivRel DiagSort
forall k a. Ord k => k -> Map k a -> a
findInMap ((Int, b, SORT)
e2, (Int, b, SORT)
e3) Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
c1
                                  , [DiagSort]
b13 <- (DiagSort, DiagSort)
-> Map (DiagSort, DiagSort) (EquivRel DiagSort)
-> EquivRel DiagSort
forall k a. Ord k => k -> Map k a -> a
findInMap (DiagSort
s1, DiagSort
s3) Map (DiagSort, DiagSort) (EquivRel DiagSort)
b ]
              cFix' :: Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
cFix' = (Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
 -> (DiagEmb, DiagEmb, DiagEmb)
 -> Map (DiagEmb, DiagEmb) (EquivRel DiagSort))
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
-> [(DiagEmb, DiagEmb, DiagEmb)]
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
-> (DiagEmb, DiagEmb, DiagEmb)
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
forall b.
Ord b =>
Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
-> ((Int, b, SORT), (Int, b, SORT), (Int, b, SORT))
-> Map ((Int, b, SORT), (Int, b, SORT)) (EquivRel DiagSort)
updC Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
cFix [(DiagEmb
e1, DiagEmb
e2, DiagEmb
e3) |
                                DiagEmb
e1 <- [DiagEmb]
embsCs, DiagEmb
e2 <- [DiagEmb]
embsCs, DiagEmb
e3 <- [DiagEmb]
embsCs]
              in if Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
cFix' Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort) -> Bool
forall a. Eq a => a -> a -> Bool
== Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
cFix then Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
cFix else Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
fixUpdRule Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
cFix'
            c3 :: Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
c3 = Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
fixUpdRule Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
c''
            checkIncl :: [(DiagEmb, DiagEmb)] -> Bool
checkIncl [] = Bool
True
            checkIncl ((e1 :: DiagEmb
e1, e2 :: DiagEmb
e2) : embprs :: [(DiagEmb, DiagEmb)]
embprs) = let
              s1 :: DiagSort
s1 = DiagEmb -> DiagSort
forall b. (Int, b, SORT) -> DiagSort
embCodS DiagEmb
e1
              s2 :: DiagSort
s2 = DiagEmb -> DiagSort
forall b. (Int, b, SORT) -> DiagSort
embCodS DiagEmb
e2
              res :: Bool
res = Maybe (DiagSort, DiagSort) -> Bool
forall a. Maybe a -> Bool
isNothing (EquivRel DiagSort
-> EquivRel DiagSort -> Maybe (DiagSort, DiagSort)
forall a. Eq a => EquivRel a -> EquivRel a -> Maybe (a, a)
subRelation ((DiagSort, DiagSort)
-> Map (DiagSort, DiagSort) (EquivRel DiagSort)
-> EquivRel DiagSort
forall k a. Ord k => k -> Map k a -> a
findInMap (DiagSort
s1, DiagSort
s2) Map (DiagSort, DiagSort) (EquivRel DiagSort)
b)
                    ((DiagEmb, DiagEmb)
-> Map (DiagEmb, DiagEmb) (EquivRel DiagSort) -> EquivRel DiagSort
forall k a. Ord k => k -> Map k a -> a
findInMap (DiagEmb
e1, DiagEmb
e2) Map (DiagEmb, DiagEmb) (EquivRel DiagSort)
c3)) Bool -> Bool -> Bool
&& [(DiagEmb, DiagEmb)] -> Bool
checkIncl [(DiagEmb, DiagEmb)]
embprs
              in Bool
res
            in [(DiagEmb, DiagEmb)] -> Bool
checkIncl [(DiagEmb
e1, DiagEmb
e2) | DiagEmb
e1 <- [DiagEmb]
embsCs, DiagEmb
e2 <- [DiagEmb]
embsCs]
                {- cs: next colimit sort to process
                m1: the order map with cs removed -}
          (cs :: DiagSort
cs, m1 :: Map DiagSort (Set DiagSort)
m1) = let
            [(cs' :: DiagSort
cs', _)] = Int -> [(DiagSort, Set DiagSort)] -> [(DiagSort, Set DiagSort)]
forall a. Int -> [a] -> [a]
take 1 (((DiagSort, Set DiagSort) -> Bool)
-> [(DiagSort, Set DiagSort)] -> [(DiagSort, Set DiagSort)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, lt :: Set DiagSort
lt) -> Set DiagSort -> Bool
forall a. Set a -> Bool
Set.null Set DiagSort
lt)
                                                          (Map DiagSort (Set DiagSort) -> [(DiagSort, Set DiagSort)]
forall k a. Map k a -> [(k, a)]
Map.toList Map DiagSort (Set DiagSort)
m))
            m' :: Map DiagSort (Set DiagSort)
m' = DiagSort
-> Map DiagSort (Set DiagSort) -> Map DiagSort (Set DiagSort)
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete DiagSort
cs' Map DiagSort (Set DiagSort)
m
            m'' :: Map DiagSort (Set DiagSort)
m'' = (Map DiagSort (Set DiagSort)
 -> DiagSort -> Map DiagSort (Set DiagSort))
-> Map DiagSort (Set DiagSort)
-> [DiagSort]
-> Map DiagSort (Set DiagSort)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((DiagSort
 -> Map DiagSort (Set DiagSort) -> Map DiagSort (Set DiagSort))
-> Map DiagSort (Set DiagSort)
-> DiagSort
-> Map DiagSort (Set DiagSort)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((DiagSort
  -> Map DiagSort (Set DiagSort) -> Map DiagSort (Set DiagSort))
 -> Map DiagSort (Set DiagSort)
 -> DiagSort
 -> Map DiagSort (Set DiagSort))
-> (DiagSort
    -> Map DiagSort (Set DiagSort) -> Map DiagSort (Set DiagSort))
-> Map DiagSort (Set DiagSort)
-> DiagSort
-> Map DiagSort (Set DiagSort)
forall a b. (a -> b) -> a -> b
$ (Set DiagSort -> Maybe (Set DiagSort))
-> DiagSort
-> Map DiagSort (Set DiagSort)
-> Map DiagSort (Set DiagSort)
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update (Set DiagSort -> Maybe (Set DiagSort)
forall a. a -> Maybe a
Just (Set DiagSort -> Maybe (Set DiagSort))
-> (Set DiagSort -> Set DiagSort)
-> Set DiagSort
-> Maybe (Set DiagSort)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DiagSort -> Set DiagSort -> Set DiagSort
forall a. Ord a => a -> Set a -> Set a
Set.delete DiagSort
cs))
                                           Map DiagSort (Set DiagSort)
m' (Map DiagSort (Set DiagSort) -> [DiagSort]
forall k a. Map k a -> [k]
Map.keys Map DiagSort (Set DiagSort)
m')
            in (DiagSort
cs', Map DiagSort (Set DiagSort)
m'')
          in DiagSort -> Bool
checkSort DiagSort
cs Bool -> Bool -> Bool
&& Map DiagSort (Set DiagSort) -> Bool
checkAllSorts Map DiagSort (Set DiagSort)
m1
        in Map DiagSort (Set DiagSort) -> Bool
checkAllSorts Map DiagSort (Set DiagSort)
ordMap

{- the old, unoptimised version of cong:
-- | Compute the \cong relation given its (finite) domain
cong :: CASLDiag
     -> [DiagEmbWord]    -- ^ the Adm_\simeq set (the domain of \cong relation)
     -> EquivRel DiagSort -- ^ the \simeq relation
     -> EquivRel DiagEmbWord
cong diag adm simeq =
    -- domCodEqual: check that domains and codomains of given words are equal
    let domCodEqual w1 w2 =
               wordDom w1 == wordDom w2 && wordCod w1 == wordCod w2

        -- diagRule: the Diag rule
        diagRule [(n1, s11, s12)] [(n2, s21, s22)] =
            isMorphSort diag (n1, s11) (n2, s21) && isMorphSort diag (n1, s12)
            (n2, s22) ||
            isMorphSort diag (n2, s21) (n1, s11) && isMorphSort diag (n2, s22)
            (n1, s12)
        diagRule _ _ = False

        -- compRule: the Comp rule works for words 1 and 2-letter long
        -- with equal domains and codomains
        compRule w1@[_] w2@[_, _] = domCodEqual w1 w2
        compRule w1@[_, _] w2@[_] = domCodEqual w1 w2
        compRule _ _ = False

        -- fixCongLc: apply Cong and Lc rules until a fixpoint is reached
        fixCongLc rel =
            let rel' = (leftCancellableClosure . congruenceClosure simeq) rel
            in if rel == rel' then rel else fixCongLc rel'

        -- compute the relation
        rel = map (\w -> (w, w)) adm
        rel' = mergeEquivClassesBy diagRule rel
        rel'' = mergeEquivClassesBy compRule rel'
        rel''' = fixCongLc rel''
    in taggedValsToEquivClasses rel'''
-}

{- | Compute the (optimised) \cong relation given its (finite) domain
and \sim relation. Optimised \cong is supposed to contain only words
composed of canonical embeddings; we also use a (CompDiag) rule
instead of (Comp) and (Diag) rules. -}
cong :: CASLDiag
     -> [DiagEmbWord]    -- ^ the Adm_\simeq set (the domain of \cong relation)
     -> EquivRel DiagSort -- ^ the \simeq relation
     -> EquivRel DiagEmb  -- ^ the \sim relation
     -> EquivRel DiagEmbWord
cong :: CASLDiag
-> [[DiagEmb]]
-> EquivRel DiagSort
-> [[DiagEmb]]
-> EquivRel [DiagEmb]
cong diag :: CASLDiag
diag adm :: [[DiagEmb]]
adm simeq' :: EquivRel DiagSort
simeq' sim' :: [[DiagEmb]]
sim' =
    -- domCodEqual: check that domains and codomains of given words are equal
    let _domCodEqual :: [DiagEmb] -> [DiagEmb] -> Bool
_domCodEqual w1 :: [DiagEmb]
w1 w2 :: [DiagEmb]
w2 =
               [DiagEmb] -> DiagSort
wordDom [DiagEmb]
w1 DiagSort -> DiagSort -> Bool
forall a. Eq a => a -> a -> Bool
== [DiagEmb] -> DiagSort
wordDom [DiagEmb]
w2 Bool -> Bool -> Bool
&& [DiagEmb] -> DiagSort
wordCod [DiagEmb]
w1 DiagSort -> DiagSort -> Bool
forall a. Eq a => a -> a -> Bool
== [DiagEmb] -> DiagSort
wordCod [DiagEmb]
w2

        -- diagRule: the Diag rule
        _diagRule :: [DiagEmb] -> [DiagEmb] -> Bool
_diagRule [(n1 :: Int
n1, s11 :: SORT
s11, s12 :: SORT
s12)] [(n2 :: Int
n2, s21 :: SORT
s21, s22 :: SORT
s22)] =
            CASLDiag -> DiagSort -> DiagSort -> Bool
isMorphSort CASLDiag
diag (Int
n1, SORT
s11) (Int
n2, SORT
s21)
                 Bool -> Bool -> Bool
&& CASLDiag -> DiagSort -> DiagSort -> Bool
isMorphSort CASLDiag
diag (Int
n1, SORT
s12) (Int
n2, SORT
s22)
            Bool -> Bool -> Bool
|| CASLDiag -> DiagSort -> DiagSort -> Bool
isMorphSort CASLDiag
diag (Int
n2, SORT
s21) (Int
n1, SORT
s11)
                   Bool -> Bool -> Bool
&& CASLDiag -> DiagSort -> DiagSort -> Bool
isMorphSort CASLDiag
diag (Int
n2, SORT
s22) (Int
n1, SORT
s12)
        _diagRule _ _ = Bool
False

        -- compDiagRule: the combination of Comp and Diag rules
        compDiagRule :: [DiagEmb] -> [DiagEmb] -> Bool
compDiagRule w1 :: [DiagEmb]
w1@[_] w2 :: [DiagEmb]
w2@[_, _] = [DiagEmb] -> [DiagEmb] -> Bool
compDiagRule [DiagEmb]
w2 [DiagEmb]
w1
        compDiagRule [e1 :: DiagEmb
e1, e2 :: DiagEmb
e2] [d :: DiagEmb
d] =
            let findSim :: DiagEmb -> [[DiagEmb]]
findSim e3 :: DiagEmb
e3 = ([DiagEmb] -> Bool) -> [[DiagEmb]] -> [[DiagEmb]]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ l :: [DiagEmb]
l -> let e :: DiagEmb
e : _ = [DiagEmb]
l in DiagEmb
e DiagEmb -> DiagEmb -> Bool
forall a. Eq a => a -> a -> Bool
== DiagEmb
e3) [[DiagEmb]]
sim'
                [ec1 :: [DiagEmb]
ec1] = DiagEmb -> [[DiagEmb]]
findSim DiagEmb
e1
                [ec2 :: [DiagEmb]
ec2] = DiagEmb -> [[DiagEmb]]
findSim DiagEmb
e2
                matches' :: [((Int, b, SORT), (Int, SORT, c))] -> Bool
matches' [] = Bool
False
                matches' (((n1 :: Int
n1, _, s12 :: SORT
s12), (n2 :: Int
n2, s21 :: SORT
s21, _)) : eps :: [((Int, b, SORT), (Int, SORT, c))]
eps) =
                    Int
n1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n2 Bool -> Bool -> Bool
&& [[DiagEmb]] -> DiagEmb -> DiagEmb -> Bool
forall a. Eq a => EquivRel a -> a -> a -> Bool
inRel [[DiagEmb]]
sim' DiagEmb
d (Int
n1, SORT
s21, SORT
s12)
                    Bool -> Bool -> Bool
|| [((Int, b, SORT), (Int, SORT, c))] -> Bool
matches' [((Int, b, SORT), (Int, SORT, c))]
eps
            in [(DiagEmb, DiagEmb)] -> Bool
forall b c. [((Int, b, SORT), (Int, SORT, c))] -> Bool
matches' [(DiagEmb
me1, DiagEmb
me2) | DiagEmb
me1 <- [DiagEmb]
ec1, DiagEmb
me2 <- [DiagEmb]
ec2]
        compDiagRule _ _ = Bool
False

        -- fixCongLc: apply Cong and Lc rules until a fixpoint is reached
        fixCongLc :: EquivRelTagged [DiagEmb] [DiagEmb]
-> EquivRelTagged [DiagEmb] [DiagEmb]
fixCongLc rel1 :: EquivRelTagged [DiagEmb] [DiagEmb]
rel1 =
            let rel2 :: EquivRelTagged [DiagEmb] [DiagEmb]
rel2 = (EquivRelTagged [DiagEmb] [DiagEmb]
-> EquivRelTagged [DiagEmb] [DiagEmb]
leftCancellableClosure (EquivRelTagged [DiagEmb] [DiagEmb]
 -> EquivRelTagged [DiagEmb] [DiagEmb])
-> (EquivRelTagged [DiagEmb] [DiagEmb]
    -> EquivRelTagged [DiagEmb] [DiagEmb])
-> EquivRelTagged [DiagEmb] [DiagEmb]
-> EquivRelTagged [DiagEmb] [DiagEmb]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                        ([DiagEmb] -> [DiagEmb] -> Bool)
-> ([DiagEmb] -> [DiagEmb] -> [DiagEmb])
-> EquivRelTagged [DiagEmb] [DiagEmb]
-> EquivRelTagged [DiagEmb] [DiagEmb]
forall a b.
(Eq a, Eq b) =>
(a -> a -> Bool)
-> (a -> a -> a) -> EquivRelTagged a b -> EquivRelTagged a b
congruenceClosure (\ w1 :: [DiagEmb]
w1 w2 :: [DiagEmb]
w2 ->
                                 EquivRel DiagSort -> DiagSort -> DiagSort -> Bool
forall a. Eq a => EquivRel a -> a -> a -> Bool
inRel EquivRel DiagSort
simeq' ([DiagEmb] -> DiagSort
wordCod [DiagEmb]
w1) ([DiagEmb] -> DiagSort
wordDom [DiagEmb]
w2))
                                          (([DiagEmb] -> [DiagEmb] -> [DiagEmb])
-> [DiagEmb] -> [DiagEmb] -> [DiagEmb]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [DiagEmb] -> [DiagEmb] -> [DiagEmb]
forall a. [a] -> [a] -> [a]
(++))) EquivRelTagged [DiagEmb] [DiagEmb]
rel1
            in if EquivRelTagged [DiagEmb] [DiagEmb]
rel1 EquivRelTagged [DiagEmb] [DiagEmb]
-> EquivRelTagged [DiagEmb] [DiagEmb] -> Bool
forall a. Eq a => a -> a -> Bool
== EquivRelTagged [DiagEmb] [DiagEmb]
rel2 then EquivRelTagged [DiagEmb] [DiagEmb]
rel1 else EquivRelTagged [DiagEmb] [DiagEmb]
-> EquivRelTagged [DiagEmb] [DiagEmb]
fixCongLc EquivRelTagged [DiagEmb] [DiagEmb]
rel2

        -- compute the relation
        rel :: EquivRelTagged [DiagEmb] [DiagEmb]
rel = ([DiagEmb] -> ([DiagEmb], [DiagEmb]))
-> [[DiagEmb]] -> EquivRelTagged [DiagEmb] [DiagEmb]
forall a b. (a -> b) -> [a] -> [b]
map (\ w :: [DiagEmb]
w -> ([DiagEmb]
w, [DiagEmb]
w)) [[DiagEmb]]
adm
        rel' :: EquivRelTagged [DiagEmb] [DiagEmb]
rel' = ([DiagEmb] -> [DiagEmb] -> Bool)
-> EquivRelTagged [DiagEmb] [DiagEmb]
-> EquivRelTagged [DiagEmb] [DiagEmb]
forall b a.
Ord b =>
(a -> a -> Bool) -> EquivRelTagged a b -> EquivRelTagged a b
mergeEquivClassesBy [DiagEmb] -> [DiagEmb] -> Bool
compDiagRule EquivRelTagged [DiagEmb] [DiagEmb]
rel
        rel'' :: EquivRelTagged [DiagEmb] [DiagEmb]
rel'' = EquivRelTagged [DiagEmb] [DiagEmb]
-> EquivRelTagged [DiagEmb] [DiagEmb]
fixCongLc EquivRelTagged [DiagEmb] [DiagEmb]
rel'
    in EquivRelTagged [DiagEmb] [DiagEmb] -> EquivRel [DiagEmb]
forall b a. Ord b => EquivRelTagged a b -> EquivRel a
taggedValsToEquivClasses EquivRelTagged [DiagEmb] [DiagEmb]
rel''


-- | Compute the \cong^R relation
congR :: CASLDiag
      -> EquivRel DiagSort -- ^ the \simeq relation
      -> EquivRel DiagEmb  -- ^ the \sim relation
      -> EquivRel DiagEmbWord
congR :: CASLDiag -> EquivRel DiagSort -> [[DiagEmb]] -> EquivRel [DiagEmb]
congR diag :: CASLDiag
diag simeq' :: EquivRel DiagSort
simeq' sim' :: [[DiagEmb]]
sim' =
    -- cong diag (looplessWords (embs diag) simeq) simeq
    CASLDiag
-> [[DiagEmb]]
-> EquivRel DiagSort
-> [[DiagEmb]]
-> EquivRel [DiagEmb]
cong CASLDiag
diag ([DiagEmb] -> EquivRel DiagSort -> [[DiagEmb]]
looplessWords ([[DiagEmb]] -> [DiagEmb]
canonicalEmbs [[DiagEmb]]
sim') EquivRel DiagSort
simeq') EquivRel DiagSort
simeq' [[DiagEmb]]
sim'


-- | Compute the \sim relation
sim :: CASLDiag
    -> [DiagEmb]
    -> EquivRel DiagEmb
sim :: CASLDiag -> [DiagEmb] -> [[DiagEmb]]
sim diag :: CASLDiag
diag embs' :: [DiagEmb]
embs' =
    let -- diagRule: the Diag rule
        diagRule :: DiagEmb -> DiagEmb -> Bool
diagRule (n1 :: Int
n1, s11 :: SORT
s11, s12 :: SORT
s12) (n2 :: Int
n2, s21 :: SORT
s21, s22 :: SORT
s22) =
            CASLDiag -> DiagSort -> DiagSort -> Bool
isMorphSort CASLDiag
diag (Int
n1, SORT
s11) (Int
n2, SORT
s21)
                Bool -> Bool -> Bool
&& CASLDiag -> DiagSort -> DiagSort -> Bool
isMorphSort CASLDiag
diag (Int
n1, SORT
s12) (Int
n2, SORT
s22)
            Bool -> Bool -> Bool
|| CASLDiag -> DiagSort -> DiagSort -> Bool
isMorphSort CASLDiag
diag (Int
n2, SORT
s21) (Int
n1, SORT
s11)
                   Bool -> Bool -> Bool
&& CASLDiag -> DiagSort -> DiagSort -> Bool
isMorphSort CASLDiag
diag (Int
n2, SORT
s22) (Int
n1, SORT
s12)

        -- the check for congruenceClosure
        check :: (Int, SORT, a) -> (Int, a, SORT) -> Bool
check (p :: Int
p, s11 :: SORT
s11, s12 :: a
s12) (q :: Int
q, s21 :: a
s21, s22 :: SORT
s22) =
            Bool -> Bool
not (Int
p Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
q Bool -> Bool -> Bool
|| a
s12 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
s21) Bool -> Bool -> Bool
&&
            (DiagEmb -> Bool) -> [DiagEmb] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ (n :: Int
n, s1 :: SORT
s1, s2 :: SORT
s2) -> Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
p Bool -> Bool -> Bool
&& SORT
s1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s11 Bool -> Bool -> Bool
&& SORT
s2 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s22) [DiagEmb]
embs'

        -- the op for congruence closure
        op :: (a, b, c) -> (a, b, c) -> (a, b, c)
op (p :: a
p, s1 :: b
s1, _) (_, _, s2 :: c
s2) = (a
p, b
s1, c
s2)

        -- fixCong: apply Cong rule until a fixpoint is reached
        fixCong :: EquivRelTagged DiagEmb b -> EquivRelTagged DiagEmb b
fixCong rel1 :: EquivRelTagged DiagEmb b
rel1 =
            let rel2 :: EquivRelTagged DiagEmb b
rel2 = (DiagEmb -> DiagEmb -> Bool)
-> (DiagEmb -> DiagEmb -> DiagEmb)
-> EquivRelTagged DiagEmb b
-> EquivRelTagged DiagEmb b
forall a b.
(Eq a, Eq b) =>
(a -> a -> Bool)
-> (a -> a -> a) -> EquivRelTagged a b -> EquivRelTagged a b
congruenceClosure DiagEmb -> DiagEmb -> Bool
forall a. Eq a => (Int, SORT, a) -> (Int, a, SORT) -> Bool
check DiagEmb -> DiagEmb -> DiagEmb
forall a b c a b c. (a, b, c) -> (a, b, c) -> (a, b, c)
op EquivRelTagged DiagEmb b
rel1
            in if EquivRelTagged DiagEmb b
rel1 EquivRelTagged DiagEmb b -> EquivRelTagged DiagEmb b -> Bool
forall a. Eq a => a -> a -> Bool
== EquivRelTagged DiagEmb b
rel2 then EquivRelTagged DiagEmb b
rel1 else EquivRelTagged DiagEmb b -> EquivRelTagged DiagEmb b
fixCong EquivRelTagged DiagEmb b
rel2

        rel :: [(DiagEmb, DiagEmb)]
rel = (DiagEmb -> (DiagEmb, DiagEmb))
-> [DiagEmb] -> [(DiagEmb, DiagEmb)]
forall a b. (a -> b) -> [a] -> [b]
map (\ e :: DiagEmb
e -> (DiagEmb
e, DiagEmb
e)) [DiagEmb]
embs'
        rel' :: [(DiagEmb, DiagEmb)]
rel' = [(DiagEmb, DiagEmb)] -> [(DiagEmb, DiagEmb)]
forall b.
Eq b =>
EquivRelTagged DiagEmb b -> EquivRelTagged DiagEmb b
fixCong [(DiagEmb, DiagEmb)]
rel
        rel'' :: [(DiagEmb, DiagEmb)]
rel'' = (DiagEmb -> DiagEmb -> Bool)
-> [(DiagEmb, DiagEmb)] -> [(DiagEmb, DiagEmb)]
forall b a.
Ord b =>
(a -> a -> Bool) -> EquivRelTagged a b -> EquivRelTagged a b
mergeEquivClassesBy DiagEmb -> DiagEmb -> Bool
diagRule [(DiagEmb, DiagEmb)]
rel'
    in [(DiagEmb, DiagEmb)] -> [[DiagEmb]]
forall b a. Ord b => EquivRelTagged a b -> EquivRel a
taggedValsToEquivClasses [(DiagEmb, DiagEmb)]
rel''


-- | Compute the CanonicalEmbs(D) set given \sim relation
canonicalEmbs :: EquivRel DiagEmb
              -> [DiagEmb]
canonicalEmbs :: [[DiagEmb]] -> [DiagEmb]
canonicalEmbs = ([DiagEmb] -> [DiagEmb] -> [DiagEmb])
-> [DiagEmb] -> [[DiagEmb]] -> [DiagEmb]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ l :: [DiagEmb]
l cl :: [DiagEmb]
cl -> let e :: DiagEmb
e : _ = [DiagEmb]
cl in DiagEmb
e DiagEmb -> [DiagEmb] -> [DiagEmb]
forall a. a -> [a] -> [a]
: [DiagEmb]
l) []

{- | Convert given \cong_\tau relation to the canonical form
w.r.t. given \sim relation -}
canonicalCongTau :: EquivRel DiagEmbWord
                  -> EquivRel DiagEmb
                  -> EquivRel DiagEmbWord
canonicalCongTau :: EquivRel [DiagEmb] -> [[DiagEmb]] -> EquivRel [DiagEmb]
canonicalCongTau ct :: EquivRel [DiagEmb]
ct sim' :: [[DiagEmb]]
sim' =
    let mapEmb :: DiagEmb -> DiagEmb
mapEmb e :: DiagEmb
e = let Just (ce :: DiagEmb
ce : _) = ([DiagEmb] -> Bool) -> [[DiagEmb]] -> Maybe [DiagEmb]
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (DiagEmb -> [DiagEmb] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem DiagEmb
e) [[DiagEmb]]
sim'
                   in DiagEmb
ce
        mapWord :: [DiagEmb] -> [DiagEmb]
mapWord = (DiagEmb -> DiagEmb) -> [DiagEmb] -> [DiagEmb]
forall a b. (a -> b) -> [a] -> [b]
map DiagEmb -> DiagEmb
mapEmb
        mapEqcl :: [[DiagEmb]] -> [[DiagEmb]]
mapEqcl = ([DiagEmb] -> [DiagEmb]) -> [[DiagEmb]] -> [[DiagEmb]]
forall a b. (a -> b) -> [a] -> [b]
map [DiagEmb] -> [DiagEmb]
mapWord
    in ([[DiagEmb]] -> [[DiagEmb]])
-> EquivRel [DiagEmb] -> EquivRel [DiagEmb]
forall a b. (a -> b) -> [a] -> [b]
map [[DiagEmb]] -> [[DiagEmb]]
mapEqcl EquivRel [DiagEmb]
ct


-- | Convert a word to a list of sorts that are embedded
wordToEmbPath :: DiagEmbWord
              -> [SORT]
wordToEmbPath :: [DiagEmb] -> [SORT]
wordToEmbPath [] = []
wordToEmbPath ((_, s1 :: SORT
s1, s2 :: SORT
s2) : embs1 :: [DiagEmb]
embs1) =
    let rest :: [(a, a, c)] -> [a]
rest [] = []
        rest ((_, s :: a
s, _) : embs2 :: [(a, a, c)]
embs2) = [(a, a, c)] -> [a]
rest [(a, a, c)]
embs2 [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a
s]
    in [DiagEmb] -> [SORT]
forall a a c. [(a, a, c)] -> [a]
rest [DiagEmb]
embs1 [SORT] -> [SORT] -> [SORT]
forall a. [a] -> [a] -> [a]
++ [SORT
s1, SORT
s2]


hasCellCaslAmalgOpt :: [CASLAmalgOpt] -> Bool
hasCellCaslAmalgOpt :: [CASLAmalgOpt] -> Bool
hasCellCaslAmalgOpt = (CASLAmalgOpt -> Bool) -> [CASLAmalgOpt] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ( \ o :: CASLAmalgOpt
o -> case CASLAmalgOpt
o of
                            Cell -> Bool
True
                            _ -> Bool
False)

hasColimitThinnessOpt :: [CASLAmalgOpt] -> Bool
hasColimitThinnessOpt :: [CASLAmalgOpt] -> Bool
hasColimitThinnessOpt = (CASLAmalgOpt -> Bool) -> [CASLAmalgOpt] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ( \ o :: CASLAmalgOpt
o -> case CASLAmalgOpt
o of
                            ColimitThinness -> Bool
True
                            _ -> Bool
False)

-- | The amalgamability checking function for CASL.
ensuresAmalgamability :: [CASLAmalgOpt]        -- ^ program options
                      -> CASLDiag              -- ^ the diagram to be checked
                      -> [(Node, CASLMor)]     -- ^ the sink
                      -> Tree.Gr String String
                    -- ^ the diagram containing descriptions of nodes and edges
                      -> Result Amalgamates
ensuresAmalgamability :: [CASLAmalgOpt]
-> CASLDiag
-> [(Int, Morphism () () ())]
-> Gr String String
-> Result Amalgamates
ensuresAmalgamability opts :: [CASLAmalgOpt]
opts diag :: CASLDiag
diag sink :: [(Int, Morphism () () ())]
sink desc :: Gr String String
desc =
    if [CASLAmalgOpt] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CASLAmalgOpt]
opts then Amalgamates -> Result Amalgamates
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Amalgamates
DontKnow "Skipping amalgamability check")
    else let -- aux. functions that help printing out diagnostics
    getNodeSig :: t -> [(t, Sign f ())] -> Sign f ()
getNodeSig _ [] = () -> Sign f ()
forall e f. e -> Sign f e
emptySign () -- this should never be the case
    getNodeSig n :: t
n ((n1 :: t
n1, sig :: Sign f ()
sig) : nss :: [(t, Sign f ())]
nss) = if t
n t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
n1 then Sign f ()
sig else t -> [(t, Sign f ())] -> Sign f ()
getNodeSig t
n [(t, Sign f ())]
nss
    lns :: [(Int, Sign () ())]
lns = CASLDiag -> [(Int, Sign () ())]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes CASLDiag
diag
    formatOp :: (a, a) -> String
formatOp (idt :: a
idt, t :: a
t) = a -> ShowS
forall a. Pretty a => a -> ShowS
showDoc a
idt " :" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> ShowS
forall a. Pretty a => a -> ShowS
showDoc a
t ""
    formatPred :: (a, a) -> String
formatPred (idt :: a
idt, t :: a
t) = a -> ShowS
forall a. Pretty a => a -> ShowS
showDoc a
idt " : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> ShowS
forall a. Pretty a => a -> ShowS
showDoc a
t ""
    formatSig :: Int -> String
formatSig n :: Int
n = case ((Int, String) -> Bool) -> [(Int, String)] -> Maybe (Int, String)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\ (n' :: Int
n', d :: String
d) -> Int
n' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n Bool -> Bool -> Bool
&& String
d String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= "") (Gr String String -> [(Int, String)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr String String
desc) of
                  Just (_, d :: String
d) -> String
d
                  Nothing -> Sign () () -> ShowS
forall a. Pretty a => a -> ShowS
showDoc (Int -> [(Int, Sign () ())] -> Sign () ()
forall t f. Eq t => t -> [(t, Sign f ())] -> Sign f ()
getNodeSig Int
n [(Int, Sign () ())]
lns) ""
              -- and now the relevant stuff
    s :: EquivRel DiagSort
s = CASLDiag -> EquivRel DiagSort
simeq CASLDiag
diag
    st :: EquivRel DiagSort
st = [(Int, Morphism () () ())] -> EquivRel DiagSort
simeqTau [(Int, Morphism () () ())]
sink
              {- 2. Check the inclusion (*). If it doesn't hold, the
                 specification is incorrect. -}
    in case EquivRel DiagSort
-> EquivRel DiagSort -> Maybe (DiagSort, DiagSort)
forall a. Eq a => EquivRel a -> EquivRel a -> Maybe (a, a)
subRelation EquivRel DiagSort
st EquivRel DiagSort
s of
    Just (ns1 :: DiagSort
ns1, ns2 :: DiagSort
ns2) -> let
      sortString1 :: String
sortString1 = SORT -> ShowS
forall a. Pretty a => a -> ShowS
showDoc (DiagSort -> SORT
forall a b. (a, b) -> b
snd DiagSort
ns1) " in\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
formatSig (DiagSort -> Int
forall a b. (a, b) -> a
fst DiagSort
ns1)
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n\n"
      sortString2 :: String
sortString2 = SORT -> ShowS
forall a. Pretty a => a -> ShowS
showDoc (DiagSort -> SORT
forall a b. (a, b) -> b
snd DiagSort
ns2) " in\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
formatSig (DiagSort -> Int
forall a b. (a, b) -> a
fst DiagSort
ns2)
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n\n"
      in Amalgamates -> Result Amalgamates
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Amalgamates
NoAmalgamation ("\nsorts " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
sortString1
                        String -> ShowS
forall a. [a] -> [a] -> [a]
++ "and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
sortString2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "might be different"))
    Nothing -> let
      sop :: EquivRel DiagOp
sop = CASLDiag -> EquivRel DiagOp
simeqOp CASLDiag
diag
      sopt :: EquivRel DiagOp
sopt = [(Int, Morphism () () ())] -> EquivRel DiagOp
simeqOpTau [(Int, Morphism () () ())]
sink
                 {- 2a. Check sharing of operations. If the check
                 fails, the specification is incorrect -}
      in case EquivRel DiagOp -> EquivRel DiagOp -> Maybe (DiagOp, DiagOp)
forall a. Eq a => EquivRel a -> EquivRel a -> Maybe (a, a)
subRelation EquivRel DiagOp
sopt EquivRel DiagOp
sop of
      Just (nop1 :: DiagOp
nop1, nop2 :: DiagOp
nop2) -> let
        opString1 :: String
opString1 = (SORT, OpType) -> String
forall a a. (Pretty a, Pretty a) => (a, a) -> String
formatOp (DiagOp -> (SORT, OpType)
forall a b. (a, b) -> b
snd DiagOp
nop1) String -> ShowS
forall a. [a] -> [a] -> [a]
++
                          " in\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
formatSig (DiagOp -> Int
forall a b. (a, b) -> a
fst DiagOp
nop1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n\n"
        opString2 :: String
opString2 = (SORT, OpType) -> String
forall a a. (Pretty a, Pretty a) => (a, a) -> String
formatOp (DiagOp -> (SORT, OpType)
forall a b. (a, b) -> b
snd DiagOp
nop2) String -> ShowS
forall a. [a] -> [a] -> [a]
++
                          " in\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
formatSig (DiagOp -> Int
forall a b. (a, b) -> a
fst DiagOp
nop2) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n\n"
        in Amalgamates -> Result Amalgamates
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Amalgamates
NoAmalgamation ("\noperations "
                              String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
opString1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
opString2
                              String -> ShowS
forall a. [a] -> [a] -> [a]
++ "might be different"))
      Nothing -> let
        spred :: EquivRel DiagPred
spred = CASLDiag -> EquivRel DiagPred
simeqPred CASLDiag
diag
        spredt :: EquivRel DiagPred
spredt = [(Int, Morphism () () ())] -> EquivRel DiagPred
simeqPredTau [(Int, Morphism () () ())]
sink
                           {- 2b. Check sharing of predicates. If the
                           check fails, the specification is incorrect -}
        in case EquivRel DiagPred
-> EquivRel DiagPred -> Maybe (DiagPred, DiagPred)
forall a. Eq a => EquivRel a -> EquivRel a -> Maybe (a, a)
subRelation EquivRel DiagPred
spredt EquivRel DiagPred
spred of
        Just (np1 :: DiagPred
np1, np2 :: DiagPred
np2) -> let
          pString1 :: String
pString1 = (SORT, PredType) -> String
forall a a. (Pretty a, Pretty a) => (a, a) -> String
formatPred (DiagPred -> (SORT, PredType)
forall a b. (a, b) -> b
snd DiagPred
np1) String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                   " in\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
formatSig (DiagPred -> Int
forall a b. (a, b) -> a
fst DiagPred
np1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n\n"
          pString2 :: String
pString2 = (SORT, PredType) -> String
forall a a. (Pretty a, Pretty a) => (a, a) -> String
formatPred (DiagPred -> (SORT, PredType)
forall a b. (a, b) -> b
snd DiagPred
np2) String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                   " in\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
formatSig (DiagPred -> Int
forall a b. (a, b) -> a
fst DiagPred
np2) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n\n"
          in Amalgamates -> Result Amalgamates
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Amalgamates
NoAmalgamation ("\npredicates "
                                       String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
pString1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
pString2
                                       String -> ShowS
forall a. [a] -> [a] -> [a]
++ "might be different"))
        Nothing -> if Bool -> Bool
not ([CASLAmalgOpt] -> Bool
hasCellCaslAmalgOpt [CASLAmalgOpt]
opts
                           Bool -> Bool -> Bool
|| [CASLAmalgOpt] -> Bool
hasColimitThinnessOpt [CASLAmalgOpt]
opts)
                   then Amalgamates -> Result Amalgamates
forall (m :: * -> *) a. Monad m => a -> m a
return Amalgamates
defaultDontKnow else let
          ct :: EquivRel [DiagEmb]
ct = CASLDiag
-> [(Int, Morphism () () ())]
-> EquivRel DiagSort
-> EquivRel [DiagEmb]
congTau CASLDiag
diag [(Int, Morphism () () ())]
sink EquivRel DiagSort
st
                        {- As we will be using a finite representation
                        of \cong_0 that may not contain some of the
                        equivalence classes with only one element
                        it's sufficient to check that the subrelation
                        ct0 of ct that has only non-reflexive
                        elements is a subrelation of \cong_0.
                        Section 4.1 in the paper -}
          ct0 :: EquivRel [DiagEmb]
ct0 = -- trace ("ct:" ++ show ct ++ "\n") $
                 ([[DiagEmb]] -> Bool) -> EquivRel [DiagEmb] -> EquivRel [DiagEmb]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ l :: [[DiagEmb]]
l -> [[DiagEmb]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[DiagEmb]]
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1) EquivRel [DiagEmb]
ct
          c0 :: EquivRel [DiagEmb]
c0 = CASLDiag -> EquivRel DiagSort -> EquivRel [DiagEmb]
cong0 CASLDiag
diag EquivRel DiagSort
s
                        {- 3. Check the simple case: \cong_0 \in
                        \cong, so if \cong_\tau \in \cong_0 the
                        specification is correct. -}
          in case EquivRel [DiagEmb]
-> EquivRel [DiagEmb] -> Maybe ([DiagEmb], [DiagEmb])
forall a. Eq a => EquivRel a -> EquivRel a -> Maybe (a, a)
subRelation EquivRel [DiagEmb]
ct0 EquivRel [DiagEmb]
c0 of
          Nothing -> Amalgamates -> Result Amalgamates
forall (m :: * -> *) a. Monad m => a -> m a
return Amalgamates
Amalgamates
          Just _ -> let
            em :: [DiagEmb]
em = CASLDiag -> [DiagEmb]
embs CASLDiag
diag
            cem :: [DiagEmb]
cem = [[DiagEmb]] -> [DiagEmb]
canonicalEmbs [[DiagEmb]]
si
            mas :: Maybe [[DiagEmb]]
mas = [DiagEmb] -> EquivRel DiagSort -> Maybe [[DiagEmb]]
finiteAdmSimeq [DiagEmb]
cem EquivRel DiagSort
s
            si :: [[DiagEmb]]
si = CASLDiag -> [DiagEmb] -> [[DiagEmb]]
sim CASLDiag
diag [DiagEmb]
em
            cct :: EquivRel [DiagEmb]
cct = EquivRel [DiagEmb] -> [[DiagEmb]] -> EquivRel [DiagEmb]
canonicalCongTau EquivRel [DiagEmb]
ct [[DiagEmb]]
si
            -- 4. Check if the set Adm_\simeq is finite.
            in case Maybe [[DiagEmb]]
mas of
            Just cas :: [[DiagEmb]]
cas -> {- 5. check the colimit thinness. If
                                  the colimit is thin then the
                                  specification is correct. -}
              if [CASLAmalgOpt] -> Bool
hasColimitThinnessOpt [CASLAmalgOpt]
opts Bool -> Bool -> Bool
&& EquivRel DiagSort -> [DiagEmb] -> EquivRel [DiagEmb] -> Bool
colimitIsThin EquivRel DiagSort
s [DiagEmb]
em EquivRel [DiagEmb]
c0
              then Amalgamates -> Result Amalgamates
forall (m :: * -> *) a. Monad m => a -> m a
return Amalgamates
Amalgamates else let
              c :: EquivRel [DiagEmb]
c = CASLDiag
-> [[DiagEmb]]
-> EquivRel DiagSort
-> [[DiagEmb]]
-> EquivRel [DiagEmb]
cong CASLDiag
diag [[DiagEmb]]
cas EquivRel DiagSort
s [[DiagEmb]]
si
                     {- c = cong diag as s
                      6. Check the cell condition in its full generality. -}
              in if [CASLAmalgOpt] -> Bool
hasCellCaslAmalgOpt [CASLAmalgOpt]
opts
                 then case EquivRel [DiagEmb]
-> EquivRel [DiagEmb] -> Maybe ([DiagEmb], [DiagEmb])
forall a. Eq a => EquivRel a -> EquivRel a -> Maybe (a, a)
subRelation EquivRel [DiagEmb]
cct EquivRel [DiagEmb]
c of
                   Just (w1 :: [DiagEmb]
w1, w2 :: [DiagEmb]
w2) -> let
                     rendEmbPath :: [a] -> String
rendEmbPath [] = []
                     rendEmbPath (h :: a
h : w :: [a]
w) = (String -> a -> String) -> String -> [a] -> String
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ t :: String
t srt :: a
srt -> String
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ " < "
                       String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> ShowS
forall a. Pretty a => a -> ShowS
showDoc a
srt "")
                       (a -> ShowS
forall a. Pretty a => a -> ShowS
showDoc a
h "") [a]
w
                     word1 :: String
word1 = [SORT] -> String
forall a. Pretty a => [a] -> String
rendEmbPath ([DiagEmb] -> [SORT]
wordToEmbPath [DiagEmb]
w1)
                     word2 :: String
word2 = [SORT] -> String
forall a. Pretty a => [a] -> String
rendEmbPath ([DiagEmb] -> [SORT]
wordToEmbPath [DiagEmb]
w2)
                     in Amalgamates -> Result Amalgamates
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Amalgamates
NoAmalgamation ("embedding paths \n    "
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
word1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nand\n    " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
word2
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nmight be different"))
                   Nothing -> Amalgamates -> Result Amalgamates
forall (m :: * -> *) a. Monad m => a -> m a
return Amalgamates
Amalgamates
                 else Amalgamates -> Result Amalgamates
forall (m :: * -> *) a. Monad m => a -> m a
return Amalgamates
defaultDontKnow
            Nothing -> let
              cR :: EquivRel [DiagEmb]
cR = CASLDiag -> EquivRel DiagSort -> [[DiagEmb]] -> EquivRel [DiagEmb]
congR CASLDiag
diag EquivRel DiagSort
s [[DiagEmb]]
si
              {- 7. Check the restricted cell condition. If it holds
              then the specification is correct. Otherwise proof
              obligations need to be generated. -}
              in if [CASLAmalgOpt] -> Bool
hasCellCaslAmalgOpt [CASLAmalgOpt]
opts then case EquivRel [DiagEmb]
-> EquivRel [DiagEmb] -> Maybe ([DiagEmb], [DiagEmb])
forall a. Eq a => EquivRel a -> EquivRel a -> Maybe (a, a)
subRelation EquivRel [DiagEmb]
cct EquivRel [DiagEmb]
cR of
                    Just _ -> Amalgamates -> Result Amalgamates
forall (m :: * -> *) a. Monad m => a -> m a
return Amalgamates
defaultDontKnow
                          -- TODO: 8 generate proof obligations
                    Nothing -> Amalgamates -> Result Amalgamates
forall (m :: * -> *) a. Monad m => a -> m a
return Amalgamates
Amalgamates
                 else Amalgamates -> Result Amalgamates
forall (m :: * -> *) a. Monad m => a -> m a
return Amalgamates
defaultDontKnow