content: {- |
  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
  