taggedValsToEquivClasses [] = []
taggedValsToEquivClasses rel' =
let -- prepMap: create a map with all the equivalence class tags mapped to
-- conv: perform actual conversion
convert ((ds, ect) : dsps) m =
in convert rel' (prepMap rel')
-- | Convert the relation representation from list of
-- equivalence classes to list of (value, tag) pairs.
equivClassesToTaggedVals :: Ord a
equivClassesToTaggedVals rel =
eqClToList eqcl@(ft : _) = map (\x -> (x, ft)) eqcl
in foldl (\vtl -> \eqcl -> vtl ++ (eqClToList eqcl)) [] rel
{- the old, n^3 version of mergeEquivClassesBy:
-- | Merge the equivalence classes for elements fulfilling given condition.
mergeEquivClassesBy :: Eq b
-- ^ the condition stating when two elements are in relation
-> EquivRelTagged a b -- ^ the input relation
-- ^ returns the input relation with equivalence classes merged according to
mergeEquivClassesBy cond rel =
-- Starting with the first element in the list an element (elem, tag) is taken
-- and cond is subsequently applied to it and all the elements
-- following it in the list. Whenever an element (elem', tag')
-- that is in relation with the chosen one is found, all the equivalence
-- class tags in the list that are equal to tag' are updated to tag.
let merge rel pos | pos >= length rel = rel
merge rel pos | otherwise =
let mergeWith cmpl _ [] = cmpl
mergeWith cmpl vtp@(elem, ec) toCmpl@((elem', ec') : _) =
let (cmpl', toCmpl') = if ec /= ec' && (cond elem elem')
then let upd (elem'', ec'') =
in mergeWith (cmpl' ++ [head toCmpl']) vtp (tail toCmpl')
(cmpl, (vtp : vtps)) = splitAt pos rel
rel' = mergeWith (cmpl ++ [vtp]) vtp vtps
data TagEqcl a b = Eqcl [a] | TagRef b
-- | Merge the equivalence classes for elements fulfilling given condition.
mergeEquivClassesBy :: (Ord b)
-- ^ the condition stating when two elements are in relation
-> EquivRelTagged a b -- ^ the input relation
-- ^ returns the input relation with equivalence classes merged according to
mergeEquivClassesBy cond rel =
{- Starting with the first element in the list an element (elem,
tag) is taken and cond is subsequently applied to it and all the
elements following it in the list. Whenever an element (elem',
tag') that is in relation with the chosen one is found, the
equivalence classes in tagMap for tag and tag' are merged: tag in
tagMap points to the merged equivalence class and tag' in tagMap
is a reference to tag. -}
let -- create the initial map mapping tags to equivalence classes
let insEl tagMap (val, tag) =
Just (Eqcl (val : eqcl))) tag tagMap
-- merge equivalence classes tagged with t1 and t2
mergeInMap inTagMap t1 t2 =
let {- find the tag and equivalence class that corresponds
to the given tag performing path compression while
traversing the referneces. -}
case findInMap t tagMap of
Eqcl eqcl -> (t, eqcl, tagMap)
(rt, eqcl, tagMap') = findEqcl t' tagMap
tagMap'' = if rt == t' then tagMap' else
(rt1, eqcl1, tagMap1) = findEqcl t1 inTagMap
(rt2, eqcl2, tagMap2) = findEqcl t2 tagMap1
in if rt1 == rt2 then tagMap2
else let (nrt1, nrt2) = if rt1 > rt2 then (rt2, rt1)
(\_ -> Just (Eqcl (eqcl1 ++ eqcl2))) nrt1 tagMap2
(\_ -> Just (TagRef nrt1)) nrt2 tagMap3
{- iterate through the relation merging equivalence classes of
merge tagMap' rel' pos | pos >= length rel' = tagMap'
merge tagMap' rel' pos | otherwise =
let mergeWith tagMap _ [] = tagMap
mergeWith tagMap vtp@(elem1, ec) toCmpl@((elem2, ec') : _) =
let tagMap1 = if ec /= ec' && (cond elem1 elem2)
then mergeInMap tagMap ec ec'
in mergeWith tagMap1 vtp (tail toCmpl)
(_, (vtp' : vtps)) = splitAt pos rel'
tagMap'' = mergeWith tagMap' vtp' vtps
in merge tagMap'' rel' (pos + 1)
-- append given equivalence class to the list of (value, tag) pairs
tagMapToRel rel' (_, TagRef _) = rel'
tagMapToRel rel' (tag, Eqcl eqcl) =
foldl (\l -> \v -> (v, tag) : l) rel' eqcl
myTagMap = merge initialTagMap rel 0
-- | Merge the equivalence classes for given tags.
mergeEquivClasses :: Eq b
mergeEquivClasses rel tag1 tag2 | tag1 == tag2 = rel
let upd (el, tag) | tag == tag2 = (el, tag1)
-- | Return true if there is an edge between srcNode and targetNode
-- and the morphism with which it's labelled maps srcSort to targetSort
isMorphSort diag (srcNode, srcSort) (targetNode, targetSort) =
let checkEdges [] = False
checkEdges ((sn, tn, Morphism { sort_map = sm }) : edgs) =
mapSort sm srcSort == targetSort
then True else checkEdges edgs
in checkEdges (out diag srcNode)
-- | Return true if there is an edge between srcNode and targetNode
-- and the morphism with which it's labelled maps srcOp to targetOp
isMorphOp diag (srcNode, srcOp) (targetNode, targetOp) =
let checkEdges [] = False
checkEdges ((sn, tn, Morphism { sort_map=sm, fun_map=fm }) : edgs) =
mapOpSym sm fm srcOp == targetOp
then True else checkEdges edgs
in checkEdges (out diag srcNode)
-- | Return true if there is an edge between srcNode and targetNode
-- and the morphism with which it's labelled maps srcPred to targetPred
isMorphPred diag (srcNode, srcPred) (targetNode, targetPred) =
let checkEdges [] = False
checkEdges ((sn, tn, Morphism { sort_map=sm, pred_map=pm }) : edgs) =
mapPredSym sm pm srcPred == targetPred
then True else checkEdges edgs
in checkEdges (out diag srcNode)
-- | Compute the simeq relation for given diagram.
simeq :: CASLDiag -- ^ the diagram for which the relation should be created
-- ^ returns the relation represented as a list of equivalence
-- classes (each represented as a list of diagram ops)
-- During the computations the relation is represented as a list of pairs
-- (DiagSort, DiagSort). The first element is a diagram sort and the second
-- denotes the equivalence class to which it belongs. All the pairs with
-- equal second element denote elements of one equivalence class.
let mergeCond ds ds' = isMorphSort diag ds ds' || isMorphSort diag ds' ds
rel = map (\ds -> (ds, ds)) (sorts diag)
rel' = mergeEquivClassesBy mergeCond rel
in taggedValsToEquivClasses rel'
-- | Compute the simeq^op relation for given diagram.
simeqOp :: CASLDiag -- ^ the diagram for which the relation should be created
-- ^ returns the relation represented as a list of equivalence
-- classes (each represented as a list of diagram ops)
-- During the computations the relation is represented as a list of pairs
-- (DiagOp, DiagOp). The first element is a diagram op and the second
-- denotes the equivalence class to which it belongs. All the pairs with
-- equal second element denote elements of one equivalence class.
let mergeCond ds ds' = isMorphOp diag ds ds' || isMorphOp diag ds' ds
rel = map (\ds -> (ds, ds)) (ops diag)
rel' = mergeEquivClassesBy mergeCond rel
in taggedValsToEquivClasses rel'
-- | Compute the simeq^pred relation for given diagram.
-- ^ the diagram for which the relation should be created
-- ^ returns the relation represented as a list of equivalence
-- classes (each represented as a list of diagram preds)
-- During the computations the relation is represented as a list of pairs
-- (DiagPred, DiagPred). The first element is a diagram pred and the second
-- denotes the equivalence class to which it belongs. All the pairs with
-- equal second element denote elements of one equivalence class.
let mergeCond ds ds' = isMorphPred diag ds ds' || isMorphPred diag ds' ds
rel = map (\ds -> (ds, ds)) (preds diag)
rel' = mergeEquivClassesBy mergeCond rel
in taggedValsToEquivClasses rel'
-- | Compute the simeq_tau relation for given diagram.
simeq_tau :: [(Node, CASLMor)]
let -- tagEdge: for given morphism m create a list of pairs
-- (a, b) where a is DiagSort from the source signature that
tagEdge (sn, Morphism { msource = src, sort_map = sm }) =
map (\ ss -> ((sn, ss), mapSort sm ss))
rel = foldl (\l -> \e -> l ++ (tagEdge e)) [] sink
in taggedValsToEquivClasses rel
-- | Compute the simeq^op_tau relation for given diagram.
simeqOp_tau :: [(Node, CASLMor)]
let -- tagEdge: for given morphism m create a list of pairs
-- (a, b) where a is DiagOp from the source signature that
tagEdge (sn, Morphism { msource=src, sort_map = sm, fun_map = fm }) =
map (\srcOp -> ((sn, srcOp), mapOpSym sm fm srcOp))
rel = foldl (\l -> \e -> l ++ (tagEdge e)) [] sink
in taggedValsToEquivClasses rel
-- | Compute the simeq^pred_tau relation for given diagram.
simeqPred_tau :: [(Node, CASLMor)]
let -- tagEdge: for given morphism m create a list of pairs
-- (a, b) where a is DiagPred from the source signature that
tagEdge (sn, Morphism { msource=src, sort_map = sm, pred_map = pm }) =
map (\srcPred -> ((sn, srcPred), mapPredSym sm pm srcPred))
rel = foldl (\l -> \e -> l ++ (tagEdge e)) [] sink
in taggedValsToEquivClasses rel
-- | Check that one equivalence relation is a subset of another.
-- The relations are represented as a lists of equivalence classes,
-- where equivalence classes are lists of elements.
=> EquivRel a -- ^ the relation that is supposed to be a subset
-> EquivRel a -- ^ the relation that is supposed to be a superset
-- ^ returns a pair of elements that are in the same equivalence class of the
-- first relation but are not in the same equivalence class of the second
-- relation or Nothing the first relation is a subset of the second one.
subRelation [] _ = Nothing
subRelation ([] : eqcls) sup = subRelation eqcls sup
-- this should never be the case
subRelation (elts'@(elt' : _) : eqcls') sup =
findEqCl elt (eqcl : eqcls) =
if elem elt eqcl then eqcl else findEqCl elt eqcls
checkEqCl (elt : elts) supEqCl =
then checkEqCl elts supEqCl
curFail = checkEqCl elts' (findEqCl elt' sup)
Nothing -> subRelation eqcls' sup
Just elt2 -> Just (elt', elt2)
-- | Compute the set of sort embeddings defined in the diagram.
embs' ((n, Sign {sortRel = sr}) : lNodes) =
(map (\(s1, s2) -> (n, s1, s2)) (
Rel.toList sr)) ++ (embs' lNodes)
-- | Compute the set of sort embeddings (relations on sorts) defined
-- in the source nodes of the sink.
sinkEmbs :: CASLDiag -- ^ the diagram
-> [(Node, CASLMor)] -- ^ the sink
sinkEmbs diag ((srcNode, _) : edgs) =
let (_, _, Sign {sortRel = sr}, _) = context diag srcNode
in (map (\(s1, s2) -> (srcNode, s1, s2)) (
Rel.toList sr))
-- | Check if the two given elements are in the given relation.
=> EquivRel a -- ^ the relation
-> a -- ^ the first element
-> a -- ^ the second element
inRel (eqc : eqcs) a b | a == b = True
case find (\x -> x == a) eqc of
Nothing -> inRel eqcs a b
Just _ -> case find (\x -> x == b) eqc of
-- | Check if two embeddings can occur subsequently in a word
-- given the simeq relation on sorts.
admissible :: EquivRel DiagSort -- ^ the \simeq relation
-> DiagEmb -- ^ the first embedding
-> DiagEmb -- ^ the second embedding
admissible simeq' (n1, s1, _) (n2, _, s2) =
inRel simeq' (n1, s1) (n2, s2)
-- | Compute the set of all the loopless, admissible
-- words over given set of embeddings.
looplessWords :: [DiagEmb] -- ^ the embeddings
-- ^ the \simeq relation that defines admissibility
looplessWords embs1 simeq1 =
let -- generate the list of all loopless words over given alphabet
looplessWords' suff@(e : _) embs2 pos | pos >= length embs2 = [suff]
ws = if admissible simeq1 emb e
then looplessWords' (emb : suff) embs' 0
in ws ++ (looplessWords' suff embs2 (pos + 1))
looplessWords' [] embs2 pos | pos >= length embs2 = []
in looplessWords' [emb] embs' 0 ++
looplessWords' [] embs2 (pos + 1)
in looplessWords' [] embs1 0
-- | Return the codomain of an embedding path.
wordCod ((n, _, s2) : _) = (n, s2)
wordCod [] = error "wordCod"
-- | Return the domain of an embedding path.
wordDom [] = error "wordDom"
wordDom w = let (n, s1, _) = last w in (n, s1)
-- | Find an equivalence class tag for given element.
findTag ((w', t) : wtps) w =
if w == w' then Just t else findTag wtps w
-- | Compute the left-cancellable closure of a relation on words.
leftCancellableClosure :: EquivRelTagged DiagEmbWord DiagEmbWord
-> EquivRelTagged DiagEmbWord DiagEmbWord
leftCancellableClosure rel1 =
let -- checkPrefixes: for each common prefix of two given words
-- merge the equivalence classes of the suffixes
checkPrefixes [] _ rel = rel
checkPrefixes _ [] rel = rel
checkPrefixes w1@(l1 : suf1) w2@(l2 : suf2) rel | w1 == w2 = rel
let tag1 = maybe (error "checkPrefixes: tag1") id
tag2 = maybe (error "checkPrefixes: tag2") id
rel' = if tag1 == tag2 then rel
else let upd (w, t) | t == tag2 = (w, tag1)
in checkPrefixes suf1 suf2 rel'
-- iterateWord1: for each pair of related words call checkPrefixes
iterateWord1 rel pos | pos >= length rel = rel
let iterateWord2 wtp1@(w1, t1) rel2 pos2
| pos2 >= length rel2 = rel2
let _wtp2@(w2, t2) = rel2 !! pos2
rel3 = if t1 == t2 then checkPrefixes w1 w2 rel2
in iterateWord2 wtp1 rel3 (pos2 + 1)
rel' = iterateWord2 wtp rel 0
in iterateWord1 rel' (pos + 1)
in {-trace ("leftCancellableClosure " ++ show rel) $-} iterateWord1 rel1 0
{- | Compute the congruence closure of an equivalence R: two pairs of
elements (1, 3) and (2, 4) are chosen such that 1 R 2 and 3 R 4. It is
then checked that elements 1, 3 and 2, 4 are in relation supplied and
if so equivalence classes for (op 1 3) and (op 1 4) in R are merged.
This function should be applied to the relation until a fixpoint is
congruenceClosure :: (Eq a, Eq b)
-- ^ the check to be performed on elements 1, 3 and 2, 4
-- ^ the operation to be performed on elements 1, 3 and 2, 4
congruenceClosure check op rel =
iterateWord1 rel1 pos1 | pos1 >= length rel1 = rel1
| otherwise = let -- iterateWord2
iterateWord2 wtp1@(_, t1) rel2 pos2 | pos2 >= length rel2 = rel2
| otherwise = let -- iterateWord3
iterateWord3 wtp1'@(w1', _) wtp2' rel3 pos3
| pos3 >= length rel3 = rel3
| otherwise = let -- iterateWord4
iterateWord4 wtp1''@(w1, _) wtp2''@(w2, _) wtp3'@(w3, t3) rel4 pos4
| pos4 >= length rel4 = rel4
rel4' = if t3 /= t4 || not (check w2 w4) then rel4 else let
mct1 = findTag rel (op w1 w3)
mct2 = findTag rel (op w2 w4)
(Nothing, _) -> rel4 -- w3w1 is not in the domain of rel
(_, Nothing) -> rel4 -- w4w2 is not in the domain of rel
(Just ct1, Just ct2) -> mergeEquivClasses rel4 ct1 ct2
in iterateWord4 wtp1'' wtp2'' wtp3' rel4' (pos4 + 1)
wtp3@(w3', _) = rel3 !! pos3
rel3' = if check w1' w3' --inRel here is usually much more efficient
-- than findTag rel (w3 ++ w1)
then iterateWord4 wtp1' wtp2' wtp3 rel3 0 else rel3
in iterateWord3 wtp1' wtp2 rel3' (pos3 + 1)
wtp2@(_, t2) = rel2 !! pos2
rel2' = if t1 /= t2 then rel2 else iterateWord3 wtp1 wtp2 rel2 0
in iterateWord2 wtp1 rel2' (pos2 + 1)
rel' = iterateWord2 wtp rel1 0
in iterateWord1 rel' (pos1 + 1)
in{- trace ("congruenceClosure " ++ show rel) $-} iterateWord1 rel 0
-- | Compute the cong_tau relation for given diagram and sink.
cong_tau :: CASLDiag -- ^ the diagram
-> [(Node, CASLMor)] -- ^ the sink
-> EquivRel DiagSort -- ^ the \simeq_tau relation
-- domCodSimeq: check that domains and codomains of given words are related
let domCodSimeq w1 w2 = inRel st (wordDom w1) (wordDom w2)
&& inRel st (wordCod w1) (wordCod w2)
embs1 = sinkEmbs diag sink
words1 = looplessWords embs1 st
rel = map (\w -> (w, w)) words1
rel' = mergeEquivClassesBy domCodSimeq rel
in taggedValsToEquivClasses rel'
-- | Compute the finite representation of cong_0 relation for given diagram.
-- The representation consists only of equivalence classes that
-- contain more than one element.
-> EquivRel DiagSort -- ^ the \simeq relation
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)
-- addToRel: add given word to given relation
addToRel ([] : _) _ = error "addToRel"
addToRel (eqcl@(refw : _) : eqcls) w =
if wordDom w == wordDom refw && wordCod w == wordCod refw
then ((w : eqcl) : eqcls)
else (eqcl : (addToRel eqcls w))
-- words2: generate all the admissible 2-letter words over given alphabet
words2 alph (_ : embs1) [] = words2 alph embs1 alph
words2 alph embs1@(emb1 : _) (emb2 : embs2) =
let ws = words2 alph embs1 embs2
in if admissible simeq' emb1 emb2
then ([emb1, emb2] : ws) else ws
rel = map (\e -> ([e], [e])) em
rel' = mergeEquivClassesBy diagRule rel
rel'' = taggedValsToEquivClasses rel'
rel''' = foldl addToRel rel'' w2s
-- | Compute the set Adm_\simeq if it's finite.
finiteAdm_simeq :: [DiagEmb] -- ^ the embeddings
-- ^ the \simeq relation that defines admissibility
-- ^ returns the computed set or Nothing if it's infinite
finiteAdm_simeq embs' simeq' =
let -- generate the list of the words over given alphabet
embWords' suff@(e : _) embs1 pos | pos >= length embs1 = Just [suff]
mws1 = if admissible simeq' emb e
then if any (\emb' -> emb' == emb) suff
else embWords' (emb : suff) embs1 0
Just _ -> embWords' suff embs1 (pos + 1)
Just ws2 -> Just (ws1 ++ ws2)
embWords' [] embs1 pos | pos >= length embs1 = Just []
embWords' [] embs1 pos | otherwise =
mws1 = embWords' [emb] embs1 0
Just _ -> embWords' [] embs1 (pos + 1)
Just ws2 -> Just (ws1 ++ ws2)
-- | Check if the colimit is thin.
colimitIsThin :: EquivRel DiagSort -- ^ the simeq relation
-> [DiagEmb] -- ^ the set of diagram embeddings
-> EquivRel DiagEmbWord -- ^ the cong_0 relation
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
let sortClasses' m [] = m
sortClasses' m ((n, s1, s2) : embs1) =
let c1 = maybe (error "sortClasses:s1") id
c2 = maybe (error "sortClasses:s2") id
in sortClasses' ordMap' embs'
-- larger: return a list of colimit sorts larger than given sort
in (srt : (foldl (\l -> \so -> l ++ (larger so)) [] dl))
-- s: the map representing sets S_{\geq s1,s2}
s = let compS m (s1, s2) =
in foldl compS
Map.empty [(s1, s2) | s1 <- sortsC, s2 <- sortsC]
-- b: the map representing sets B_{s1,s2}
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
let -- checkSort: check if for given colimit sort C = B
embsCs = filter (\e -> embDomS e == chs) embs'
[(d, e) | d <- embsCs, e <- embsCs]
in
Map.update (\_ -> Just (findInMap (s1, s2) b)) (d, e) c1
[(d, e) | d <- embsCs, e <- embsCs, inRel c0 [d] [e]]
updC c1 (d@(n1, _, cod1), e@(n2, _, cod2)) = let
in if filter (\(n, dom, cod) -> (n, dom) == (n1, cod1)
&& (n, cod) == (n2, cod2)) embs' == []
[absCls] = filter (\ac -> any (s2==) ac)
(l ++ [absCls])) k c2) c1 [(d, e), (e, d)]
in foldl updC c' [(d, e) | d <- embsCs,
e <- embsCs, wordDom [d] == wordDom [e]]
updC c1 (e1, e2, e3) = let
updC' c2 (b12, b23, b13) = let
c2' = if any (\l -> l == b13) (findInMap (e1, e3) c2)
else
Map.update (\l -> Just (l ++ [b13])) (e1, e3) c2
in if any (\l -> l == b13) (findInMap (e1, e3) c2')
else
Map.update (\l -> Just (l ++ [b13])) (e3, e1) c2'
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'
checkIncl ((e1, e2) : embprs) = let
res = if subRelation (findInMap (s1, s2) b)
(findInMap (e1, e2) c3) == Nothing then checkIncl embprs
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)) ++
in checkIncl [(e1, e2) | e1 <- embsCs, e2 <- embsCs]
-- cs: next colimit sort to process
-- m1: the order map with cs removed
[(cs', _)] = take 1 (filter (\(_, lt) ->
Set.null lt)
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
-> [DiagEmbWord] -- ^ the Adm_\simeq set (the domain of \cong relation)
-> EquivRel DiagSort -- ^ the \simeq relation
-- domCodEqual: check that domains and codomains of given words are equal
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)
isMorphSort diag (n2, s21) (n1, s11) && isMorphSort diag (n2, s22)
-- 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
-- fixCongLc: apply Cong and Lc rules until a fixpoint is reached
let rel' = (leftCancellableClosure . congruenceClosure simeq) rel
in if rel == rel' then rel else fixCongLc rel'
rel = map (\w -> (w, w)) adm
rel' = mergeEquivClassesBy diagRule rel
rel'' = mergeEquivClassesBy compRule 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. -}
-> [DiagEmbWord] -- ^ the Adm_\simeq set (the domain of \cong relation)
-> EquivRel DiagSort -- ^ the \simeq relation
-> EquivRel DiagEmb -- ^ the \sim relation
cong diag adm simeq' sim' =
-- domCodEqual: check that domains and codomains of given words are equal
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)
-- 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' (((n1, _, s12), (n2, s21, _)) : eps) =
if n1 == n2 && inRel sim' d (n1, s21, s12)
in matches' [(me1, me2) | me1 <- ec1, me2 <- ec2]
-- fixCongLc: apply Cong and Lc rules until a fixpoint is reached
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
rel = map (\w -> (w, w)) adm
rel' = mergeEquivClassesBy compDiagRule rel
in taggedValsToEquivClasses rel''
-- | Compute the \cong^R relation
-> EquivRel DiagSort -- ^ the \simeq relation
-> EquivRel DiagEmb -- ^ the \sim relation
--cong diag (looplessWords (embs diag) simeq) simeq
cong diag (looplessWords (canonicalEmbs sim') simeq') simeq' sim'
-- | Compute the \sim relation
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
let rel2 = congruenceClosure check op rel1
in if rel1 == rel2 then rel1 else fixCong rel2
rel = map (\e -> (e, e)) embs'
rel'' = mergeEquivClassesBy diagRule rel'
in taggedValsToEquivClasses rel''
-- | Compute the CanonicalEmbs(D) set given \sim relation
canonicalEmbs :: EquivRel DiagEmb
foldl (\l -> \(e : _) -> (e : l)) [] sim'
-- | Convert given \cong_\tau relation to the canonical form
canonicalCong_tau :: EquivRel DiagEmbWord
canonicalCong_tau ct sim' =
let mapEmb e = let Just (ce : _) = find (elem e) sim'
mapEqcl ec = map mapWord ec
-- | Convert a word to a list of sorts that are embedded
wordToEmbPath :: DiagEmbWord
wordToEmbPath ((_, s1, s2) : embs1) =
rest ((_, s, _) : embs2) = (rest embs2) ++ [s]
in (rest embs1) ++ [s1, s2]
hasCellCaslAmalgOpt :: [CASLAmalgOpt] -> Bool
hasCellCaslAmalgOpt = any ( \ o -> case o of
hasColimitThinnessOpt :: [CASLAmalgOpt] -> Bool
hasColimitThinnessOpt = any ( \ o -> case o of
-- | The amalgamability checking function for CASL.
ensuresAmalgamability :: [CASLAmalgOpt] -- ^ program options
-> CASLDiag -- ^ the diagram to be checked
-> [(Node, CASLMor)] -- ^ the sink
-- ^ the diagram containing descriptions of nodes and edges
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
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
Nothing -> showDoc (getNodeSig n lns) ""
-- and now the relevant stuff
s = {-trace ("Diagram: " ++ showDoc diag "\n Sink: "
++ showDoc sink "")-} simeq diag
{- 1. Check the inclusion (*). If it doesn't hold, the
specification is incorrect. -}
in case subRelation st s of
sortString1 = showDoc (snd ns1) " in\n\n" ++ formatSig (fst ns1)
sortString2 = showDoc (snd ns2) " in\n\n" ++ formatSig (fst ns2)
in return (NoAmalgamation ("\nsorts " ++ sortString1
++ "and " ++ sortString2 ++ "might be different"))
{- 2. Check sharing of operations. If the check
fails, the specification is incorrect -}
in case subRelation sopt sop of
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"))
spredt = simeqPred_tau sink
{- 3. Check sharing of predicates. If the
check fails, the specification is incorrect -}
in case subRelation spredt spred of
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
{- 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
mas = finiteAdm_simeq cem s
cct = canonicalCong_tau ct si
-- 3. Check if the set Adm_\simeq is finite.
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
-- 5. Check the cell condition in its full generality.
in if hasCellCaslAmalgOpt opts
then case subRelation cct c of
rendEmbPath (h : w) = foldl (\t -> \srt -> t ++ " < "
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
{- 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