Amalgamability.hs revision e6d40133bc9f858308654afb1262b8b483ec5922
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder{- |
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederDescription : Amalgamability analysis for CASL.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederCopyright : (c) Maciek Makowski, Warsaw University 2004-2006
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : till@tzi.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederPortability : portable
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaederAmalgamability analysis for CASL.
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski Follows the algorithm outlined in MFCS 2001 (LNCS 2136, pp. 451-463,
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski Springer 2001) paper.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{-
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederTODO:
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder* generalize for CASL extensions (at least for formulas. this is easy)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder* optimisations in congruenceClosure (Nelson-Oppen algorithm?)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder* optimisation in colimitIsThin (fixUpdRule)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder* optimisations in the whole algorithm
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang-}
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maedermodule CASL.Amalgamability(-- * Types
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder CASLSign, CASLMor, CASLDiag,
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder -- * Functions
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang ensuresAmalgamability) where
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport CASL.AS_Basic_CASL
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport Common.Id
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport Data.Graph.Inductive.Graph
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maederimport qualified Common.Lib.Graph as Tree
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederimport qualified Common.Lib.Map as Map
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Rel as Rel
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maederimport qualified Common.Lib.Set as Set
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maederimport Common.Doc
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettichimport Common.DocUtils
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maederimport Common.Result
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettichimport Common.Amalgamate
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport CASL.Sign
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport CASL.Morphism
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport Data.List
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu-- Exported types
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maedertype CASLSign = Sign () ()
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maedertype CASLMor = Morphism () () ()
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder-- Miscellaneous types
03136b84a0c70d877e227444f0875e209506b9e4Christian Maedertype CASLDiag = Tree.Gr CASLSign CASLMor
03136b84a0c70d877e227444f0875e209506b9e4Christian Maedertype DiagSort = (Node, SORT)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maedertype DiagOp = (Node, (Id, OpType))
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maedertype DiagPred = (Node, (Id, PredType))
03136b84a0c70d877e227444f0875e209506b9e4Christian Maedertype DiagEmb = (Node, SORT, SORT)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maedertype DiagEmbWord = [DiagEmb]
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder-- | equivalence classes are represented as lists of elements
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maedertype EquivClass a = [a]
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder-- | equivalence relations are represented as lists of equivalence classes
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maedertype EquivRel a = [EquivClass a]
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder-- | or, sometimes, as lists of pairs (element, equiv. class tag)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maedertype EquivRelTagged a b = [(a, b)]
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder-- Pretty instance (for diagnostic output)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maederinstance (Pretty a, Pretty b) => Pretty (Tree.Gr a b) where
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder pretty diag =
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder text "nodes:"
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder <+> pretty (labNodes diag)
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder $+$ text "edges:"
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder <+> pretty (labEdges diag)
e6dccba746efe07338d3107fed512e713fd50b28Christian Maeder
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder-- | find in Map
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaederfindInMap :: Ord k => k -> Map.Map k a -> a
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederfindInMap k m = maybe (error "Amalgamability.findInMap") id $
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder Map.lookup k m
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder-- | Compute the Sorts set -- a disjoint union of all the sorts
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder-- in the diagram.
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maedersorts :: CASLDiag -- ^ the diagram to get the sorts from
9a6779c8495854bdf36e4a87f98f095e8d0a6e45Christian Maeder -> [DiagSort]
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maedersorts diag =
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder let mkNodeSortPair n srt = (n, srt)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder appendSorts sl (n, Sign { sortSet = s }) =
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder sl ++ (map (mkNodeSortPair n) (Set.toList s))
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder in foldl appendSorts [] (labNodes diag)
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder-- | Compute the Ops set -- a disjoint union of all the operation symbols
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder-- in the diagram.
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederops :: CASLDiag -- ^ the diagram to get the ops from
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder -> [DiagOp]
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maederops diag =
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder let mkNodeOp n opId opType ol = ol ++ [(n, (opId, opType))]
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder mkNodeOps n opId opTypes ol =
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder ol ++ Set.fold (mkNodeOp n opId) [] opTypes
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder appendOps ol (n, Sign { opMap = m }) =
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder ol ++ Map.foldWithKey (mkNodeOps n) [] m
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder in foldl appendOps [] (labNodes diag)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- | Compute the Preds set -- a disjoint union of all the predicate symbols
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- in the diagram.
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maederpreds :: CASLDiag -- ^ the diagram to get the preds from
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder -> [DiagPred]
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederpreds diag =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let mkNodePred n predId predType pl = pl ++ [(n, (predId, predType))]
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mkNodePreds n predId predTypes pl =
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder pl ++ Set.fold (mkNodePred n predId) [] predTypes
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder appendPreds pl (n, Sign { predMap = m }) =
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder pl ++ Map.foldWithKey (mkNodePreds n) [] m
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski in foldl appendPreds [] (labNodes diag)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder-- | Convert the relation representation from list of pairs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- (val, equiv. class tag) to a list of equivalence classes.
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedertaggedValsToEquivClasses :: Ord b
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder => EquivRelTagged a b -- ^ a list of (value,tag) pairs
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -> EquivRel a
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian MaedertaggedValsToEquivClasses [] = []
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedertaggedValsToEquivClasses rel' =
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let -- prepMap: create a map with all the equivalence class tags mapped to
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- empty lists
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder prepMap rel =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski foldl (\m -> \k -> Map.insert (snd k) [] m) Map.empty rel
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- conv: perform actual conversion
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski convert [] m = map snd (Map.toList m)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder convert ((ds, ect) : dsps) m =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder let m' = Map.update (\ec -> Just (ds : ec)) ect m
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in convert dsps m'
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder in convert rel' (prepMap rel')
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder-- | Convert the relation representation from list of
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder-- equivalence classes to list of (value, tag) pairs.
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederequivClassesToTaggedVals :: Ord a
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder => EquivRel a
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -> EquivRelTagged a a
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederequivClassesToTaggedVals rel =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let eqClToList [] = []
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder eqClToList eqcl@(ft : _) = map (\x -> (x, ft)) eqcl
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in foldl (\vtl -> \eqcl -> vtl ++ (eqClToList eqcl)) [] rel
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{- the old, n^3 version of mergeEquivClassesBy:
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder-- | Merge the equivalence classes for elements fulfilling given condition.
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermergeEquivClassesBy :: Eq b
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder => (a -> a -> Bool)
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder -- ^ the condition stating when two elements are in relation
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder -> EquivRelTagged a b -- ^ the input relation
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> EquivRelTagged a b
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- ^ returns the input relation with equivalence classes merged according to
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder-- the condition.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermergeEquivClassesBy cond rel =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- Starting with the first element in the list an element (elem, tag) is taken
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- and cond is subsequently applied to it and all the elements
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- following it in the list. Whenever an element (elem', tag')
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder -- that is in relation with the chosen one is found, all the equivalence
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- class tags in the list that are equal to tag' are updated to tag.
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder let merge rel pos | pos >= length rel = rel
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski merge rel pos | otherwise =
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz let mergeWith cmpl _ [] = cmpl
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz mergeWith cmpl vtp@(elem, ec) toCmpl@((elem', ec') : _) =
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz let (cmpl', toCmpl') = if ec /= ec' && (cond elem elem')
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz then let upd (elem'', ec'') =
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz if ec'' == ec'
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz then (elem'', ec)
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz else (elem'', ec'')
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz in (map upd cmpl,
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz map upd toCmpl)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder else (cmpl, toCmpl)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder in mergeWith (cmpl' ++ [head toCmpl']) vtp (tail toCmpl')
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz (cmpl, (vtp : vtps)) = splitAt pos rel
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz rel' = mergeWith (cmpl ++ [vtp]) vtp vtps
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz in merge rel' (pos + 1)
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz in merge rel 0
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz-}
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulzdata TagEqcl a b = Eqcl [a] | TagRef b
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder deriving Show
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder-- | Merge the equivalence classes for elements fulfilling given condition.
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedermergeEquivClassesBy :: (Ord b)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder => (a -> a -> Bool)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- ^ the condition stating when two elements are in relation
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> EquivRelTagged a b -- ^ the input relation
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> EquivRelTagged a b
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder-- ^ returns the input relation with equivalence classes merged according to
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder-- the condition.
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaedermergeEquivClassesBy cond rel =
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder {- Starting with the first element in the list an element (elem,
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder tag) is taken and cond is subsequently applied to it and all the
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder elements following it in the list. Whenever an element (elem',
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder tag') that is in relation with the chosen one is found, the
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder equivalence classes in tagMap for tag and tag' are merged: tag in
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder tagMap points to the merged equivalence class and tag' in tagMap
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder is a reference to tag. -}
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder let -- create the initial map mapping tags to equivalence classes
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder initialTagMap =
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder let insEl tagMap (val, tag) =
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder case Map.member tag tagMap of
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder True -> Map.update (\(Eqcl eqcl) ->
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder Just (Eqcl (val : eqcl))) tag tagMap
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder False -> Map.insert tag (Eqcl [val]) tagMap
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder in foldl insEl Map.empty rel
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder -- merge equivalence classes tagged with t1 and t2
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder mergeInMap inTagMap t1 t2 =
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder let {- find the tag and equivalence class that corresponds
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder to the given tag performing path compression while
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder traversing the referneces. -}
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder findEqcl t tagMap =
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder case findInMap t tagMap of
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder Eqcl eqcl -> (t, eqcl, tagMap)
4e144aa4be1f50519f8fa377a7883edfbc76d406Christian Maeder TagRef t' -> let
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder (rt, eqcl, tagMap') = findEqcl t' tagMap
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder tagMap'' = if rt == t' then tagMap' else
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder Map.update (\_ -> Just (TagRef rt)) t tagMap'
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder in (rt, eqcl, tagMap'')
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (rt1, eqcl1, tagMap1) = findEqcl t1 inTagMap
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (rt2, eqcl2, tagMap2) = findEqcl t2 tagMap1
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder in if rt1 == rt2 then tagMap2
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder else let (nrt1, nrt2) = if rt1 > rt2 then (rt2, rt1)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder else (rt1, rt2)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder tagMap3 = Map.update
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder (\_ -> Just (Eqcl (eqcl1 ++ eqcl2))) nrt1 tagMap2
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder tagMap4 = Map.update
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder (\_ -> Just (TagRef nrt1)) nrt2 tagMap3
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder in tagMap4
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder {- iterate through the relation merging equivalence classes of
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder appropriate elements -}
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder merge tagMap' rel' pos | pos >= length rel' = tagMap'
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder merge tagMap' rel' pos | otherwise =
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder let mergeWith tagMap _ [] = tagMap
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder mergeWith tagMap vtp@(elem1, ec) toCmpl@((elem2, ec') : _) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let tagMap1 = if ec /= ec' && (cond elem1 elem2)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder then mergeInMap tagMap ec ec'
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder else tagMap
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder in mergeWith tagMap1 vtp (tail toCmpl)
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder (_, (vtp' : vtps)) = splitAt pos rel'
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder tagMap'' = mergeWith tagMap' vtp' vtps
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder in merge tagMap'' rel' (pos + 1)
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder -- append given equivalence class to the list of (value, tag) pairs
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder tagMapToRel rel' (_, TagRef _) = rel'
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder tagMapToRel rel' (tag, Eqcl eqcl) =
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder foldl (\l -> \v -> (v, tag) : l) rel' eqcl
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder myTagMap = merge initialTagMap rel 0
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder in foldl tagMapToRel [] (Map.toList myTagMap)
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder-- | Merge the equivalence classes for given tags.
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedermergeEquivClasses :: Eq b
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder => EquivRelTagged a b
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder -> b -- ^ tag 1
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> b -- ^ tag 2
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> EquivRelTagged a b
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedermergeEquivClasses rel tag1 tag2 | tag1 == tag2 = rel
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder | otherwise =
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder let upd (el, tag) | tag == tag2 = (el, tag1)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder | otherwise = (el, tag)
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder in map upd rel
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder-- | Return true if there is an edge between srcNode and targetNode
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder-- and the morphism with which it's labelled maps srcSort to targetSort
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian MaederisMorphSort :: CASLDiag
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> DiagSort
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> DiagSort
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> Bool
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederisMorphSort diag (srcNode, srcSort) (targetNode, targetSort) =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let checkEdges [] = False
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder checkEdges ((sn, tn, Morphism { sort_map = sm }) : edgs) =
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder if sn == srcNode &&
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder tn == targetNode &&
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder mapSort sm srcSort == targetSort
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder then True else checkEdges edgs
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder in checkEdges (out diag srcNode)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- | Return true if there is an edge between srcNode and targetNode
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder-- and the morphism with which it's labelled maps srcOp to targetOp
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian MaederisMorphOp :: CASLDiag
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder -> DiagOp
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> DiagOp
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> Bool
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaederisMorphOp diag (srcNode, srcOp) (targetNode, targetOp) =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let checkEdges [] = False
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder checkEdges ((sn, tn, Morphism { sort_map=sm, fun_map=fm }) : edgs) =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder if sn == srcNode &&
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder tn == targetNode &&
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder mapOpSym sm fm srcOp == targetOp
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder then True else checkEdges edgs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder in checkEdges (out diag srcNode)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- | Return true if there is an edge between srcNode and targetNode
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- and the morphism with which it's labelled maps srcPred to targetPred
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaederisMorphPred :: CASLDiag
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder -> DiagPred
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> DiagPred
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -> Bool
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederisMorphPred diag (srcNode, srcPred) (targetNode, targetPred) =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let checkEdges [] = False
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder checkEdges ((sn, tn, Morphism { sort_map=sm, pred_map=pm }) : edgs) =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder if sn == srcNode &&
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder tn == targetNode &&
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder mapPredSym sm pm srcPred == targetPred
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder then True else checkEdges edgs
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder in checkEdges (out diag srcNode)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- | Compute the simeq relation for given diagram.
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maedersimeq :: CASLDiag -- ^ the diagram for which the relation should be created
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> EquivRel DiagSort
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- ^ returns the relation represented as a list of equivalence
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- classes (each represented as a list of diagram ops)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maedersimeq diag =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- During the computations the relation is represented as a list of pairs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- (DiagSort, DiagSort). The first element is a diagram sort and the second
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- denotes the equivalence class to which it belongs. All the pairs with
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- equal second element denote elements of one equivalence class.
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let mergeCond ds ds' = isMorphSort diag ds ds' || isMorphSort diag ds' ds
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- compute the relation
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder rel = map (\ds -> (ds, ds)) (sorts diag)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder rel' = mergeEquivClassesBy mergeCond rel
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder in taggedValsToEquivClasses rel'
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- | Compute the simeq^op relation for given diagram.
99476ac2689c74251219db4782e57fe713a24a52Christian MaedersimeqOp :: CASLDiag -- ^ the diagram for which the relation should be created
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder -> EquivRel DiagOp
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder-- ^ returns the relation represented as a list of equivalence
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder-- classes (each represented as a list of diagram ops)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedersimeqOp diag =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- During the computations the relation is represented as a list of pairs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- (DiagOp, DiagOp). The first element is a diagram op and the second
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- denotes the equivalence class to which it belongs. All the pairs with
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- equal second element denote elements of one equivalence class.
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let mergeCond ds ds' = isMorphOp diag ds ds' || isMorphOp diag ds' ds
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- compute the relation
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder rel = map (\ds -> (ds, ds)) (ops diag)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder rel' = mergeEquivClassesBy mergeCond rel
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder in taggedValsToEquivClasses rel'
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- | Compute the simeq^pred relation for given diagram.
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedersimeqPred :: CASLDiag
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder -- ^ the diagram for which the relation should be created
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> EquivRel DiagPred
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- ^ returns the relation represented as a list of equivalence
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- classes (each represented as a list of diagram preds)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedersimeqPred diag =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- During the computations the relation is represented as a list of pairs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- (DiagPred, DiagPred). The first element is a diagram pred and the second
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- denotes the equivalence class to which it belongs. All the pairs with
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- equal second element denote elements of one equivalence class.
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let mergeCond ds ds' = isMorphPred diag ds ds' || isMorphPred diag ds' ds
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- compute the relation
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder rel = map (\ds -> (ds, ds)) (preds diag)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski rel' = mergeEquivClassesBy mergeCond rel
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder in taggedValsToEquivClasses rel'
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder-- | Compute the simeq_tau relation for given diagram.
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maedersimeq_tau :: [(Node, CASLMor)]
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -> EquivRel DiagSort
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maedersimeq_tau sink =
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder let -- tagEdge: for given morphism m create a list of pairs
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder -- (a, b) where a is DiagSort from the source signature that
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -- is mapped by m to b
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder tagEdge (sn, Morphism { msource = src, sort_map = sm }) =
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder map (\ ss -> ((sn, ss), mapSort sm ss))
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder (Set.toList $ sortSet src)
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder rel = foldl (\l -> \e -> l ++ (tagEdge e)) [] sink
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder in taggedValsToEquivClasses rel
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder-- | Compute the simeq^op_tau relation for given diagram.
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaedersimeqOp_tau :: [(Node, CASLMor)]
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -> EquivRel DiagOp
a74f814d3b445eadad6f68737a98a7a303698affChristian MaedersimeqOp_tau sink =
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder let -- tagEdge: for given morphism m create a list of pairs
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -- (a, b) where a is DiagOp from the source signature that
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -- is mapped by m to b
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder tagEdge (sn, Morphism { msource=src, sort_map = sm, fun_map = fm }) =
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder map (\srcOp -> ((sn, srcOp), mapOpSym sm fm srcOp))
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder (concatMap ( \ (i, s) ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder map ( \ ot -> (i, ot)) $ Set.toList s)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $ Map.toList $ opMap src)
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder rel = foldl (\l -> \e -> l ++ (tagEdge e)) [] sink
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder in taggedValsToEquivClasses rel
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder-- | Compute the simeq^pred_tau relation for given diagram.
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaedersimeqPred_tau :: [(Node, CASLMor)]
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder -> EquivRel DiagPred
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaedersimeqPred_tau sink =
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder let -- tagEdge: for given morphism m create a list of pairs
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder -- (a, b) where a is DiagPred from the source signature that
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski -- is mapped by m to b
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder tagEdge (sn, Morphism { msource=src, sort_map = sm, pred_map = pm }) =
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder map (\srcPred -> ((sn, srcPred), mapPredSym sm pm srcPred))
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder (concatMap ( \ (i, s) ->
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder map ( \ pt -> (i, pt)) $ Set.toList s)
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder $ Map.toList $ predMap src)
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maeder rel = foldl (\l -> \e -> l ++ (tagEdge e)) [] sink
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder in taggedValsToEquivClasses rel
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder-- | Check that one equivalence relation is a subset of another.
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder-- The relations are represented as a lists of equivalence classes,
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- where equivalence classes are lists of elements.
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedersubRelation :: Eq a
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder => EquivRel a -- ^ the relation that is supposed to be a subset
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder -> EquivRel a -- ^ the relation that is supposed to be a superset
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -> Maybe (a, a)
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder-- ^ returns a pair of elements that are in the same equivalence class of the
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- first relation but are not in the same equivalence class of the second
808b2db6b704633517cf3a1a9630166beab28df7Christian Maeder-- relation or Nothing the first relation is a subset of the second one.
808b2db6b704633517cf3a1a9630166beab28df7Christian MaedersubRelation [] _ = Nothing
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaedersubRelation ([] : eqcls) sup = subRelation eqcls sup
808b2db6b704633517cf3a1a9630166beab28df7Christian Maeder -- this should never be the case
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian MaedersubRelation (elts'@(elt' : _) : eqcls') sup =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let findEqCl _ [] = []
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder findEqCl elt (eqcl : eqcls) =
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder if elem elt eqcl then eqcl else findEqCl elt eqcls
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder checkEqCl [] _ = Nothing
808b2db6b704633517cf3a1a9630166beab28df7Christian Maeder checkEqCl (elt : elts) supEqCl =
808b2db6b704633517cf3a1a9630166beab28df7Christian Maeder if elem elt supEqCl
808b2db6b704633517cf3a1a9630166beab28df7Christian Maeder then checkEqCl elts supEqCl
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder else Just elt
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder curFail = checkEqCl elts' (findEqCl elt' sup)
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder in case curFail of
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder Nothing -> subRelation eqcls' sup
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder Just elt2 -> Just (elt', elt2)
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski-- | Compute the set of sort embeddings defined in the diagram.
74d9a385499bf903b24848dff450a153f525bda7Christian Maederembs :: CASLDiag
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -> [DiagEmb]
a74f814d3b445eadad6f68737a98a7a303698affChristian Maederembs diag =
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder let embs' [] = []
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski embs' ((n, Sign {sortRel = sr}) : lNodes) =
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder (map (\(s1, s2) -> (n, s1, s2)) (Rel.toList sr)) ++ (embs' lNodes)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski in embs' (labNodes diag)
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski-- | Compute the set of sort embeddings (relations on sorts) defined
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski-- in the source nodes of the sink.
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedersinkEmbs :: CASLDiag -- ^ the diagram
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -> [(Node, CASLMor)] -- ^ the sink
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> [DiagEmb]
5e46b572ed576c0494768998b043d9d340594122Till MossakowskisinkEmbs _ [] = []
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian MaedersinkEmbs diag ((srcNode, _) : edgs) =
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder let (_, _, Sign {sortRel = sr}, _) = context diag srcNode
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder in (map (\(s1, s2) -> (srcNode, s1, s2)) (Rel.toList sr))
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder ++ (sinkEmbs diag edgs)
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder-- | Check if the two given elements are in the given relation.
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian MaederinRel :: Eq a
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder => EquivRel a -- ^ the relation
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder -> a -- ^ the first element
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder -> a -- ^ the second element
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder -> Bool
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian MaederinRel [] _ _ = False
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian MaederinRel (eqc : eqcs) a b | a == b = True
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder | otherwise =
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder case find (\x -> x == a) eqc of
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder Nothing -> inRel eqcs a b
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder Just _ -> case find (\x -> x == b) eqc of
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder Nothing -> False
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder Just _ -> True
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder-- | Check if two embeddings can occur subsequently in a word
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder-- given the simeq relation on sorts.
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maederadmissible :: EquivRel DiagSort -- ^ the \simeq relation
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder -> DiagEmb -- ^ the first embedding
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -> DiagEmb -- ^ the second embedding
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder -> Bool
d058429727dd696a0327cdc28cadd268c34c36baChristian Maederadmissible simeq' (n1, s1, _) (n2, _, s2) =
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder inRel simeq' (n1, s1) (n2, s2)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder-- | Compute the set of all the loopless, admissible
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder-- words over given set of embeddings.
a74f814d3b445eadad6f68737a98a7a303698affChristian MaederlooplessWords :: [DiagEmb] -- ^ the embeddings
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder -> EquivRel DiagSort
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder -- ^ the \simeq relation that defines admissibility
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> [DiagEmbWord]
d058429727dd696a0327cdc28cadd268c34c36baChristian MaederlooplessWords embs1 simeq1 =
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder let -- generate the list of all loopless words over given alphabet
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -- with given suffix
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder looplessWords' suff@(e : _) embs2 pos | pos >= length embs2 = [suff]
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder | otherwise =
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder let emb = embs2 !! pos
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder embs' = embs2 \\ [emb]
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ws = if admissible simeq1 emb e
5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder then looplessWords' (emb : suff) embs' 0
5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder else []
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder in ws ++ (looplessWords' suff embs2 (pos + 1))
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder looplessWords' [] embs2 pos | pos >= length embs2 = []
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder | otherwise =
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski let emb = embs2 !! pos
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder embs' = embs2 \\ [emb]
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder in looplessWords' [emb] embs' 0 ++
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder looplessWords' [] embs2 (pos + 1)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder in looplessWords' [] embs1 0
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder-- | Return the codomain of an embedding path.
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederwordCod :: DiagEmbWord
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder -> DiagSort
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederwordCod ((n, _, s2) : _) = (n, s2)
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian MaederwordCod [] = error "wordCod"
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder
27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder-- | Return the domain of an embedding path.
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian MaederwordDom :: DiagEmbWord
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -> DiagSort
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederwordDom [] = error "wordDom"
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederwordDom w = let (n, s1, _) = last w in (n, s1)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
32562a567baac248a00782d2727716c13117dc4aChristian Maeder
32562a567baac248a00782d2727716c13117dc4aChristian Maeder-- | Find an equivalence class tag for given element.
32562a567baac248a00782d2727716c13117dc4aChristian MaederfindTag :: Eq a
32562a567baac248a00782d2727716c13117dc4aChristian Maeder => EquivRelTagged a b
32562a567baac248a00782d2727716c13117dc4aChristian Maeder -> a
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder -> Maybe b
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian MaederfindTag [] _ = Nothing
fa373bc327620e08861294716b4454be8d25669fChristian MaederfindTag ((w', t) : wtps) w =
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder if w == w' then Just t else findTag wtps w
fa373bc327620e08861294716b4454be8d25669fChristian Maeder
fa373bc327620e08861294716b4454be8d25669fChristian Maeder
fa373bc327620e08861294716b4454be8d25669fChristian Maeder-- | Compute the left-cancellable closure of a relation on words.
fa373bc327620e08861294716b4454be8d25669fChristian MaederleftCancellableClosure :: EquivRelTagged DiagEmbWord DiagEmbWord
fa373bc327620e08861294716b4454be8d25669fChristian Maeder -> EquivRelTagged DiagEmbWord DiagEmbWord
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian MaederleftCancellableClosure rel1 =
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder let -- checkPrefixes: for each common prefix of two given words
32562a567baac248a00782d2727716c13117dc4aChristian Maeder -- merge the equivalence classes of the suffixes
32562a567baac248a00782d2727716c13117dc4aChristian Maeder checkPrefixes [] _ rel = rel
32562a567baac248a00782d2727716c13117dc4aChristian Maeder checkPrefixes _ [] rel = rel
fa373bc327620e08861294716b4454be8d25669fChristian Maeder checkPrefixes w1@(l1 : suf1) w2@(l2 : suf2) rel | w1 == w2 = rel
fa373bc327620e08861294716b4454be8d25669fChristian Maeder | l1 /= l2 = rel
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder | otherwise =
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder let tag1 = maybe (error "checkPrefixes: tag1") id
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder $ findTag rel suf1
32562a567baac248a00782d2727716c13117dc4aChristian Maeder tag2 = maybe (error "checkPrefixes: tag2") id
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder $ findTag rel suf2
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder rel' = if tag1 == tag2 then rel
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder else let upd (w, t) | t == tag2 = (w, tag1)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder | otherwise = (w, t)
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder in map upd rel
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder in checkPrefixes suf1 suf2 rel'
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -- iterateWord1: for each pair of related words call checkPrefixes
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder iterateWord1 rel pos | pos >= length rel = rel
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder | otherwise =
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder let iterateWord2 wtp1@(w1, t1) rel2 pos2
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder | pos2 >= length rel2 = rel2
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder | otherwise =
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder let _wtp2@(w2, t2) = rel2 !! pos2
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder rel3 = if t1 == t2 then checkPrefixes w1 w2 rel2
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder else rel2
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder in iterateWord2 wtp1 rel3 (pos2 + 1)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder wtp = rel !! pos
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder rel' = iterateWord2 wtp rel 0
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder in iterateWord1 rel' (pos + 1)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder in {-trace ("leftCancellableClosure " ++ show rel) $-} iterateWord1 rel1 0
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder{- | Compute the congruence closure of an equivalence R: two pairs of
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederelements (1, 3) and (2, 4) are chosen such that 1 R 2 and 3 R 4. It is
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederthen checked that elements 1, 3 and 2, 4 are in relation supplied and
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederif so equivalence classes for (op 1 3) and (op 1 4) in R are merged.
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederThis function should be applied to the relation until a fixpoint is
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederreached. -}
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaedercongruenceClosure :: (Eq a, Eq b)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder => (a -> a -> Bool)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder -- ^ the check to be performed on elements 1, 3 and 2, 4
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder -> (a -> a -> a)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder -- ^ the operation to be performed on elements 1, 3 and 2, 4
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder -> EquivRelTagged a b
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder -> EquivRelTagged a b
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaedercongruenceClosure check op rel =
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder let -- iterateWord1
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder iterateWord1 rel1 pos1 | pos1 >= length rel1 = rel1
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder | otherwise = let -- iterateWord2
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder iterateWord2 wtp1@(_, t1) rel2 pos2 | pos2 >= length rel2 = rel2
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder | otherwise = let -- iterateWord3
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder iterateWord3 wtp1'@(w1', _) wtp2' rel3 pos3
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder | pos3 >= length rel3 = rel3
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder | otherwise = let -- iterateWord4
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder iterateWord4 wtp1''@(w1, _) wtp2''@(w2, _) wtp3'@(w3, t3) rel4 pos4
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder | pos4 >= length rel4 = rel4
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder | otherwise = let
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder (w4, t4) = rel4 !! pos4
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder rel4' = if t3 /= t4 || not (check w2 w4) then rel4 else let
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder mct1 = findTag rel (op w1 w3)
32562a567baac248a00782d2727716c13117dc4aChristian Maeder mct2 = findTag rel (op w2 w4)
32562a567baac248a00782d2727716c13117dc4aChristian Maeder in case (mct1, mct2) of
32562a567baac248a00782d2727716c13117dc4aChristian Maeder (Nothing, _) -> rel4 -- w3w1 is not in the domain of rel
fa373bc327620e08861294716b4454be8d25669fChristian Maeder (_, Nothing) -> rel4 -- w4w2 is not in the domain of rel
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder (Just ct1, Just ct2) -> mergeEquivClasses rel4 ct1 ct2
fa373bc327620e08861294716b4454be8d25669fChristian Maeder in iterateWord4 wtp1'' wtp2'' wtp3' rel4' (pos4 + 1)
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder wtp3@(w3', _) = rel3 !! pos3
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder rel3' = if check w1' w3' --inRel here is usually much more efficient
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder -- than findTag rel (w3 ++ w1)
32562a567baac248a00782d2727716c13117dc4aChristian Maeder then iterateWord4 wtp1' wtp2' wtp3 rel3 0 else rel3
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski in iterateWord3 wtp1' wtp2 rel3' (pos3 + 1)
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder wtp2@(_, t2) = rel2 !! pos2
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder rel2' = if t1 /= t2 then rel2 else iterateWord3 wtp1 wtp2 rel2 0
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder in iterateWord2 wtp1 rel2' (pos2 + 1)
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder wtp = rel1 !! pos1
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder rel' = iterateWord2 wtp rel1 0
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder in iterateWord1 rel' (pos1 + 1)
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder in{- trace ("congruenceClosure " ++ show rel) $-} iterateWord1 rel 0
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder
3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till Mossakowski
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- | Compute the cong_tau relation for given diagram and sink.
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maedercong_tau :: CASLDiag -- ^ the diagram
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder -> [(Node, CASLMor)] -- ^ the sink
3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till Mossakowski -> EquivRel DiagSort -- ^ the \simeq_tau relation
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder -> EquivRel DiagEmbWord
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maedercong_tau diag sink st =
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder -- domCodSimeq: check that domains and codomains of given words are related
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder let domCodSimeq w1 w2 = inRel st (wordDom w1) (wordDom w2)
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till Mossakowski && inRel st (wordCod w1) (wordCod w2)
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder embs1 = sinkEmbs diag sink
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder words1 = looplessWords embs1 st
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder rel = map (\w -> (w, w)) words1
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder rel' = mergeEquivClassesBy domCodSimeq rel
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder in taggedValsToEquivClasses rel'
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till Mossakowski-- | Compute the finite representation of cong_0 relation for given diagram.
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang-- The representation consists only of equivalence classes that
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang-- contain more than one element.
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangcong_0 :: CASLDiag
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder -> EquivRel DiagSort -- ^ the \simeq relation
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> EquivRel DiagEmbWord
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maedercong_0 diag simeq' =
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder let -- diagRule: the Diag rule
fc033b8680245bf692c9c09723fd3046ff38971eChristian Maeder diagRule [(n1, s11, s12)] [(n2, s21, s22)] =
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder isMorphSort diag (n1, s11) (n2, s21)
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder && isMorphSort diag (n1, s12) (n2, s22)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder || isMorphSort diag (n2, s21) (n1, s11)
5824312cc0cfccce61f195fbe92307a21a467049Christian Maeder && isMorphSort diag (n2, s22) (n1, s12)
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder diagRule _ _ = False
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder -- addToRel: add given word to given relation
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder addToRel [] _ = []
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder addToRel ([] : _) _ = error "addToRel"
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder addToRel (eqcl@(refw : _) : eqcls) w =
fc033b8680245bf692c9c09723fd3046ff38971eChristian Maeder if wordDom w == wordDom refw && wordCod w == wordCod refw
fc033b8680245bf692c9c09723fd3046ff38971eChristian Maeder then ((w : eqcl) : eqcls)
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder else (eqcl : (addToRel eqcls w))
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder -- words2: generate all the admissible 2-letter words over given alphabet
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder words2 _ [] _ = []
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder words2 alph (_ : embs1) [] = words2 alph embs1 alph
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder words2 alph embs1@(emb1 : _) (emb2 : embs2) =
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang let ws = words2 alph embs1 embs2
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder in if admissible simeq' emb1 emb2
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder then ([emb1, emb2] : ws) else ws
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder -- compute the relation
em = embs diag
rel = map (\e -> ([e], [e])) em
rel' = mergeEquivClassesBy diagRule rel
rel'' = taggedValsToEquivClasses rel'
w2s = words2 em em em
rel''' = foldl addToRel rel'' w2s
in rel'''
-- | Compute the set Adm_\simeq if it's finite.
finiteAdm_simeq :: [DiagEmb] -- ^ the embeddings
-> EquivRel DiagSort
-- ^ the \simeq relation that defines admissibility
-> Maybe [DiagEmbWord]
-- ^ returns the computed set or Nothing if it's infinite
finiteAdm_simeq embs' simeq' =
let -- generate the list of the words over given alphabet
-- with given suffix
embWords' suff@(e : _) embs1 pos | pos >= length embs1 = Just [suff]
| otherwise =
let emb = embs1 !! pos
mws1 = if admissible simeq' emb e
then if any (\emb' -> emb' == emb) suff
then Nothing
else embWords' (emb : suff) embs1 0
else Just []
mws2 = case mws1 of
Nothing -> Nothing
Just _ -> embWords' suff embs1 (pos + 1)
in case mws1 of
Nothing -> Nothing
Just ws1 -> case mws2 of
Nothing -> Nothing
Just ws2 -> Just (ws1 ++ ws2)
embWords' [] embs1 pos | pos >= length embs1 = Just []
embWords' [] embs1 pos | otherwise =
let emb = embs1 !! pos
mws1 = embWords' [emb] embs1 0
mws2 = case mws1 of
Nothing -> Nothing
Just _ -> embWords' [] embs1 (pos + 1)
in case mws1 of
Nothing -> Nothing
Just ws1 -> case mws2 of
Nothing -> Nothing
Just ws2 -> Just (ws1 ++ ws2)
in embWords' [] 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 simeq' embs' c0 =
let -- sortsC: a list of colimit sorts
sortsC = foldl (\ls -> \eqcl -> (head eqcl : ls)) [] simeq'
simeqT = equivClassesToTaggedVals simeq'
-- ordMap: map representing the topological order on sorts in the colimit
ordMap =
let sortClasses' m [] = m
sortClasses' m ((n, s1, s2) : embs1) =
let c1 = maybe (error "sortClasses:s1") id
$ findTag simeqT (n, s1)
c2 = maybe (error "sortClasses:s2") id
$ findTag simeqT (n, s2)
in sortClasses' (Map.update (\se -> Just
(Set.insert c2 se)) c1 m) embs1
ordMap' = foldl (\m -> \cl -> Map.insert cl Set.empty m)
Map.empty sortsC
in sortClasses' ordMap' embs'
-- larger: return a list of colimit sorts larger than given sort
larger srt =
let dl = Set.toList (findInMap srt ordMap)
in (srt : (foldl (\l -> \so -> l ++ (larger so)) [] dl))
-- s: the map representing sets S_{\geq s1,s2}
s = let compS m (s1, s2) =
let ls1 = Set.fromList (larger s1)
ls2 = Set.fromList (larger s2)
in Map.insert (s1, s2) (Set.intersection ls1 ls2) m
in foldl compS Map.empty [(s1, s2) | s1 <- sortsC, s2 <- sortsC]
-- b: the map representing sets B_{s1,s2}
b = let compB m sp =
let sim' s' s'' = not (Set.null (findInMap (s', s'') s))
rel = map (\x -> (x, x)) (Set.toList (findInMap sp s))
rel' = mergeEquivClassesBy sim' rel
in Map.insert sp (taggedValsToEquivClasses rel') m
in foldl compB Map.empty [(s1, s2) | s1 <- sortsC, s2 <- sortsC]
embDomS (n, dom, _) = maybe (error "embDomS") id
$ findTag simeqT (n, dom)
embCodS (n, _, cod) = maybe (error "embCodS") id
$ findTag simeqT (n, cod)
-- checkAllSorts: check the C = B condition for all colimit sorts
checkAllSorts m | Map.null m = {-trace "CT: Yes"-} True
| otherwise =
let -- checkSort: check if for given colimit sort C = B
checkSort chs = let
embsCs = filter (\e -> embDomS e == chs) embs'
c = foldl (\ma -> \ep -> Map.insert ep [] ma) Map.empty
[(d, e) | d <- embsCs, e <- embsCs]
c' = let
updC c1 (d, e) = let
s1 = embCodS d
s2 = embCodS e
in Map.update (\_ -> Just (findInMap (s1, s2) b)) (d, e) c1
in foldl updC c
[(d, e) | d <- embsCs, e <- embsCs, inRel c0 [d] [e]]
c'' = let
updC c1 (d@(n1, _, cod1), e@(n2, _, cod2)) = let
s1 = embCodS d
s2 = embCodS e
in if filter (\(n, dom, cod) -> (n, dom) == (n1, cod1)
&& (n, cod) == (n2, cod2)) embs' == []
then c else let
[absCls] = filter (\ac -> any (s2==) ac)
(findInMap (s1, s2) b)
in foldl (\c2 k -> Map.update (\l -> Just
(l ++ [absCls])) k c2) c1 [(d, e), (e, d)]
in foldl updC c' [(d, e) | d <- embsCs,
e <- embsCs, wordDom [d] == wordDom [e]]
fixUpdRule cFix = let
updC c1 (e1, e2, e3) = let
updC' c2 (b12, b23, b13) = let
sb12 = Set.fromList b12
sb23 = Set.fromList b23
sb13 = Set.fromList b13
comm = Set.intersection sb12 (Set.intersection sb23 sb13)
in if Set.null comm then c2 else let
c2' = if any (\l -> l == b13) (findInMap (e1, e3) c2)
then c2
else Map.update (\l -> Just (l ++ [b13])) (e1, e3) c2
in if any (\l -> l == b13) (findInMap (e1, e3) c2')
then c2'
else Map.update (\l -> Just (l ++ [b13])) (e3, e1) c2'
s1 = embCodS e1
s3 = embCodS e3
in foldl updC' c1 [(b12, b23, b13) |
b12 <- (findInMap (e1, e2) c1),
b23 <- (findInMap (e2, e3) c1),
b13 <- (findInMap (s1, s3) b)]
cFix' = foldl updC cFix [(e1, e2, e3) |
e1 <- embsCs, e2 <- embsCs, e3 <- embsCs]
in if cFix' == cFix then cFix else fixUpdRule cFix'
c3 = fixUpdRule c''
checkIncl [] = True
checkIncl ((e1, e2) : embprs) = let
s1 = embCodS e1
s2 = embCodS e2
res = if subRelation (findInMap (s1, s2) b)
(findInMap (e1, e2) c3) == Nothing then checkIncl embprs
else False
in {- trace ("B[" ++ (show s1) ++ ", " ++ (show s2) ++ ":\n"
++ (show (findInMap (s1, s2) b))
++ "\n" ++ "C[" ++ (show e1) ++
", " ++ (show e2) ++ ":\n" ++
(show (findInMap (e1, e2) c3)) ++
"\n\n") -} res
in checkIncl [(e1, e2) | e1 <- embsCs, e2 <- embsCs]
-- cs: next colimit sort to process
-- m1: the order map with cs removed
(cs, m1) = let
[(cs', _)] = take 1 (filter (\(_, lt) -> Set.null lt)
(Map.toList m))
m' = Map.delete cs' m
m'' = foldl (\ma -> \k -> Map.update (\lt -> Just
(Set.delete cs lt)) k ma)
m' (Map.keys m')
in (cs', m'')
in if checkSort cs then checkAllSorts m1
else {-trace "CT: No"-} False
in {-trace ("\\simeq: " ++ (show simeq) ++ "\nEmbs: " ++ (show
embs) ++ "\n\\cong_0: " ++ show c0)-} checkAllSorts 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 diag adm simeq' sim' =
-- 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
-- compDiagRule: the combination of Comp and Diag rules
compDiagRule w1@[_] w2@[_, _] = compDiagRule w2 w1
compDiagRule [e1, e2] [d] =
let [ec1] = filter (\(e : _) -> e == e1) sim'
[ec2] = filter (\(e : _) -> e == e2) sim'
matches' [] = False
matches' (((n1, _, s12), (n2, s21, _)) : eps) =
if n1 == n2 && inRel sim' d (n1, s21, s12)
then True
else matches' eps
in matches' [(me1, me2) | me1 <- ec1, me2 <- ec2]
compDiagRule _ _ = False
-- fixCongLc: apply Cong and Lc rules until a fixpoint is reached
fixCongLc rel1 =
let rel2 = (leftCancellableClosure .
congruenceClosure (\w1 -> \w2 ->
inRel simeq' (wordCod w1) (wordDom w2))
(\w1 -> \w2 -> w2 ++ w1)) rel1
in if rel1 == rel2 then rel1 else fixCongLc rel2
-- compute the relation
rel = map (\w -> (w, w)) adm
rel' = mergeEquivClassesBy compDiagRule rel
rel'' = fixCongLc rel'
in taggedValsToEquivClasses rel''
-- | Compute the \cong^R relation
congR :: CASLDiag
-> EquivRel DiagSort -- ^ the \simeq relation
-> EquivRel DiagEmb -- ^ the \sim relation
-> EquivRel DiagEmbWord
congR diag simeq' sim' =
--cong diag (looplessWords (embs diag) simeq) simeq
cong diag (looplessWords (canonicalEmbs sim') simeq') simeq' sim'
-- | Compute the \sim relation
sim :: CASLDiag
-> [DiagEmb]
-> EquivRel DiagEmb
sim diag embs' =
let -- 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)
-- the check for congruenceClosure
check (p, s11, s12) (q, s21, s22) =
if p /= q || s12 /= s21 then False
else any (\(n, s1, s2) -> n == p && s1 == s11 && s2 == s22) embs'
-- the op for congruence closure
op (p, s1, _) (_, _, s2) = (p, s1, s2)
-- fixCong: apply Cong rule until a fixpoint is reached
fixCong rel1 =
let rel2 = congruenceClosure check op rel1
in if rel1 == rel2 then rel1 else fixCong rel2
rel = map (\e -> (e, e)) embs'
rel' = fixCong rel
rel'' = mergeEquivClassesBy diagRule rel'
in taggedValsToEquivClasses rel''
-- | Compute the CanonicalEmbs(D) set given \sim relation
canonicalEmbs :: EquivRel DiagEmb
-> [DiagEmb]
canonicalEmbs sim' =
foldl (\l -> \(e : _) -> (e : l)) [] sim'
-- | Convert given \cong_\tau relation to the canonical form
-- w.r.t. given \sim relation
canonicalCong_tau :: EquivRel DiagEmbWord
-> EquivRel DiagEmb
-> EquivRel DiagEmbWord
canonicalCong_tau ct sim' =
let mapEmb e = let Just (ce : _) = find (elem e) sim'
in ce
mapWord w = map mapEmb w
mapEqcl ec = map mapWord ec
in map mapEqcl ct
-- | Convert a word to a list of sorts that are embedded
wordToEmbPath :: DiagEmbWord
-> [SORT]
wordToEmbPath [] = []
wordToEmbPath ((_, s1, s2) : embs1) =
let rest [] = []
rest ((_, s, _) : embs2) = (rest embs2) ++ [s]
in (rest embs1) ++ [s1, s2]
hasCellCaslAmalgOpt :: [CASLAmalgOpt] -> Bool
hasCellCaslAmalgOpt = any ( \ o -> case o of
Cell -> True
_ -> False)
hasColimitThinnessOpt :: [CASLAmalgOpt] -> Bool
hasColimitThinnessOpt = any ( \ o -> case o of
ColimitThinness -> True
_ -> 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 opts diag sink desc =
if null opts then return (DontKnow "Skipping amalgamability check")
else let -- aux. functions that help printing out diagnostics
getNodeSig _ [] = emptySign () -- this should never be the case
getNodeSig n ((n1, sig) : nss) = if n == n1 then sig else getNodeSig n nss
lns = labNodes diag
formatOp (idt, t) = showDoc idt " :" ++ showDoc t ""
formatPred (idt, t) = showDoc idt " : " ++ showDoc t ""
formatSig n = case find (\(n', d) -> n' == n && d /= "") (labNodes desc) of
Just (_, d) -> d
Nothing -> showDoc (getNodeSig n lns) ""
-- and now the relevant stuff
s = {-trace ("Diagram: " ++ showDoc diag "\n Sink: "
++ showDoc sink "")-} simeq diag
st = simeq_tau sink
{- 1. Check the inclusion (*). If it doesn't hold, the
specification is incorrect. -}
in case subRelation st s of
Just (ns1, ns2) -> let
sortString1 = showDoc (snd ns1) " in\n\n" ++ formatSig (fst ns1)
++ "\n\n"
sortString2 = showDoc (snd ns2) " in\n\n" ++ formatSig (fst ns2)
++ "\n\n"
in return (NoAmalgamation ("\nsorts " ++ sortString1
++ "and " ++ sortString2 ++ "might be different"))
Nothing -> let
sop = simeqOp diag
sopt = simeqOp_tau sink
{- 2. Check sharing of operations. If the check
fails, the specification is incorrect -}
in case subRelation sopt sop of
Just (nop1, nop2) -> let
opString1 = formatOp (snd nop1) ++
" in\n\n" ++ formatSig (fst nop1) ++ "\n\n"
opString2 = formatOp (snd nop2) ++
" in\n\n" ++ formatSig (fst nop2) ++ "\n\n"
in return (NoAmalgamation ("\noperations "
++ opString1 ++ "and " ++ opString2
++ "might be different"))
Nothing -> let
spred = simeqPred diag
spredt = simeqPred_tau sink
{- 3. Check sharing of predicates. If the
check fails, the specification is incorrect -}
in case subRelation spredt spred of
Just (np1, np2) -> let
pString1 = formatPred (snd np1) ++
" in\n\n" ++ formatSig (fst np1) ++ "\n\n"
pString2 = formatPred (snd np2) ++
" in\n\n" ++ formatSig (fst np2) ++ "\n\n"
in return (NoAmalgamation ("\npredicates "
++ pString1 ++ "and " ++ pString2
++ "might be different"))
Nothing -> if not (hasCellCaslAmalgOpt opts
|| hasColimitThinnessOpt opts)
then return defaultDontKnow else let
ct = cong_tau diag sink 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. -}
ct0 = filter (\l -> length l > 1) ct
c0 = cong_0 diag s
{- 2. Check the simple case: \cong_0 \in
\cong, so if \cong_\tau \in \cong_0 the
specification is correct. -}
in case subRelation ct0 c0 of
Nothing -> return Amalgamates
Just _ -> let
em = embs diag
cem = canonicalEmbs si
mas = finiteAdm_simeq cem s
si = sim diag em
cct = canonicalCong_tau ct si
-- 3. Check if the set Adm_\simeq is finite.
in case mas of
Just cas -> {- 4. check the colimit thinness. If
the colimit is thing then the
specification is correct. -}
if hasColimitThinnessOpt opts && colimitIsThin s em c0
then return Amalgamates else let
c = cong diag cas s si
--c = cong diag as s
-- 5. Check the cell condition in its full generality.
in if hasCellCaslAmalgOpt opts
then case subRelation cct c of
Just (w1, w2) -> let
rendEmbPath [] = []
rendEmbPath (h : w) = foldl (\t -> \srt -> t ++ " < "
++ showDoc srt "")
(showDoc h "") w
word1 = rendEmbPath (wordToEmbPath w1)
word2 = rendEmbPath (wordToEmbPath w2)
in return (NoAmalgamation ("embedding paths \n "
++ word1 ++ "\nand\n " ++ word2
++ "\nmight be different"))
Nothing -> return Amalgamates
else return defaultDontKnow
Nothing -> let
cR = congR diag s si
{- 6. Check the restricted cell condition. If it holds
then the specification is correct. Otherwise proof
obligations need to be generated. -}
in if hasCellCaslAmalgOpt opts then case subRelation cct cR of
Just _ -> return defaultDontKnow
-- TODO: generate proof obligations
Nothing -> return Amalgamates
else return defaultDontKnow