{- |
Module      :  ./Proofs/EdgeUtils.hs
Description :  utility functions for edges of development graphs
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)

utility functions for edges of development graphs
-}

module Proofs.EdgeUtils where

import Logic.Grothendieck
import Logic.Logic

import Static.DevGraph
import Static.DgUtils
import Static.History

import Common.Consistency
import Common.Result
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.Graph as Tree

import Data.Graph.Inductive.Graph
import Data.Graph.Inductive.Basic (elfilter)
import Data.List
import Data.Maybe (isNothing)
import qualified Data.Set as Set
import qualified Data.Map as Map
import Control.Exception (assert)
import qualified Control.Monad.Fail as Fail

-- * other methods on edges

eqLEdge :: (DGLinkLab -> DGLinkLab -> Bool) -> LEdge DGLinkLab
        -> LEdge DGLinkLab -> Bool
eqLEdge :: (DGLinkLab -> DGLinkLab -> Bool)
-> LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
eqLEdge f :: DGLinkLab -> DGLinkLab -> Bool
f (v :: Node
v, w :: Node
w, l :: DGLinkLab
l) (v2 :: Node
v2, w2 :: Node
w2, l2 :: DGLinkLab
l2) = Node
v Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
v2 Bool -> Bool -> Bool
&& Node
w Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
w2 Bool -> Bool -> Bool
&& DGLinkLab -> DGLinkLab -> Bool
f DGLinkLab
l DGLinkLab
l2

noPath :: LEdge DGLinkLab -> [LEdge DGLinkLab] -> Bool
noPath :: LEdge DGLinkLab -> [LEdge DGLinkLab] -> Bool
noPath e :: LEdge DGLinkLab
e l :: [LEdge DGLinkLab]
l = case [LEdge DGLinkLab]
l of
    [e2 :: LEdge DGLinkLab
e2] -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (DGLinkLab -> DGLinkLab -> Bool)
-> LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
eqLEdge DGLinkLab -> DGLinkLab -> Bool
eqDGLinkLabById LEdge DGLinkLab
e LEdge DGLinkLab
e2
    _ -> Bool
True

{- | try to get the given edge from the given DGraph or the given list of
     DGChange to advoid duplicate inserting of an edge. -}
tryToGetEdge :: LEdge DGLinkLab -> DGraph -> Maybe (LEdge DGLinkLab)
tryToGetEdge :: LEdge DGLinkLab -> DGraph -> Maybe (LEdge DGLinkLab)
tryToGetEdge (src :: Node
src, tgt :: Node
tgt, lb :: DGLinkLab
lb) dgraph :: DGraph
dgraph = (DGLinkLab -> LEdge DGLinkLab)
-> Maybe DGLinkLab -> Maybe (LEdge DGLinkLab)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ l :: DGLinkLab
l -> (Node
src, Node
tgt, DGLinkLab
l))
  (Maybe DGLinkLab -> Maybe (LEdge DGLinkLab))
-> Maybe DGLinkLab -> Maybe (LEdge DGLinkLab)
forall a b. (a -> b) -> a -> b
$ (DGLinkLab -> Bool) -> [DGLinkLab] -> Maybe DGLinkLab
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (DGLinkLab -> DGLinkLab -> Bool
eqDGLinkLabContent DGLinkLab
lb) ([DGLinkLab] -> Maybe DGLinkLab) -> [DGLinkLab] -> Maybe DGLinkLab
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Gr DGNodeLab DGLinkLab -> [DGLinkLab]
forall a b. Node -> Node -> Gr a b -> [b]
Tree.getLEdges Node
src Node
tgt (Gr DGNodeLab DGLinkLab -> [DGLinkLab])
-> Gr DGNodeLab DGLinkLab -> [DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dgraph

{- | try to insert an edge into the given dgraph, if the edge exists, the
edge's id should match, too. -}
insertDGLEdge :: LEdge DGLinkLab -> DGraph -> DGraph
insertDGLEdge :: LEdge DGLinkLab -> DGraph -> DGraph
insertDGLEdge edge :: LEdge DGLinkLab
edge dgraph :: DGraph
dgraph =
  case LEdge DGLinkLab -> DGraph -> Maybe (LEdge DGLinkLab)
tryToGetEdge LEdge DGLinkLab
edge DGraph
dgraph of
    Nothing -> DGraph -> DGChange -> DGraph
changeDGH DGraph
dgraph (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
edge
    Just _ -> DGraph
dgraph

-- | get the edge id out of a given edge
getEdgeId :: LEdge DGLinkLab -> EdgeId
getEdgeId :: LEdge DGLinkLab -> EdgeId
getEdgeId (_, _, label :: DGLinkLab
label) = DGLinkLab -> EdgeId
dgl_id DGLinkLab
label

-- * methods that calculate paths of certain types

getAllPathsOfTypeFromGoalList :: DGraph -> (DGLinkType -> Bool)
                              -> [LEdge DGLinkLab] -> [[LEdge DGLinkLab]]
getAllPathsOfTypeFromGoalList :: DGraph
-> (DGLinkType -> Bool) -> [LEdge DGLinkLab] -> [[LEdge DGLinkLab]]
getAllPathsOfTypeFromGoalList dgraph :: DGraph
dgraph isType :: DGLinkType -> Bool
isType ls :: [LEdge DGLinkLab]
ls = let
      sources :: [Node]
sources = Set Node -> [Node]
forall a. Set a -> [a]
Set.toList (Set Node -> [Node]) -> Set Node -> [Node]
forall a b. (a -> b) -> a -> b
$ [Node] -> Set Node
forall a. Ord a => [a] -> Set a
Set.fromList ([Node] -> Set Node) -> [Node] -> Set Node
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> Node) -> [LEdge DGLinkLab] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: Node
s, _, _) -> Node
s) [LEdge DGLinkLab]
ls
      targets :: [Node]
targets = Set Node -> [Node]
forall a. Set a -> [a]
Set.toList (Set Node -> [Node]) -> Set Node -> [Node]
forall a b. (a -> b) -> a -> b
$ [Node] -> Set Node
forall a. Ord a => [a] -> Set a
Set.fromList ([Node] -> Set Node) -> [Node] -> Set Node
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> Node) -> [LEdge DGLinkLab] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, t :: Node
t, _) -> Node
t) [LEdge DGLinkLab]
ls
  in (Node -> [[LEdge DGLinkLab]]) -> [Node] -> [[LEdge DGLinkLab]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ source :: Node
source ->
       (Node -> [[LEdge DGLinkLab]]) -> [Node] -> [[LEdge DGLinkLab]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DGraph
-> (DGLinkType -> Bool) -> Node -> Node -> [[LEdge DGLinkLab]]
getAllPathsOfTypeBetween DGraph
dgraph DGLinkType -> Bool
isType Node
source) [Node]
targets)
         [Node]
sources

{- | returns all paths consisting of edges of the given type in the given
   development graph -}
getAllPathsOfType :: DGraph -> (DGLinkType -> Bool) -> [[LEdge DGLinkLab]]
getAllPathsOfType :: DGraph -> (DGLinkType -> Bool) -> [[LEdge DGLinkLab]]
getAllPathsOfType dgraph :: DGraph
dgraph isType :: DGLinkType -> Bool
isType =
    DGraph
-> (DGLinkType -> Bool) -> [LEdge DGLinkLab] -> [[LEdge DGLinkLab]]
getAllPathsOfTypeFromGoalList DGraph
dgraph DGLinkType -> Bool
isType ([LEdge DGLinkLab] -> [[LEdge DGLinkLab]])
-> [LEdge DGLinkLab] -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> a -> b
$ DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dgraph

-- | morphisms of (co)free definitions are identities
realMorphism :: DGLinkLab -> Maybe GMorphism
realMorphism :: DGLinkLab -> Maybe GMorphism
realMorphism lbl :: DGLinkLab
lbl = let mor :: GMorphism
mor = DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
lbl in case DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lbl of
  ScopedLink {} -> GMorphism -> Maybe GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return GMorphism
mor
  HidingDefLink -> String -> Maybe GMorphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "hiding definition link"
  FreeOrCofreeDefLink _ _ -> GMorphism -> Maybe GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (GMorphism -> Maybe GMorphism) -> GMorphism -> Maybe GMorphism
forall a b. (a -> b) -> a -> b
$ G_sign -> GMorphism
forall object morphism.
Category object morphism =>
object -> morphism
ide (G_sign -> GMorphism) -> G_sign -> GMorphism
forall a b. (a -> b) -> a -> b
$ GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
mor
  HidingFreeOrCofreeThm {} -> String -> Maybe GMorphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "hiding or free thm link"

-- | determines the morphism of a given path
calculateMorphismOfPath :: [LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath :: [LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath p :: [LEdge DGLinkLab]
p = case [LEdge DGLinkLab]
p of
  (_, _, lbl :: DGLinkLab
lbl) : r :: [LEdge DGLinkLab]
r -> do
    GMorphism
morphism <- DGLinkLab -> Maybe GMorphism
realMorphism DGLinkLab
lbl
    if [LEdge DGLinkLab] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LEdge DGLinkLab]
r then GMorphism -> Maybe GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return GMorphism
morphism else do
       GMorphism
rmor <- [LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath [LEdge DGLinkLab]
r
       Result GMorphism -> Maybe GMorphism
forall a. Result a -> Maybe a
resultToMaybe (Result GMorphism -> Maybe GMorphism)
-> Result GMorphism -> Maybe GMorphism
forall a b. (a -> b) -> a -> b
$ GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
composeMorphisms GMorphism
morphism GMorphism
rmor
  [] -> String -> Maybe GMorphism
forall a. HasCallStack => String -> a
error "calculateMorphismOfPath"

{- | returns all paths from the given list whose morphism is equal to the
   given one -}
filterPathsByMorphism :: GMorphism -> [[LEdge DGLinkLab]]
                      -> [[LEdge DGLinkLab]]
filterPathsByMorphism :: GMorphism -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
filterPathsByMorphism morphism :: GMorphism
morphism =
    ([LEdge DGLinkLab] -> Bool)
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Maybe GMorphism -> Maybe GMorphism -> Bool
forall a. Eq a => a -> a -> Bool
== GMorphism -> Maybe GMorphism
forall a. a -> Maybe a
Just GMorphism
morphism) (Maybe GMorphism -> Bool)
-> ([LEdge DGLinkLab] -> Maybe GMorphism)
-> [LEdge DGLinkLab]
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath)

{- | returns all paths consisting of global edges only
   or of one local edge followed by any number of global edges -}
getAllLocGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllLocGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllLocGlobPathsBetween dgraph :: DGraph
dgraph src :: Node
src tgt :: Node
tgt = let
    outEdges :: [LEdge DGLinkLab]
outEdges = DGraph -> Node -> [LEdge DGLinkLab]
outDG DGraph
dgraph Node
src
    locEdges :: [LEdge DGLinkLab]
locEdges = (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
isLocalEdge) [LEdge DGLinkLab]
outEdges
    locGlobPaths :: [[LEdge DGLinkLab]]
locGlobPaths =
       (LEdge DGLinkLab -> [[LEdge DGLinkLab]])
-> [LEdge DGLinkLab] -> [[LEdge DGLinkLab]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ edge :: LEdge DGLinkLab
edge@(_, node :: Node
node, _) -> ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> [a] -> [b]
map (LEdge DGLinkLab
edge LEdge DGLinkLab -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. a -> [a] -> [a]
:)
                  ([[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]])
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllGlobPathsBetween DGraph
dgraph Node
node Node
tgt) [LEdge DGLinkLab]
locEdges
    globPaths :: [[LEdge DGLinkLab]]
globPaths = DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllGlobPathsBetween DGraph
dgraph Node
src Node
tgt
  in [[LEdge DGLinkLab]]
locGlobPaths [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a. [a] -> [a] -> [a]
++ [[LEdge DGLinkLab]]
globPaths

{- | returns all paths of globalDef edges or globalThm edges
   between the given source and target node -}
getAllGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllGlobPathsBetween dgraph :: DGraph
dgraph = DGraph
-> (DGLinkType -> Bool) -> Node -> Node -> [[LEdge DGLinkLab]]
getAllPathsOfTypeBetween DGraph
dgraph DGLinkType -> Bool
isGlobalEdge

{- | returns all cyclic paths consisting of edges of the given type between the
   given two nodes -}
getAllPathsOfTypeBetween :: DGraph -> (DGLinkType -> Bool) -> Node
                         -> Node -> [[LEdge DGLinkLab]]
getAllPathsOfTypeBetween :: DGraph
-> (DGLinkType -> Bool) -> Node -> Node -> [[LEdge DGLinkLab]]
getAllPathsOfTypeBetween dgraph :: DGraph
dgraph isType :: DGLinkType -> Bool
isType src :: Node
src tgt :: Node
tgt =
    Node -> Node -> Gr DGNodeLab DGLinkLab -> [[LEdge DGLinkLab]]
forall a b. Node -> Node -> Gr a b -> [[LEdge b]]
Tree.getPathsTo Node
src Node
tgt (Gr DGNodeLab DGLinkLab -> [[LEdge DGLinkLab]])
-> (Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab)
-> Gr DGNodeLab DGLinkLab
-> [[LEdge DGLinkLab]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DGLinkLab -> Bool)
-> Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
(b -> Bool) -> gr a b -> gr a b
elfilter (DGLinkType -> Bool
isType (DGLinkType -> Bool)
-> (DGLinkLab -> DGLinkType) -> DGLinkLab -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGLinkLab -> DGLinkType
dgl_type) (Gr DGNodeLab DGLinkLab -> [[LEdge DGLinkLab]])
-> Gr DGNodeLab DGLinkLab -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dgraph

-- | return all non-cyclic paths starting from the given node
getAllPathsOfTypeFrom :: DGraph -> Node -> [[LEdge DGLinkLab]]
getAllPathsOfTypeFrom :: DGraph -> Node -> [[LEdge DGLinkLab]]
getAllPathsOfTypeFrom dgraph :: DGraph
dgraph src :: Node
src =
   Node -> Gr DGNodeLab DGLinkLab -> [[LEdge DGLinkLab]]
forall a b. Node -> Gr a b -> [[LEdge b]]
Tree.getPaths Node
src (Gr DGNodeLab DGLinkLab -> [[LEdge DGLinkLab]])
-> (Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab)
-> Gr DGNodeLab DGLinkLab
-> [[LEdge DGLinkLab]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DGLinkLab -> Bool)
-> Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
(b -> Bool) -> gr a b -> gr a b
elfilter (Bool -> Bool
not (Bool -> Bool) -> (DGLinkLab -> Bool) -> DGLinkLab -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGLinkType -> Bool
isHidingEdge (DGLinkType -> Bool)
-> (DGLinkLab -> DGLinkType) -> DGLinkLab -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGLinkLab -> DGLinkType
dgl_type) (Gr DGNodeLab DGLinkLab -> [[LEdge DGLinkLab]])
-> Gr DGNodeLab DGLinkLab -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dgraph

-- * methods to check and select proof basis

checkEdgeIds :: DGraph -> Maybe [EdgeId]
checkEdgeIds :: DGraph -> Maybe [EdgeId]
checkEdgeIds dg :: DGraph
dg =
    let pBl :: [EdgeId]
pBl = (LEdge DGLinkLab -> EdgeId) -> [LEdge DGLinkLab] -> [EdgeId]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, _, l :: DGLinkLab
l) -> DGLinkLab -> EdgeId
dgl_id DGLinkLab
l) ([LEdge DGLinkLab] -> [EdgeId]) -> [LEdge DGLinkLab] -> [EdgeId]
forall a b. (a -> b) -> a -> b
$ Gr DGNodeLab DGLinkLab -> [LEdge DGLinkLab]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges (Gr DGNodeLab DGLinkLab -> [LEdge DGLinkLab])
-> Gr DGNodeLab DGLinkLab -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
        pBs :: Set EdgeId
pBs = [EdgeId] -> Set EdgeId
forall a. Ord a => [a] -> Set a
Set.fromList [EdgeId]
pBl
        pBl2 :: [EdgeId]
pBl2 = Set EdgeId -> [EdgeId]
forall a. Set a -> [a]
Set.toList Set EdgeId
pBs
    in case [EdgeId]
pBl [EdgeId] -> [EdgeId] -> [EdgeId]
forall a. Eq a => [a] -> [a] -> [a]
\\ [EdgeId]
pBl2 of
         [] -> if EdgeId -> Set EdgeId -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member EdgeId
defaultEdgeId Set EdgeId
pBs
               then [EdgeId] -> Maybe [EdgeId]
forall a. a -> Maybe a
Just [EdgeId
defaultEdgeId] else Maybe [EdgeId]
forall a. Maybe a
Nothing
         l :: [EdgeId]
l -> [EdgeId] -> Maybe [EdgeId]
forall a. a -> Maybe a
Just [EdgeId]
l

{- | determines all proven paths in the given list and tries to select a
   proof basis from these (s. selectProofBasisAux);
   if this fails the same is done for the rest of the given paths, i.e.
   for the unproven ones -}
selectProofBasis :: DGraph -> LEdge DGLinkLab -> [[LEdge DGLinkLab]]
                 -> ProofBasis
selectProofBasis :: DGraph -> LEdge DGLinkLab -> [[LEdge DGLinkLab]] -> ProofBasis
selectProofBasis dg :: DGraph
dg ledge :: LEdge DGLinkLab
ledge paths :: [[LEdge DGLinkLab]]
paths = let
  (provenPaths :: [[LEdge DGLinkLab]]
provenPaths, unprovenPaths :: [[LEdge DGLinkLab]]
unprovenPaths) = ([LEdge DGLinkLab] -> Bool)
-> [[LEdge DGLinkLab]]
-> ([[LEdge DGLinkLab]], [[LEdge DGLinkLab]])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> Bool)
-> (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> Bool
forall a b. (a -> b) -> a -> b
$ (DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
isProven) [[LEdge DGLinkLab]]
paths
  pBl :: [(EdgeId, Set EdgeId)]
pBl = (LEdge DGLinkLab -> (EdgeId, Set EdgeId))
-> [LEdge DGLinkLab] -> [(EdgeId, Set EdgeId)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, _, l :: DGLinkLab
l) ->
               (DGLinkLab -> EdgeId
dgl_id DGLinkLab
l, ProofBasis -> Set EdgeId
proofBasis (ProofBasis -> Set EdgeId) -> ProofBasis -> Set EdgeId
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> ProofBasis
getProofBasis DGLinkLab
l))
              ([LEdge DGLinkLab] -> [(EdgeId, Set EdgeId)])
-> [LEdge DGLinkLab] -> [(EdgeId, Set EdgeId)]
forall a b. (a -> b) -> a -> b
$ Gr DGNodeLab DGLinkLab -> [LEdge DGLinkLab]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges (Gr DGNodeLab DGLinkLab -> [LEdge DGLinkLab])
-> Gr DGNodeLab DGLinkLab -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
  rel :: Map EdgeId (Set EdgeId)
rel = Bool -> Map EdgeId (Set EdgeId) -> Map EdgeId (Set EdgeId)
forall a. HasCallStack => Bool -> a -> a
assert (Maybe [EdgeId] -> Bool
forall a. Maybe a -> Bool
isNothing (DGraph -> Maybe [EdgeId]
checkEdgeIds DGraph
dg) Bool -> Bool -> Bool
&&
                ((EdgeId, Set EdgeId) -> Bool) -> [(EdgeId, Set EdgeId)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ (e :: EdgeId
e, pB :: Set EdgeId
pB) -> Bool -> Bool
not (EdgeId -> Set EdgeId -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member EdgeId
e Set EdgeId
pB)) [(EdgeId, Set EdgeId)]
pBl) (Map EdgeId (Set EdgeId) -> Map EdgeId (Set EdgeId))
-> Map EdgeId (Set EdgeId) -> Map EdgeId (Set EdgeId)
forall a b. (a -> b) -> a -> b
$
        Rel EdgeId -> Map EdgeId (Set EdgeId)
forall a. Rel a -> Map a (Set a)
Rel.toMap (Rel EdgeId -> Map EdgeId (Set EdgeId))
-> Rel EdgeId -> Map EdgeId (Set EdgeId)
forall a b. (a -> b) -> a -> b
$ Rel EdgeId -> Rel EdgeId
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel EdgeId -> Rel EdgeId) -> Rel EdgeId -> Rel EdgeId
forall a b. (a -> b) -> a -> b
$ Map EdgeId (Set EdgeId) -> Rel EdgeId
forall a. Map a (Set a) -> Rel a
Rel.fromMap (Map EdgeId (Set EdgeId) -> Rel EdgeId)
-> Map EdgeId (Set EdgeId) -> Rel EdgeId
forall a b. (a -> b) -> a -> b
$ [(EdgeId, Set EdgeId)] -> Map EdgeId (Set EdgeId)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(EdgeId, Set EdgeId)]
pBl
  in Map EdgeId (Set EdgeId)
-> LEdge DGLinkLab -> [[LEdge DGLinkLab]] -> ProofBasis
selectProofBasisAux Map EdgeId (Set EdgeId)
rel LEdge DGLinkLab
ledge ([[LEdge DGLinkLab]] -> ProofBasis)
-> [[LEdge DGLinkLab]] -> ProofBasis
forall a b. (a -> b) -> a -> b
$ [[LEdge DGLinkLab]]
provenPaths [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a. [a] -> [a] -> [a]
++ [[LEdge DGLinkLab]]
unprovenPaths

{- | selects the first path that does not form a proof cycle with the given
 label (if such a path exits) and returns the labels of its edges -}
selectProofBasisAux :: Map.Map EdgeId (Set.Set EdgeId) -> LEdge DGLinkLab
                    -> [[LEdge DGLinkLab]] -> ProofBasis
selectProofBasisAux :: Map EdgeId (Set EdgeId)
-> LEdge DGLinkLab -> [[LEdge DGLinkLab]] -> ProofBasis
selectProofBasisAux _ _ [] = ProofBasis
emptyProofBasis
selectProofBasisAux rel :: Map EdgeId (Set EdgeId)
rel ledge :: LEdge DGLinkLab
ledge (path :: [LEdge DGLinkLab]
path : list :: [[LEdge DGLinkLab]]
list) =
  let b :: ProofBasis
b = Map EdgeId (Set EdgeId) -> [LEdge DGLinkLab] -> ProofBasis
calculateProofBasis Map EdgeId (Set EdgeId)
rel [LEdge DGLinkLab]
path in
    if EdgeId -> ProofBasis -> Bool
edgeInProofBasis (LEdge DGLinkLab -> EdgeId
getEdgeId LEdge DGLinkLab
ledge) ProofBasis
b
       then Map EdgeId (Set EdgeId)
-> LEdge DGLinkLab -> [[LEdge DGLinkLab]] -> ProofBasis
selectProofBasisAux Map EdgeId (Set EdgeId)
rel LEdge DGLinkLab
ledge [[LEdge DGLinkLab]]
list
       else ProofBasis
b               -- OK, no cyclic proof

{- | calculates the proofBasis of the given path,
 i.e. (recursively) close the list of DGLinkLabs under the relation
 'is proved using'. If a DGLinkLab has proof status LeftOpen,
 look up in the development graph for its current status -}
calculateProofBasis :: Map.Map EdgeId (Set.Set EdgeId) -> [LEdge DGLinkLab]
                    -> ProofBasis
calculateProofBasis :: Map EdgeId (Set EdgeId) -> [LEdge DGLinkLab] -> ProofBasis
calculateProofBasis rel :: Map EdgeId (Set EdgeId)
rel = Set EdgeId -> ProofBasis
ProofBasis (Set EdgeId -> ProofBasis)
-> ([LEdge DGLinkLab] -> Set EdgeId)
-> [LEdge DGLinkLab]
-> ProofBasis
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LEdge DGLinkLab -> Set EdgeId -> Set EdgeId)
-> Set EdgeId -> [LEdge DGLinkLab] -> Set EdgeId
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
    (\ (_, _, l :: DGLinkLab
l) -> let eid :: EdgeId
eid = DGLinkLab -> EdgeId
dgl_id DGLinkLab
l in EdgeId -> Set EdgeId -> Set EdgeId
forall a. Ord a => a -> Set a -> Set a
Set.insert EdgeId
eid
     (Set EdgeId -> Set EdgeId)
-> (Set EdgeId -> Set EdgeId) -> Set EdgeId -> Set EdgeId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set EdgeId -> Set EdgeId -> Set EdgeId
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set EdgeId -> EdgeId -> Map EdgeId (Set EdgeId) -> Set EdgeId
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set EdgeId
forall a. Set a
Set.empty EdgeId
eid Map EdgeId (Set EdgeId)
rel))
    Set EdgeId
forall a. Set a
Set.empty

invalidateProof :: DGLinkType -> DGLinkType
invalidateProof :: DGLinkType -> DGLinkType
invalidateProof t :: DGLinkType
t = case DGLinkType
t of
    ScopedLink sc :: Scope
sc dl :: LinkKind
dl (ConsStatus c :: Conservativity
c _ _) ->
      Scope -> LinkKind -> ConsStatus -> DGLinkType
ScopedLink Scope
sc (case LinkKind
dl of
        ThmLink _ -> ThmLinkStatus -> LinkKind
ThmLink ThmLinkStatus
LeftOpen
        _ -> LinkKind
dl) (ConsStatus -> DGLinkType) -> ConsStatus -> DGLinkType
forall a b. (a -> b) -> a -> b
$ Conservativity -> Conservativity -> ThmLinkStatus -> ConsStatus
ConsStatus Conservativity
c Conservativity
None ThmLinkStatus
LeftOpen
    HidingFreeOrCofreeThm mh :: Maybe FreeOrCofree
mh n :: Node
n gm :: GMorphism
gm _ -> Maybe FreeOrCofree
-> Node -> GMorphism -> ThmLinkStatus -> DGLinkType
HidingFreeOrCofreeThm Maybe FreeOrCofree
mh Node
n GMorphism
gm ThmLinkStatus
LeftOpen
    _ -> DGLinkType
t

-- | adopts the edges of the old node to the new node
adoptEdges :: DGraph -> Node -> Node -> DGraph
adoptEdges :: DGraph -> Node -> Node -> DGraph
adoptEdges dgraph :: DGraph
dgraph oldNode :: Node
oldNode newNode :: Node
newNode =
  if Node
oldNode Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
newNode then DGraph
dgraph else
  let (inEdges' :: Adj DGLinkLab
inEdges', _, _, outEdges' :: Adj DGLinkLab
outEdges') = String
-> DGraph
-> Node
-> (Adj DGLinkLab, Node, DGNodeLab, Adj DGLinkLab)
safeContextDG "adoptEdges" DGraph
dgraph Node
oldNode
      inEdges :: [LEdge DGLinkLab]
inEdges = ((DGLinkLab, Node) -> LEdge DGLinkLab)
-> Adj DGLinkLab -> [LEdge DGLinkLab]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (l :: DGLinkLab
l, v :: Node
v) -> (Node
v, Node
oldNode, DGLinkLab
l)) Adj DGLinkLab
inEdges'
      outEdges :: [LEdge DGLinkLab]
outEdges = ((DGLinkLab, Node) -> LEdge DGLinkLab)
-> Adj DGLinkLab -> [LEdge DGLinkLab]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (l :: DGLinkLab
l, v :: Node
v) -> (Node
oldNode, Node
v, DGLinkLab
l)) Adj DGLinkLab
outEdges'
      newIn :: [LEdge DGLinkLab]
newIn = (LEdge DGLinkLab -> LEdge DGLinkLab)
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> [a] -> [b]
map (Node -> Bool -> LEdge DGLinkLab -> LEdge DGLinkLab
adoptEdgesAux Node
newNode Bool
True) [LEdge DGLinkLab]
inEdges
      newOut :: [LEdge DGLinkLab]
newOut = (LEdge DGLinkLab -> LEdge DGLinkLab)
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> [a] -> [b]
map (Node -> Bool -> LEdge DGLinkLab -> LEdge DGLinkLab
adoptEdgesAux Node
newNode Bool
False) [LEdge DGLinkLab]
outEdges
      allChanges :: [DGChange]
allChanges = (LEdge DGLinkLab -> DGChange) -> [LEdge DGLinkLab] -> [DGChange]
forall a b. (a -> b) -> [a] -> [b]
map LEdge DGLinkLab -> DGChange
DeleteEdge ([LEdge DGLinkLab]
inEdges [LEdge DGLinkLab] -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. [a] -> [a] -> [a]
++ [LEdge DGLinkLab]
outEdges)
                   [DGChange] -> [DGChange] -> [DGChange]
forall a. [a] -> [a] -> [a]
++ (LEdge DGLinkLab -> DGChange) -> [LEdge DGLinkLab] -> [DGChange]
forall a b. (a -> b) -> [a] -> [b]
map LEdge DGLinkLab -> DGChange
InsertEdge ([LEdge DGLinkLab]
newIn [LEdge DGLinkLab] -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. [a] -> [a] -> [a]
++ [LEdge DGLinkLab]
newOut)
  in DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dgraph [DGChange]
allChanges

-- | auxiliary method for adoptEdges
adoptEdgesAux :: Node -> Bool -> LEdge DGLinkLab -> LEdge DGLinkLab
adoptEdgesAux :: Node -> Bool -> LEdge DGLinkLab -> LEdge DGLinkLab
adoptEdgesAux node :: Node
node areIngoingEdges :: Bool
areIngoingEdges (src :: Node
src, tgt :: Node
tgt, edgelab :: DGLinkLab
edgelab) =
  let (newSrc :: Node
newSrc, newTgt :: Node
newTgt) = if Node
src Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
tgt then (Node
node, Node
node) else (Node
src, Node
tgt)
  in if Bool
areIngoingEdges then (Node
newSrc, Node
node, DGLinkLab
edgelab)
     else (Node
node, Node
newTgt, DGLinkLab
edgelab)

getAllOpenNodeGoals :: [DGNodeLab] -> [DGNodeLab]
getAllOpenNodeGoals :: [DGNodeLab] -> [DGNodeLab]
getAllOpenNodeGoals = (DGNodeLab -> Bool) -> [DGNodeLab] -> [DGNodeLab]
forall a. (a -> Bool) -> [a] -> [a]
filter DGNodeLab -> Bool
hasOpenGoals

{- | return a warning text if the given label has incoming hiding edge,
     otherwise just an empty string. -}
hidingLabelWarning :: DGNodeLab -> String
hidingLabelWarning :: DGNodeLab -> String
hidingLabelWarning lbl :: DGNodeLab
lbl = if DGNodeLab -> Bool
labelHasHiding DGNodeLab
lbl then
       [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ "<Warning>" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ("  " String -> String -> String
forall a. [a] -> [a] -> [a]
++) [String]
hidingWarning [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["</Warning>"]
       else ""

{- | return a warning text if the given node has incoming hiding edge,
     otherwise just an empty string. -}
addHasInHidingWarning :: DGraph -> Node -> String
addHasInHidingWarning :: DGraph -> Node -> String
addHasInHidingWarning dgraph :: DGraph
dgraph = DGNodeLab -> String
hidingLabelWarning (DGNodeLab -> String) -> (Node -> DGNodeLab) -> Node -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Node -> DGNodeLab
labDG DGraph
dgraph

hidingWarning :: [String]
hidingWarning :: [String]
hidingWarning =
  [ "This node has incoming hiding links!"
  , "The theory shown may be too weak for proving."
  , "A consistency check may wrongly succeed."
  , "If possible use the normal form of this node." ]