content: {- |
  Module      :  ./Proofs/Conservativity.hs
  Description :  conservativity proof rule for development graphs
  Copyright   :  (c) Markus Gross, DFKI 2009
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  mgross@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  non-portable(Logic)
  
  conservativity proof rule for development graphs
     Follows Sect. IV:4.4.2 of the CASL Reference Manual.
  -}
  
  module Proofs.Conservativity (conservativity) where
  
  import Common.Amalgamate (Amalgamates (Amalgamates), CASLAmalgOpt (..))
  import Common.Consistency
  import Common.LibName (LibName)
  import Common.Result (resultToMaybe)
  import Common.Utils (nubOrdOn)
  
  import Proofs.EdgeUtils (getAllPathsOfTypeFrom)
  import Proofs.ComputeColimit (makeDiagram)
  
  import Static.DevGraph
  import Static.DgUtils
  import Static.GTheory (gEnsuresAmalgamability)
  import Static.History
  
  import Data.Graph.Inductive.Graph (LEdge, LNode)
  import qualified Data.Map as Map
  
  -- * Conservativity rules
  
  {- A pair is defined as:
  
  (e1, e2)
  
  n ---- e2 ----> n
  |
  |
  e1
  |
  |
  v
  n
  
  -}
  type Pair = (LEdge DGLinkLab, LEdge DGLinkLab)
  
  {- A quad is defined as:
  
  ((e1, e2), (e3, e4))
  
  n ---- e2 ----> n
  |               |
  |               |
  e1              e4
  |               |
  |               |
  v               v
  n ---- e3 ----> n
  
  -}
  type Quad = (Pair, Pair)
  
  -- Main function, calls all rules.
  conservativity :: LibName -> LibEnv -> LibEnv
  conservativity = Map.adjust (shift . freeIsMono . monoIsFree . compCons)
  
  {- Shift-Rule.
  First a list of edge pairs with the same source node is generated.
  Then all pairs are positioned correctly. All pairs which have
  one edge with a cons value are kept.
  A list of quads (pair, pair) is generated. Each input pair is combined with
  another pair, which has the same target and where the edges have the same
  source nodes. (See type Quad for a picture.)
  The target node of the quads must be isolated and the quad has to be
  amalgamable.
  Afterwards the quad is positioned correctly and the edges are updated. -}
  shift :: DGraph -> DGraph
  shift dg = groupHistory dg (DGRule "conservativityShift") $
             changesDGH dg changes
    where
      edgs = filter (liftE isGlobalEdge) $ labEdgesDG dg
      globThmEdges = filter (liftE isGlobalThm) edgs
      consEdgs = [ e | e <- globThmEdges, getConservativity e > None ]
      pairs1 = nubOrdOn pairInd
        [ (e1, e2)
        | e1@(s1, t1, _) <- consEdgs
        , e2@(s2, t2, _) <- globThmEdges
        , s1 == s2, t1 /= s1, t2 /= s2, not (eqDGLEdge e1 e2) ]
      pairs2 = nubOrdOn pairInd
        [ (e3, e4)
        | e3@(_, t3, _) <- edgs
        , e4@(_, t4, _) <- edgs
        , t3 == t4, not (eqDGLEdge e3 e4) ]
      quads = filter (isAmalgamable dg) $
              filter (isolated edgs . snd) $ map posQuad
        [ ((e1, e2), (e3, e4))
        | (e1@(_, t1, _), e2@(_, t2, _)) <- pairs1
        , (e3@(s3, _, _), e4@(s4, _, _)) <- pairs2
        , t1 == s3 && t2 == s4 || t1 == s4 && t2 == s3 ]
      changes = concatMap process quads
      {- Updates the e4 edge with the cons value from the e1 edge.
      The quads have to be positioned correctly before using this function. -}
      process :: Quad -> [DGChange]
      process ((e1, _), (_, e4)) =
        let cons = getConservativity e1
         in genEdgeChange
              (\ (ConsStatus co pc tl) -> ConsStatus (max cons co) pc tl) e4
  
  -- Checks if a quad is amalgamable.
  isAmalgamable :: DGraph -> Quad -> Bool
  isAmalgamable dg ((e1@(s1, _, _), e2), (e3@(s3, _, l3), e4@(s4, t4, l4))) =
    case resultToMaybe amal of
      Just Amalgamates -> True
      _ -> False
    where
      sink = [(s3, dgl_morphism l3), (s4, dgl_morphism l4)]
      diag = makeDiagram dg [s1, s3, s4, t4] [e1, e2, e3, e4]
      amal = gEnsuresAmalgamability [ColimitThinness, Cell] diag sink
  
  -- | Checks whether a pair is duplicate (disregarding pair order).
  pairInd :: Pair -> ((Int, Int, EdgeId), (Int, Int, EdgeId))
  pairInd ((s1, t1, l1), (s2, t2, l2)) =
    let e1 = (s1, t1, dgl_id l1)
        e2 = (s2, t2, dgl_id l2)
    in if e1 < e2 then (e1, e2) else (e2, e1)
  
  eqDGLEdge :: LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
  eqDGLEdge (s1, t1, l1) (s2, t2, l2) = (s1, t1) == (s2, t2)
    && eqDGLinkLabById l1 l2
  
  {- Positions a quad so that the e4 edge is the one whose source node is the
  target node of e2. Also checks if the e4 has no conservativity value. -}
  posQuad :: Quad -> Quad
  posQuad q@((e1@(_, t1, _), e2@(_, t2, _)), (e3@(s3, _, _), e4))
    | s3 == t1 = q
    | s3 == t2 = ((e1, e2), (e4, e3))
    | otherwise = error "Proofs.Conservativity.posQuad"
  
  {- Checks wether the node of the pair is isolated.
  Both edges of the pair have the same target node. -}
  isolated :: [LEdge DGLinkLab] -> Pair -> Bool
  isolated edgs (e1@(_, t1, _), e2) =
    not $ any (\ x@(_, t, _) -> t == t1 && not (eqDGLEdge x e1)
               && not (eqDGLEdge x e2)) $ filter (liftE isGlobalDef) edgs
  
  {- First get all free links in the graph. Then all cons links.
  When the free and cons link point to the same node, the cons link is upgraded
  to mono. -}
  freeIsMono :: DGraph -> DGraph
  freeIsMono dg = groupHistory dg (DGRule "freeIsMono") $ changesDGH dg changes
    where
      edgs = labEdgesDG dg
      free = filter (liftE isFreeEdge) edgs
      cons = [ e | e <- edgs, liftE isGlobalThm e, getConservativity e == Cons ]
      mono = nubOrdOn (\ (s, t, l) -> (s, t, dgl_id l))
             [ c | c@(_, ct, _) <- cons, (_, ft, _) <- free, ct == ft ]
      changes = concatMap (genEdgeChange
                          (\ (ConsStatus _ pc tl) -> ConsStatus Mono pc tl)) mono
  
  -- Generates a list of changes for the development graph.
  genEdgeChange :: (ConsStatus -> ConsStatus) -> LEdge DGLinkLab -> [DGChange]
  genEdgeChange f e = [ DeleteEdge e, InsertEdge $ modifyEdgeCons e f ]
  
  -- Modifies the ConsStatus of an edge.
  modifyEdgeCons :: LEdge DGLinkLab
    -> (ConsStatus -> ConsStatus) -> LEdge DGLinkLab
  modifyEdgeCons (s, t, l) f =
    (s, t, l {
       dgl_type = case dgl_type l of
                  ScopedLink sc dl cs -> ScopedLink sc dl $ f cs
                  tp -> tp
     , dgl_origin = DGLinkProof
     , dgl_id = defaultEdgeId
    })
  
  monoIsFree :: DGraph -> DGraph
  monoIsFree dg = groupHistory dg (DGRule "monoIsFree") $ changesDGH dg changes
    where
      mono = filter (\ n -> getNodeConservativity n == Mono) $ labNodesDG dg
      thmEdges = filter (\ e -> getConservativity e == None) $
                 filter (liftE isGlobalThm) $ labEdgesDG dg
      freeEdges = [ e | (n, _) <- mono, e@(s, _, _) <- thmEdges, n == s ]
      changes = concatMap process freeEdges
      process :: LEdge DGLinkLab -> [DGChange]
      process e@(s, t, l) = [ DeleteEdge e, InsertEdge (s, t, l {
          dgl_type = case dgl_type l of
                     ScopedLink _ _ (ConsStatus _ _ ls) -> HidingFreeOrCofreeThm
                                                           (Just Free) s
                                                           (dgl_morphism l) ls
                     tp -> tp
        })]
  
  -- If Node n is cons and the path to Node m is also cons then m is cons too.
  compCons :: DGraph -> DGraph
  compCons dg = groupHistory dg (DGRule "compCons") $ changesDGH dg changes
    where
      consNodes = filter (\ n -> getNodeConservativity n /= None) $ labNodesDG dg
      changes = concatMap (compConsAux dg) consNodes
  
  {- First get all paths. Check if the path cons matches with the node cons.
  If the target node cons is weaker than the path cons replace it. -}
  compConsAux :: DGraph -> LNode DGNodeLab -> [DGChange]
  compConsAux dg n@(i, _) = changes
    where
      nodeCons = getNodeConservativity n
      nodePaths = getAllPathsOfTypeFrom dg i
      consPaths = filter (\ p -> snd p == nodeCons) $ zip nodePaths
                  (map getConservativityOfPath nodePaths)
      changes = concatMap process consPaths
      process :: ([LEdge DGLinkLab], Conservativity) -> [DGChange]
      process (path, sourceCons) =
        [ SetNodeLab lab (node, lab') | targetNodeCons < sourceCons ]
        where
          (_, node, _) = last path
          lab = labDG dg node
          targetNodeCons = getNodeCons lab
          nInfo = nodeInfo lab
          lab' = lab {
              nodeInfo = nInfo { node_cons_status = mkConsStatus sourceCons }
            }
  