content: {- |
  Module      :  ./Proofs/Composition.hs
  Description :  Composition rules in the development graphs calculus
  Copyright   :  (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable(Logic)
  
  Composition rules in the development graphs calculus.
    Follows Sect. IV:4.4 of the CASL Reference Manual, while combining
    several rules into one.
  -}
  
  module Proofs.Composition
      ( composition
      , compositionCreatingEdges
      , compositionFromList
      , compositionCreatingEdgesFromList
      ) where
  
  import Proofs.EdgeUtils
  
  import Static.DevGraph
  import Static.DgUtils
  import Static.History
  
  import Logic.Grothendieck
  
  import Common.Consistency
  import Common.LibName
  import qualified Common.Lib.Graph as Tree
  
  import qualified Data.Map as Map
  import Data.Graph.Inductive.Graph
  
  compositionCreatingEdgesFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv
                                   -> LibEnv
  compositionCreatingEdgesFromList libname ls proofStatus =
        let dgraph = lookupDGraph libname proofStatus
            pathsToCompose = filter ((> 1) . length) $
                getAllPathsOfTypeFromGoalList dgraph isGlobalThm ls
            newDGraph = compositionCreatingEdgesAux dgraph pathsToCompose
        in Map.insert libname newDGraph proofStatus
  
  {- | creates new edges by composing all paths of global theorem edges
     in the current development graph. These new edges are proven global
     theorems with the morphism and the conservativity of the corresponding
     path. If a new edge is the proven version of a previsously existing
     edge, that edge is deleted. -}
  compositionCreatingEdges :: LibName -> LibEnv -> LibEnv
  compositionCreatingEdges libname proofStatus =
      let dgraph = lookupDGraph libname proofStatus
          allEdges = labEdgesDG dgraph
      in compositionCreatingEdgesFromList libname allEdges proofStatus
  
  -- auxiliary method for compositionCreatingEdges
  compositionCreatingEdgesAux :: DGraph -> [[LEdge DGLinkLab]] -> DGraph
  compositionCreatingEdgesAux dgraph [] = dgraph
  compositionCreatingEdgesAux dgraph (path : paths) =
   case calculateMorphismOfPath path of
     Nothing -> compositionCreatingEdgesAux dgraph paths
     Just _ -> let
      (src, _, _) = head path
      (_, tgt, _) = last path
      Just morph = calculateMorphismOfPath path
      cons = case getConservativityOfPath path of
               Mono -> if isTransportable morph then Mono else Cons
               c -> c
      es = map getEdgeId path
      rl = Composition es
      newEdge = (src, tgt, defDGLink morph
        (ScopedLink Global
            (ThmLink (Proven rl
                     $ foldl addEdgeId emptyProofBasis es))
            $ ConsStatus cons None LeftOpen)
        DGLinkProof)
      newDGraph = insertDGLEdge newEdge dgraph
      newDGraph2 = deleteRedundantEdges newDGraph newEdge
      in groupHistory dgraph rl newDGraph2
  
  {- | this method is used by compositionCreatingEdgesAux.  It selects
  all unproven global theorem edges in the given development graph that
  have the same source, target, morphism and conservativity as the given
  one. It then deletes them from the given graph and adds a
  corresponding change -}
  deleteRedundantEdges :: DGraph -> LEdge DGLinkLab -> DGraph
  deleteRedundantEdges dgraph (src, tgt, labl) = let
      redundantEdges =
        [ (src, tgt, l) | l <- Tree.getLEdges src tgt $ dgBody dgraph
        , isUnprovenGlobalThm $ dgl_type l
        , dgl_morphism l == dgl_morphism labl
        , haveSameCons l labl ]
      haveSameCons :: DGLinkLab -> DGLinkLab -> Bool
      haveSameCons lab1 lab2 = case (dgl_type lab1, dgl_type lab2) of
            (ScopedLink Global (ThmLink LeftOpen) (ConsStatus cons1 _ status1),
             ScopedLink Global (ThmLink _) (ConsStatus cons2 _ status2)) ->
               cons1 == cons2 &&
               isProvenThmLinkStatus status1 == isProvenThmLinkStatus status2
            _ -> False
     in foldl deleteRedundantEdgesAux dgraph redundantEdges
  
  -- auxiliary method for deleteRedundantEdgesAux
  deleteRedundantEdgesAux :: DGraph -> LEdge DGLinkLab -> DGraph
  deleteRedundantEdgesAux dgraph = changeDGH dgraph . DeleteEdge
  
  -- | composition without creating new new edges
  compositionFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
  compositionFromList libname glbThmEdge proofStatus = let
      dgraph = lookupDGraph libname proofStatus
      newDGraph = foldl compositionAux dgraph
        $ filter (liftE isGlobalThm) glbThmEdge
    in Map.insert libname newDGraph proofStatus
  
  {- | gets all unproven global theorem edges in the current development graph
     and checks, if they are a composition of a global theorem path. If so,
     the edge is proven, with the corresponding path as its proof basis.
     If there is more than one path, the first of them is arbitrarily taken. -}
  composition :: LibName -> LibEnv -> LibEnv
  composition libname proofStatus =
    let dgraph = lookupDGraph libname proofStatus
        globalThmEdges = labEdgesDG dgraph
    in compositionFromList libname globalThmEdges proofStatus
  
  -- | auxiliary method for composition
  compositionAux :: DGraph -> LEdge DGLinkLab -> DGraph
  compositionAux dgraph edge =
    case compositionForOneEdge dgraph edge of
      Nothing -> dgraph
      Just (newEdge, proofbasis) -> let
        newDGraph = changesDGH dgraph [DeleteEdge edge, InsertEdge newEdge]
        in groupHistory dgraph (Composition $ map getEdgeId proofbasis) newDGraph
  
  {- | checks for the given edges, if there is a path in the given
  development graph that it is a composition of. If so, it is replaced
  by a proven version with the path as its proof basis.  The method
  returns Nothing if there is no such path or else the new edge and the
  path. -}
  compositionForOneEdge :: DGraph -> LEdge DGLinkLab
                        -> Maybe (LEdge DGLinkLab, [LEdge DGLinkLab])
  compositionForOneEdge dgraph edge@(src, tgt, labl) =
    compositionForOneEdgeAux edge [path | path <- pathsOfMorphism,
                                   noPath edge path]
    where
      globThmPaths = getAllPathsOfTypeBetween dgraph isGlobalThm src tgt
      pathsOfMorphism = filterPathsByMorphism (dgl_morphism labl) globThmPaths
  
  -- auxiliary method for compositionForOneEdge
  compositionForOneEdgeAux :: LEdge DGLinkLab -> [[LEdge DGLinkLab]]
                           -> Maybe (LEdge DGLinkLab, [LEdge DGLinkLab])
  compositionForOneEdgeAux _ [] = Nothing
  compositionForOneEdgeAux edge@(src, tgt, labl) (path : paths)
    | cons <= pathCons = if cons == Mono
                          then handleConservativityMono newEdge path
                           else Just (newEdge, path)
    | otherwise = compositionForOneEdgeAux edge paths
    where
      cons = getConservativity edge
      pathCons = getConservativityOfPath path
      es = map getEdgeId path
      newEdge = (src, tgt, labl
        { dgl_type = setProof (Proven (Composition es)
            $ foldl addEdgeId emptyProofBasis es)
            $ dgl_type labl
        , dgl_origin = DGLinkProof
        , dgl_id = defaultEdgeId })
  
  {- | checks if the morphism of the given path is transportable. This
  is necessary for the composition of a path, if its conservativity is
  Mono.  This method is used by compositionForOneEdgeAux to check, if a
  composition in case of conservativity Mono is possible. -}
  handleConservativityMono :: LEdge DGLinkLab -> [LEdge DGLinkLab]
                           -> Maybe (LEdge DGLinkLab, [LEdge DGLinkLab])
  handleConservativityMono newEdge path =
    case calculateMorphismOfPath path of
      Nothing -> Nothing
      Just morph -> if isTransportable morph then Just (newEdge, path)
                     else Nothing
  