Amalgamability.hs revision c248f80cee36f5060f5c30c94587ec2bd1c225e9
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaederModule : $Header$
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederCopyright : (c) Maciek Makowski, Warsaw University 2004
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : hets@tzi.de
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederStability : provisional
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederPortability : portable
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Amalgamability analysis for CASL.
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder Follows the algorithm outlined in MFCS 2001 (LNCS 2136, pp. 451-463,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Springer 2001) paper.
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder* optimisations in congruenceClosure (Nelson-Oppen algorithm?)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder* optimisation in colimitIsThin (fixUpdRule)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder* optimisations in the whole algorithm
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder CASLSign, CASLMor,
85e1d54a475bfc30b3eac5ae6c5e42a2d7e93f10Christian Maeder -- * Functions
85e1d54a475bfc30b3eac5ae6c5e42a2d7e93f10Christian Maeder ensuresAmalgamability) where
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport qualified Common.Lib.Map as Map
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport qualified Common.Lib.Set as Set
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport qualified Options
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder-- Exported types
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maedertype CASLSign = Sign () ()
b53688bfed888214b485cf76439d57262d80e0a7Christian Maedertype CASLMor = Morphism () () ()
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder-- Miscellaneous types
b53688bfed888214b485cf76439d57262d80e0a7Christian Maedertype CASLDiag = Diagram CASLSign CASLMor
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maedertype DiagSort = (Node, SORT)
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maedertype DiagOp = (Node, (Id, OpType))
b53688bfed888214b485cf76439d57262d80e0a7Christian Maedertype DiagPred = (Node, (Id, PredType))
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maedertype DiagEmb = (Node, SORT, SORT)
3a9d784341454573b50b32fa1b494e7418df3086Christian Maedertype DiagEmbWord = [DiagEmb]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | equivalence classes are represented as lists of elements
b53688bfed888214b485cf76439d57262d80e0a7Christian Maedertype EquivClass a = [a]
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder-- | equivalence relations are represented as lists of equivalence classes
b53688bfed888214b485cf76439d57262d80e0a7Christian Maedertype EquivRel a = [EquivClass a]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | or, sometimes, as lists of pairs (element, equiv. class tag)
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maedertype EquivRelTagged a b = [(a, b)]
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder-- PrettyPrint instance (for diagnostic output)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance PrettyPrint CASLDiag where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder printText0 ga diag =
38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder ptext "nodes: "
38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder <+> (printText0 ga (labNodes diag))
38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder <+> ptext "\nedges: "
38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder <+> (printText0 ga (labEdges diag))
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | Compute the Sorts set -- a disjoint union of all the sorts
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- in the diagram.
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maedersorts :: CASLDiag -- ^ the diagram to get the sorts from
cb2044812811d66efe038d914966e04290be93faChristian Maeder -> [DiagSort]
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder let mkNodeSortPair n sort = (n, sort)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder appendSorts sl (n, Sign { sortSet = s }) =
d81905a5b924415c524d702df26204683c82c12eChristian Maeder sl ++ (map (mkNodeSortPair n) (Set.toList s))
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in foldl appendSorts [] (labNodes diag)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | Compute the Ops set -- a disjoint union of all the operation symbols
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- in the diagram.
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederops :: CASLDiag -- ^ the diagram to get the ops from
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let mkNodeOp n opId opType ol = ol ++ [(n, (opId, opType))]
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder mkNodeOps n opId opTypes ol =
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder ol ++ Set.fold (mkNodeOp n opId) [] opTypes
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder appendOps ol (n, Sign { opMap = m }) =
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder ol ++ Map.foldWithKey (mkNodeOps n) [] m
6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu in foldl appendOps [] (labNodes diag)
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu-- | Compute the Preds set -- a disjoint union of all the predicate symbols
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder-- in the diagram.
966519955f5f7111abac20118563132b9dd41165Christian Maederpreds :: CASLDiag -- ^ the diagram to get the preds from
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder -> [DiagPred]
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maeder let mkNodePred n predId predType pl = pl ++ [(n, (predId, predType))]
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maeder mkNodePreds n predId predTypes pl =
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maeder pl ++ Set.fold (mkNodePred n predId) [] predTypes
8865728716566f42fa73e7e0bc080ba3225df764Christian Maeder appendPreds pl (n, Sign { predMap = m }) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder pl ++ Map.foldWithKey (mkNodePreds n) [] m
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in foldl appendPreds [] (labNodes diag)
2360728d4185c0c04279c999941c64d36626af79Christian Maeder-- | Convert the relation representation from list of pairs
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- (val, equiv. class tag) to a list of equivalence classes.
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedertaggedValsToEquivClasses :: Ord b
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder => EquivRelTagged a b -- ^ a list of (value, tag) pairs
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder -> EquivRel a
fdac680252d7347858bd67b4c2a2aaa52e623815Christian MaedertaggedValsToEquivClasses [] = []
fdac680252d7347858bd67b4c2a2aaa52e623815Christian MaedertaggedValsToEquivClasses rel =
a9e804dbec424ec36e34bab955cbe90edac5baa6Christian Maeder let -- prepMap: create a map with all the equivalence class tags mapped to
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz -- empty lists
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder prepMap rel =
b76d27eba526ecac2a20400fa505ec5c642ae7d2Dominik Luecke foldl (\m -> \k -> Map.insert (snd k) [] m) Map.empty rel
b76d27eba526ecac2a20400fa505ec5c642ae7d2Dominik Luecke -- conv: perform actual conversion
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich convert [] m = map snd (Map.toAscList m)
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich convert ((ds, ect) : dsps) m =
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich let m' = Map.update (\ec -> Just (ds : ec)) ect m
2353f65833a3da763392f771223250cd50b8d873Christian Maeder in convert dsps m'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in convert rel (prepMap rel)
2353f65833a3da763392f771223250cd50b8d873Christian Maeder-- | Convert the relation representation from list of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- equivalence classes to list of (value, tag) pairs.
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederequivClassesToTaggedVals :: Ord a
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder => EquivRel a
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> EquivRelTagged a a
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederequivClassesToTaggedVals rel =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let eqClToList [] = []
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder eqClToList eqcl@(fst : _) = map (\x -> (x, fst)) eqcl
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in foldl (\vtl -> \eqcl -> vtl ++ (eqClToList eqcl)) [] rel
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder{- the old, n^3 version of mergeEquivClassesBy:
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder-- | Merge the equivalence classes for elements fulfilling given condition.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedermergeEquivClassesBy :: Eq b
cb2044812811d66efe038d914966e04290be93faChristian Maeder => (a -> a -> Bool) -- ^ the condition stating when two elements are in relation
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> EquivRelTagged a b -- ^ the input relation
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> EquivRelTagged a b
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- ^ returns the input relation with equivalence classes merged according to
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder-- the condition.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedermergeEquivClassesBy cond rel =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- Starting with the first element in the list an element (elem, tag) is taken
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- and cond is subsequently applied to it and all the elements
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- following it in the list. Whenever an element (elem', tag')
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- that is in relation with the chosen one is found, all the equivalence
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- class tags in the list that are equal to tag' are updated to tag.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let merge rel pos | pos >= length rel = rel
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder merge rel pos | otherwise =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let mergeWith cmpl _ [] = cmpl
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder mergeWith cmpl vtp@(elem, ec) toCmpl@((elem', ec') : _) =
966519955f5f7111abac20118563132b9dd41165Christian Maeder let (cmpl', toCmpl') = if ec /= ec' && (cond elem elem')
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder then let upd (elem'', ec'') =
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder if ec'' == ec'
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder then (elem'', ec)
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder else (elem'', ec'')
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder in (map upd cmpl, map upd toCmpl)
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder else (cmpl, toCmpl)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in mergeWith (cmpl' ++ [head toCmpl']) vtp (tail toCmpl')
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (cmpl, (vtp : vtps)) = splitAt pos rel
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder rel' = mergeWith (cmpl ++ [vtp]) vtp vtps
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder in merge rel' (pos + 1)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in merge rel 0
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederdata TagEqcl a b = Eqcl [a] | TagRef b
2360728d4185c0c04279c999941c64d36626af79Christian Maeder deriving Show
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Merge the equivalence classes for elements fulfilling given condition.
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian MaedermergeEquivClassesBy :: (Ord b)
2360728d4185c0c04279c999941c64d36626af79Christian Maeder => (a -> a -> Bool) -- ^ the condition stating when two elements are in relation
2360728d4185c0c04279c999941c64d36626af79Christian Maeder -> EquivRelTagged a b -- ^ the input relation
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> EquivRelTagged a b
2360728d4185c0c04279c999941c64d36626af79Christian Maeder-- ^ returns the input relation with equivalence classes merged according to
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- the condition.
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian MaedermergeEquivClassesBy cond rel =
2360728d4185c0c04279c999941c64d36626af79Christian Maeder -- Starting with the first element in the list an element (elem, tag) is taken
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- and cond is subsequently applied to it and all the elements
2360728d4185c0c04279c999941c64d36626af79Christian Maeder -- following it in the list. Whenever an element (elem', tag')
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- that is in relation with the chosen one is found, the equivalence classes
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- in tagMap for tag and tag' are merged: tag in tagMap points to the merged
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- equivalence class and tag' in tagMap is a reference to tag.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let -- create the initial map mapping tags to equivalence classes
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder initialTagMap =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let insEl tagMap (val, tag) =
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder case Map.member tag tagMap of
966519955f5f7111abac20118563132b9dd41165Christian Maeder True -> Map.update (\(Eqcl eqcl) -> Just (Eqcl (val : eqcl))) tag tagMap
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder False -> Map.insert tag (Eqcl [val]) tagMap
5a448e9be8c4482a978b174b744237757335140fChristian Maeder in foldl insEl Map.empty rel
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder -- merge equivalence classes tagged with t1 and t2
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder mergeInMap tagMap t1 t2 =
2360728d4185c0c04279c999941c64d36626af79Christian Maeder let -- find the tag and equivalence class that corresponds to the given tag
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- performing path compression while traversing the referneces.
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder findEqcl t tagMap =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case Map.find t tagMap of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Eqcl eqcl -> (t, eqcl, tagMap)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let (rt, eqcl, tagMap') = findEqcl t' tagMap
cb2044812811d66efe038d914966e04290be93faChristian Maeder tagMap'' = if rt == t' then tagMap'
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder else Map.update (\_ -> Just (TagRef rt)) t tagMap'
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder in (rt, eqcl, tagMap'')
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (rt1, eqcl1, tagMap') = findEqcl t1 tagMap
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (rt2, eqcl2, tagMap'') = findEqcl t2 tagMap'
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder in if rt1 == rt2 then tagMap''
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder else let (nrt1, nrt2) = if rt1 > rt2 then (rt2, rt1) else (rt1, rt2)
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder tagMap3 = Map.update (\_ -> Just (Eqcl (eqcl1 ++ eqcl2))) rt1 tagMap''
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder tagMap4 = Map.update (\_ -> Just (TagRef rt1)) rt2 tagMap3
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- iterate through the relation merging equivalence classes of appropriate elements
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder merge tagMap rel pos | pos >= length rel = tagMap
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder merge tagMap rel pos | otherwise =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let mergeWith tagMap _ [] = tagMap
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder mergeWith tagMap vtp@(elem, ec) toCmpl@((elem', ec') : _) =
966519955f5f7111abac20118563132b9dd41165Christian Maeder let tagMap' = if ec /= ec' && (cond elem elem')
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder then mergeInMap tagMap ec ec'
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder in mergeWith tagMap' vtp (tail toCmpl)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (_, (vtp : vtps)) = splitAt pos rel
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder tagMap' = mergeWith tagMap vtp vtps
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in merge tagMap' rel (pos + 1)
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder -- append given equivalence class to the list of (value, tag) pairs
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder tagMapToRel rel (_, TagRef _) = rel
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder tagMapToRel rel (tag, Eqcl eqcl) =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder foldl (\l -> \v -> (v, tag) : l) rel eqcl
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder tagMap = merge initialTagMap rel 0
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in foldl tagMapToRel [] (Map.toAscList tagMap)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Merge the equivalence classes for given tags.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedermergeEquivClasses :: Eq b
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder => EquivRelTagged a b
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> b -- ^ tag 1
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> b -- ^ tag 2
cb2044812811d66efe038d914966e04290be93faChristian Maeder -> EquivRelTagged a b
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedermergeEquivClasses rel tag1 tag2 | tag1 == tag2 = rel
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder | otherwise =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let upd (el, tag) | tag == tag2 = (el, tag1)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | otherwise = (el, tag)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in map upd rel
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Return true if there is an edge between srcNode and targetNode
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- and the morphism with which it's labelled maps srcSort to targetSort
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederisMorphSort :: CASLDiag
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian MaederisMorphSort diag (srcNode, srcSort) (targetNode, targetSort) =
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maeder let checkEdges [] = False
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder checkEdges ((sn, tn, Morphism { sort_map = sm }) : edges) =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder if sn == srcNode &&
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder tn == targetNode &&
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder mapSort sm srcSort == targetSort
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder then True else checkEdges edges
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder in checkEdges (out diag srcNode)
2360728d4185c0c04279c999941c64d36626af79Christian Maeder-- | Return true if there is an edge between srcNode and targetNode
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- and the morphism with which it's labelled maps srcOp to targetOp
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian MaederisMorphOp :: CASLDiag
d81905a5b924415c524d702df26204683c82c12eChristian MaederisMorphOp diag (srcNode, srcOp) (targetNode, targetOp) =
2360728d4185c0c04279c999941c64d36626af79Christian Maeder let checkEdges [] = False
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder checkEdges ((sn, tn, Morphism { sort_map = sm, fun_map = fm }) : edges) =
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder if sn == srcNode &&
2360728d4185c0c04279c999941c64d36626af79Christian Maeder tn == targetNode &&
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder mapOpSym sm fm srcOp == targetOp
966519955f5f7111abac20118563132b9dd41165Christian Maeder then True else checkEdges edges
2360728d4185c0c04279c999941c64d36626af79Christian Maeder in checkEdges (out diag srcNode)
2360728d4185c0c04279c999941c64d36626af79Christian Maeder-- | Return true if there is an edge between srcNode and targetNode
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder-- and the morphism with which it's labelled maps srcPred to targetPred
2360728d4185c0c04279c999941c64d36626af79Christian MaederisMorphPred :: CASLDiag
2360728d4185c0c04279c999941c64d36626af79Christian MaederisMorphPred diag (srcNode, srcPred) (targetNode, targetPred) =
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder let checkEdges [] = False
8994ef587ce7c7c39ddd20f0f7e4575838a6694aChristian Maeder checkEdges ((sn, tn, Morphism { sort_map = sm, pred_map = pm }) : edges) =
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maeder if sn == srcNode &&
2360728d4185c0c04279c999941c64d36626af79Christian Maeder tn == targetNode &&
2360728d4185c0c04279c999941c64d36626af79Christian Maeder mapPredSym sm pm srcPred == targetPred
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder then True else checkEdges edges
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in checkEdges (out diag srcNode)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | Compute the simeq relation for given diagram.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maedersimeq :: CASLDiag -- ^ the diagram for which the relation should be created
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> EquivRel DiagSort
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- ^ returns the relation represented as a list of equivalence
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- classes (each represented as a list of diagram ops)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- During the computations the relation is represented as a list of pairs
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- (DiagSort, DiagSort). The first element is a diagram sort and the second
d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer -- denotes the equivalence class to which it belongs. All the pairs with
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- equal second element denote elements of one equivalence class.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let mergeCond ds ds' = isMorphSort diag ds ds' || isMorphSort diag ds' ds
2360728d4185c0c04279c999941c64d36626af79Christian Maeder -- compute the relation
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder rel = map (\ds -> (ds, ds)) (sorts diag)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder rel' = mergeEquivClassesBy mergeCond rel
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in taggedValsToEquivClasses rel'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Compute the simeq^op relation for given diagram.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedersimeqOp :: CASLDiag -- ^ the diagram for which the relation should be created
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> EquivRel DiagOp
76d027be764e2ff61bef959efb3ac8f56499e646Christian Maeder-- ^ returns the relation represented as a list of equivalence
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova-- classes (each represented as a list of diagram ops)
a166da43d4e8f9dfa7a2651d033c6bea02627ca6Mihai CodescusimeqOp diag =
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder -- During the computations the relation is represented as a list of pairs
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- (DiagOp, DiagOp). The first element is a diagram op and the second
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- denotes the equivalence class to which it belongs. All the pairs with
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz -- equal second element denote elements of one equivalence class.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let mergeCond ds ds' = isMorphOp diag ds ds' || isMorphOp diag ds' ds
b47b1ea8a412f6e4c731779f6a572384e7cf06d8Christian Maeder -- compute the relation
26b1c101b72100b69045effdfaab3889de6c8c93Christian Maeder rel = map (\ds -> (ds, ds)) (ops diag)
c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance rel' = mergeEquivClassesBy mergeCond rel
897a04683fb30873e84dc3360dea770a4435971cChristian Maeder in taggedValsToEquivClasses rel'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Compute the simeq^pred relation for given diagram.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedersimeqPred :: CASLDiag -- ^ the diagram for which the relation should be created
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> EquivRel DiagPred
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- ^ returns the relation represented as a list of equivalence
2360728d4185c0c04279c999941c64d36626af79Christian Maeder-- classes (each represented as a list of diagram preds)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedersimeqPred diag =
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz -- During the computations the relation is represented as a list of pairs
76d027be764e2ff61bef959efb3ac8f56499e646Christian Maeder -- (DiagPred, DiagPred). The first element is a diagram pred and the second
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova -- denotes the equivalence class to which it belongs. All the pairs with
a166da43d4e8f9dfa7a2651d033c6bea02627ca6Mihai Codescu -- equal second element denote elements of one equivalence class.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let mergeCond ds ds' = isMorphPred diag ds ds' || isMorphPred diag ds' ds
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- compute the relation
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder rel = map (\ds -> (ds, ds)) (preds diag)
af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz rel' = mergeEquivClassesBy mergeCond rel
b47b1ea8a412f6e4c731779f6a572384e7cf06d8Christian Maeder in taggedValsToEquivClasses rel'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | Compute the simeq_tau relation for given diagram.
b53688bfed888214b485cf76439d57262d80e0a7Christian Maedersimeq_tau :: [(Node, CASLMor)]
2353f65833a3da763392f771223250cd50b8d873Christian Maeder -> EquivRel DiagSort
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maedersimeq_tau sink =
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder let -- tagEdge: for given morphism m create a list of pairs
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder -- (a, b) where a is DiagSort from the source signature that
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder -- is mapped by m to b
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder tagEdge (sn, Morphism { sort_map = sm }) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder map (\(ss, ts) -> ((sn, ss), ts)) (Map.toList sm)
897a04683fb30873e84dc3360dea770a4435971cChristian Maeder rel = foldl (\l -> \e -> l ++ (tagEdge e)) [] sink
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in taggedValsToEquivClasses rel
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Compute the simeq^op_tau relation for given diagram.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedersimeqOp_tau :: [(Node, CASLMor)]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> EquivRel DiagOp
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedersimeqOp_tau sink =
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder let -- tagEdge: for given morphism m create a list of pairs
26b1c101b72100b69045effdfaab3889de6c8c93Christian Maeder -- (a, b) where a is DiagOp from the source signature that
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder -- is mapped by m to b
b47b1ea8a412f6e4c731779f6a572384e7cf06d8Christian Maeder tagEdge (sn, Morphism { sort_map = sm, fun_map = fm }) =
b47b1ea8a412f6e4c731779f6a572384e7cf06d8Christian Maeder map (\srcOp -> ((sn, srcOp), mapOpSym sm fm srcOp)) (Map.keys fm)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder rel = foldl (\l -> \e -> l ++ (tagEdge e)) [] sink
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in taggedValsToEquivClasses rel
7ebcceae3d34771cae3bbb8c8060bef0b894376eChristian Maeder-- | Compute the simeq^pred_tau relation for given diagram.
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus LuettichsimeqPred_tau :: [(Node, CASLMor)]
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich -> EquivRel DiagPred
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedersimeqPred_tau sink =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let -- tagEdge: for given morphism m create a list of pairs
2360728d4185c0c04279c999941c64d36626af79Christian Maeder -- (a, b) where a is DiagPred from the source signature that
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich -- is mapped by m to b
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich tagEdge (sn, Morphism { sort_map = sm, pred_map = pm }) =
7ebcceae3d34771cae3bbb8c8060bef0b894376eChristian Maeder map (\srcPred -> ((sn, srcPred), mapPredSym sm pm srcPred)) (Map.keys pm)
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich rel = foldl (\l -> \e -> l ++ (tagEdge e)) [] sink
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in taggedValsToEquivClasses rel
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Check that one equivalence relation is a subset of another.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- The relations are represented as a lists of equivalence classes,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- where equivalence classes are lists of elements.
59aa5703ac7f3b99e97cd5926e77088b256c5f40Christian MaedersubRelation :: Eq a
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa => EquivRel a -- ^ the relation that is supposed to be a subset
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> EquivRel a -- ^ the relation that is supposed to be a superset
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder -> Maybe (a, a)
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz-- ^ returns a pair of elements that are in the same equivalence class of the
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- first relation but are not in the same equivalence class of the second
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz-- relation or Nothing the first relation is a subset of the second one.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedersubRelation [] _ = Nothing
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedersubRelation ([] : eqcls) sup = subRelation eqcls sup -- this should never be the case
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedersubRelation (elts@(elt : _) : eqcls) sup =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let findEqCl _ [] = []
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder findEqCl elt (eqcl : eqcls) =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder if elem elt eqcl then eqcl else findEqCl elt eqcls
c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance checkEqCl [] _ = Nothing
c30231257d9116b514dce02703a515fe21cd427dTill Mossakowski checkEqCl (elt : elts) supEqCl =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder if elem elt supEqCl
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder then checkEqCl elts supEqCl
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder else Just elt
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder curFail = checkEqCl elts (findEqCl elt sup)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in case curFail of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Nothing -> subRelation eqcls sup
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Just elt2 -> Just (elt, elt2)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Compute the set of sort embeddings defined in the diagram.
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maederembs :: CASLDiag
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz let embs' [] = []
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder embs' ((n, Sign {sortRel = sr}) : lNodes) =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (map (\(s1, s2) -> (n, s1, s2)) (toList sr)) ++ (embs' lNodes)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in embs' (labNodes diag)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Compute the set of sort embeddings (relations on sorts) defined
c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance-- in the source nodes of the sink.
c30231257d9116b514dce02703a515fe21cd427dTill MossakowskisinkEmbs :: CASLDiag -- ^ the diagram
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder -> [(Node, CASLMor)] -- ^ the sink
59aa5703ac7f3b99e97cd5926e77088b256c5f40Christian MaedersinkEmbs _ [] = []
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen KuksasinkEmbs diag ((srcNode, _) : edges) =
c30231257d9116b514dce02703a515fe21cd427dTill Mossakowski let (_, _, Sign {sortRel = sr}, _) = context srcNode diag
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder in (map (\(s1, s2) -> (srcNode, s1, s2)) (toList sr)) ++ (sinkEmbs diag edges)
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder-- | Check if the two given elements are in the given relation.
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder => EquivRel a -- ^ the relation
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder -> a -- ^ the first element
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich -> a -- ^ the second element
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaederinRel [] _ _ = False
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederinRel (eqc : eqcs) a b | a == b = True
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder | otherwise =
2360728d4185c0c04279c999941c64d36626af79Christian Maeder case find (\x -> x == a) eqc of
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder Nothing -> inRel eqcs a b
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder Just _ -> case find (\x -> x == b) eqc of
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder Nothing -> False
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder Just _ -> True
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Check if two embeddings can occur subsequently in a word
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- given the simeq relation on sorts.
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maederadmissible :: EquivRel DiagSort -- ^ the \simeq relation
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder -> DiagEmb -- ^ the first embedding
511284753313165e629cedf508752d6818ccc4d2Christian Maeder -> DiagEmb -- ^ the second embedding
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederadmissible simeq (n1, s1, _) (n2, _, s2) =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder inRel simeq (n1, s1) (n2, s2)
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder-- | Compute the set of all the loopless, admissible
511284753313165e629cedf508752d6818ccc4d2Christian Maeder-- words over given set of embeddings.
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederlooplessWords :: [DiagEmb] -- ^ the embeddings
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> EquivRel DiagSort -- ^ the \simeq relation that defines admissibility
511284753313165e629cedf508752d6818ccc4d2Christian Maeder -> [DiagEmbWord]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederlooplessWords embs simeq =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let -- generate the list of all loopless words over given alphabet
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- with given suffix
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder looplessWords' suff@(e : _) embs pos | pos >= length embs = [suff]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder | otherwise =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let emb = embs !! pos
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder embs' = embs \\ [emb]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ws = if admissible simeq emb e
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder then looplessWords' (emb : suff) embs' 0
8865728716566f42fa73e7e0bc080ba3225df764Christian Maeder in ws ++ (looplessWords' suff embs (pos + 1))
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder looplessWords' [] embs pos | pos >= length embs = []
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder | otherwise =
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder let emb = embs !! pos
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder embs' = embs \\ [emb]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in (looplessWords' [emb] embs' 0) ++ (looplessWords' [] embs (pos + 1))
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder in looplessWords' [] embs 0
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Return the codomain of an embedding path.
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian MaederwordCod :: DiagEmbWord
91ba5d95b2472cb075646b6120a559dc6581a867Christian MaederwordCod ((n, _, s2) : _) = (n, s2)
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder-- | Return the domain of an embedding path.
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederwordDom :: DiagEmbWord
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederwordDom w = let (n, s1, _) = last w in (n, s1)
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder-- | Find an equivalence class tag for given element.
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaederfindTag :: Eq a
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder => EquivRelTagged a b
f03420e44d8204b2945edaab5c70a84e7c381892Christian MaederfindTag [] _ = Nothing
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaederfindTag ((w', t) : wtps) w =
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder if w == w' then Just t else findTag wtps w
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder-- | Compute the left-cancellable closure of a relation on words.
91ba5d95b2472cb075646b6120a559dc6581a867Christian MaederleftCancellableClosure :: EquivRelTagged DiagEmbWord DiagEmbWord
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder -> EquivRelTagged DiagEmbWord DiagEmbWord
f03420e44d8204b2945edaab5c70a84e7c381892Christian MaederleftCancellableClosure rel =
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder let -- checkPrefixes: for each common prefix of two given words
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder -- merge the equivalence classes of the suffixes
d81905a5b924415c524d702df26204683c82c12eChristian Maeder checkPrefixes [] _ rel = rel
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder checkPrefixes _ [] rel = rel
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder checkPrefixes w1@(l1 : suf1) w2@(l2 : suf2) rel | w1 == w2 = rel
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder | l1 /= l2 = rel
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder | otherwise =
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder let Just tag1 = findTag rel suf1
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder Just tag2 = findTag rel suf2
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder rel' = if tag1 == tag2 then rel
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder else let upd (w, t) | t == tag2 = (w, tag1)
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder | otherwise = (w, t)
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder in map upd rel
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder in checkPrefixes suf1 suf2 rel'
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder -- iterateWord1: for each pair of related words call checkPrefixes
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder iterateWord1 rel pos | pos >= length rel = rel
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder | otherwise =
818b228955ef40dd5a253bd942dd6ab8779ed713Christian Maeder let iterateWord2 wtp1@(w1, t1) rel pos | pos >= length rel = rel
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder | otherwise =
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder let wtp2@(w2, t2) = rel !! pos
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder rel' = if t1 == t2 then checkPrefixes w1 w2 rel else rel
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder in iterateWord2 wtp1 rel' (pos + 1)
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder wtp = rel !! pos
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maeder rel' = iterateWord2 wtp rel 0
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder in iterateWord1 rel' (pos + 1)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in {-trace ("leftCancellableClosure " ++ show rel) $-} iterateWord1 rel 0
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder-- | Compute the congruence closure of an equivalence R: two pairs of elements (1, 3) and
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder-- (2, 4) are chosen such that 1 R 2 and 3 R 4. It is then checked that elements 1, 3 and
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder-- 2, 4 are in relation supplied and if so equivalence classes for (op 1 3) and (op 1 4)
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder-- in R are merged.
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder-- This function should be applied to the relation until a fixpoint is reached.
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaedercongruenceClosure :: (Eq a, Eq b)
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder => (a -> a -> Bool) -- ^ the check to be performed on elements 1, 3 and 2, 4
ab2f38d9cd1249f6bc9cc5b838dc2fcd76189c0fChristian Maeder -> (a -> a -> a) -- ^ the operation to be performed on elements 1, 3 and 2, 4
974b0baababf2878820de073b8fad8db68bef08aDominik Luecke -> EquivRelTagged a b
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder -> EquivRelTagged a b
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian MaedercongruenceClosure check op rel =
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder let -- iterateWord1
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder iterateWord1 rel pos | pos >= length rel = rel
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder | otherwise =
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder let -- iterateWord2
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder iterateWord2 wtp1@(_, t1) rel pos | pos >= length rel = rel
966519955f5f7111abac20118563132b9dd41165Christian Maeder | otherwise =
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder let -- iterateWord3
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder iterateWord3 wtp1@(w1, _) wtp2 rel pos | pos >= length rel = rel
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder | otherwise =
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder let -- iterateWord4
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder iterateWord4 wtp1@(w1, _) wtp2@(w2, _) wtp3@(w3, t3) rel pos | pos >= length rel = rel
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder | otherwise =
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder let (w4, t4) = rel !! pos
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder rel' = if t3 /= t4 || not (check w2 w4) then rel
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder else let mct1 = findTag rel (op w1 w3)
2353f65833a3da763392f771223250cd50b8d873Christian Maeder mct2 = findTag rel (op w2 w4)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in case (mct1, mct2) of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (Nothing, _) -> rel -- w3w1 is not in the domain of rel
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (_, Nothing) -> rel -- w4w2 is not in the domain of rel
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (Just ct1, Just ct2) -> mergeEquivClasses rel ct1 ct2
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in iterateWord4 wtp1 wtp2 wtp3 rel' (pos + 1)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder wtp3@(w3, _) = rel !! pos
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder rel' = if check w1 w3
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- inRel here is usually much more efficient
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- than findTag rel (w3 ++ w1)
2360728d4185c0c04279c999941c64d36626af79Christian Maeder then iterateWord4 wtp1 wtp2 wtp3 rel 0
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in iterateWord3 wtp1 wtp2 rel' (pos + 1)
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder wtp2@(_, t2) = rel !! pos
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder rel' = if t1 /= t2 then rel
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder else iterateWord3 wtp1 wtp2 rel 0
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder in iterateWord2 wtp1 rel' (pos + 1)
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu wtp = rel !! pos
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu rel' = iterateWord2 wtp rel 0
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu in iterateWord1 rel' (pos + 1)
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu in{- trace ("congruenceClosure " ++ show rel) $-} iterateWord1 rel 0
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu-- | Compute the cong_tau relation for given diagram and sink.
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanucong_tau :: CASLDiag -- ^ the diagram
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu -> [(Node, CASLMor)] -- ^ the sink
66a774f13272fde036481edd2298081ab3d04678Razvan Pascanu -> EquivRel DiagSort -- ^ the \simeq_tau relation
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder -> EquivRel DiagEmbWord
2360728d4185c0c04279c999941c64d36626af79Christian Maedercong_tau diag sink st =
66a774f13272fde036481edd2298081ab3d04678Razvan Pascanu let -- domCodSimeq: check that domains and codomains of given words are related
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder domCodSimeq w1 w2 =
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder inRel st (wordDom w1) (wordDom w2) && inRel st (wordCod w1) (wordCod w2)
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder embs = sinkEmbs diag sink
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder words = looplessWords embs st
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder rel = map (\w -> (w, w)) words
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder rel' = mergeEquivClassesBy domCodSimeq rel
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in taggedValsToEquivClasses rel'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Compute the finite representation of cong_0 relation for given diagram.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- The representation consists only of equivalence classes that
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder-- contain more than one element.
0ea2cddb8715a770e646895e16b7b8085f49167cChristian Maedercong_0 :: CASLDiag
0ea2cddb8715a770e646895e16b7b8085f49167cChristian Maeder -> EquivRel DiagSort -- ^ the \simeq relation
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder -> EquivRel DiagEmbWord
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maedercong_0 diag simeq =
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder let -- diagRule: the Diag rule
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder diagRule [(n1, s11, s12)] [(n2, s21, s22)] =
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder isMorphSort diag (n1, s11) (n2, s21) && isMorphSort diag (n1, s12) (n2, s22) ||
0ea2cddb8715a770e646895e16b7b8085f49167cChristian Maeder isMorphSort diag (n2, s21) (n1, s11) && isMorphSort diag (n2, s22) (n1, s12)
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder diagRule _ _ = False
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder -- addToRel: add given word to given relation
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder addToRel [] _ = []
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder addToRel (eqcl@(refw : _) : eqcls) w =
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder if wordDom w == wordDom refw && wordCod w == wordCod refw
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder then ((w : eqcl) : eqcls)
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder else (eqcl : (addToRel eqcls w))
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder -- words2: generate all the admissible 2-letter words over given alphabet
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder words2 _ [] _ = []
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder words2 alph (_ : embs) [] = words2 alph embs alph
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder words2 alph embs1@(emb1 : _) (emb2 : embs2) =
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder let ws = words2 alph embs1 embs2
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder in if admissible simeq emb1 emb2
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder then ([emb1, emb2] : ws) else ws
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder -- compute the relation
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder em = embs diag
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder rel = map (\e -> ([e], [e])) em
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder rel' = mergeEquivClassesBy diagRule rel
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder rel'' = taggedValsToEquivClasses rel'
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder w2s = words2 em em em
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder rel''' = foldl addToRel rel'' w2s
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | Compute the set Adm_\simeq if it's finite.
9d6562465b41f17c7967d4e5678f34811d958cb2Christian MaederfiniteAdm_simeq :: [DiagEmb] -- ^ the embeddings
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder -> EquivRel DiagSort -- ^ the \simeq relation that defines admissibility
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder -> Maybe [DiagEmbWord]
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder-- ^ returns the computed set or Nothing if it's infinite
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederfiniteAdm_simeq embs simeq =
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder let -- generate the list of the words over given alphabet
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder -- with given suffix
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder embWords' suff@(e : _) embs pos | pos >= length embs = Just [suff]
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder | otherwise =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let emb = embs !! pos
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder mws1 = if admissible simeq emb e
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder then if any (\emb' -> emb' == emb) suff
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder else embWords' (emb : suff) embs 0
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder mws2 = case mws1 of
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder Nothing -> Nothing
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder Just _ -> embWords' suff embs (pos + 1)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in case mws1 of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Nothing -> Nothing
93bc87ee96c68506945dbad8c704badaa42ecf14Christian Maeder Just ws1 -> case mws2 of
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder Nothing -> Nothing
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder Just ws2 -> Just (ws1 ++ ws2)
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder embWords' [] embs pos | pos >= length embs = Just []
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder embWords' [] embs pos | otherwise =
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder let emb = embs !! pos
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder mws1 = embWords' [emb] embs 0
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder mws2 = case mws1 of
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder Nothing -> Nothing
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder Just _ -> embWords' [] embs (pos + 1)
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder in case mws1 of
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder Nothing -> Nothing
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Just ws1 -> case mws2 of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Nothing -> Nothing
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Just ws2 -> Just (ws1 ++ ws2)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in embWords' [] embs 0
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | Check if the colimit is thin.
2353f65833a3da763392f771223250cd50b8d873Christian MaedercolimitIsThin :: EquivRel DiagSort -- ^ the simeq relation
2353f65833a3da763392f771223250cd50b8d873Christian Maeder -> [DiagEmb] -- ^ the set of diagram embeddings
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> EquivRel DiagEmbWord -- ^ the cong_0 relation
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercolimitIsThin simeq embs c0 =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let -- sortsC: a list of colimit sorts
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder sortsC = foldl (\s -> \eqcl -> (head eqcl : s)) [] simeq
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder simeqT = equivClassesToTaggedVals simeq
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- ordMap: map representing the topological order on sorts in the colimit
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let sortClasses' m [] = m
2353f65833a3da763392f771223250cd50b8d873Christian Maeder sortClasses' m ((n, s1, s2) : embs) =
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder let Just c1 = findTag simeqT (n, s1)
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder Just c2 = findTag simeqT (n, s2)
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder in sortClasses' (Map.update (\s -> Just (Set.insert c2 s)) c1 m) embs
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder ordMap' = foldl (\m -> \cl -> Map.insert cl Set.empty m) Map.empty sortsC
528539f3d544c24afe14e979fe51f03e50aa6e9cChristian Maeder in sortClasses' ordMap' embs
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder -- larger: return a list of colimit sorts larger than given sort
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in (s : (foldl (\l -> \s -> l ++ (larger s)) [] dl))
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- s: the map representing sets S_{\geq s1,s2}
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder s = let compS m (s1, s2) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let ls1 = Set.fromList (larger s1)
59a10395caff224b2ec541f94dac5082a506c00fChristian Maeder ls2 = Set.fromList (larger s2)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in Map.insert (s1, s2) (Set.intersection ls1 ls2) m
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder in foldl compS Map.empty [(s1, s2) | s1 <- sortsC, s2 <- sortsC]
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder -- b: the map representing sets B_{s1,s2}
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder b = let compB m sp =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let sim s' s'' = not (Set.isEmpty (Map.find (s', s'') s))
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder rel = map (\x -> (x, x)) (Set.toList (Map.find sp s))
2353f65833a3da763392f771223250cd50b8d873Christian Maeder rel' = mergeEquivClassesBy sim rel
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in Map.insert sp (taggedValsToEquivClasses rel') m
2353f65833a3da763392f771223250cd50b8d873Christian Maeder in foldl compB Map.empty [(s1, s2) | s1 <- sortsC, s2 <- sortsC]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder embDomS (n, dom, _) = let Just s = findTag simeqT (n, dom) in s
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder embCodS (n, _, cod) = let Just s = findTag simeqT (n, cod) in s
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- checkAllSorts: check the C = B condition for all colimit sorts
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder checkAllSorts m | Map.isEmpty m = {-trace "CT: Yes"-} True
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder | otherwise =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let -- checkSort: check if for given colimit sort C = B
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder checkSort cs =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let embsCs = filter (\e -> embDomS e == cs) embs
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder c = foldl (\m -> \ep -> Map.insert ep [] m) Map.empty
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder [(d, e) | d <- embsCs, e <- embsCs]
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder c' = let updC c (d, e) =
964ee9fff06b8c821e1d00207f6f185301371be8Christian Maeder let s1 = embCodS d
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder s2 = embCodS e
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder in Map.update (\_ -> Just (Map.find (s1, s2) b)) (d, e) c
964ee9fff06b8c821e1d00207f6f185301371be8Christian Maeder in foldl updC c [(d, e) | d <- embsCs, e <- embsCs, inRel c0 [d] [e]]
964ee9fff06b8c821e1d00207f6f185301371be8Christian Maeder c'' = let updC c (d@(n1, _, cod1), e@(n2, _, cod2)) =
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder let s1 = embCodS d
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder s2 = embCodS e
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder in if (filter (\(n, dom, cod) -> (n, dom) == (n1, cod1) && (n, cod) == (n2, cod2)) embs) == []
964ee9fff06b8c821e1d00207f6f185301371be8Christian Maeder else let [absCls] = filter (\ac -> any (s2==) ac) (Map.find (s1, s2) b)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in foldl (\c -> \k -> Map.update (\l -> Just (l ++ [absCls])) k c) c [(d, e), (e, d)]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in foldl updC c' [(d, e) | d <- embsCs, e <- embsCs, wordDom [d] == wordDom [e]]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder fixUpdRule c =
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder let updC c (e1, e2, e3) =
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder let updC' c (b12, b23, b13) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder comm = Set.intersection sb12 (Set.intersection sb23 sb13)
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder in if Set.isEmpty comm then c
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder else let c' = if any (\l -> l == b13) (Map.find (e1, e3) c)
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder else Map.update (\l -> Just (l ++ [b13])) (e1, e3) c
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder in if any (\l -> l == b13) (Map.find (e1, e3) c')
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder else Map.update (\l -> Just (l ++ [b13])) (e3, e1) c'
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder s1 = embCodS e1
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder s3 = embCodS e3
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder in foldl updC' c [(b12, b23, b13) |
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder b12 <- (Map.find (e1, e2) c),
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder b23 <- (Map.find (e2, e3) c),
59a10395caff224b2ec541f94dac5082a506c00fChristian Maeder b13 <- (Map.find (s1, s3) b)]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder c' = foldl updC c [(e1, e2, e3) |
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder e1 <- embsCs, e2 <- embsCs, e3 <- embsCs]
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder in if c' == c then c else fixUpdRule c'
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder c3 = fixUpdRule c''
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder checkIncl [] = True
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder checkIncl ((e1, e2) : embprs) =
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder let s1 = embCodS e1
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder s2 = embCodS e2
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder res = if subRelation (Map.find (s1, s2) b) (Map.find (e1, e2) c3) == Nothing
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder then checkIncl embprs
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in {-trace ("B[" ++ (show s1) ++ ", " ++ (show s2) ++ ":\n" ++ (show (Map.find (s1, s2) b)) ++ "\n" ++
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "C[" ++ (show e1) ++ ", " ++ (show e2) ++ ":\n" ++ (show (Map.find (e1, e2) c3)) ++ "\n\n")-}
4b1833c7d3af466e6bcba24f16304e0a78e8da87Christian Maeder in checkIncl [(e1, e2) | e1 <- embsCs, e2 <- embsCs]
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder -- cs: next colimit sort to process
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder -- m': the order map with cs removed
4b1833c7d3af466e6bcba24f16304e0a78e8da87Christian Maeder (cs, m') = let [(cs, _)] = take 1 (filter (\(_, lt) -> Set.isEmpty lt)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder m'' = foldl (\m -> \k -> Map.update (\lt -> Just (Set.delete cs lt)) k m)
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder in if checkSort cs then checkAllSorts m' else {-trace "CT: No"-} False
2353f65833a3da763392f771223250cd50b8d873Christian Maeder in {-trace ("\\simeq: " ++ (show simeq) ++ "\nEmbs: " ++ (show embs) ++ "\n\\cong_0: " ++ show c0)-}
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder checkAllSorts ordMap
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder{- the old, unoptimised version of cong:
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder-- | Compute the \cong relation given its (finite) domain
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maedercong :: CASLDiag
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder -> [DiagEmbWord] -- ^ the Adm_\simeq set (the domain of \cong relation)
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder -> EquivRel DiagSort -- ^ the \simeq relation
2353f65833a3da763392f771223250cd50b8d873Christian Maeder -> EquivRel DiagEmbWord
dbc98cd8a9a829e020cfa0a9f3aff89de75caaa9Christian Maedercong diag adm simeq =
2353f65833a3da763392f771223250cd50b8d873Christian Maeder let -- domCodEqual: check that domains and codomains of given words are equal
cb2044812811d66efe038d914966e04290be93faChristian Maeder domCodEqual w1 w2 =
cb2044812811d66efe038d914966e04290be93faChristian Maeder wordDom w1 == wordDom w2 && wordCod w1 == wordCod w2
cb2044812811d66efe038d914966e04290be93faChristian Maeder -- diagRule: the Diag rule
2353f65833a3da763392f771223250cd50b8d873Christian Maeder diagRule [(n1, s11, s12)] [(n2, s21, s22)] =
cb2044812811d66efe038d914966e04290be93faChristian Maeder isMorphSort diag (n1, s11) (n2, s21) && isMorphSort diag (n1, s12) (n2, s22) ||
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder isMorphSort diag (n2, s21) (n1, s11) && isMorphSort diag (n2, s22) (n1, s12)
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder diagRule _ _ = False
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder -- compRule: the Comp rule works for words 1 and 2-letter long
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder -- with equal domains and codomains
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder compRule w1@[_] w2@[_, _] = domCodEqual w1 w2
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder compRule w1@[_, _] w2@[_] = domCodEqual w1 w2
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder compRule _ _ = False
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder -- fixCongLc: apply Cong and Lc rules until a fixpoint is reached
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder fixCongLc rel =
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder let rel' = (leftCancellableClosure . congruenceClosure simeq) rel
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder in if rel == rel' then rel else fixCongLc rel'
2353f65833a3da763392f771223250cd50b8d873Christian Maeder -- compute the relation
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder rel = map (\w -> (w, w)) adm
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder rel' = mergeEquivClassesBy diagRule rel
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder rel'' = mergeEquivClassesBy compRule rel'
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder rel''' = fixCongLc rel''
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder in taggedValsToEquivClasses rel'''
cb2044812811d66efe038d914966e04290be93faChristian Maeder-- | Compute the (optimised) \cong relation given its (finite) domain and \sim relation.
2360728d4185c0c04279c999941c64d36626af79Christian Maeder-- Optimised \cong is supposed to contain only words composed of canonical embeddings;
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder-- we also use a (CompDiag) rule instead of (Comp) and (Diag) rules.
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maedercong :: CASLDiag
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder -> [DiagEmbWord] -- ^ the Adm_\simeq set (the domain of \cong relation)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> EquivRel DiagSort -- ^ the \simeq relation
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> EquivRel DiagEmb -- ^ the \sim relation
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> EquivRel DiagEmbWord
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maedercong diag adm simeq sim =
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder let -- domCodEqual: check that domains and codomains of given words are equal
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder domCodEqual w1 w2 =
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder wordDom w1 == wordDom w2 && wordCod w1 == wordCod w2
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- diagRule: the Diag rule
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder diagRule [(n1, s11, s12)] [(n2, s21, s22)] =
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder isMorphSort diag (n1, s11) (n2, s21) && isMorphSort diag (n1, s12) (n2, s22) ||
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder isMorphSort diag (n2, s21) (n1, s11) && isMorphSort diag (n2, s22) (n1, s12)
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder diagRule _ _ = False
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- compDiagRule: the combination of Comp and Diag rules
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder compDiagRule w1@[_] w2@[_, _] = compDiagRule w2 w1
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder compDiagRule [e1, e2] [d] =
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder let [ec1] = filter (\(e : _) -> e == e1) sim
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder [ec2] = filter (\(e : _) -> e == e2) sim
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder matches [] = False
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder matches (((n1, _, s12), (n2, s21, _)) : eps) =
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder if n1 == n2 && inRel sim d (n1, s21, s12)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder else matches eps
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder in matches [(me1, me2) | me1 <- ec1, me2 <- ec2]
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder compDiagRule _ _ = False
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder -- fixCongLc: apply Cong and Lc rules until a fixpoint is reached
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder fixCongLc rel =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let rel' = (leftCancellableClosure .
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder congruenceClosure (\w1 -> \w2 -> inRel simeq (wordCod w1) (wordDom w2))
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (\w1 -> \w2 -> w2 ++ w1)) rel
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in if rel == rel' then rel else fixCongLc rel'
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder -- compute the relation
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder rel = map (\w -> (w, w)) adm
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder rel' = mergeEquivClassesBy compDiagRule rel
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder rel'' = fixCongLc rel'
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder in taggedValsToEquivClasses rel''
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder-- | Compute the \cong^R relation
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian MaedercongR :: CASLDiag
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> EquivRel DiagSort -- ^ the \simeq relation
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder -> EquivRel DiagEmb -- ^ the \sim relation
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> EquivRel DiagEmbWord
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedercongR diag simeq sim =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder --cong diag (looplessWords (embs diag) simeq) simeq
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder cong diag (looplessWords (canonicalEmbs sim) simeq) simeq sim
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Compute the \sim relation
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maedersim :: CASLDiag
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> EquivRel DiagEmb
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maedersim diag embs =
5941ba0b9a99ac98f78a89a9f3303102657e36ccChristian Maeder let -- diagRule: the Diag rule
5941ba0b9a99ac98f78a89a9f3303102657e36ccChristian Maeder diagRule (n1, s11, s12) (n2, s21, s22) =
-- w.r.t. given \sim relation
ensuresAmalgamability :: Options.HetcatsOpts -- ^ program options
do if Options.caslAmalg opts == [] then return (DontKnow "Skipping amalgamability check")