{- |
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 -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
compositionCreatingEdgesFromList libname :: LibName
libname ls :: [LEdge DGLinkLab]
ls proofStatus :: LibEnv
proofStatus =
      let dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
libname LibEnv
proofStatus
          pathsToCompose :: [[LEdge DGLinkLab]]
pathsToCompose = ([LEdge DGLinkLab] -> Bool)
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1) (Int -> Bool)
-> ([LEdge DGLinkLab] -> Int) -> [LEdge DGLinkLab] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LEdge DGLinkLab] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) ([[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]])
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> a -> b
$
              DGraph
-> (DGLinkType -> Bool) -> [LEdge DGLinkLab] -> [[LEdge DGLinkLab]]
getAllPathsOfTypeFromGoalList DGraph
dgraph DGLinkType -> Bool
isGlobalThm [LEdge DGLinkLab]
ls
          newDGraph :: DGraph
newDGraph = DGraph -> [[LEdge DGLinkLab]] -> DGraph
compositionCreatingEdgesAux DGraph
dgraph [[LEdge DGLinkLab]]
pathsToCompose
      in LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
libname DGraph
newDGraph LibEnv
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 -> LibEnv -> LibEnv
compositionCreatingEdges libname :: LibName
libname proofStatus :: LibEnv
proofStatus =
    let dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
libname LibEnv
proofStatus
        allEdges :: [LEdge DGLinkLab]
allEdges = DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dgraph
    in LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
compositionCreatingEdgesFromList LibName
libname [LEdge DGLinkLab]
allEdges LibEnv
proofStatus

-- auxiliary method for compositionCreatingEdges
compositionCreatingEdgesAux :: DGraph -> [[LEdge DGLinkLab]] -> DGraph
compositionCreatingEdgesAux :: DGraph -> [[LEdge DGLinkLab]] -> DGraph
compositionCreatingEdgesAux dgraph :: DGraph
dgraph [] = DGraph
dgraph
compositionCreatingEdgesAux dgraph :: DGraph
dgraph (path :: [LEdge DGLinkLab]
path : paths :: [[LEdge DGLinkLab]]
paths) =
 case [LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath [LEdge DGLinkLab]
path of
   Nothing -> DGraph -> [[LEdge DGLinkLab]] -> DGraph
compositionCreatingEdgesAux DGraph
dgraph [[LEdge DGLinkLab]]
paths
   Just _ -> let
    (src :: Int
src, _, _) = [LEdge DGLinkLab] -> LEdge DGLinkLab
forall a. [a] -> a
head [LEdge DGLinkLab]
path
    (_, tgt :: Int
tgt, _) = [LEdge DGLinkLab] -> LEdge DGLinkLab
forall a. [a] -> a
last [LEdge DGLinkLab]
path
    Just morph :: GMorphism
morph = [LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath [LEdge DGLinkLab]
path
    cons :: Conservativity
cons = case [LEdge DGLinkLab] -> Conservativity
getConservativityOfPath [LEdge DGLinkLab]
path of
             Mono -> if GMorphism -> Bool
isTransportable GMorphism
morph then Conservativity
Mono else Conservativity
Cons
             c :: Conservativity
c -> Conservativity
c
    es :: [EdgeId]
es = (LEdge DGLinkLab -> EdgeId) -> [LEdge DGLinkLab] -> [EdgeId]
forall a b. (a -> b) -> [a] -> [b]
map LEdge DGLinkLab -> EdgeId
getEdgeId [LEdge DGLinkLab]
path
    rl :: DGRule
rl = [EdgeId] -> DGRule
Composition [EdgeId]
es
    newEdge :: LEdge DGLinkLab
newEdge = (Int
src, Int
tgt, GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink GMorphism
morph
      (Scope -> LinkKind -> ConsStatus -> DGLinkType
ScopedLink Scope
Global
          (ThmLinkStatus -> LinkKind
ThmLink (DGRule -> ProofBasis -> ThmLinkStatus
Proven DGRule
rl
                   (ProofBasis -> ThmLinkStatus) -> ProofBasis -> ThmLinkStatus
forall a b. (a -> b) -> a -> b
$ (ProofBasis -> EdgeId -> ProofBasis)
-> ProofBasis -> [EdgeId] -> ProofBasis
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ProofBasis -> EdgeId -> ProofBasis
addEdgeId ProofBasis
emptyProofBasis [EdgeId]
es))
          (ConsStatus -> DGLinkType) -> ConsStatus -> DGLinkType
forall a b. (a -> b) -> a -> b
$ Conservativity -> Conservativity -> ThmLinkStatus -> ConsStatus
ConsStatus Conservativity
cons Conservativity
None ThmLinkStatus
LeftOpen)
      DGLinkOrigin
DGLinkProof)
    newDGraph :: DGraph
newDGraph = LEdge DGLinkLab -> DGraph -> DGraph
insertDGLEdge LEdge DGLinkLab
newEdge DGraph
dgraph
    newDGraph2 :: DGraph
newDGraph2 = DGraph -> LEdge DGLinkLab -> DGraph
deleteRedundantEdges DGraph
newDGraph LEdge DGLinkLab
newEdge
    in DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dgraph DGRule
rl DGraph
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 -> LEdge DGLinkLab -> DGraph
deleteRedundantEdges dgraph :: DGraph
dgraph (src :: Int
src, tgt :: Int
tgt, labl :: DGLinkLab
labl) = let
    redundantEdges :: [LEdge DGLinkLab]
redundantEdges =
      [ (Int
src, Int
tgt, DGLinkLab
l) | DGLinkLab
l <- Int -> Int -> Gr DGNodeLab DGLinkLab -> [DGLinkLab]
forall a b. Int -> Int -> Gr a b -> [b]
Tree.getLEdges Int
src Int
tgt (Gr DGNodeLab DGLinkLab -> [DGLinkLab])
-> Gr DGNodeLab DGLinkLab -> [DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dgraph
      , DGLinkType -> Bool
isUnprovenGlobalThm (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l
      , DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
l GMorphism -> GMorphism -> Bool
forall a. Eq a => a -> a -> Bool
== DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
labl
      , DGLinkLab -> DGLinkLab -> Bool
haveSameCons DGLinkLab
l DGLinkLab
labl ]
    haveSameCons :: DGLinkLab -> DGLinkLab -> Bool
    haveSameCons :: DGLinkLab -> DGLinkLab -> Bool
haveSameCons lab1 :: DGLinkLab
lab1 lab2 :: DGLinkLab
lab2 = case (DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lab1, DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lab2) of
          (ScopedLink Global (ThmLink LeftOpen) (ConsStatus cons1 :: Conservativity
cons1 _ status1 :: ThmLinkStatus
status1),
           ScopedLink Global (ThmLink _) (ConsStatus cons2 :: Conservativity
cons2 _ status2 :: ThmLinkStatus
status2)) ->
             Conservativity
cons1 Conservativity -> Conservativity -> Bool
forall a. Eq a => a -> a -> Bool
== Conservativity
cons2 Bool -> Bool -> Bool
&&
             ThmLinkStatus -> Bool
isProvenThmLinkStatus ThmLinkStatus
status1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== ThmLinkStatus -> Bool
isProvenThmLinkStatus ThmLinkStatus
status2
          _ -> Bool
False
   in (DGraph -> LEdge DGLinkLab -> DGraph)
-> DGraph -> [LEdge DGLinkLab] -> DGraph
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DGraph -> LEdge DGLinkLab -> DGraph
deleteRedundantEdgesAux DGraph
dgraph [LEdge DGLinkLab]
redundantEdges

-- auxiliary method for deleteRedundantEdgesAux
deleteRedundantEdgesAux :: DGraph -> LEdge DGLinkLab -> DGraph
deleteRedundantEdgesAux :: DGraph -> LEdge DGLinkLab -> DGraph
deleteRedundantEdgesAux dgraph :: DGraph
dgraph = DGraph -> DGChange -> DGraph
changeDGH DGraph
dgraph (DGChange -> DGraph)
-> (LEdge DGLinkLab -> DGChange) -> LEdge DGLinkLab -> DGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LEdge DGLinkLab -> DGChange
DeleteEdge

-- | composition without creating new new edges
compositionFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
compositionFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
compositionFromList libname :: LibName
libname glbThmEdge :: [LEdge DGLinkLab]
glbThmEdge proofStatus :: LibEnv
proofStatus = let
    dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
libname LibEnv
proofStatus
    newDGraph :: DGraph
newDGraph = (DGraph -> LEdge DGLinkLab -> DGraph)
-> DGraph -> [LEdge DGLinkLab] -> DGraph
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DGraph -> LEdge DGLinkLab -> DGraph
compositionAux DGraph
dgraph
      ([LEdge DGLinkLab] -> DGraph) -> [LEdge DGLinkLab] -> DGraph
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
isGlobalThm) [LEdge DGLinkLab]
glbThmEdge
  in LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
libname DGraph
newDGraph LibEnv
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 -> LibEnv -> LibEnv
composition libname :: LibName
libname proofStatus :: LibEnv
proofStatus =
  let dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
libname LibEnv
proofStatus
      globalThmEdges :: [LEdge DGLinkLab]
globalThmEdges = DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dgraph
  in LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
compositionFromList LibName
libname [LEdge DGLinkLab]
globalThmEdges LibEnv
proofStatus

-- | auxiliary method for composition
compositionAux :: DGraph -> LEdge DGLinkLab -> DGraph
compositionAux :: DGraph -> LEdge DGLinkLab -> DGraph
compositionAux dgraph :: DGraph
dgraph edge :: LEdge DGLinkLab
edge =
  case DGraph
-> LEdge DGLinkLab -> Maybe (LEdge DGLinkLab, [LEdge DGLinkLab])
compositionForOneEdge DGraph
dgraph LEdge DGLinkLab
edge of
    Nothing -> DGraph
dgraph
    Just (newEdge :: LEdge DGLinkLab
newEdge, proofbasis :: [LEdge DGLinkLab]
proofbasis) -> let
      newDGraph :: DGraph
newDGraph = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dgraph [LEdge DGLinkLab -> DGChange
DeleteEdge LEdge DGLinkLab
edge, LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
newEdge]
      in DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dgraph ([EdgeId] -> DGRule
Composition ([EdgeId] -> DGRule) -> [EdgeId] -> DGRule
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> EdgeId) -> [LEdge DGLinkLab] -> [EdgeId]
forall a b. (a -> b) -> [a] -> [b]
map LEdge DGLinkLab -> EdgeId
getEdgeId [LEdge DGLinkLab]
proofbasis) DGraph
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
-> LEdge DGLinkLab -> Maybe (LEdge DGLinkLab, [LEdge DGLinkLab])
compositionForOneEdge dgraph :: DGraph
dgraph edge :: LEdge DGLinkLab
edge@(src :: Int
src, tgt :: Int
tgt, labl :: DGLinkLab
labl) =
  LEdge DGLinkLab
-> [[LEdge DGLinkLab]]
-> Maybe (LEdge DGLinkLab, [LEdge DGLinkLab])
compositionForOneEdgeAux LEdge DGLinkLab
edge [[LEdge DGLinkLab]
path | [LEdge DGLinkLab]
path <- [[LEdge DGLinkLab]]
pathsOfMorphism,
                                 LEdge DGLinkLab -> [LEdge DGLinkLab] -> Bool
noPath LEdge DGLinkLab
edge [LEdge DGLinkLab]
path]
  where
    globThmPaths :: [[LEdge DGLinkLab]]
globThmPaths = DGraph -> (DGLinkType -> Bool) -> Int -> Int -> [[LEdge DGLinkLab]]
getAllPathsOfTypeBetween DGraph
dgraph DGLinkType -> Bool
isGlobalThm Int
src Int
tgt
    pathsOfMorphism :: [[LEdge DGLinkLab]]
pathsOfMorphism = GMorphism -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
filterPathsByMorphism (DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
labl) [[LEdge DGLinkLab]]
globThmPaths

-- auxiliary method for compositionForOneEdge
compositionForOneEdgeAux :: LEdge DGLinkLab -> [[LEdge DGLinkLab]]
                         -> Maybe (LEdge DGLinkLab, [LEdge DGLinkLab])
compositionForOneEdgeAux :: LEdge DGLinkLab
-> [[LEdge DGLinkLab]]
-> Maybe (LEdge DGLinkLab, [LEdge DGLinkLab])
compositionForOneEdgeAux _ [] = Maybe (LEdge DGLinkLab, [LEdge DGLinkLab])
forall a. Maybe a
Nothing
compositionForOneEdgeAux edge :: LEdge DGLinkLab
edge@(src :: Int
src, tgt :: Int
tgt, labl :: DGLinkLab
labl) (path :: [LEdge DGLinkLab]
path : paths :: [[LEdge DGLinkLab]]
paths)
  | Conservativity
cons Conservativity -> Conservativity -> Bool
forall a. Ord a => a -> a -> Bool
<= Conservativity
pathCons = if Conservativity
cons Conservativity -> Conservativity -> Bool
forall a. Eq a => a -> a -> Bool
== Conservativity
Mono
                        then LEdge DGLinkLab
-> [LEdge DGLinkLab] -> Maybe (LEdge DGLinkLab, [LEdge DGLinkLab])
handleConservativityMono LEdge DGLinkLab
newEdge [LEdge DGLinkLab]
path
                         else (LEdge DGLinkLab, [LEdge DGLinkLab])
-> Maybe (LEdge DGLinkLab, [LEdge DGLinkLab])
forall a. a -> Maybe a
Just (LEdge DGLinkLab
newEdge, [LEdge DGLinkLab]
path)
  | Bool
otherwise = LEdge DGLinkLab
-> [[LEdge DGLinkLab]]
-> Maybe (LEdge DGLinkLab, [LEdge DGLinkLab])
compositionForOneEdgeAux LEdge DGLinkLab
edge [[LEdge DGLinkLab]]
paths
  where
    cons :: Conservativity
cons = LEdge DGLinkLab -> Conservativity
getConservativity LEdge DGLinkLab
edge
    pathCons :: Conservativity
pathCons = [LEdge DGLinkLab] -> Conservativity
getConservativityOfPath [LEdge DGLinkLab]
path
    es :: [EdgeId]
es = (LEdge DGLinkLab -> EdgeId) -> [LEdge DGLinkLab] -> [EdgeId]
forall a b. (a -> b) -> [a] -> [b]
map LEdge DGLinkLab -> EdgeId
getEdgeId [LEdge DGLinkLab]
path
    newEdge :: LEdge DGLinkLab
newEdge = (Int
src, Int
tgt, DGLinkLab
labl
      { dgl_type :: DGLinkType
dgl_type = ThmLinkStatus -> DGLinkType -> DGLinkType
setProof (DGRule -> ProofBasis -> ThmLinkStatus
Proven ([EdgeId] -> DGRule
Composition [EdgeId]
es)
          (ProofBasis -> ThmLinkStatus) -> ProofBasis -> ThmLinkStatus
forall a b. (a -> b) -> a -> b
$ (ProofBasis -> EdgeId -> ProofBasis)
-> ProofBasis -> [EdgeId] -> ProofBasis
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ProofBasis -> EdgeId -> ProofBasis
addEdgeId ProofBasis
emptyProofBasis [EdgeId]
es)
          (DGLinkType -> DGLinkType) -> DGLinkType -> DGLinkType
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
labl
      , dgl_origin :: DGLinkOrigin
dgl_origin = DGLinkOrigin
DGLinkProof
      , dgl_id :: EdgeId
dgl_id = EdgeId
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 :: LEdge DGLinkLab
-> [LEdge DGLinkLab] -> Maybe (LEdge DGLinkLab, [LEdge DGLinkLab])
handleConservativityMono newEdge :: LEdge DGLinkLab
newEdge path :: [LEdge DGLinkLab]
path =
  case [LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath [LEdge DGLinkLab]
path of
    Nothing -> Maybe (LEdge DGLinkLab, [LEdge DGLinkLab])
forall a. Maybe a
Nothing
    Just morph :: GMorphism
morph -> if GMorphism -> Bool
isTransportable GMorphism
morph then (LEdge DGLinkLab, [LEdge DGLinkLab])
-> Maybe (LEdge DGLinkLab, [LEdge DGLinkLab])
forall a. a -> Maybe a
Just (LEdge DGLinkLab
newEdge, [LEdge DGLinkLab]
path)
                   else Maybe (LEdge DGLinkLab, [LEdge DGLinkLab])
forall a. Maybe a
Nothing