WACocone.hs

{- |
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 l diag = do
          (sig, sink) <- signature_colimit l diag
          return (sig, 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 graph = let
  nodeList = nodes graph
  root = head nodeList
  availNodes = Map.fromList $ zip nodeList (repeat True)
  bfs queue avail = case queue of
     [] -> avail
     n : ns -> let
       avail1 = Map.insert n False avail
       nbs = filter (\ x -> Map.findWithDefault (error "isconnected") x avail)
             $ neighbors graph n
      in bfs (ns ++ nbs) avail1
  in not $ any (\ x -> Map.findWithDefault (error "iscon 2") x
                   (bfs [root] availNodes)) nodeList

-- | checks whether the graph is thin

isThin :: Gr a b -> Bool
isThin = checkThinness Map.empty . edges

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


-- | checks whether a graph is acyclic

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

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

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

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

commonBounds :: (Eq a) => Map.Map Node [(Node, a)] -> Node -> Node -> [(Node, a)]
commonBounds funDesc n1 n2 = filter
  (\ x -> x `elem` (Map.!) funDesc n1 && x `elem` (Map.!) funDesc n2 )
  $ nub $ (Map.!) funDesc n1 ++ (Map.!) funDesc 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 funDesc n1 n2 = let
 cDescs = commonBounds funDesc n1 n2
 subList [] _ = True
 subList (x : xs) l2 = x `elem` l2 && subList xs l2
 glbList = filter (\ (n, x) -> subList
    (filter (\ (n0, x0) -> (n, x) /= (n0, x0)) cDescs) (funDesc Map.! n)
           ) 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 glbList of
     [] -> Nothing
     x : _ -> Just 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 funDesc n1 n2 = let
  cDescs = commonBounds funDesc n1 n2
  isDesc n0 (n, y) = (n, y) `elem` funDesc Map.! n0
  noDescs (n, y) = not $ any (\ (n0, _) -> isDesc n0 (n, y)) cDescs
 in filter noDescs cDescs

-- dijsktra algorithm for finding the the shortest path between two nodes
dijkstra :: GDiagram -> Node -> Node -> Result GMorphism
dijkstra graph source target = do
 let
  dist = Map.insert source 0 $ Map.fromList $
         zip (nodes graph) $ repeat $ 2 * length (edges graph)
  prev = if source == target then Map.insert source source Map.empty
         else Map.empty
  q = nodes graph
  com = case lab graph source of
    Nothing -> Map.empty -- shouldnt be the case
    Just gt -> Map.insert source (ide $ signOf gt) Map.empty
  extractMin queue dMap = let
   u = head $
     filter (\ x -> Map.findWithDefault (error "dijkstra") x dMap ==
             minimum
               (map (\ x1 -> Map.findWithDefault (error "dijkstra") x1 dMap)
               queue))
               queue
   in ( Set.toList $ Set.difference (Set.fromList queue) (Set.fromList [u]) , u)
  updateNeighbors d p c u gr = let
    outEdges = out gr u
    upNeighbor dMap pMap cMap uNode edgeList = case edgeList of
     [] -> (dMap, pMap, cMap)
     (_, v, (_, gmor)) : edgeL -> let
       alt = Map.findWithDefault (error "dijkstra") uNode dMap + 1
      in
        if alt >= Map.findWithDefault (error "dijsktra") v dMap then
          upNeighbor dMap pMap cMap uNode edgeL
        else let
      d1 = Map.insert v alt dMap
      p1 = Map.insert v uNode pMap
      c1 = Map.insert v gmor cMap
      in upNeighbor d1 p1 c1 uNode edgeL
   in upNeighbor d p c u outEdges
  -- for each neighbor of u, if d(u)+1 < d(v), modify p(v) = u, d(v) = d(u)+1
  mainloop gr sn tn qL d p c = let
   (q1, u) = extractMin qL d
   (d1, p1, c1) = updateNeighbors d p c u gr
   in if u == tn then shortPath sn p1 c1 [] tn
     else mainloop gr sn tn q1 d1 p1 c1
  shortPath sn p1 c s u =
   if u `notElem` Map.keys p1 then Fail.fail "path not found"
    else let
    x = Map.findWithDefault (error $ show u) u p1 in
    if x == sn then return (u : s, c)
     else shortPath sn p1 c (u : s) x
 (nodeList, com1) <- mainloop graph source target q dist prev com
 foldM comp ((Map.!) com1 source) . map ((Map.!) com1) $ 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 initGraph newGraph = do
 let (maxNode, sigma) = head $ filter (\ (node, _) -> outdeg newGraph node == 0) $
                        labNodes newGraph
     buildMor pairList solList =
      case pairList of
       (n, _) : pairs -> do nMor <- dijkstra newGraph n maxNode
                            buildMor pairs (solList ++ [(n, nMor)])
       [] -> return solList
 morList <- buildMor (labNodes initGraph) []
 return (sigma, Map.fromList 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 oldGraph
               (G_theory lid _ extSign _ _ _)
               gt1@(G_theory lid1 _ extSign1 idx1 _ _)
               gt2@(G_theory lid2 _ extSign2 idx2 _ _)
               n
               n1
               n2
               (GMorphism cid1 ss1 _ mor1 _)
               (GMorphism cid2 ss2 _ mor2 _)
               funDesc maxNodes = do
 let newNode = 1 + maximum (nodes oldGraph) -- get a new node
 s1 <- coerceSign lid1 lid "addToNodeGraph" extSign1
 s2 <- coerceSign lid2 lid "addToNodeGraph" extSign2
 m1 <- coerceMorphism (targetLogic cid1) lid "addToNodeGraph" mor1
 m2 <- coerceMorphism (targetLogic cid2) lid "addToNodeGraph" mor2
 let spanGr = Graph.mkGraph
       [(n, plainSign extSign), (n1, plainSign s1), (n2, plainSign s2)]
       [(n, n1, (1, m1)), (n, n2, (1, m2))]
 (sig, morMap) <- weakly_amalgamable_colimit lid spanGr
      -- must  coerce here
 m11 <- coerceMorphism lid (targetLogic cid1) "addToNodeGraph" $
        morMap Map.! n1
 m22 <- coerceMorphism lid (targetLogic cid2) "addToNodeGraph" $
        morMap Map.! n2
 let gth = noSensGTheory lid (mkExtSign sig) startSigId
     gmor1 = GMorphism cid1 ss1 idx1 m11 startMorId
     gmor2 = GMorphism cid2 ss2 idx2 m22 startMorId
 case maxNodes of
   [] -> do
    let newGraph = insEdges [(n1, newNode, (1, gmor1)), (n2, newNode, (1, gmor2))] $
                   insNode (newNode, gth) oldGraph
        funDesc1 = Map.insert newNode
                     (nub $ (Map.!) funDesc n1 ++ (Map.!) funDesc n2 ) funDesc
    return (newGraph, funDesc1)
   _ -> computeCoeqs oldGraph funDesc (n1, gt1) (n2, gt2)
                           (newNode, gth) gmor1 gmor2 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 oldGraph funDesc (n1, _) (n2, _) (newN, newGt) gmor1 gmor2 [] = do
 let newGraph = insEdges [(n1, newN, (1, gmor1)), (n2, newN, (1, gmor2))] $
                insNode (newN, newGt) oldGraph
     descFun1 = Map.insert newN
                (nub $ (Map.!) funDesc n1 ++ (Map.!) funDesc n2 ) funDesc
 return (newGraph, descFun1)
computeCoeqs graph funDesc (n1, gt1) (n2, gt2)
                    (newN, _newGt@(G_theory tlid _ tsign _ _ _))
                    _gmor1@(GMorphism cid1 sig1 idx1 mor1 _ )
                    _gmor2@(GMorphism cid2 sig2 idx2 mor2 _ ) ((n, gt) : descs) = do
 _rho1@(GMorphism cid3 _ _ mor3 _) <- dijkstra graph n n1
 _rho2@(GMorphism cid4 _ _ mor4 _) <- dijkstra graph n n2
 com1 <- compComorphism (Comorphism cid1) (Comorphism cid3)
 com2 <- compComorphism (Comorphism cid1) (Comorphism cid3)
 if com1 /= com2 then Fail.fail "Unable to compute coequalizer" else do
   _gtM@(G_theory lidM _ signM _idxM _ _) <- mapG_theory False com1 gt
   s1 <- coerceSign lidM tlid "coequalizers" signM
   mor3' <- coerceMorphism (targetLogic cid3) (sourceLogic cid1) "coeqs" mor3
   mor4' <- coerceMorphism (targetLogic cid4) (sourceLogic cid2) "coeqs" mor4
   m1 <- map_morphism cid1 mor3'
   m2 <- map_morphism cid2 mor4'
   phi1' <- comp m1 mor1
   phi2' <- comp m2 mor2
   phi1 <- coerceMorphism (targetLogic cid1) tlid "coeqs" phi1'
   phi2 <- coerceMorphism (targetLogic cid2) tlid "coeqs" phi2'
   -- build the double arrow for computing the coequalizers
   let doubleArrow = Graph.mkGraph
         [(n, plainSign s1), (newN, plainSign tsign)]
         [(n, newN, (1, phi1)), (n, newN, (1, phi2))]
   (colS, colM) <- weakly_amalgamable_colimit tlid doubleArrow
   let newGt1 = noSensGTheory tlid (mkExtSign colS) startSigId
   mor11' <- coerceMorphism tlid (targetLogic cid1) "coeqs" $ (Map.!) colM newN
   mor11 <- comp mor1 mor11'
   mor22' <- coerceMorphism tlid (targetLogic cid2) "coeqs" $ (Map.!) colM newN
   mor22 <- comp mor2 mor22'
   let gMor11 = GMorphism cid1 sig1 idx1 mor11 startMorId
   let gMor22 = GMorphism cid2 sig2 idx2 mor22 startMorId
   computeCoeqs graph funDesc (n1, gt1) (n2, gt2) (newN, newGt1)
                       gMor11 gMor22 descs

-- returns a maximal node available
pickMaxNode :: (MonadPlus t) => Gr a b -> t (Node, a)
pickMaxNode graph = msum $ map return $
                    filter (\ (node, _) -> outdeg graph node == 0) $
                    labNodes 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 funDesc n1 n2 = case glb funDesc n1 n2 of
                            Just x -> [x]
                            Nothing -> maxBounds funDesc n1 n2

-- returns a weakly amalgamable square of lax triangles
pickSquare :: (MonadPlus t, Fail.MonadFail t) => Result GMorphism -> Result GMorphism
  -> t Square
pickSquare (Result _ (Just phi1@(GMorphism cid1 _ _ _ _)))
           (Result _ (Just phi2@(GMorphism cid2 _ _ _ _))) =
   if isHomogeneous phi1 && isHomogeneous phi2 then
      return $ mkIdSquare $ Logic $ sourceLogic 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
          | isHomogeneous phi1 = [mkDefSquare $ Comorphism cid2]
          | isHomogeneous phi2 = [mirrorSquare $ mkDefSquare $ Comorphism cid1]
          | otherwise = []
    case maybeResult $ lookupSquare_in_LG (Comorphism cid1) (Comorphism cid2) of
          Nothing -> msum $ map return defaultSquare
          Just sqList -> msum $ map return $ sqList ++ defaultSquare

pickSquare (Result _ Nothing) _ = Fail.fail "Error computing comorphisms"
pickSquare _ (Result _ Nothing) = 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 graph
          funDesc
          d@(Comorphism _cidD)
          e1@(Comorphism cidE1)
          e2@(Comorphism cidE2)
          _d1@(Comorphism _cidD1)
          _d2@(Comorphism _cidD2)
          _m1@(Modification cidM1)
          _m2@(Modification cidM2)
          gt@(G_theory lid _ sign _ _ _)
          gt1@(G_theory lid1 _ sign1 _ _ _)
          gt2@(G_theory lid2 _ sign2 _ _ _)
          _phi1@(GMorphism cid1 _ _ mor1 _)
          _phi2@(GMorphism cid2 _ _ mor2 _)
          n n1 n2
          maxNodes
           = do
 sig@(G_theory _lid0 _ _sign0 _ _ _) <- mapG_theory False d gt -- phi^d(Sigma)
 sig1 <- mapG_theory False e1 gt1 -- phi^e1(Sigma1)
 sig2 <- mapG_theory False e2 gt2 -- phi^e2(Sigma2)
 mor1' <- coerceMorphism (targetLogic cid1) (sourceLogic cidE1) "buildSpan" mor1
 eps1 <- map_morphism cidE1 mor1' -- phi^e1(sigma1)
 sign' <- coerceSign lid (sourceLogic $ sourceComorphism cidM1) "buildSpan" sign
 tau1 <- tauSigma cidM1 (plainSign sign') -- I^u1_Sigma
 tau1' <- coerceMorphism (targetLogic $ sourceComorphism cidM1)
                         (targetLogic cidE1) "buildSpan" tau1
 rho1 <- comp tau1' eps1
 mor2' <- coerceMorphism (targetLogic cid2) (sourceLogic cidE2) "buildSpan" mor2
 eps2 <- map_morphism cidE2 mor2' -- phi^e2(sigma2)
 sign'' <- coerceSign lid (sourceLogic $ sourceComorphism cidM2) "buildSpan" sign
 tau2 <- tauSigma cidM2 (plainSign sign'') -- I^u2_Sigma
 tau2' <- coerceMorphism (targetLogic $ sourceComorphism cidM2)
                         (targetLogic cidE2) "buildSpan" tau2
 rho2 <- comp tau2' eps2
 signE1 <- coerceSign lid1 (sourceLogic cidE1) " " sign1
 signE2 <- coerceSign lid2 (sourceLogic cidE2) " " sign2
 (graph1, funDesc1) <- addNodeToGraph graph sig sig1 sig2 n n1 n2
     (GMorphism cidE1 signE1 startSigId rho1 startMorId)
     (GMorphism cidE2 signE2 startSigId rho2 startMorId)
     funDesc maxNodes
 return (graph1, funDesc1)

pickMaximalDesc :: (MonadPlus t) => [(Node, G_theory)] -> t (Node, G_theory)
pickMaximalDesc descList = msum $ map return descList

nrMaxNodes :: Gr a b -> Int
nrMaxNodes graph = length $ filter (\ n -> outdeg graph n == 0) $ nodes 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 graph funDesc =
 if nrMaxNodes graph == 1 then return graph
 else once $ do
  (n1, gt1) <- pickMaxNode graph
  (n2, gt2) <- pickMaxNode graph
  guard (n1 < n2) -- to consider each pair of maximal nodes only once
  let descList = commonDesc funDesc n1 n2
  case length descList of
    0 -> 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, gt) <- pickMaximalDesc descList
     let phi1 = dijkstra graph n n1
         phi2 = dijkstra graph n n2
     square <- pickSquare phi1 phi2
     let d = laxTarget $ leftTriangle square
         e1 = laxFst $ leftTriangle square
         d1 = laxSnd $ leftTriangle square
         e2 = laxFst $ rightTriangle square
         d2 = laxSnd $ rightTriangle square
         m1 = laxModif $ leftTriangle square
         m2 = laxModif $ rightTriangle square
     case maybeResult phi1 of
      Nothing -> mzero
      Just phi1' -> case maybeResult phi2 of
       Nothing -> mzero
       Just phi2' -> do
        let mGraph = buildSpan graph funDesc d e1 e2 d1 d2 m1 m2 gt gt1 gt2
                      phi1' phi2' n n1 n2 $ filter (\ (nx, _) -> nx /= n) descList
        case maybeResult mGraph of
         Nothing -> mzero
         Just (graph1, funDesc1) -> hetWeakAmalgCocone graph1 funDesc1