content: {- |
  Module      :  ./Proofs/DGFlattening.hs
  Description :  flattening parts of development graphs
  Copyright   :  (c) Igor Stassiy, DFKI Bremen 2008
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable(Logic)
  
  In this module we introduce flattening of the graph:
  
  Flattening importings - deleting all inclusion links,
   and inserting a new node, with new computed theory (computeTheory).
  
  Flattening non-disjoint unions - for each node with more than two importings
   modify importings in such a way that at each level, only non-disjoint
   signatures are imported.
  
  Flattening renaming - deterimining renaming link,
  inserting a new node with the renaming morphism applied to theory of a
  source, deleting the link and setting a new inclusion link between a
  new node and the target node.
  
  Flattening hiding links - for each compute normal form if there is such
   and eliminate hiding links.
  
  Flattening heterogeneity - for each heterogeneous link, compute theory of
   a target node and eliminate heterogeneous link.
  
  -}
  
  module Proofs.DGFlattening
    ( dgFlatImports
    , libFlatImports   -- importing
    , dgFlatDUnions
    , libFlatDUnions   -- non-disjoint unions
    , dgFlatRenamings
    , libFlatRenamings -- import with renaming
    , dgFlatHiding
    , libFlatHiding    -- hiding
    , dgFlatHeterogen
    , libFlatHeterogen -- heterogeniety
    , singleTreeFlatDUnions
    ) where
  
  import Common.ExtSign
  import Common.Id
  import Common.IRI (simpleIdToIRI)
  import Common.LibName
  import Common.Result
  
  import Comorphisms.LogicGraph
  
  import Logic.Coerce
  import Logic.Grothendieck
  import Logic.Logic
  
  import Proofs.EdgeUtils
  import Proofs.NormalForm
  
  import Static.ComputeTheory
  import Static.DevGraph
  import Static.DgUtils
  import Static.GTheory
  import Static.History
  
  import Data.Graph.Inductive.Graph hiding (empty)
  import Data.List
  import Data.Maybe
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  
  mkFlatStr :: String -> DGRule
  mkFlatStr = DGRule . ("Flat " ++)
  
  flatImports :: DGRule
  flatImports = mkFlatStr "all imports"
  
  flatNonDisjUnion :: DGRule
  flatNonDisjUnion = mkFlatStr "non-disjoint union"
  
  flatRename :: DGRule
  flatRename = mkFlatStr "renaming"
  
  flatHide :: DGRule
  flatHide = mkFlatStr "hiding"
  
  flatHet :: DGRule
  flatHet = mkFlatStr "heterogeneity"
  
  cErr :: String -> Node -> a
  cErr str n = error $ str ++ " no global theory for node " ++ show n
  
  -- this function performs flattening of import links
  dgFlatImports :: LibEnv -> LibName -> DGraph -> DGraph
  dgFlatImports libEnv ln dg = let
    nds = nodesDG dg
    -- part for dealing with the graph itself
    updLib = updateLib libEnv ln nds
    updDG = lookupDGraph ln updLib
    -- it seems changes of the labels are lost and all edges are simply deleted
    n_dg = changesDGH dg $ map DeleteEdge $ labEdgesDG updDG
    in groupHistory dg flatImports n_dg
    where
     updateNode :: LibEnv -> LibName -> Node -> DGChange
     updateNode lib_Env l_n n =
      let
       labRf = labDG (lookupDGraph l_n lib_Env) n
        {- have to consider references here. computeTheory is applied
        to the node at the end of the chain of references only. -}
      in case computeTheory lib_Env l_n n of
           Just ndgn_theory ->
             SetNodeLab labRf (n, labRf {dgn_theory = ndgn_theory})
           Nothing ->
             cErr "dgFlatImports" n
     updateLib :: LibEnv -> LibName -> [Node] -> LibEnv
     updateLib lib_Env l_n nds =
      case nds of
       [] -> lib_Env
       hd : tl -> let
                 change = updateNode lib_Env l_n hd
                 ref_dg = lookupDGraph l_n lib_Env
                 u_dg = changeDGH ref_dg change
                 new_dg = groupHistory ref_dg flatImports u_dg
                in
                 updateLib (Map.insert l_n new_dg lib_Env) l_n tl
  
  -- this function performs flattening of imports for the whole library
  libFlatImports :: LibEnv -> Result LibEnv
  libFlatImports lib = return $ Map.mapWithKey (dgFlatImports lib) lib
  
  {- this function performs flattening of imports with renamings
  links for a given developement graph -}
  dgFlatRenamings :: LibEnv -> LibName -> DGraph -> DGraph
  dgFlatRenamings lib_Env l_n dg =
    let
     l_edges = labEdgesDG dg
     renamings = filter (\ (_, _, x) -> let l_type = getRealDGLinkType x in
       case l_type of
         DGEdgeType { edgeTypeModInc = GlobalDef, isInc = False} -> True
         _ -> False ) l_edges
     fin_dg = applyUpdDG renamings dg
    {- no need to care about references as each node
    is preserved during flattening. -}
    in computeDGraphTheories lib_Env l_n fin_dg
      where
       updateDGWithChanges :: LEdge DGLinkLab -> DGraph -> DGraph
       updateDGWithChanges l_edg@( v1, v2, label) d_graph =
        let
        -- update nodes
         lv1 = labDG d_graph v1
         lv2 = labDG d_graph v2
         name = dgn_name lv1
         n_node = getNewNodeDG d_graph
         nlv1 = case computeTheory lib_Env l_n v1 of
           Just n_dgn_theory -> lv1 {dgn_theory = n_dgn_theory }
           Nothing -> cErr "dgFlatRenamings1" v1
         nlv2 = case computeTheory lib_Env l_n v2 of
           Just n_dgn_theory -> lv2 {dgn_theory = n_dgn_theory }
           Nothing -> cErr "dgFlatRenamings2" v2
         n_lnode@(_, n_lv) = propagateErrors "dgFlatRenamings3" $ do
               t_dgn_theory <- translateG_theory (dgl_morphism label)
                               $ dgn_theory nlv1
               return (n_node, newInfoNodeLab name
                                       (newNodeInfo DGFlattening)
                                       t_dgn_theory)
         -- create edge
         sign_source = signOf $ dgn_theory n_lv
         sign_target = signOf $ dgn_theory lv2
         n_edg = do
                   ng_morphism <- ginclusion logicGraph sign_source sign_target
                   return (n_node,
                           v2,
                           label { dgl_morphism = ng_morphism,
                                   dgl_type = globalDef ,
                                   dgl_origin = DGLinkFlatteningRename,
                                   dgl_id = defaultEdgeId })
         change_dg = [SetNodeLab lv1 (v1, nlv1),
                      SetNodeLab lv2 (v2, nlv2),
                      DeleteEdge l_edg,
                      InsertNode n_lnode,
                      InsertEdge (propagateErrors "dgFlatRenamings4" n_edg)]
        in
         changesDGH d_graph change_dg
  
       applyUpdDG :: [LEdge DGLinkLab] -> DGraph -> DGraph
       applyUpdDG l_list d_g = case l_list of
        [] -> d_g
        hd : tl -> let
                  dev_g = updateDGWithChanges hd d_g
                 in applyUpdDG tl $ groupHistory d_g flatRename dev_g
  
  -- this function performs flattening of imports with renamings
  libFlatRenamings :: LibEnv -> Result LibEnv
  libFlatRenamings lib = return $ Map.mapWithKey (dgFlatRenamings lib) lib
  
  -- this function performs flattening of hiding links
  dgFlatHiding :: DGraph -> DGraph
  dgFlatHiding dg = let
     hids = filter (\ (_, _, x) -> (case dgl_type x of
                                           HidingDefLink -> True
                                           _ -> False)) $ labEdgesDG dg
    {- no need to care about references either, as nodes are preserved
    after flattening, as well as references. -}
     n_dg = changesDGH dg $ map DeleteEdge hids
    in groupHistory dg flatHide n_dg
  
  -- this function performs flattening of heterogeniety for the whole library
  libFlatHiding :: LibEnv -> Result LibEnv
  libFlatHiding = fmap (Map.map dgFlatHiding) . normalFormLibEnv
  
  {- this function performs flattening of heterogeniety
  for a given developement graph -}
  dgFlatHeterogen :: LibEnv -> LibName -> DGraph -> DGraph
  dgFlatHeterogen libEnv ln dg = let
    het_comorph = filter
      (\ (_, _, x) -> not $ isHomogeneous $ dgl_morphism x) $ labEdgesDG dg
    het_del_changes = map DeleteEdge het_comorph
    updLib = updateNodes libEnv ln . Set.toList . Set.fromList
      $ map ( \ (_, t, l) -> (t, isDefEdge $ dgl_type l)) het_comorph
    udg = lookupDGraph ln updLib
    ndg = changesDGH udg het_del_changes
    in groupHistory udg flatHet ndg
    where
     updateNodes :: LibEnv -> LibName -> [(Node, Bool)] -> LibEnv
     updateNodes lib_Env l_n nds = case nds of
      [] -> lib_Env
      (hd, isHetDef) : tl -> let
        {- have to consider references here. The global theory is taken as
        local one at the end of the reference chain. -}
        (lname, odg, (nd, labRf)) =
            lookupRefNode lib_Env l_n (lookupDGraph l_n lib_Env) hd
        change = case globalTheory labRf of
          Just ndgn_theory ->
            SetNodeLab labRf (nd, labRf {dgn_theory = ndgn_theory})
          Nothing -> cErr "dgFlatHeterogen" nd
        cdg = changeDGH odg change
        n_dg = groupHistory odg flatHet cdg
       in updateNodes (if isHetDef then Map.insert lname n_dg lib_Env
                      else lib_Env) l_n tl
  
  -- this function performs flattening of heterogeniety for the whole library
  libFlatHeterogen :: LibEnv -> Result LibEnv
  libFlatHeterogen lib =
    return $ Map.mapWithKey (dgFlatHeterogen lib) lib
  
  {- this function performs flattening of non-disjoint unions for the given
  DGraph -}
  dgFlatDUnions :: LibEnv -> LibName -> DGraph -> DGraph
  dgFlatDUnions le ln dg =
   let
    all_nodes = nodesDG dg
    imp_nds = filter (\ x -> length (innDG dg x) > 1) all_nodes
   {- lower_nodes = filter (\ x -> (outDG dg x == [])) (nodesDG dg)
   as previously, no need to care about reference nodes,
   as previous one remain same. -}
   in computeDGraphTheories le ln $ applyToAllNodes dg imp_nds
  
  -- this funciton given a list og G_sign returns intersection of them
  getIntersectionOfAll :: [G_sign] -> G_sign
  getIntersectionOfAll signs =
    case signs of
     [] -> error "getIntersectionOfAll1: empty signatures list"
     [hd] -> hd
     G_sign lid1 extSign1 _ : G_sign lid2 (ExtSign signtr2 _) _ : tl -> let
              n_signtr = propagateErrors "getIntersectionOfAll2" $ do
                 ExtSign sign1 _ <- coerceSign lid1
                                                 lid2
                                                 "getIntersectionOfAll"
                                                 extSign1
                 n_sign <- intersection lid2 sign1 signtr2
                 return $ G_sign lid2 (mkExtSign n_sign) startSigId
             in
              if n_signtr == emptyG_sign (Logic lid2) then n_signtr
              else getIntersectionOfAll (n_signtr : tl)
  
  {- this function given a list of all possible combinations of nodes
  of a given length -}
  getAllCombinations :: Int -> [Node] -> [[Node]]
  getAllCombinations 0 _ = [ [] ]
  getAllCombinations n xs = [ y : ys | y : xs' <- tails xs
                             , ys <- getAllCombinations (n - 1) xs']
  
  -- tells if two lists are equal or one contained in the other
  containedInList :: [Node] -> [Node] -> Bool
  containedInList l1 l2 = all (`elem` l2) l1
  
  -- attach new nodes to the level
  attachNewNodes :: [([Node], G_sign)] -> Int -> [([Node], Node, G_sign)]
  attachNewNodes [] _ = []
  attachNewNodes ((hd, sg) : tl) n = (hd, n, sg) : attachNewNodes tl (n + 1)
  
   -- search for a match for a given combination in a level
  searchForMatch :: [Node] -> [([Node], Node, G_sign)]
                 -> Maybe ([Node], Node, G_sign)
  searchForMatch _ [] = Nothing
  searchForMatch l (tripl@(nds, _, _) : tl) =
    if containedInList l nds then Just tripl else searchForMatch l tl
  
   {- take a combination of nodes, previous level,
   and get the signature for the next level -}
  matchCombinations :: [Node] -> [([Node], Node, G_sign)]
                    -> Maybe ([Node], G_sign)
  matchCombinations [] _ = Nothing
  matchCombinations ([_]) _ = Nothing
  matchCombinations l@(hd1 : hd2 : tl) trpls =
    case searchForMatch (hd1 : tl) trpls of
     Nothing -> Nothing
     Just (_, _, gsig1@(G_sign lid _ _)) ->
       case searchForMatch (hd2 : tl) trpls of
           Nothing -> Nothing
           Just (_, _, gsig2) ->
              let
               n_sig = getIntersectionOfAll [gsig1, gsig2]
              in
               if n_sig == emptyG_sign (Logic lid) then Nothing
               else Just (l, n_sig)
  
   -- for a dg and a level, create labels for the new nodes
  createLabels :: DGraph -> [([Node], Node, G_sign)] -> [LNode DGNodeLab]
  createLabels dg tripls = case tripls of
    [] -> error "createLabels: empty list on input"
    _ -> let
          labels = map (\ (x, y, G_sign lid (ExtSign sign symb) ind) -> let
               -- name intersection by interspersing a string for a SimpleId
               s_id = mkSimpleId . intercalate "'"
                 $ map (`getNameOfNode` dg) x
               n_theory = noSensGTheory lid (ExtSign sign symb) ind
               n_name = makeName $ simpleIdToIRI s_id
               n_info = newNodeInfo DGFlattening
              in
               (y, newInfoNodeLab n_name n_info n_theory)) tripls
         in labels
  
  -- create links connecting given node with a list of nodes
  createLinks :: DGraph -> LNode DGNodeLab -> [Node] -> DGraph
  createLinks dg _ [] = dg
  createLinks dg (nd, lb) (hd : tl) =
    let
     sign_source = signOf (dgn_theory lb)
     sign_target = signOf (dgn_theory $ labDG dg hd)
     n_edg = propagateErrors "DGFlattening.createLinks" $ do
        ng_morphism <- ginclusion logicGraph sign_source sign_target
        return (nd, hd, globDefLink ng_morphism DGLinkFlatteningUnion)
     u_dg = case tryToGetEdge n_edg dg of
              Nothing -> changeDGH dg $ InsertEdge n_edg
              Just _ -> dg
     n_dg = groupHistory dg flatNonDisjUnion u_dg
    in
     createLinks n_dg (nd, lb) tl
  
  {- given an element in the level and a lower link, function searches
  elements in the given level, which are suitable for inserting a link
  connecting given element. -}
  searchForLink :: ([Node], Node, G_sign) -> [([Node], Node, G_sign)] -> [Node]
  searchForLink el@(nds1, _, _) down_level = case down_level of
    [] -> []
    (nds2, nd2, _) : tl -> [ nd2 | containedInList nds2 nds1 ]
                           ++ searchForLink el tl
  
  {- given two levels of the graph, insert links between them, so that the
  signatures are imported properly -}
  linkLevels :: DGraph -> [([Node], Node, G_sign)] -> [([Node], Node, G_sign)]
             -> DGraph
  linkLevels dg up_level down_level = case up_level of
    [] -> dg
    hd@(_, nd, _) : tl -> let
              nds = searchForLink hd down_level
              label = labDG dg nd
              n_dg = createLinks dg (nd, label) nds
             in
              linkLevels n_dg tl down_level
  
  {- given a list of the lower nodes, gives a DGraph with a first level
  of nodes inserted in this graph -}
  createFirstLevel :: DGraph -> [Node] -> (DGraph, [([Node], Node, G_sign)])
  createFirstLevel dg nds =
    let
     combs = getAllCombinations 2 nds
     init_level = map (\ l -> let
                           [x, y] = l
                           signx = signOf $ dgn_theory (labDG dg x)
                           signy = signOf $ dgn_theory (labDG dg y)
                           n_sign = getIntersectionOfAll [signx, signy]
                           in (l, n_sign)) combs
     n_empty = filter (\ (_, sign@(G_sign lid _ _)) ->
                                 sign /= emptyG_sign (Logic lid)) init_level
    in
     case length n_empty of
      0 -> (dg, [])
      _ -> let
            atch_level = attachNewNodes n_empty (getNewNodeDG dg)
            labels = createLabels dg atch_level
            changes = map InsertNode labels
            u_dg = changesDGH dg changes
            n_dg = groupHistory dg flatNonDisjUnion u_dg
            zero_level = map (\ x ->
                          ([x], x, signOf $ dgn_theory (labDG n_dg x))) nds
            lnk_dg = linkLevels n_dg atch_level zero_level
           in
            (lnk_dg, atch_level)
  
  {- given a level of nodes and a graph, constructs upper level,
  inserting the nodes of the new level to the DGraph -}
  createNewLevel :: DGraph -> [Node] -> [([Node], Node, G_sign)]
                 -> (DGraph, [([Node], Node, G_sign)])
  createNewLevel c_dg nds tripls = case tripls of
    [] -> (c_dg, [])
    [_] -> (c_dg, tripls)
    (nd_s, _, _) : _ -> if length nd_s - length nds == 0 then (c_dg, [])
      else let
       combs = getAllCombinations (length nd_s + 1) nds
       n_level = mapMaybe (`matchCombinations` tripls) combs
      in if null n_level then (c_dg, []) else
             let
              atch_level = attachNewNodes n_level (getNewNodeDG c_dg)
              labels = createLabels c_dg atch_level
              chngs = map InsertNode labels
              u_dg = changesDGH c_dg chngs
              n_dg = groupHistory c_dg flatNonDisjUnion u_dg
              lnk_dg = linkLevels n_dg atch_level tripls
             in
              (lnk_dg, atch_level)
  
   {- iterate the procedure for all levels
   (the level passed is already inserted in the graph) -}
  iterateForAllLevels :: DGraph -> [Node] -> [([Node], Node, G_sign)] -> DGraph
  iterateForAllLevels i_dg nds init_level =
    if length init_level < 2 then i_dg else
     let (n_dg, n_level) = createNewLevel i_dg nds init_level
     in if null n_level then n_dg else
           iterateForAllLevels n_dg nds n_level
  
  -- applies itteration for all the nodes in the graph
  applyToAllNodes :: DGraph -> [Node] -> DGraph
  applyToAllNodes a_dg nds = case nds of
   [] -> a_dg
   hd : tl -> let
              inc_nds = map (\ (x, _, _) -> x) (innDG a_dg hd)
              (init_dg, init_level) = createFirstLevel a_dg inc_nds
              final_dg = iterateForAllLevels init_dg inc_nds init_level
             in
              applyToAllNodes final_dg tl
  {- given a lower level of nodes, gives upper level of nodes,
  which are ingoing nodes for the lower level -}
  filterIngoing :: DGraph -> [Node] -> [Node]
  filterIngoing dg nds = case nds of
    [] -> []
    hd : tl -> let ind = map (\ (x, _, _) -> x) (innDG dg hd) in
               ind ++ filterIngoing dg (ind ++ tl)
  
  {- this function takes a node and performs flattening
  of non-disjoint unions for the ingoing tree of nodes to the given node -}
  singleTreeFlatDUnions :: LibEnv -> LibName -> Node -> Result LibEnv
  singleTreeFlatDUnions libEnv libName nd = let
    dg = lookupDGraph libName libEnv
    in_nds = filterIngoing dg [nd]
    n_dg = applyToAllNodes dg in_nds
    in return $ Map.insert libName n_dg libEnv
  
  {- this functions performs flattening of
  non-disjoint unions for the whole library -}
  libFlatDUnions :: LibEnv -> Result LibEnv
  libFlatDUnions le = return $ Map.mapWithKey (\ln dg -> dgFlatDUnions le ln dg) le
  