hets/Proofs/Composition.hs

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