{- |
Module      :  ./Static/WACocone.hs
Description :  heterogeneous signatures colimits approximations
Copyright   :  (c) Mihai Codescu, and Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  mcodescu@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable

Heterogeneous version of weakly_amalgamable_cocones.
Needs some improvements (see TO DO).

-}

module Static.WACocone (isConnected,
                       isAcyclic,
                       isThin,
                       removeIdentities,
                       hetWeakAmalgCocone,
                       initDescList,
                       dijkstra,
                       buildStrMorphisms,
                       weakly_amalgamable_colimit
                       ) where

import Control.Monad
import Data.List (nub)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Graph.Inductive.Graph as Graph

import Common.Lib.Graph as Tree
import Common.ExtSign
import Common.Result
import Common.LogicT
import qualified Control.Monad.Fail as Fail

import Logic.Logic
import Logic.Comorphism
import Logic.Modification
import Logic.Grothendieck
import Logic.Coerce
import Static.GTheory
import Comorphisms.LogicGraph

weakly_amalgamable_colimit :: StaticAnalysis lid
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol
    => lid -> Tree.Gr sign (Int, morphism)
           -> Result (sign, Map.Map Int morphism)
weakly_amalgamable_colimit :: lid -> Gr sign (Int, morphism) -> Result (sign, Map Int morphism)
weakly_amalgamable_colimit l :: lid
l diag :: Gr sign (Int, morphism)
diag = do
          (sig :: sign
sig, sink :: Map Int morphism
sink) <- lid -> Gr sign (Int, morphism) -> Result (sign, Map Int morphism)
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> Gr sign (Int, morphism) -> Result (sign, Map Int morphism)
signature_colimit lid
l Gr sign (Int, morphism)
diag
          (sign, Map Int morphism) -> Result (sign, Map Int morphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (sign
sig, Map Int morphism
sink)
{- until amalgamability check is fixed, just return a colimit
get (commented out) code from rev:11881 -}

-- | checks whether a graph is connected

isConnected :: Gr a b -> Bool
isConnected :: Gr a b -> Bool
isConnected graph :: Gr a b
graph = let
  nodeList :: [Int]
nodeList = Gr a b -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Int]
nodes Gr a b
graph
  root :: Int
root = [Int] -> Int
forall a. [a] -> a
head [Int]
nodeList
  availNodes :: Map Int Bool
availNodes = [(Int, Bool)] -> Map Int Bool
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Bool)] -> Map Int Bool) -> [(Int, Bool)] -> Map Int Bool
forall a b. (a -> b) -> a -> b
$ [Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
nodeList (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
True)
  bfs :: [Int] -> Map Int Bool -> Map Int Bool
bfs queue :: [Int]
queue avail :: Map Int Bool
avail = case [Int]
queue of
     [] -> Map Int Bool
avail
     n :: Int
n : ns :: [Int]
ns -> let
       avail1 :: Map Int Bool
avail1 = Int -> Bool -> Map Int Bool -> Map Int Bool
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
n Bool
False Map Int Bool
avail
       nbs :: [Int]
nbs = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: Int
x -> Bool -> Int -> Map Int Bool -> Bool
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Bool
forall a. HasCallStack => [Char] -> a
error "isconnected") Int
x Map Int Bool
avail)
             ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Gr a b -> Int -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Int -> [Int]
neighbors Gr a b
graph Int
n
      in [Int] -> Map Int Bool -> Map Int Bool
bfs ([Int]
ns [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int]
nbs) Map Int Bool
avail1
  in Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ x :: Int
x -> Bool -> Int -> Map Int Bool -> Bool
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Bool
forall a. HasCallStack => [Char] -> a
error "iscon 2") Int
x
                   ([Int] -> Map Int Bool -> Map Int Bool
bfs [Int
root] Map Int Bool
availNodes)) [Int]
nodeList

-- | checks whether the graph is thin

isThin :: Gr a b -> Bool
isThin :: Gr a b -> Bool
isThin = Map Edge Int -> [Edge] -> Bool
checkThinness Map Edge Int
forall k a. Map k a
Map.empty ([Edge] -> Bool) -> (Gr a b -> [Edge]) -> Gr a b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gr a b -> [Edge]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Edge]
edges

checkThinness :: Map.Map Edge Int -> [Edge] -> Bool
checkThinness :: Map Edge Int -> [Edge] -> Bool
checkThinness paths :: Map Edge Int
paths eList :: [Edge]
eList =
  case [Edge]
eList of
   [] -> Bool
True
   (sn :: Int
sn, tn :: Int
tn) : eList' :: [Edge]
eList' ->
      (Int
sn, Int
tn) Edge -> [Edge] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Map Edge Int -> [Edge]
forall k a. Map k a -> [k]
Map.keys Map Edge Int
paths Bool -> Bool -> Bool
&&
        -- multiple paths between (sn, tn)
      let pathsToS :: [Edge]
pathsToS = (Edge -> Bool) -> [Edge] -> [Edge]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, y :: Int
y) -> Int
y Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
sn) ([Edge] -> [Edge]) -> [Edge] -> [Edge]
forall a b. (a -> b) -> a -> b
$ Map Edge Int -> [Edge]
forall k a. Map k a -> [k]
Map.keys Map Edge Int
paths
          updatePaths :: Map (a, t) a -> t -> [(a, b)] -> Maybe (Map (a, t) a)
updatePaths pathF :: Map (a, t) a
pathF dest :: t
dest pList :: [(a, b)]
pList =
            case [(a, b)]
pList of
              [] -> Map (a, t) a -> Maybe (Map (a, t) a)
forall a. a -> Maybe a
Just Map (a, t) a
pathF
              (x :: a
x, _) : pList' :: [(a, b)]
pList' ->
                if (a
x, t
dest) (a, t) -> [(a, t)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map (a, t) a -> [(a, t)]
forall k a. Map k a -> [k]
Map.keys Map (a, t) a
pathF then Maybe (Map (a, t) a)
forall a. Maybe a
Nothing
                else Map (a, t) a -> t -> [(a, b)] -> Maybe (Map (a, t) a)
updatePaths ((a, t) -> a -> Map (a, t) a -> Map (a, t) a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (a
x, t
dest) 1 Map (a, t) a
pathF) t
dest [(a, b)]
pList'
      in case Map Edge Int -> Int -> [Edge] -> Maybe (Map Edge Int)
forall a t a b.
(Ord a, Ord t, Num a) =>
Map (a, t) a -> t -> [(a, b)] -> Maybe (Map (a, t) a)
updatePaths Map Edge Int
paths Int
tn [Edge]
pathsToS of
            Nothing -> Bool
False
            Just paths' :: Map Edge Int
paths' -> Map Edge Int -> [Edge] -> Bool
checkThinness (Edge -> Int -> Map Edge Int -> Map Edge Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Int
sn, Int
tn) 1 Map Edge Int
paths') [Edge]
eList'


-- | checks whether a graph is acyclic

isAcyclic :: (Eq b) => Gr a b -> Bool
isAcyclic :: Gr a b -> Bool
isAcyclic graph :: Gr a b
graph = let
  filterIns :: gr a b -> [Int] -> [Int]
filterIns gr :: gr a b
gr = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: Int
x -> gr a b -> Int -> Int
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Int -> Int
indeg gr a b
gr Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0)
  queue :: [Int]
queue = Gr a b -> [Int] -> [Int]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> [Int] -> [Int]
filterIns Gr a b
graph ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Gr a b -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Int]
nodes Gr a b
graph
  topologicalSort :: [Int] -> gr a b -> Bool
topologicalSort q :: [Int]
q gr :: gr a b
gr = case [Int]
q of
   [] -> [Edge] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Edge] -> Bool) -> [Edge] -> Bool
forall a b. (a -> b) -> a -> b
$ gr a b -> [Edge]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Edge]
edges gr a b
gr
   n :: Int
n : ns :: [Int]
ns -> let
     oEdges :: [(Int, b)]
oEdges = gr a b -> Int -> [(Int, b)]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> [(Int, b)]
lsuc gr a b
gr Int
n
     graph1 :: gr a b
graph1 = (gr a b -> LEdge b -> gr a b) -> gr a b -> [LEdge b] -> gr a b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((LEdge b -> gr a b -> gr a b) -> gr a b -> LEdge b -> gr a b
forall a b c. (a -> b -> c) -> b -> a -> c
flip LEdge b -> gr a b -> gr a b
forall (gr :: * -> * -> *) b a.
(DynGraph gr, Eq b) =>
LEdge b -> gr a b -> gr a b
Graph.delLEdge) gr a b
gr
              ([LEdge b] -> gr a b) -> [LEdge b] -> gr a b
forall a b. (a -> b) -> a -> b
$ ((Int, b) -> LEdge b) -> [(Int, b)] -> [LEdge b]
forall a b. (a -> b) -> [a] -> [b]
map (\ (y :: Int
y, label :: b
label) -> (Int
n, Int
y, b
label)) [(Int, b)]
oEdges
     succs :: [Int]
succs = gr a b -> [Int] -> [Int]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> [Int] -> [Int]
filterIns gr a b
graph1 ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ gr a b -> Int -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Int -> [Int]
suc gr a b
gr Int
n
    in [Int] -> gr a b -> Bool
topologicalSort ([Int]
ns [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int]
succs) gr a b
graph1
 in [Int] -> Gr a b -> Bool
forall (gr :: * -> * -> *) b a.
(DynGraph gr, Eq b) =>
[Int] -> gr a b -> Bool
topologicalSort [Int]
queue Gr a b
graph

-- | auxiliary for removing the identity edges from a graph

removeIdentities :: Gr a b -> Gr a b
removeIdentities :: Gr a b -> Gr a b
removeIdentities graph :: Gr a b
graph = let
 addEdges :: gr a b -> [(Int, Int, b)] -> gr a b
addEdges gr :: gr a b
gr eList :: [(Int, Int, b)]
eList = case [(Int, Int, b)]
eList of
   [] -> gr a b
gr
   (sn :: Int
sn, tn :: Int
tn, label :: b
label) : eList1 :: [(Int, Int, b)]
eList1 -> if Int
sn Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
tn then gr a b -> [(Int, Int, b)] -> gr a b
addEdges gr a b
gr [(Int, Int, b)]
eList1
                             else gr a b -> [(Int, Int, b)] -> gr a b
addEdges ((Int, Int, b) -> gr a b -> gr a b
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Int
sn, Int
tn, b
label) gr a b
gr) [(Int, Int, b)]
eList1
 in Gr a b -> [(Int, Int, b)] -> Gr a b
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
gr a b -> [(Int, Int, b)] -> gr a b
addEdges ([LNode a] -> Gr a b -> Gr a b
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
[LNode a] -> gr a b -> gr a b
insNodes (Gr a b -> [LNode a]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr a b
graph) Gr a b
forall (gr :: * -> * -> *) a b. Graph gr => gr a b
Graph.empty) ([(Int, Int, b)] -> Gr a b) -> [(Int, Int, b)] -> Gr a b
forall a b. (a -> b) -> a -> b
$ Gr a b -> [(Int, Int, b)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges Gr a b
graph

-- assigns to a node all proper descendents
initDescList :: (Eq a, Eq b) => Gr a b -> Map.Map Node [(Node, a)]
initDescList :: Gr a b -> Map Int [(Int, a)]
initDescList graph :: Gr a b
graph = let
 descsOf :: Int -> [Int]
descsOf n :: Int
n = let
  nodeList :: [Int]
nodeList = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/=) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Gr a b -> Int -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Int -> [Int]
pre Gr a b
graph Int
n
  f :: Map Int Bool
f = [(Int, Bool)] -> Map Int Bool
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Bool)] -> Map Int Bool) -> [(Int, Bool)] -> Map Int Bool
forall a b. (a -> b) -> a -> b
$ [Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
nodeList (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)
  precs :: [Int] -> [Int] -> Map Int Bool -> [Int]
precs nList :: [Int]
nList nList' :: [Int]
nList' avail :: Map Int Bool
avail =
    case [Int]
nList of
      [] -> [Int]
nList'
      _ -> let
            nList'' :: [Int]
nList'' = (Int -> [Int]) -> [Int] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ y :: Int
y -> (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter
              (\ x :: Int
x -> Int
x Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Map Int Bool -> [Int]
forall k a. Map k a -> [k]
Map.keys Map Int Bool
avail Bool -> Bool -> Bool
||
                      Bool -> Int -> Map Int Bool -> Bool
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Bool
forall a. HasCallStack => [Char] -> a
error "iDL") Int
x Map Int Bool
avail) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$
              (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int
y Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/=) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Gr a b -> Int -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Int -> [Int]
pre Gr a b
graph Int
y) [Int]
nList
            avail' :: Map Int Bool
avail' = Map Int Bool -> Map Int Bool -> Map Int Bool
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Int Bool
avail (Map Int Bool -> Map Int Bool) -> Map Int Bool -> Map Int Bool
forall a b. (a -> b) -> a -> b
$
                     [(Int, Bool)] -> Map Int Bool
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Bool)] -> Map Int Bool) -> [(Int, Bool)] -> Map Int Bool
forall a b. (a -> b) -> a -> b
$ [Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
nList'' (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)
           in [Int] -> [Int] -> Map Int Bool -> [Int]
precs ([Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub [Int]
nList'') ([Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Int]
nList' [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int]
nList'') Map Int Bool
avail'
             in [Int] -> [Int] -> Map Int Bool -> [Int]
precs [Int]
nodeList [Int]
nodeList Map Int Bool
f
  in [(Int, [(Int, a)])] -> Map Int [(Int, a)]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, [(Int, a)])] -> Map Int [(Int, a)])
-> [(Int, [(Int, a)])] -> Map Int [(Int, a)]
forall a b. (a -> b) -> a -> b
$ (Int -> (Int, [(Int, a)])) -> [Int] -> [(Int, [(Int, a)])]
forall a b. (a -> b) -> [a] -> [b]
map (\ node :: Int
node -> (Int
node, ((Int, a) -> Bool) -> [(Int, a)] -> [(Int, a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: (Int, a)
x -> (Int, a) -> Int
forall a b. (a, b) -> a
fst (Int, a)
x Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`
                                                   Int -> [Int]
descsOf Int
node)
                                       ([(Int, a)] -> [(Int, a)]) -> [(Int, a)] -> [(Int, a)]
forall a b. (a -> b) -> a -> b
$ Gr a b -> [(Int, a)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr a b
graph )) ([Int] -> [(Int, [(Int, a)])]) -> [Int] -> [(Int, [(Int, a)])]
forall a b. (a -> b) -> a -> b
$ Gr a b -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Int]
nodes Gr a b
graph

commonBounds :: (Eq a) => Map.Map Node [(Node, a)] -> Node -> Node -> [(Node, a)]
commonBounds :: Map Int [(Int, a)] -> Int -> Int -> [(Int, a)]
commonBounds funDesc :: Map Int [(Int, a)]
funDesc n1 :: Int
n1 n2 :: Int
n2 = ((Int, a) -> Bool) -> [(Int, a)] -> [(Int, a)]
forall a. (a -> Bool) -> [a] -> [a]
filter
  (\ x :: (Int, a)
x -> (Int, a)
x (Int, a) -> [(Int, a)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map Int [(Int, a)] -> Int -> [(Int, a)]
forall k a. Ord k => Map k a -> k -> a
(Map.!) Map Int [(Int, a)]
funDesc Int
n1 Bool -> Bool -> Bool
&& (Int, a)
x (Int, a) -> [(Int, a)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map Int [(Int, a)] -> Int -> [(Int, a)]
forall k a. Ord k => Map k a -> k -> a
(Map.!) Map Int [(Int, a)]
funDesc Int
n2 )
  ([(Int, a)] -> [(Int, a)]) -> [(Int, a)] -> [(Int, a)]
forall a b. (a -> b) -> a -> b
$ [(Int, a)] -> [(Int, a)]
forall a. Eq a => [a] -> [a]
nub ([(Int, a)] -> [(Int, a)]) -> [(Int, a)] -> [(Int, a)]
forall a b. (a -> b) -> a -> b
$ Map Int [(Int, a)] -> Int -> [(Int, a)]
forall k a. Ord k => Map k a -> k -> a
(Map.!) Map Int [(Int, a)]
funDesc Int
n1 [(Int, a)] -> [(Int, a)] -> [(Int, a)]
forall a. [a] -> [a] -> [a]
++ Map Int [(Int, a)] -> Int -> [(Int, a)]
forall k a. Ord k => Map k a -> k -> a
(Map.!) Map Int [(Int, a)]
funDesc Int
n2

-- returns the greatest lower bound of two maximal nodes,if it exists
glb :: (Eq a) => Map.Map Node [(Node, a)] -> Node -> Node -> Maybe (Node, a)
glb :: Map Int [(Int, a)] -> Int -> Int -> Maybe (Int, a)
glb funDesc :: Map Int [(Int, a)]
funDesc n1 :: Int
n1 n2 :: Int
n2 = let
 cDescs :: [(Int, a)]
cDescs = Map Int [(Int, a)] -> Int -> Int -> [(Int, a)]
forall a. Eq a => Map Int [(Int, a)] -> Int -> Int -> [(Int, a)]
commonBounds Map Int [(Int, a)]
funDesc Int
n1 Int
n2
 subList :: [a] -> t a -> Bool
subList [] _ = Bool
True
 subList (x :: a
x : xs :: [a]
xs) l2 :: t a
l2 = a
x a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
l2 Bool -> Bool -> Bool
&& [a] -> t a -> Bool
subList [a]
xs t a
l2
 glbList :: [(Int, a)]
glbList = ((Int, a) -> Bool) -> [(Int, a)] -> [(Int, a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (n :: Int
n, x :: a
x) -> [(Int, a)] -> [(Int, a)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => [a] -> t a -> Bool
subList
    (((Int, a) -> Bool) -> [(Int, a)] -> [(Int, a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (n0 :: Int
n0, x0 :: a
x0) -> (Int
n, a
x) (Int, a) -> (Int, a) -> Bool
forall a. Eq a => a -> a -> Bool
/= (Int
n0, a
x0)) [(Int, a)]
cDescs) (Map Int [(Int, a)]
funDesc Map Int [(Int, a)] -> Int -> [(Int, a)]
forall k a. Ord k => Map k a -> k -> a
Map.! Int
n)
           ) [(Int, a)]
cDescs
    {- a node n is glb of n1 and n2 iff
    all common bounds of n1 and n2 are also descendants of n -}
  in case [(Int, a)]
glbList of
     [] -> Maybe (Int, a)
forall a. Maybe a
Nothing
     x :: (Int, a)
x : _ -> (Int, a) -> Maybe (Int, a)
forall a. a -> Maybe a
Just (Int, a)
x -- because if it exists, there can be only one

-- if no greatest lower bound exists, compute all maximal bounds of the nodes
maxBounds :: (Eq a) => Map.Map Node [(Node, a)] -> Node -> Node -> [(Node, a)]
maxBounds :: Map Int [(Int, a)] -> Int -> Int -> [(Int, a)]
maxBounds funDesc :: Map Int [(Int, a)]
funDesc n1 :: Int
n1 n2 :: Int
n2 = let
  cDescs :: [(Int, a)]
cDescs = Map Int [(Int, a)] -> Int -> Int -> [(Int, a)]
forall a. Eq a => Map Int [(Int, a)] -> Int -> Int -> [(Int, a)]
commonBounds Map Int [(Int, a)]
funDesc Int
n1 Int
n2
  isDesc :: Int -> (Int, a) -> Bool
isDesc n0 :: Int
n0 (n :: Int
n, y :: a
y) = (Int
n, a
y) (Int, a) -> [(Int, a)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map Int [(Int, a)]
funDesc Map Int [(Int, a)] -> Int -> [(Int, a)]
forall k a. Ord k => Map k a -> k -> a
Map.! Int
n0
  noDescs :: (Int, a) -> Bool
noDescs (n :: Int
n, y :: a
y) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ((Int, a) -> Bool) -> [(Int, a)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ (n0 :: Int
n0, _) -> Int -> (Int, a) -> Bool
isDesc Int
n0 (Int
n, a
y)) [(Int, a)]
cDescs
 in ((Int, a) -> Bool) -> [(Int, a)] -> [(Int, a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int, a) -> Bool
noDescs [(Int, a)]
cDescs

-- dijsktra algorithm for finding the the shortest path between two nodes
dijkstra :: GDiagram -> Node -> Node -> Result GMorphism
dijkstra :: GDiagram -> Int -> Int -> Result GMorphism
dijkstra graph :: GDiagram
graph source :: Int
source target :: Int
target = do
 let
  dist :: Map Int Int
dist = Int -> Int -> Map Int Int -> Map Int Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
source 0 (Map Int Int -> Map Int Int) -> Map Int Int -> Map Int Int
forall a b. (a -> b) -> a -> b
$ [Edge] -> Map Int Int
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([Edge] -> Map Int Int) -> [Edge] -> Map Int Int
forall a b. (a -> b) -> a -> b
$
         [Int] -> [Int] -> [Edge]
forall a b. [a] -> [b] -> [(a, b)]
zip (GDiagram -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Int]
nodes GDiagram
graph) ([Int] -> [Edge]) -> [Int] -> [Edge]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. a -> [a]
repeat (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ 2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* [Edge] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (GDiagram -> [Edge]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Edge]
edges GDiagram
graph)
  prev :: Map Int Int
prev = if Int
source Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
target then Int -> Int -> Map Int Int -> Map Int Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
source Int
source Map Int Int
forall k a. Map k a
Map.empty
         else Map Int Int
forall k a. Map k a
Map.empty
  q :: [Int]
q = GDiagram -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Int]
nodes GDiagram
graph
  com :: Map Int GMorphism
com = case GDiagram -> Int -> Maybe G_theory
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> Maybe a
lab GDiagram
graph Int
source of
    Nothing -> Map Int GMorphism
forall k a. Map k a
Map.empty -- shouldnt be the case
    Just gt :: G_theory
gt -> Int -> GMorphism -> Map Int GMorphism -> Map Int GMorphism
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
source (G_sign -> GMorphism
forall object morphism.
Category object morphism =>
object -> morphism
ide (G_sign -> GMorphism) -> G_sign -> GMorphism
forall a b. (a -> b) -> a -> b
$ G_theory -> G_sign
signOf G_theory
gt) Map Int GMorphism
forall k a. Map k a
Map.empty
  extractMin :: [k] -> Map k a -> ([k], k)
extractMin queue :: [k]
queue dMap :: Map k a
dMap = let
   u :: k
u = [k] -> k
forall a. [a] -> a
head ([k] -> k) -> [k] -> k
forall a b. (a -> b) -> a -> b
$
     (k -> Bool) -> [k] -> [k]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: k
x -> a -> k -> Map k a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> a
forall a. HasCallStack => [Char] -> a
error "dijkstra") k
x Map k a
dMap a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==
             [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum
               ((k -> a) -> [k] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (\ x1 :: k
x1 -> a -> k -> Map k a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> a
forall a. HasCallStack => [Char] -> a
error "dijkstra") k
x1 Map k a
dMap)
               [k]
queue))
               [k]
queue
   in ( Set k -> [k]
forall a. Set a -> [a]
Set.toList (Set k -> [k]) -> Set k -> [k]
forall a b. (a -> b) -> a -> b
$ Set k -> Set k -> Set k
forall a. Ord a => Set a -> Set a -> Set a
Set.difference ([k] -> Set k
forall a. Ord a => [a] -> Set a
Set.fromList [k]
queue) ([k] -> Set k
forall a. Ord a => [a] -> Set a
Set.fromList [k
u]) , k
u)
  updateNeighbors :: Map Int a
-> Map Int Int
-> Map Int b
-> Int
-> gr a (a, b)
-> (Map Int a, Map Int Int, Map Int b)
updateNeighbors d :: Map Int a
d p :: Map Int Int
p c :: Map Int b
c u :: Int
u gr :: gr a (a, b)
gr = let
    outEdges :: [LEdge (a, b)]
outEdges = gr a (a, b) -> Int -> [LEdge (a, b)]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> [LEdge b]
out gr a (a, b)
gr Int
u
    upNeighbor :: Map a a
-> Map a a
-> Map a b
-> a
-> [(a, a, (a, b))]
-> (Map a a, Map a a, Map a b)
upNeighbor dMap :: Map a a
dMap pMap :: Map a a
pMap cMap :: Map a b
cMap uNode :: a
uNode edgeList :: [(a, a, (a, b))]
edgeList = case [(a, a, (a, b))]
edgeList of
     [] -> (Map a a
dMap, Map a a
pMap, Map a b
cMap)
     (_, v :: a
v, (_, gmor :: b
gmor)) : edgeL :: [(a, a, (a, b))]
edgeL -> let
       alt :: a
alt = a -> a -> Map a a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> a
forall a. HasCallStack => [Char] -> a
error "dijkstra") a
uNode Map a a
dMap a -> a -> a
forall a. Num a => a -> a -> a
+ 1
      in
        if a
alt a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a -> a -> Map a a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> a
forall a. HasCallStack => [Char] -> a
error "dijsktra") a
v Map a a
dMap then
          Map a a
-> Map a a
-> Map a b
-> a
-> [(a, a, (a, b))]
-> (Map a a, Map a a, Map a b)
upNeighbor Map a a
dMap Map a a
pMap Map a b
cMap a
uNode [(a, a, (a, b))]
edgeL
        else let
      d1 :: Map a a
d1 = a -> a -> Map a a -> Map a a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
v a
alt Map a a
dMap
      p1 :: Map a a
p1 = a -> a -> Map a a -> Map a a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
v a
uNode Map a a
pMap
      c1 :: Map a b
c1 = a -> b -> Map a b -> Map a b
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
v b
gmor Map a b
cMap
      in Map a a
-> Map a a
-> Map a b
-> a
-> [(a, a, (a, b))]
-> (Map a a, Map a a, Map a b)
upNeighbor Map a a
d1 Map a a
p1 Map a b
c1 a
uNode [(a, a, (a, b))]
edgeL
   in Map Int a
-> Map Int Int
-> Map Int b
-> Int
-> [LEdge (a, b)]
-> (Map Int a, Map Int Int, Map Int b)
forall a a b a a.
(Ord a, Num a, Ord a) =>
Map a a
-> Map a a
-> Map a b
-> a
-> [(a, a, (a, b))]
-> (Map a a, Map a a, Map a b)
upNeighbor Map Int a
d Map Int Int
p Map Int b
c Int
u [LEdge (a, b)]
outEdges
  -- for each neighbor of u, if d(u)+1 < d(v), modify p(v) = u, d(v) = d(u)+1
  mainloop :: gr a (a, b)
-> Int
-> Int
-> [Int]
-> Map Int a
-> Map Int Int
-> Map Int b
-> m ([Int], Map Int b)
mainloop gr :: gr a (a, b)
gr sn :: Int
sn tn :: Int
tn qL :: [Int]
qL d :: Map Int a
d p :: Map Int Int
p c :: Map Int b
c = let
   (q1 :: [Int]
q1, u :: Int
u) = [Int] -> Map Int a -> ([Int], Int)
forall k a. (Ord k, Ord a) => [k] -> Map k a -> ([k], k)
extractMin [Int]
qL Map Int a
d
   (d1 :: Map Int a
d1, p1 :: Map Int Int
p1, c1 :: Map Int b
c1) = Map Int a
-> Map Int Int
-> Map Int b
-> Int
-> gr a (a, b)
-> (Map Int a, Map Int Int, Map Int b)
forall a (gr :: * -> * -> *) b a a.
(Ord a, Num a, Graph gr) =>
Map Int a
-> Map Int Int
-> Map Int b
-> Int
-> gr a (a, b)
-> (Map Int a, Map Int Int, Map Int b)
updateNeighbors Map Int a
d Map Int Int
p Map Int b
c Int
u gr a (a, b)
gr
   in if Int
u Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
tn then Int
-> Map Int Int -> Map Int b -> [Int] -> Int -> m ([Int], Map Int b)
forall t (m :: * -> *) t.
(MonadFail m, Ord t, Show t) =>
t -> Map t t -> t -> [t] -> t -> m ([t], t)
shortPath Int
sn Map Int Int
p1 Map Int b
c1 [] Int
tn
     else gr a (a, b)
-> Int
-> Int
-> [Int]
-> Map Int a
-> Map Int Int
-> Map Int b
-> m ([Int], Map Int b)
mainloop gr a (a, b)
gr Int
sn Int
tn [Int]
q1 Map Int a
d1 Map Int Int
p1 Map Int b
c1
  shortPath :: t -> Map t t -> t -> [t] -> t -> m ([t], t)
shortPath sn :: t
sn p1 :: Map t t
p1 c :: t
c s :: [t]
s u :: t
u =
   if t
u t -> [t] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Map t t -> [t]
forall k a. Map k a -> [k]
Map.keys Map t t
p1 then [Char] -> m ([t], t)
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail "path not found"
    else let
    x :: t
x = t -> t -> Map t t -> t
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> t
forall a. HasCallStack => [Char] -> a
error ([Char] -> t) -> [Char] -> t
forall a b. (a -> b) -> a -> b
$ t -> [Char]
forall a. Show a => a -> [Char]
show t
u) t
u Map t t
p1 in
    if t
x t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
sn then ([t], t) -> m ([t], t)
forall (m :: * -> *) a. Monad m => a -> m a
return (t
u t -> [t] -> [t]
forall a. a -> [a] -> [a]
: [t]
s, t
c)
     else t -> Map t t -> t -> [t] -> t -> m ([t], t)
shortPath t
sn Map t t
p1 t
c (t
u t -> [t] -> [t]
forall a. a -> [a] -> [a]
: [t]
s) t
x
 (nodeList :: [Int]
nodeList, com1 :: Map Int GMorphism
com1) <- GDiagram
-> Int
-> Int
-> [Int]
-> Map Int Int
-> Map Int Int
-> Map Int GMorphism
-> Result ([Int], Map Int GMorphism)
forall (m :: * -> *) a (gr :: * -> * -> *) a a b.
(MonadFail m, Ord a, Num a, Graph gr) =>
gr a (a, b)
-> Int
-> Int
-> [Int]
-> Map Int a
-> Map Int Int
-> Map Int b
-> m ([Int], Map Int b)
mainloop GDiagram
graph Int
source Int
target [Int]
q Map Int Int
dist Map Int Int
prev Map Int GMorphism
com
 (GMorphism -> GMorphism -> Result GMorphism)
-> GMorphism -> [GMorphism] -> Result GMorphism
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp (Map Int GMorphism -> Int -> GMorphism
forall k a. Ord k => Map k a -> k -> a
(Map.!) Map Int GMorphism
com1 Int
source) ([GMorphism] -> Result GMorphism)
-> ([Int] -> [GMorphism]) -> [Int] -> Result GMorphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> GMorphism) -> [Int] -> [GMorphism]
forall a b. (a -> b) -> [a] -> [b]
map (Map Int GMorphism -> Int -> GMorphism
forall k a. Ord k => Map k a -> k -> a
(Map.!) Map Int GMorphism
com1) ([Int] -> Result GMorphism) -> [Int] -> Result GMorphism
forall a b. (a -> b) -> a -> b
$ [Int]
nodeList

{- builds the arrows from the nodes of the original graph
to the unique maximal node of the obtained graph -}

buildStrMorphisms :: GDiagram -> GDiagram
                    -> Result (G_theory, Map.Map Node GMorphism)
buildStrMorphisms :: GDiagram -> GDiagram -> Result (G_theory, Map Int GMorphism)
buildStrMorphisms initGraph :: GDiagram
initGraph newGraph :: GDiagram
newGraph = do
 let (maxNode :: Int
maxNode, sigma :: G_theory
sigma) = [(Int, G_theory)] -> (Int, G_theory)
forall a. [a] -> a
head ([(Int, G_theory)] -> (Int, G_theory))
-> [(Int, G_theory)] -> (Int, G_theory)
forall a b. (a -> b) -> a -> b
$ ((Int, G_theory) -> Bool) -> [(Int, G_theory)] -> [(Int, G_theory)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (node :: Int
node, _) -> GDiagram -> Int -> Int
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Int -> Int
outdeg GDiagram
newGraph Int
node Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0) ([(Int, G_theory)] -> [(Int, G_theory)])
-> [(Int, G_theory)] -> [(Int, G_theory)]
forall a b. (a -> b) -> a -> b
$
                        GDiagram -> [(Int, G_theory)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes GDiagram
newGraph
     buildMor :: [(Int, b)] -> [(Int, GMorphism)] -> Result [(Int, GMorphism)]
buildMor pairList :: [(Int, b)]
pairList solList :: [(Int, GMorphism)]
solList =
      case [(Int, b)]
pairList of
       (n :: Int
n, _) : pairs :: [(Int, b)]
pairs -> do GMorphism
nMor <- GDiagram -> Int -> Int -> Result GMorphism
dijkstra GDiagram
newGraph Int
n Int
maxNode
                            [(Int, b)] -> [(Int, GMorphism)] -> Result [(Int, GMorphism)]
buildMor [(Int, b)]
pairs ([(Int, GMorphism)]
solList [(Int, GMorphism)] -> [(Int, GMorphism)] -> [(Int, GMorphism)]
forall a. [a] -> [a] -> [a]
++ [(Int
n, GMorphism
nMor)])
       [] -> [(Int, GMorphism)] -> Result [(Int, GMorphism)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int, GMorphism)]
solList
 [(Int, GMorphism)]
morList <- [(Int, G_theory)]
-> [(Int, GMorphism)] -> Result [(Int, GMorphism)]
forall b.
[(Int, b)] -> [(Int, GMorphism)] -> Result [(Int, GMorphism)]
buildMor (GDiagram -> [(Int, G_theory)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes GDiagram
initGraph) []
 (G_theory, Map Int GMorphism)
-> Result (G_theory, Map Int GMorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory
sigma, [(Int, GMorphism)] -> Map Int GMorphism
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Int, GMorphism)]
morList)

-- computes the colimit and inserts it into the graph
addNodeToGraph :: GDiagram -> G_theory -> G_theory -> G_theory -> Int -> Int
               -> Int -> GMorphism -> GMorphism
               -> Map.Map Node [(Node, G_theory)] -> [(Int, G_theory)]
               -> Result (GDiagram, Map.Map Node [(Node, G_theory)])
addNodeToGraph :: GDiagram
-> G_theory
-> G_theory
-> G_theory
-> Int
-> Int
-> Int
-> GMorphism
-> GMorphism
-> Map Int [(Int, G_theory)]
-> [(Int, G_theory)]
-> Result (GDiagram, Map Int [(Int, G_theory)])
addNodeToGraph oldGraph :: GDiagram
oldGraph
               (G_theory lid :: lid
lid _ extSign :: ExtSign sign symbol
extSign _ _ _)
               gt1 :: G_theory
gt1@(G_theory lid1 :: lid
lid1 _ extSign1 :: ExtSign sign symbol
extSign1 idx1 :: SigId
idx1 _ _)
               gt2 :: G_theory
gt2@(G_theory lid2 :: lid
lid2 _ extSign2 :: ExtSign sign symbol
extSign2 idx2 :: SigId
idx2 _ _)
               n :: Int
n
               n1 :: Int
n1
               n2 :: Int
n2
               (GMorphism cid1 :: cid
cid1 ss1 :: ExtSign sign1 symbol1
ss1 _ mor1 :: morphism2
mor1 _)
               (GMorphism cid2 :: cid
cid2 ss2 :: ExtSign sign1 symbol1
ss2 _ mor2 :: morphism2
mor2 _)
               funDesc :: Map Int [(Int, G_theory)]
funDesc maxNodes :: [(Int, G_theory)]
maxNodes = do
 let newNode :: Int
newNode = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (GDiagram -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Int]
nodes GDiagram
oldGraph) -- get a new node
 ExtSign sign symbol
s1 <- lid
-> lid
-> [Char]
-> ExtSign sign symbol
-> Result (ExtSign sign symbol)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> [Char]
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid1 lid
lid "addToNodeGraph" ExtSign sign symbol
extSign1
 ExtSign sign symbol
s2 <- lid
-> lid
-> [Char]
-> ExtSign sign symbol
-> Result (ExtSign sign symbol)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> [Char]
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid2 lid
lid "addToNodeGraph" ExtSign sign symbol
extSign2
 morphism
m1 <- lid2 -> lid -> [Char] -> morphism2 -> Result morphism
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> morphism1 -> m morphism2
coerceMorphism (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid1) lid
lid "addToNodeGraph" morphism2
mor1
 morphism
m2 <- lid2 -> lid -> [Char] -> morphism2 -> Result morphism
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> morphism1 -> m morphism2
coerceMorphism (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid2) lid
lid "addToNodeGraph" morphism2
mor2
 let spanGr :: Gr sign (Int, morphism)
spanGr = [LNode sign] -> [LEdge (Int, morphism)] -> Gr sign (Int, morphism)
forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
Graph.mkGraph
       [(Int
n, ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
extSign), (Int
n1, ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
s1), (Int
n2, ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
s2)]
       [(Int
n, Int
n1, (1, morphism
m1)), (Int
n, Int
n2, (1, morphism
m2))]
 (sig :: sign
sig, morMap :: Map Int morphism
morMap) <- lid -> Gr sign (Int, morphism) -> Result (sign, Map Int morphism)
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> Gr sign (Int, morphism) -> Result (sign, Map Int morphism)
weakly_amalgamable_colimit lid
lid Gr sign (Int, morphism)
spanGr
      -- must  coerce here
 morphism2
m11 <- lid -> lid2 -> [Char] -> morphism -> Result morphism2
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> morphism1 -> m morphism2
coerceMorphism lid
lid (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid1) "addToNodeGraph" (morphism -> Result morphism2) -> morphism -> Result morphism2
forall a b. (a -> b) -> a -> b
$
        Map Int morphism
morMap Map Int morphism -> Int -> morphism
forall k a. Ord k => Map k a -> k -> a
Map.! Int
n1
 morphism2
m22 <- lid -> lid2 -> [Char] -> morphism -> Result morphism2
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> morphism1 -> m morphism2
coerceMorphism lid
lid (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid2) "addToNodeGraph" (morphism -> Result morphism2) -> morphism -> Result morphism2
forall a b. (a -> b) -> a -> b
$
        Map Int morphism
morMap Map Int morphism -> Int -> morphism
forall k a. Ord k => Map k a -> k -> a
Map.! Int
n2
 let gth :: G_theory
gth = lid -> ExtSign sign symbol -> SigId -> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
lid (sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign
sig) SigId
startSigId
     gmor1 :: GMorphism
gmor1 = cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism cid
cid1 ExtSign sign1 symbol1
ss1 SigId
idx1 morphism2
m11 MorId
startMorId
     gmor2 :: GMorphism
gmor2 = cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism cid
cid2 ExtSign sign1 symbol1
ss2 SigId
idx2 morphism2
m22 MorId
startMorId
 case [(Int, G_theory)]
maxNodes of
   [] -> do
    let newGraph :: GDiagram
newGraph = [LEdge (Int, GMorphism)] -> GDiagram -> GDiagram
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
[LEdge b] -> gr a b -> gr a b
insEdges [(Int
n1, Int
newNode, (1, GMorphism
gmor1)), (Int
n2, Int
newNode, (1, GMorphism
gmor2))] (GDiagram -> GDiagram) -> GDiagram -> GDiagram
forall a b. (a -> b) -> a -> b
$
                   (Int, G_theory) -> GDiagram -> GDiagram
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Int
newNode, G_theory
gth) GDiagram
oldGraph
        funDesc1 :: Map Int [(Int, G_theory)]
funDesc1 = Int
-> [(Int, G_theory)]
-> Map Int [(Int, G_theory)]
-> Map Int [(Int, G_theory)]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
newNode
                     ([(Int, G_theory)] -> [(Int, G_theory)]
forall a. Eq a => [a] -> [a]
nub ([(Int, G_theory)] -> [(Int, G_theory)])
-> [(Int, G_theory)] -> [(Int, G_theory)]
forall a b. (a -> b) -> a -> b
$ Map Int [(Int, G_theory)] -> Int -> [(Int, G_theory)]
forall k a. Ord k => Map k a -> k -> a
(Map.!) Map Int [(Int, G_theory)]
funDesc Int
n1 [(Int, G_theory)] -> [(Int, G_theory)] -> [(Int, G_theory)]
forall a. [a] -> [a] -> [a]
++ Map Int [(Int, G_theory)] -> Int -> [(Int, G_theory)]
forall k a. Ord k => Map k a -> k -> a
(Map.!) Map Int [(Int, G_theory)]
funDesc Int
n2 ) Map Int [(Int, G_theory)]
funDesc
    (GDiagram, Map Int [(Int, G_theory)])
-> Result (GDiagram, Map Int [(Int, G_theory)])
forall (m :: * -> *) a. Monad m => a -> m a
return (GDiagram
newGraph, Map Int [(Int, G_theory)]
funDesc1)
   _ -> GDiagram
-> Map Int [(Int, G_theory)]
-> (Int, G_theory)
-> (Int, G_theory)
-> (Int, G_theory)
-> GMorphism
-> GMorphism
-> [(Int, G_theory)]
-> Result (GDiagram, Map Int [(Int, G_theory)])
computeCoeqs GDiagram
oldGraph Map Int [(Int, G_theory)]
funDesc (Int
n1, G_theory
gt1) (Int
n2, G_theory
gt2)
                           (Int
newNode, G_theory
gth) GMorphism
gmor1 GMorphism
gmor2 [(Int, G_theory)]
maxNodes

{- for each node in the list, check whether the coequalizer can be computed
if so, modify the maximal node of graph and the edges to it from n1 and n2 -}
computeCoeqs :: GDiagram -> Map.Map Node [(Node, G_theory)]
                   -> (Node, G_theory) -> (Node, G_theory) -> (Node, G_theory)
                   -> GMorphism -> GMorphism -> [(Node, G_theory)] ->
                       Result (GDiagram, Map.Map Node [(Node, G_theory)])
computeCoeqs :: GDiagram
-> Map Int [(Int, G_theory)]
-> (Int, G_theory)
-> (Int, G_theory)
-> (Int, G_theory)
-> GMorphism
-> GMorphism
-> [(Int, G_theory)]
-> Result (GDiagram, Map Int [(Int, G_theory)])
computeCoeqs oldGraph :: GDiagram
oldGraph funDesc :: Map Int [(Int, G_theory)]
funDesc (n1 :: Int
n1, _) (n2 :: Int
n2, _) (newN :: Int
newN, newGt :: G_theory
newGt) gmor1 :: GMorphism
gmor1 gmor2 :: GMorphism
gmor2 [] = do
 let newGraph :: GDiagram
newGraph = [LEdge (Int, GMorphism)] -> GDiagram -> GDiagram
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
[LEdge b] -> gr a b -> gr a b
insEdges [(Int
n1, Int
newN, (1, GMorphism
gmor1)), (Int
n2, Int
newN, (1, GMorphism
gmor2))] (GDiagram -> GDiagram) -> GDiagram -> GDiagram
forall a b. (a -> b) -> a -> b
$
                (Int, G_theory) -> GDiagram -> GDiagram
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Int
newN, G_theory
newGt) GDiagram
oldGraph
     descFun1 :: Map Int [(Int, G_theory)]
descFun1 = Int
-> [(Int, G_theory)]
-> Map Int [(Int, G_theory)]
-> Map Int [(Int, G_theory)]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
newN
                ([(Int, G_theory)] -> [(Int, G_theory)]
forall a. Eq a => [a] -> [a]
nub ([(Int, G_theory)] -> [(Int, G_theory)])
-> [(Int, G_theory)] -> [(Int, G_theory)]
forall a b. (a -> b) -> a -> b
$ Map Int [(Int, G_theory)] -> Int -> [(Int, G_theory)]
forall k a. Ord k => Map k a -> k -> a
(Map.!) Map Int [(Int, G_theory)]
funDesc Int
n1 [(Int, G_theory)] -> [(Int, G_theory)] -> [(Int, G_theory)]
forall a. [a] -> [a] -> [a]
++ Map Int [(Int, G_theory)] -> Int -> [(Int, G_theory)]
forall k a. Ord k => Map k a -> k -> a
(Map.!) Map Int [(Int, G_theory)]
funDesc Int
n2 ) Map Int [(Int, G_theory)]
funDesc
 (GDiagram, Map Int [(Int, G_theory)])
-> Result (GDiagram, Map Int [(Int, G_theory)])
forall (m :: * -> *) a. Monad m => a -> m a
return (GDiagram
newGraph, Map Int [(Int, G_theory)]
descFun1)
computeCoeqs graph :: GDiagram
graph funDesc :: Map Int [(Int, G_theory)]
funDesc (n1 :: Int
n1, gt1 :: G_theory
gt1) (n2 :: Int
n2, gt2 :: G_theory
gt2)
                    (newN :: Int
newN, _newGt :: G_theory
_newGt@(G_theory tlid :: lid
tlid _ tsign :: ExtSign sign symbol
tsign _ _ _))
                    _gmor1 :: GMorphism
_gmor1@(GMorphism cid1 :: cid
cid1 sig1 :: ExtSign sign1 symbol1
sig1 idx1 :: SigId
idx1 mor1 :: morphism2
mor1 _ )
                    _gmor2 :: GMorphism
_gmor2@(GMorphism cid2 :: cid
cid2 sig2 :: ExtSign sign1 symbol1
sig2 idx2 :: SigId
idx2 mor2 :: morphism2
mor2 _ ) ((n :: Int
n, gt :: G_theory
gt) : descs :: [(Int, G_theory)]
descs) = do
 _rho1 :: GMorphism
_rho1@(GMorphism cid3 :: cid
cid3 _ _ mor3 :: morphism2
mor3 _) <- GDiagram -> Int -> Int -> Result GMorphism
dijkstra GDiagram
graph Int
n Int
n1
 _rho2 :: GMorphism
_rho2@(GMorphism cid4 :: cid
cid4 _ _ mor4 :: morphism2
mor4 _) <- GDiagram -> Int -> Int -> Result GMorphism
dijkstra GDiagram
graph Int
n Int
n2
 AnyComorphism
com1 <- AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (cid -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism cid
cid1) (cid -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism cid
cid3)
 AnyComorphism
com2 <- AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (cid -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism cid
cid1) (cid -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism cid
cid3)
 if AnyComorphism
com1 AnyComorphism -> AnyComorphism -> Bool
forall a. Eq a => a -> a -> Bool
/= AnyComorphism
com2 then [Char] -> Result (GDiagram, Map Int [(Int, G_theory)])
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail "Unable to compute coequalizer" else do
   _gtM :: G_theory
_gtM@(G_theory lidM :: lid
lidM _ signM :: ExtSign sign symbol
signM _idxM :: SigId
_idxM _ _) <- Bool -> AnyComorphism -> G_theory -> Result G_theory
mapG_theory Bool
False AnyComorphism
com1 G_theory
gt
   ExtSign sign symbol
s1 <- lid
-> lid
-> [Char]
-> ExtSign sign symbol
-> Result (ExtSign sign symbol)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> [Char]
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lidM lid
tlid "coequalizers" ExtSign sign symbol
signM
   morphism1
mor3' <- lid2 -> lid1 -> [Char] -> morphism2 -> Result morphism1
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> morphism1 -> m morphism2
coerceMorphism (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid3) (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cid1) "coeqs" morphism2
mor3
   morphism1
mor4' <- lid2 -> lid1 -> [Char] -> morphism2 -> Result morphism1
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> morphism1 -> m morphism2
coerceMorphism (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid4) (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cid2) "coeqs" morphism2
mor4
   morphism2
m1 <- cid -> morphism1 -> Result morphism2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> morphism1 -> Result morphism2
map_morphism cid
cid1 morphism1
mor3'
   morphism2
m2 <- cid -> morphism1 -> Result morphism2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> morphism1 -> Result morphism2
map_morphism cid
cid2 morphism1
mor4'
   morphism2
phi1' <- morphism2 -> morphism2 -> Result morphism2
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp morphism2
m1 morphism2
mor1
   morphism2
phi2' <- morphism2 -> morphism2 -> Result morphism2
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp morphism2
m2 morphism2
mor2
   morphism
phi1 <- lid2 -> lid -> [Char] -> morphism2 -> Result morphism
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> morphism1 -> m morphism2
coerceMorphism (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid1) lid
tlid "coeqs" morphism2
phi1'
   morphism
phi2 <- lid2 -> lid -> [Char] -> morphism2 -> Result morphism
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> morphism1 -> m morphism2
coerceMorphism (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid2) lid
tlid "coeqs" morphism2
phi2'
   -- build the double arrow for computing the coequalizers
   let doubleArrow :: Gr sign (Int, morphism)
doubleArrow = [LNode sign] -> [LEdge (Int, morphism)] -> Gr sign (Int, morphism)
forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
Graph.mkGraph
         [(Int
n, ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
s1), (Int
newN, ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
tsign)]
         [(Int
n, Int
newN, (1, morphism
phi1)), (Int
n, Int
newN, (1, morphism
phi2))]
   (colS :: sign
colS, colM :: Map Int morphism
colM) <- lid -> Gr sign (Int, morphism) -> Result (sign, Map Int morphism)
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> Gr sign (Int, morphism) -> Result (sign, Map Int morphism)
weakly_amalgamable_colimit lid
tlid Gr sign (Int, morphism)
doubleArrow
   let newGt1 :: G_theory
newGt1 = lid -> ExtSign sign symbol -> SigId -> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
tlid (sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign
colS) SigId
startSigId
   morphism2
mor11' <- lid -> lid2 -> [Char] -> morphism -> Result morphism2
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> morphism1 -> m morphism2
coerceMorphism lid
tlid (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid1) "coeqs" (morphism -> Result morphism2) -> morphism -> Result morphism2
forall a b. (a -> b) -> a -> b
$ Map Int morphism -> Int -> morphism
forall k a. Ord k => Map k a -> k -> a
(Map.!) Map Int morphism
colM Int
newN
   morphism2
mor11 <- morphism2 -> morphism2 -> Result morphism2
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp morphism2
mor1 morphism2
mor11'
   morphism2
mor22' <- lid -> lid2 -> [Char] -> morphism -> Result morphism2
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> morphism1 -> m morphism2
coerceMorphism lid
tlid (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid2) "coeqs" (morphism -> Result morphism2) -> morphism -> Result morphism2
forall a b. (a -> b) -> a -> b
$ Map Int morphism -> Int -> morphism
forall k a. Ord k => Map k a -> k -> a
(Map.!) Map Int morphism
colM Int
newN
   morphism2
mor22 <- morphism2 -> morphism2 -> Result morphism2
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp morphism2
mor2 morphism2
mor22'
   let gMor11 :: GMorphism
gMor11 = cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism cid
cid1 ExtSign sign1 symbol1
sig1 SigId
idx1 morphism2
mor11 MorId
startMorId
   let gMor22 :: GMorphism
gMor22 = cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism cid
cid2 ExtSign sign1 symbol1
sig2 SigId
idx2 morphism2
mor22 MorId
startMorId
   GDiagram
-> Map Int [(Int, G_theory)]
-> (Int, G_theory)
-> (Int, G_theory)
-> (Int, G_theory)
-> GMorphism
-> GMorphism
-> [(Int, G_theory)]
-> Result (GDiagram, Map Int [(Int, G_theory)])
computeCoeqs GDiagram
graph Map Int [(Int, G_theory)]
funDesc (Int
n1, G_theory
gt1) (Int
n2, G_theory
gt2) (Int
newN, G_theory
newGt1)
                       GMorphism
gMor11 GMorphism
gMor22 [(Int, G_theory)]
descs

-- returns a maximal node available
pickMaxNode :: (MonadPlus t) => Gr a b -> t (Node, a)
pickMaxNode :: Gr a b -> t (Int, a)
pickMaxNode graph :: Gr a b
graph = [t (Int, a)] -> t (Int, a)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([t (Int, a)] -> t (Int, a)) -> [t (Int, a)] -> t (Int, a)
forall a b. (a -> b) -> a -> b
$ ((Int, a) -> t (Int, a)) -> [(Int, a)] -> [t (Int, a)]
forall a b. (a -> b) -> [a] -> [b]
map (Int, a) -> t (Int, a)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, a)] -> [t (Int, a)]) -> [(Int, a)] -> [t (Int, a)]
forall a b. (a -> b) -> a -> b
$
                    ((Int, a) -> Bool) -> [(Int, a)] -> [(Int, a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (node :: Int
node, _) -> Gr a b -> Int -> Int
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Int -> Int
outdeg Gr a b
graph Int
node Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0) ([(Int, a)] -> [(Int, a)]) -> [(Int, a)] -> [(Int, a)]
forall a b. (a -> b) -> a -> b
$
                    Gr a b -> [(Int, a)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr a b
graph

{- returns a list of common descendants of two maximal nodes:
one node if a glb exists, or all maximal descendants otherwise -}
commonDesc :: Map.Map Node [(Node, G_theory)] -> Node -> Node
            -> [(Node, G_theory)]
commonDesc :: Map Int [(Int, G_theory)] -> Int -> Int -> [(Int, G_theory)]
commonDesc funDesc :: Map Int [(Int, G_theory)]
funDesc n1 :: Int
n1 n2 :: Int
n2 = case Map Int [(Int, G_theory)] -> Int -> Int -> Maybe (Int, G_theory)
forall a.
Eq a =>
Map Int [(Int, a)] -> Int -> Int -> Maybe (Int, a)
glb Map Int [(Int, G_theory)]
funDesc Int
n1 Int
n2 of
                            Just x :: (Int, G_theory)
x -> [(Int, G_theory)
x]
                            Nothing -> Map Int [(Int, G_theory)] -> Int -> Int -> [(Int, G_theory)]
forall a. Eq a => Map Int [(Int, a)] -> Int -> Int -> [(Int, a)]
maxBounds Map Int [(Int, G_theory)]
funDesc Int
n1 Int
n2

-- returns a weakly amalgamable square of lax triangles
pickSquare :: (MonadPlus t, Fail.MonadFail t) => Result GMorphism -> Result GMorphism
  -> t Square
pickSquare :: Result GMorphism -> Result GMorphism -> t Square
pickSquare (Result _ (Just phi1 :: GMorphism
phi1@(GMorphism cid1 :: cid
cid1 _ _ _ _)))
           (Result _ (Just phi2 :: GMorphism
phi2@(GMorphism cid2 :: cid
cid2 _ _ _ _))) =
   if GMorphism -> Bool
isHomogeneous GMorphism
phi1 Bool -> Bool -> Bool
&& GMorphism -> Bool
isHomogeneous GMorphism
phi2 then
      Square -> t Square
forall (m :: * -> *) a. Monad m => a -> m a
return (Square -> t Square) -> Square -> t Square
forall a b. (a -> b) -> a -> b
$ AnyLogic -> Square
mkIdSquare (AnyLogic -> Square) -> AnyLogic -> Square
forall a b. (a -> b) -> a -> b
$ lid1 -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic (lid1 -> AnyLogic) -> lid1 -> AnyLogic
forall a b. (a -> b) -> a -> b
$ cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cid1
    -- since they have the same target, both homogeneous implies same logic
   else do
    {- if one of them is homogeneous, build the square
    with identity modification of the other comorphism -}
    let defaultSquare :: [Square]
defaultSquare
          | GMorphism -> Bool
isHomogeneous GMorphism
phi1 = [AnyComorphism -> Square
mkDefSquare (AnyComorphism -> Square) -> AnyComorphism -> Square
forall a b. (a -> b) -> a -> b
$ cid -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism cid
cid2]
          | GMorphism -> Bool
isHomogeneous GMorphism
phi2 = [Square -> Square
mirrorSquare (Square -> Square) -> Square -> Square
forall a b. (a -> b) -> a -> b
$ AnyComorphism -> Square
mkDefSquare (AnyComorphism -> Square) -> AnyComorphism -> Square
forall a b. (a -> b) -> a -> b
$ cid -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism cid
cid1]
          | Bool
otherwise = []
    case Result [Square] -> Maybe [Square]
forall a. Result a -> Maybe a
maybeResult (Result [Square] -> Maybe [Square])
-> Result [Square] -> Maybe [Square]
forall a b. (a -> b) -> a -> b
$ AnyComorphism -> AnyComorphism -> Result [Square]
lookupSquare_in_LG (cid -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism cid
cid1) (cid -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism cid
cid2) of
          Nothing -> [t Square] -> t Square
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([t Square] -> t Square) -> [t Square] -> t Square
forall a b. (a -> b) -> a -> b
$ (Square -> t Square) -> [Square] -> [t Square]
forall a b. (a -> b) -> [a] -> [b]
map Square -> t Square
forall (m :: * -> *) a. Monad m => a -> m a
return [Square]
defaultSquare
          Just sqList :: [Square]
sqList -> [t Square] -> t Square
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([t Square] -> t Square) -> [t Square] -> t Square
forall a b. (a -> b) -> a -> b
$ (Square -> t Square) -> [Square] -> [t Square]
forall a b. (a -> b) -> [a] -> [b]
map Square -> t Square
forall (m :: * -> *) a. Monad m => a -> m a
return ([Square] -> [t Square]) -> [Square] -> [t Square]
forall a b. (a -> b) -> a -> b
$ [Square]
sqList [Square] -> [Square] -> [Square]
forall a. [a] -> [a] -> [a]
++ [Square]
defaultSquare

pickSquare (Result _ Nothing) _ = [Char] -> t Square
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail "Error computing comorphisms"
pickSquare _ (Result _ Nothing) = [Char] -> t Square
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail "Error computing comorphisms"

-- builds the span for which the colimit is computed
buildSpan :: GDiagram ->
             Map.Map Node [(Node, G_theory)] ->
             AnyComorphism ->
             AnyComorphism ->
             AnyComorphism ->
             AnyComorphism ->
             AnyComorphism ->
             AnyModification ->
             AnyModification ->
             G_theory ->
             G_theory ->
             G_theory ->
             GMorphism ->
             GMorphism ->
             Int -> Int -> Int ->
             [(Int, G_theory)] ->
             Result (GDiagram, Map.Map Node [(Node, G_theory)])
buildSpan :: GDiagram
-> Map Int [(Int, G_theory)]
-> AnyComorphism
-> AnyComorphism
-> AnyComorphism
-> AnyComorphism
-> AnyComorphism
-> AnyModification
-> AnyModification
-> G_theory
-> G_theory
-> G_theory
-> GMorphism
-> GMorphism
-> Int
-> Int
-> Int
-> [(Int, G_theory)]
-> Result (GDiagram, Map Int [(Int, G_theory)])
buildSpan graph :: GDiagram
graph
          funDesc :: Map Int [(Int, G_theory)]
funDesc
          d :: AnyComorphism
d@(Comorphism _cidD :: cid
_cidD)
          e1 :: AnyComorphism
e1@(Comorphism cidE1 :: cid
cidE1)
          e2 :: AnyComorphism
e2@(Comorphism cidE2 :: cid
cidE2)
          _d1 :: AnyComorphism
_d1@(Comorphism _cidD1 :: cid
_cidD1)
          _d2 :: AnyComorphism
_d2@(Comorphism _cidD2 :: cid
_cidD2)
          _m1 :: AnyModification
_m1@(Modification cidM1 :: lid
cidM1)
          _m2 :: AnyModification
_m2@(Modification cidM2 :: lid
cidM2)
          gt :: G_theory
gt@(G_theory lid :: lid
lid _ sign :: ExtSign sign symbol
sign _ _ _)
          gt1 :: G_theory
gt1@(G_theory lid1 :: lid
lid1 _ sign1 :: ExtSign sign symbol
sign1 _ _ _)
          gt2 :: G_theory
gt2@(G_theory lid2 :: lid
lid2 _ sign2 :: ExtSign sign symbol
sign2 _ _ _)
          _phi1 :: GMorphism
_phi1@(GMorphism cid1 :: cid
cid1 _ _ mor1 :: morphism2
mor1 _)
          _phi2 :: GMorphism
_phi2@(GMorphism cid2 :: cid
cid2 _ _ mor2 :: morphism2
mor2 _)
          n :: Int
n n1 :: Int
n1 n2 :: Int
n2
          maxNodes :: [(Int, G_theory)]
maxNodes
           = do
 sig :: G_theory
sig@(G_theory _lid0 :: lid
_lid0 _ _sign0 :: ExtSign sign symbol
_sign0 _ _ _) <- Bool -> AnyComorphism -> G_theory -> Result G_theory
mapG_theory Bool
False AnyComorphism
d G_theory
gt -- phi^d(Sigma)
 G_theory
sig1 <- Bool -> AnyComorphism -> G_theory -> Result G_theory
mapG_theory Bool
False AnyComorphism
e1 G_theory
gt1 -- phi^e1(Sigma1)
 G_theory
sig2 <- Bool -> AnyComorphism -> G_theory -> Result G_theory
mapG_theory Bool
False AnyComorphism
e2 G_theory
gt2 -- phi^e2(Sigma2)
 morphism1
mor1' <- lid2 -> lid1 -> [Char] -> morphism2 -> Result morphism1
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> morphism1 -> m morphism2
coerceMorphism (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid1) (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cidE1) "buildSpan" morphism2
mor1
 morphism2
eps1 <- cid -> morphism1 -> Result morphism2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> morphism1 -> Result morphism2
map_morphism cid
cidE1 morphism1
mor1' -- phi^e1(sigma1)
 ExtSign sign1 symbol1
sign' <- lid
-> log1
-> [Char]
-> ExtSign sign symbol
-> Result (ExtSign sign1 symbol1)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> [Char]
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid (cid1 -> log1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic (cid1 -> log1) -> cid1 -> log1
forall a b. (a -> b) -> a -> b
$ lid -> cid1
forall lid cid1 cid2 log1 sublogics1 basic_spec1 sentence1
       symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1
       proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2
       symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2
       log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
       sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4
       basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4
       symbol4 raw_symbol4 proof_tree4.
Modification
  lid
  cid1
  cid2
  log1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  log2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2
  log3
  sublogics3
  basic_spec3
  sentence3
  symb_items3
  symb_map_items3
  sign3
  morphism3
  symbol3
  raw_symbol3
  proof_tree3
  log4
  sublogics4
  basic_spec4
  sentence4
  symb_items4
  symb_map_items4
  sign4
  morphism4
  symbol4
  raw_symbol4
  proof_tree4 =>
lid -> cid1
sourceComorphism lid
cidM1) "buildSpan" ExtSign sign symbol
sign
 morphism2
tau1 <- lid -> sign1 -> Result morphism2
forall lid cid1 cid2 log1 sublogics1 basic_spec1 sentence1
       symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1
       proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2
       symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2
       log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
       sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4
       basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4
       symbol4 raw_symbol4 proof_tree4.
Modification
  lid
  cid1
  cid2
  log1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  log2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2
  log3
  sublogics3
  basic_spec3
  sentence3
  symb_items3
  symb_map_items3
  sign3
  morphism3
  symbol3
  raw_symbol3
  proof_tree3
  log4
  sublogics4
  basic_spec4
  sentence4
  symb_items4
  symb_map_items4
  sign4
  morphism4
  symbol4
  raw_symbol4
  proof_tree4 =>
lid -> sign1 -> Result morphism2
tauSigma lid
cidM1 (ExtSign sign1 symbol1 -> sign1
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign1 symbol1
sign') -- I^u1_Sigma
 morphism2
tau1' <- log2 -> lid2 -> [Char] -> morphism2 -> Result morphism2
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> morphism1 -> m morphism2
coerceMorphism (cid1 -> log2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic (cid1 -> log2) -> cid1 -> log2
forall a b. (a -> b) -> a -> b
$ lid -> cid1
forall lid cid1 cid2 log1 sublogics1 basic_spec1 sentence1
       symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1
       proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2
       symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2
       log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
       sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4
       basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4
       symbol4 raw_symbol4 proof_tree4.
Modification
  lid
  cid1
  cid2
  log1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  log2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2
  log3
  sublogics3
  basic_spec3
  sentence3
  symb_items3
  symb_map_items3
  sign3
  morphism3
  symbol3
  raw_symbol3
  proof_tree3
  log4
  sublogics4
  basic_spec4
  sentence4
  symb_items4
  symb_map_items4
  sign4
  morphism4
  symbol4
  raw_symbol4
  proof_tree4 =>
lid -> cid1
sourceComorphism lid
cidM1)
                         (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cidE1) "buildSpan" morphism2
tau1
 morphism2
rho1 <- morphism2 -> morphism2 -> Result morphism2
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp morphism2
tau1' morphism2
eps1
 morphism1
mor2' <- lid2 -> lid1 -> [Char] -> morphism2 -> Result morphism1
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> morphism1 -> m morphism2
coerceMorphism (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid2) (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cidE2) "buildSpan" morphism2
mor2
 morphism2
eps2 <- cid -> morphism1 -> Result morphism2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> morphism1 -> Result morphism2
map_morphism cid
cidE2 morphism1
mor2' -- phi^e2(sigma2)
 ExtSign sign1 symbol1
sign'' <- lid
-> log1
-> [Char]
-> ExtSign sign symbol
-> Result (ExtSign sign1 symbol1)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> [Char]
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid (cid1 -> log1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic (cid1 -> log1) -> cid1 -> log1
forall a b. (a -> b) -> a -> b
$ lid -> cid1
forall lid cid1 cid2 log1 sublogics1 basic_spec1 sentence1
       symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1
       proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2
       symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2
       log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
       sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4
       basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4
       symbol4 raw_symbol4 proof_tree4.
Modification
  lid
  cid1
  cid2
  log1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  log2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2
  log3
  sublogics3
  basic_spec3
  sentence3
  symb_items3
  symb_map_items3
  sign3
  morphism3
  symbol3
  raw_symbol3
  proof_tree3
  log4
  sublogics4
  basic_spec4
  sentence4
  symb_items4
  symb_map_items4
  sign4
  morphism4
  symbol4
  raw_symbol4
  proof_tree4 =>
lid -> cid1
sourceComorphism lid
cidM2) "buildSpan" ExtSign sign symbol
sign
 morphism2
tau2 <- lid -> sign1 -> Result morphism2
forall lid cid1 cid2 log1 sublogics1 basic_spec1 sentence1
       symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1
       proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2
       symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2
       log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
       sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4
       basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4
       symbol4 raw_symbol4 proof_tree4.
Modification
  lid
  cid1
  cid2
  log1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  log2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2
  log3
  sublogics3
  basic_spec3
  sentence3
  symb_items3
  symb_map_items3
  sign3
  morphism3
  symbol3
  raw_symbol3
  proof_tree3
  log4
  sublogics4
  basic_spec4
  sentence4
  symb_items4
  symb_map_items4
  sign4
  morphism4
  symbol4
  raw_symbol4
  proof_tree4 =>
lid -> sign1 -> Result morphism2
tauSigma lid
cidM2 (ExtSign sign1 symbol1 -> sign1
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign1 symbol1
sign'') -- I^u2_Sigma
 morphism2
tau2' <- log2 -> lid2 -> [Char] -> morphism2 -> Result morphism2
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> morphism1 -> m morphism2
coerceMorphism (cid1 -> log2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic (cid1 -> log2) -> cid1 -> log2
forall a b. (a -> b) -> a -> b
$ lid -> cid1
forall lid cid1 cid2 log1 sublogics1 basic_spec1 sentence1
       symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1
       proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2
       symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2
       log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
       sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4
       basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4
       symbol4 raw_symbol4 proof_tree4.
Modification
  lid
  cid1
  cid2
  log1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  log2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2
  log3
  sublogics3
  basic_spec3
  sentence3
  symb_items3
  symb_map_items3
  sign3
  morphism3
  symbol3
  raw_symbol3
  proof_tree3
  log4
  sublogics4
  basic_spec4
  sentence4
  symb_items4
  symb_map_items4
  sign4
  morphism4
  symbol4
  raw_symbol4
  proof_tree4 =>
lid -> cid1
sourceComorphism lid
cidM2)
                         (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cidE2) "buildSpan" morphism2
tau2
 morphism2
rho2 <- morphism2 -> morphism2 -> Result morphism2
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp morphism2
tau2' morphism2
eps2
 ExtSign sign1 symbol1
signE1 <- lid
-> lid1
-> [Char]
-> ExtSign sign symbol
-> Result (ExtSign sign1 symbol1)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> [Char]
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid1 (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cidE1) " " ExtSign sign symbol
sign1
 ExtSign sign1 symbol1
signE2 <- lid
-> lid1
-> [Char]
-> ExtSign sign symbol
-> Result (ExtSign sign1 symbol1)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> [Char]
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid2 (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cidE2) " " ExtSign sign symbol
sign2
 (graph1 :: GDiagram
graph1, funDesc1 :: Map Int [(Int, G_theory)]
funDesc1) <- GDiagram
-> G_theory
-> G_theory
-> G_theory
-> Int
-> Int
-> Int
-> GMorphism
-> GMorphism
-> Map Int [(Int, G_theory)]
-> [(Int, G_theory)]
-> Result (GDiagram, Map Int [(Int, G_theory)])
addNodeToGraph GDiagram
graph G_theory
sig G_theory
sig1 G_theory
sig2 Int
n Int
n1 Int
n2
     (cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism cid
cidE1 ExtSign sign1 symbol1
signE1 SigId
startSigId morphism2
rho1 MorId
startMorId)
     (cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism cid
cidE2 ExtSign sign1 symbol1
signE2 SigId
startSigId morphism2
rho2 MorId
startMorId)
     Map Int [(Int, G_theory)]
funDesc [(Int, G_theory)]
maxNodes
 (GDiagram, Map Int [(Int, G_theory)])
-> Result (GDiagram, Map Int [(Int, G_theory)])
forall (m :: * -> *) a. Monad m => a -> m a
return (GDiagram
graph1, Map Int [(Int, G_theory)]
funDesc1)

pickMaximalDesc :: (MonadPlus t) => [(Node, G_theory)] -> t (Node, G_theory)
pickMaximalDesc :: [(Int, G_theory)] -> t (Int, G_theory)
pickMaximalDesc descList :: [(Int, G_theory)]
descList = [t (Int, G_theory)] -> t (Int, G_theory)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([t (Int, G_theory)] -> t (Int, G_theory))
-> [t (Int, G_theory)] -> t (Int, G_theory)
forall a b. (a -> b) -> a -> b
$ ((Int, G_theory) -> t (Int, G_theory))
-> [(Int, G_theory)] -> [t (Int, G_theory)]
forall a b. (a -> b) -> [a] -> [b]
map (Int, G_theory) -> t (Int, G_theory)
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int, G_theory)]
descList

nrMaxNodes :: Gr a b -> Int
nrMaxNodes :: Gr a b -> Int
nrMaxNodes graph :: Gr a b
graph = [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ n :: Int
n -> Gr a b -> Int -> Int
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Int -> Int
outdeg Gr a b
graph Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Gr a b -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Int]
nodes Gr a b
graph

-- | backtracking function for heterogeneous weak amalgamable cocones
hetWeakAmalgCocone :: (Fail.MonadFail m, LogicT t, MonadPlus (t m),
                      Fail.MonadFail (t m)) =>
                     GDiagram -> Map.Map Int [(Int, G_theory)] -> t m GDiagram
hetWeakAmalgCocone :: GDiagram -> Map Int [(Int, G_theory)] -> t m GDiagram
hetWeakAmalgCocone graph :: GDiagram
graph funDesc :: Map Int [(Int, G_theory)]
funDesc =
 if GDiagram -> Int
forall a b. Gr a b -> Int
nrMaxNodes GDiagram
graph Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then GDiagram -> t m GDiagram
forall (m :: * -> *) a. Monad m => a -> m a
return GDiagram
graph
 else t m GDiagram -> t m GDiagram
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(LogicT t, Monad m, MonadPlus (t m)) =>
t m a -> t m a
once (t m GDiagram -> t m GDiagram) -> t m GDiagram -> t m GDiagram
forall a b. (a -> b) -> a -> b
$ do
  (n1 :: Int
n1, gt1 :: G_theory
gt1) <- GDiagram -> t m (Int, G_theory)
forall (t :: * -> *) a b. MonadPlus t => Gr a b -> t (Int, a)
pickMaxNode GDiagram
graph
  (n2 :: Int
n2, gt2 :: G_theory
gt2) <- GDiagram -> t m (Int, G_theory)
forall (t :: * -> *) a b. MonadPlus t => Gr a b -> t (Int, a)
pickMaxNode GDiagram
graph
  Bool -> t m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Int
n1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n2) -- to consider each pair of maximal nodes only once
  let descList :: [(Int, G_theory)]
descList = Map Int [(Int, G_theory)] -> Int -> Int -> [(Int, G_theory)]
commonDesc Map Int [(Int, G_theory)]
funDesc Int
n1 Int
n2
  case [(Int, G_theory)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Int, G_theory)]
descList of
    0 -> t m GDiagram
forall (m :: * -> *) a. MonadPlus m => m a
mzero -- no common descendants for n1 and n2
    _ -> do {- just one common descendant implies greatest lower bound
            for several, the tail is not empty and we compute coequalizers -}
     (n :: Int
n, gt :: G_theory
gt) <- [(Int, G_theory)] -> t m (Int, G_theory)
forall (t :: * -> *).
MonadPlus t =>
[(Int, G_theory)] -> t (Int, G_theory)
pickMaximalDesc [(Int, G_theory)]
descList
     let phi1 :: Result GMorphism
phi1 = GDiagram -> Int -> Int -> Result GMorphism
dijkstra GDiagram
graph Int
n Int
n1
         phi2 :: Result GMorphism
phi2 = GDiagram -> Int -> Int -> Result GMorphism
dijkstra GDiagram
graph Int
n Int
n2
     Square
square <- Result GMorphism -> Result GMorphism -> t m Square
forall (t :: * -> *).
(MonadPlus t, MonadFail t) =>
Result GMorphism -> Result GMorphism -> t Square
pickSquare Result GMorphism
phi1 Result GMorphism
phi2
     let d :: AnyComorphism
d = LaxTriangle -> AnyComorphism
laxTarget (LaxTriangle -> AnyComorphism) -> LaxTriangle -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ Square -> LaxTriangle
leftTriangle Square
square
         e1 :: AnyComorphism
e1 = LaxTriangle -> AnyComorphism
laxFst (LaxTriangle -> AnyComorphism) -> LaxTriangle -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ Square -> LaxTriangle
leftTriangle Square
square
         d1 :: AnyComorphism
d1 = LaxTriangle -> AnyComorphism
laxSnd (LaxTriangle -> AnyComorphism) -> LaxTriangle -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ Square -> LaxTriangle
leftTriangle Square
square
         e2 :: AnyComorphism
e2 = LaxTriangle -> AnyComorphism
laxFst (LaxTriangle -> AnyComorphism) -> LaxTriangle -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ Square -> LaxTriangle
rightTriangle Square
square
         d2 :: AnyComorphism
d2 = LaxTriangle -> AnyComorphism
laxSnd (LaxTriangle -> AnyComorphism) -> LaxTriangle -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ Square -> LaxTriangle
rightTriangle Square
square
         m1 :: AnyModification
m1 = LaxTriangle -> AnyModification
laxModif (LaxTriangle -> AnyModification) -> LaxTriangle -> AnyModification
forall a b. (a -> b) -> a -> b
$ Square -> LaxTriangle
leftTriangle Square
square
         m2 :: AnyModification
m2 = LaxTriangle -> AnyModification
laxModif (LaxTriangle -> AnyModification) -> LaxTriangle -> AnyModification
forall a b. (a -> b) -> a -> b
$ Square -> LaxTriangle
rightTriangle Square
square
     case Result GMorphism -> Maybe GMorphism
forall a. Result a -> Maybe a
maybeResult Result GMorphism
phi1 of
      Nothing -> t m GDiagram
forall (m :: * -> *) a. MonadPlus m => m a
mzero
      Just phi1' :: GMorphism
phi1' -> case Result GMorphism -> Maybe GMorphism
forall a. Result a -> Maybe a
maybeResult Result GMorphism
phi2 of
       Nothing -> t m GDiagram
forall (m :: * -> *) a. MonadPlus m => m a
mzero
       Just phi2' :: GMorphism
phi2' -> do
        let mGraph :: Result (GDiagram, Map Int [(Int, G_theory)])
mGraph = GDiagram
-> Map Int [(Int, G_theory)]
-> AnyComorphism
-> AnyComorphism
-> AnyComorphism
-> AnyComorphism
-> AnyComorphism
-> AnyModification
-> AnyModification
-> G_theory
-> G_theory
-> G_theory
-> GMorphism
-> GMorphism
-> Int
-> Int
-> Int
-> [(Int, G_theory)]
-> Result (GDiagram, Map Int [(Int, G_theory)])
buildSpan GDiagram
graph Map Int [(Int, G_theory)]
funDesc AnyComorphism
d AnyComorphism
e1 AnyComorphism
e2 AnyComorphism
d1 AnyComorphism
d2 AnyModification
m1 AnyModification
m2 G_theory
gt G_theory
gt1 G_theory
gt2
                      GMorphism
phi1' GMorphism
phi2' Int
n Int
n1 Int
n2 ([(Int, G_theory)] -> Result (GDiagram, Map Int [(Int, G_theory)]))
-> [(Int, G_theory)]
-> Result (GDiagram, Map Int [(Int, G_theory)])
forall a b. (a -> b) -> a -> b
$ ((Int, G_theory) -> Bool) -> [(Int, G_theory)] -> [(Int, G_theory)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (nx :: Int
nx, _) -> Int
nx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
n) [(Int, G_theory)]
descList
        case Result (GDiagram, Map Int [(Int, G_theory)])
-> Maybe (GDiagram, Map Int [(Int, G_theory)])
forall a. Result a -> Maybe a
maybeResult Result (GDiagram, Map Int [(Int, G_theory)])
mGraph of
         Nothing -> t m GDiagram
forall (m :: * -> *) a. MonadPlus m => m a
mzero
         Just (graph1 :: GDiagram
graph1, funDesc1 :: Map Int [(Int, G_theory)]
funDesc1) -> GDiagram -> Map Int [(Int, G_theory)] -> t m GDiagram
forall (m :: * -> *) (t :: (* -> *) -> * -> *).
(MonadFail m, LogicT t, MonadPlus (t m), MonadFail (t m)) =>
GDiagram -> Map Int [(Int, G_theory)] -> t m GDiagram
hetWeakAmalgCocone GDiagram
graph1 Map Int [(Int, G_theory)]
funDesc1