{- |
Module      :  ./Proofs/Global.hs
Description :  global proof rules for 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(DevGraph)

global proof rules for development graphs.
   Follows Sect. IV:4.4 of the CASL Reference Manual.
-}

module Proofs.Global
    ( globSubsume
    , globDecomp
    , globDecompAux -- for Test.hs
    , globDecompFromList
    , globSubsumeFromList
    ) where

import Data.Graph.Inductive.Graph
import qualified Data.Map as Map
import Data.Maybe

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

import Common.LibName
import Common.Utils

import Proofs.EdgeUtils
import Proofs.StatusUtils

globDecompRule :: EdgeId -> DGRule
globDecompRule :: EdgeId -> DGRule
globDecompRule = String -> EdgeId -> DGRule
DGRuleWithEdge "Global-Decomposition"

{- apply rule GlobDecomp to all global theorem links in the current DG
   current DG = DGm
   add to proof status the pair ([GlobDecomp e1,...,GlobDecomp en],DGm+1)
   where e1...en are the global theorem links in DGm
   DGm+1 results from DGm by application of GlobDecomp e1,...,GlobDecomp en -}


{- | applies global decomposition to the list of edges given (global
     theorem edges) if possible, if empty list is given then to all
     unproven global theorems.
     Notice: (for ticket 5, which solves the problem across library border)
     1. before the actual global decomposition is applied, the whole DGraph is
     updated firstly by calling the function updateDGraph.
     2. The changes of the update action should be added as the head of the
     history.
-}
globDecompFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
globDecompFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
globDecompFromList ln :: LibName
ln globalThmEdges :: [LEdge DGLinkLab]
globalThmEdges proofStatus :: LibEnv
proofStatus =
    let dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
proofStatus
        finalGlobalThmEdges :: [LEdge DGLinkLab]
finalGlobalThmEdges = (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
isUnprovenGlobalThm) [LEdge DGLinkLab]
globalThmEdges
        auxGraph :: DGraph
auxGraph = (DGraph -> Node -> DGraph) -> DGraph -> [Node] -> DGraph
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (LibEnv -> DGraph -> Node -> DGraph
updateDGraph LibEnv
proofStatus) DGraph
dgraph
           ([Node] -> DGraph) -> [Node] -> DGraph
forall a b. (a -> b) -> a -> b
$ [Node] -> [Node]
forall a. Ord a => [a] -> [a]
nubOrd ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> Node) -> [LEdge DGLinkLab] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (\ (src :: Node
src, _, _) -> Node
src) [LEdge DGLinkLab]
finalGlobalThmEdges
        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
globDecompAux DGraph
auxGraph [LEdge DGLinkLab]
finalGlobalThmEdges
    in LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
newDGraph LibEnv
proofStatus

{- | update the given DGraph with source nodes of all global unproven
     links.
     The idea is, to expand the given DGraph by adding all the referenced
     nodes related to the given source nodes in other libraries and the
     corresponding links as well.
     If a certain node is a referenced node and not expanded yet, then its
     parents will be found by calling getRefParents.
     These parents will be added into current DGraph using updateDGraphAux
-}
updateDGraph :: LibEnv -> DGraph
             -> Node -- source nodes of all global unproven links
             -> DGraph
updateDGraph :: LibEnv -> DGraph -> Node -> DGraph
updateDGraph le :: LibEnv
le dg :: DGraph
dg x :: Node
x =
    case LibEnv
-> Maybe LibName
-> DGraph
-> Node
-> (Maybe LibName, DGraph, LNode DGNodeLab)
lookupRefNodeM LibEnv
le Maybe LibName
forall a. Maybe a
Nothing DGraph
dg Node
x of
      (Just refl :: LibName
refl, refDg :: DGraph
refDg, (refn :: Node
refn, _)) ->
            let
            parents :: [(Node, [DGLinkLab])]
parents = DGraph -> Node -> [(Node, [DGLinkLab])]
getRefParents DGraph
refDg Node
refn
            {- important for those, who's doing redo/undo function:
               notice that if the node is expanded, then it should be
               deleted out of the unexpanded map using
               deleteFromRefNodesDG -}
            auxDG :: DGraph
auxDG = (DGraph -> (Node, [DGLinkLab]) -> DGraph)
-> DGraph -> [(Node, [DGLinkLab])] -> DGraph
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (LibEnv
-> Node
-> LibName
-> DGraph
-> DGraph
-> (Node, [DGLinkLab])
-> DGraph
updateDGraphAux LibEnv
le Node
x LibName
refl DGraph
refDg)
                DGraph
dg [(Node, [DGLinkLab])]
parents
            in DGraph
auxDG
      _ -> DGraph
dg

{- | get all the parents, namely the related referenced nodes and the links
     between them and the present to be expanded node.
-}
getRefParents :: DGraph
              -> Node -- the present to be expanded node
              -> [(Node, [DGLinkLab])]
getRefParents :: DGraph -> Node -> [(Node, [DGLinkLab])]
getRefParents dg :: DGraph
dg refn :: Node
refn =
   let
   -- get the previous objects to the current one
   pres :: [LEdge DGLinkLab]
pres = DGraph -> Node -> [LEdge DGLinkLab]
innDG DGraph
dg Node
refn
   in [LEdge DGLinkLab] -> [(Node, [DGLinkLab])]
modifyPs [LEdge DGLinkLab]
pres

{- | modify the parents to a better form.
     e.g. if the list is like:
     [(a, 1), (b, 1), (c, 2), (d, 2), (e, 2)]
     which means that node 1 is related via links a and b, and node 2 is
     related via links c, d and e.
     then to advoid too many checking by inserting, we can modify the list
     above to a form like this:
     [(1, [a, b]), (2, [c, d, e])]
     which simplifies the inserting afterwards ;)
-}

modifyPs :: [LEdge DGLinkLab] -> [(Node, [DGLinkLab])]
modifyPs :: [LEdge DGLinkLab] -> [(Node, [DGLinkLab])]
modifyPs = Map Node [DGLinkLab] -> [(Node, [DGLinkLab])]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Node [DGLinkLab] -> [(Node, [DGLinkLab])])
-> ([LEdge DGLinkLab] -> Map Node [DGLinkLab])
-> [LEdge DGLinkLab]
-> [(Node, [DGLinkLab])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([DGLinkLab] -> [DGLinkLab] -> [DGLinkLab])
-> [(Node, [DGLinkLab])] -> Map Node [DGLinkLab]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith [DGLinkLab] -> [DGLinkLab] -> [DGLinkLab]
forall a. [a] -> [a] -> [a]
(++)
  ([(Node, [DGLinkLab])] -> Map Node [DGLinkLab])
-> ([LEdge DGLinkLab] -> [(Node, [DGLinkLab])])
-> [LEdge DGLinkLab]
-> Map Node [DGLinkLab]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LEdge DGLinkLab -> (Node, [DGLinkLab]))
-> [LEdge DGLinkLab] -> [(Node, [DGLinkLab])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (k :: Node
k, _, v :: DGLinkLab
v) -> (Node
k, [DGLinkLab
v]))

{- | the actual update function to insert a list of related parents to the
     present to be expanded node.
     It inserts the related referenced node first by calling addParentNode.
     Then it inserts the related links by calling addParentLinks.
-}
updateDGraphAux :: LibEnv -> Node -- the present to be expanded node
                -> LibName
                -> DGraph -- ^ the reference graph for the libname
                -> DGraph -> (Node, [DGLinkLab])
                -> DGraph
updateDGraphAux :: LibEnv
-> Node
-> LibName
-> DGraph
-> DGraph
-> (Node, [DGLinkLab])
-> DGraph
updateDGraphAux libenv :: LibEnv
libenv n :: Node
n refl :: LibName
refl refDg :: DGraph
refDg dg :: DGraph
dg (pn :: Node
pn, pls :: [DGLinkLab]
pls) =
   let
   (auxDG :: DGraph
auxDG, newN :: Node
newN) = LibEnv -> DGraph -> LibName -> DGraph -> Node -> (DGraph, Node)
addParentNode LibEnv
libenv DGraph
dg LibName
refl DGraph
refDg Node
pn
   in DGraph -> Node -> Node -> [DGLinkLab] -> DGraph
addParentLinks DGraph
auxDG Node
newN Node
n [DGLinkLab]
pls

-- | add the given parent node into the current dgraph
addParentNode :: LibEnv -> DGraph -> LibName
              -> DGraph -- ^ the reference graph for the libname
              -> Node -- the referenced parent node
              -> (DGraph, Node)
addParentNode :: LibEnv -> DGraph -> LibName -> DGraph -> Node -> (DGraph, Node)
addParentNode libenv :: LibEnv
libenv dg :: DGraph
dg refl :: LibName
refl refDg :: DGraph
refDg refn :: Node
refn =
   let
   {-
     To advoid the chain which is desribed in ticket 5, the parent node should
     be a non referenced node firstly, so that the actual parent node can be
     related.
   -}
   (newRefl :: LibName
newRefl, _, (newRefn :: Node
newRefn, nodelab :: DGNodeLab
nodelab)) = LibEnv
-> LibName -> DGraph -> Node -> (LibName, DGraph, LNode DGNodeLab)
lookupRefNode LibEnv
libenv LibName
refl
     DGraph
refDg Node
refn
   {-
     Set the sgMap and tMap too.
     Notice for those who are doing undo/redo, because the DGraph is actually
     changed if the maps are changed ;)

   creates an empty GTh, please check the definition of this function
   because there can be some problem or errors at this place. -}
   newGTh :: G_theory
newGTh = case DGNodeLab -> G_theory
dgn_theory DGNodeLab
nodelab of
     G_theory lid :: lid
lid _ sig :: ExtSign sign symbol
sig ind :: SigId
ind _ _ -> lid -> ExtSign sign symbol -> SigId -> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
lid ExtSign sign symbol
sig SigId
ind
   refInfo :: DGNodeInfo
refInfo = LibName -> Node -> DGNodeInfo
newRefInfo LibName
newRefl Node
newRefn
   newRefNode :: DGNodeLab
newRefNode = (NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab (DGNodeLab -> NodeName
dgn_name DGNodeLab
nodelab) DGNodeInfo
refInfo G_theory
newGTh)
     { globalTheory :: Maybe G_theory
globalTheory = DGNodeLab -> Maybe G_theory
globalTheory DGNodeLab
nodelab }
   in
   {- checks if this node exists in the current dg, if so, nothing needs to be
   done. -}
   case DGNodeInfo -> DGraph -> Maybe Node
lookupInAllRefNodesDG DGNodeInfo
refInfo DGraph
dg of
        Nothing -> let newN :: Node
newN = DGraph -> Node
getNewNodeDG DGraph
dg in
           (DGraph -> DGChange -> DGraph
changeDGH DGraph
dg (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ LNode DGNodeLab -> DGChange
InsertNode (Node
newN, DGNodeLab
newRefNode), Node
newN)
        Just extN :: Node
extN -> (DGraph
dg, Node
extN)

-- | add a list of links between the given two node ids.
addParentLinks :: DGraph -> Node -> Node -> [DGLinkLab] -> DGraph
addParentLinks :: DGraph -> Node -> Node -> [DGLinkLab] -> DGraph
addParentLinks dg :: DGraph
dg src :: Node
src tgt :: Node
tgt ls :: [DGLinkLab]
ls =
  let oldLinks :: [DGLinkLab]
oldLinks = (LEdge DGLinkLab -> DGLinkLab) -> [LEdge DGLinkLab] -> [DGLinkLab]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, _, l :: DGLinkLab
l) -> DGLinkLab
l)
        ([LEdge DGLinkLab] -> [DGLinkLab])
-> [LEdge DGLinkLab] -> [DGLinkLab]
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (s :: Node
s, _, _) -> Node
s Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
src) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> [LEdge DGLinkLab]
innDG DGraph
dg Node
tgt
      newLinks :: [DGLinkLab]
newLinks = (DGLinkLab -> DGLinkLab) -> [DGLinkLab] -> [DGLinkLab]
forall a b. (a -> b) -> [a] -> [b]
map (\ l :: DGLinkLab
l -> DGLinkLab
l
                         { dgl_id :: EdgeId
dgl_id = EdgeId
defaultEdgeId
                         , dgl_type :: DGLinkType
dgl_type = DGLinkType -> DGLinkType
invalidateProof (DGLinkType -> DGLinkType) -> DGLinkType -> DGLinkType
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l }) [DGLinkLab]
ls
  in if [DGLinkLab] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DGLinkLab]
oldLinks then
         DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg ([DGChange] -> DGraph) -> [DGChange] -> DGraph
forall a b. (a -> b) -> a -> b
$ (DGLinkLab -> DGChange) -> [DGLinkLab] -> [DGChange]
forall a b. (a -> b) -> [a] -> [b]
map (\ l :: DGLinkLab
l -> LEdge DGLinkLab -> DGChange
InsertEdge (Node
src, Node
tgt, DGLinkLab
l)) [DGLinkLab]
newLinks
     else DGraph
dg -- assume ingoing links are already properly set

{- applies global decomposition to all unproven global theorem edges
   if possible -}
globDecomp :: LibName -> LibEnv -> LibEnv
globDecomp :: LibName -> LibEnv -> LibEnv
globDecomp ln :: LibName
ln proofStatus :: LibEnv
proofStatus =
    let dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
proofStatus
        globalThmEdges :: [LEdge DGLinkLab]
globalThmEdges = DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dgraph
    in
    LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
globDecompFromList LibName
ln [LEdge DGLinkLab]
globalThmEdges LibEnv
proofStatus

{- auxiliary function for globDecomp (above)
   actual implementation -}
globDecompAux :: DGraph -> LEdge DGLinkLab -> DGraph
globDecompAux :: DGraph -> LEdge DGLinkLab -> DGraph
globDecompAux dgraph :: DGraph
dgraph edge :: LEdge DGLinkLab
edge =
  let newDGraph :: DGraph
newDGraph = DGraph -> LEdge DGLinkLab -> DGraph
globDecompForOneEdge DGraph
dgraph LEdge DGLinkLab
edge
  in DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dgraph (EdgeId -> DGRule
globDecompRule (EdgeId -> DGRule) -> EdgeId -> DGRule
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> EdgeId
getEdgeId LEdge DGLinkLab
edge) DGraph
newDGraph

-- applies global decomposition to a single edge
globDecompForOneEdge :: DGraph -> LEdge DGLinkLab -> DGraph
globDecompForOneEdge :: DGraph -> LEdge DGLinkLab -> DGraph
globDecompForOneEdge dgraph :: DGraph
dgraph edge :: LEdge DGLinkLab
edge@(source :: Node
source, target :: Node
target, edgeLab :: DGLinkLab
edgeLab) = let
    defEdgesToSource :: [LEdge DGLinkLab]
defEdgesToSource = (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
isDefEdge) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> [LEdge DGLinkLab]
innDG DGraph
dgraph Node
source
    paths :: [[LEdge DGLinkLab]]
paths = [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]
map (LEdge DGLinkLab -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. a -> [a] -> [a]
: [LEdge DGLinkLab
edge]) [LEdge DGLinkLab]
defEdgesToSource
    (newGr :: DGraph
newGr, proof_basis :: ProofBasis
proof_basis) = ((DGraph, ProofBasis) -> [LEdge DGLinkLab] -> (DGraph, ProofBasis))
-> (DGraph, ProofBasis)
-> [[LEdge DGLinkLab]]
-> (DGraph, ProofBasis)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
      (Node
-> (DGraph, ProofBasis)
-> [LEdge DGLinkLab]
-> (DGraph, ProofBasis)
globDecompForOneEdgeAux Node
target) (DGraph
dgraph, ProofBasis
emptyProofBasis) [[LEdge DGLinkLab]]
paths
    provenEdge :: LEdge DGLinkLab
provenEdge = (Node
source, Node
target, DGLinkLab
edgeLab
        { dgl_type :: DGLinkType
dgl_type = ThmLinkStatus -> DGLinkType -> DGLinkType
setProof (DGRule -> ProofBasis -> ThmLinkStatus
Proven (EdgeId -> DGRule
globDecompRule (EdgeId -> DGRule) -> EdgeId -> DGRule
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> EdgeId
getEdgeId LEdge DGLinkLab
edge)
                                      ProofBasis
proof_basis)
            (DGLinkType -> DGLinkType) -> DGLinkType -> DGLinkType
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
edgeLab
        , dglPending :: Bool
dglPending = Bool
True
        , dgl_origin :: DGLinkOrigin
dgl_origin = DGLinkOrigin
DGLinkProof })
    in DGraph -> [DGChange] -> DGraph
changesDGH DGraph
newGr [LEdge DGLinkLab -> DGChange
DeleteEdge LEdge DGLinkLab
edge, LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
provenEdge]

{- auxiliary function for globDecompForOneEdge (above)
   actual implementation -}
globDecompForOneEdgeAux :: Node -> (DGraph, ProofBasis)
                        -> [LEdge DGLinkLab]
                        -> (DGraph, ProofBasis)
-- for each path an unproven localThm edge is inserted
globDecompForOneEdgeAux :: Node
-> (DGraph, ProofBasis)
-> [LEdge DGLinkLab]
-> (DGraph, ProofBasis)
globDecompForOneEdgeAux target :: Node
target (dgraph :: DGraph
dgraph, proof_basis :: ProofBasis
proof_basis) path :: [LEdge DGLinkLab]
path =
  case [LEdge DGLinkLab]
path of
    [] -> String -> (DGraph, ProofBasis)
forall a. HasCallStack => String -> a
error "globDecompForOneEdgeAux"
    (node :: Node
node, tar :: Node
tar, lbl :: DGLinkLab
lbl) : rpath :: [LEdge DGLinkLab]
rpath -> let
      lbltype :: DGLinkType
lbltype = DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lbl
      isHiding :: Bool
isHiding = DGLinkType -> Bool
isHidingDef DGLinkType
lbltype
      morphismPath :: [LEdge DGLinkLab]
morphismPath = if Bool
isHiding then [LEdge DGLinkLab]
rpath else [LEdge DGLinkLab]
path
      morphism :: GMorphism
morphism = GMorphism -> Maybe GMorphism -> GMorphism
forall a. a -> Maybe a -> a
fromMaybe
        (String -> GMorphism
forall a. HasCallStack => String -> a
error "globDecomp: could not determine morphism of new edge")
        (Maybe GMorphism -> GMorphism) -> Maybe GMorphism -> GMorphism
forall a b. (a -> b) -> a -> b
$ [LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath [LEdge DGLinkLab]
morphismPath
      defEdgesToTarget :: [LEdge DGLinkLab]
defEdgesToTarget = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter
        (\ (s :: Node
s, _, l :: DGLinkLab
l) -> Node
s Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
node Bool -> Bool -> Bool
&& DGLinkType -> Bool
isGlobalDef (DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l)
        Bool -> Bool -> Bool
&& DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
l GMorphism -> GMorphism -> Bool
forall a. Eq a => a -> a -> Bool
== GMorphism
morphism)
        ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> [LEdge DGLinkLab]
innDG DGraph
dgraph Node
target
      newEdgeLbl :: DGLinkLab
newEdgeLbl = GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink GMorphism
morphism
        (if Bool
isHiding then Node -> GMorphism -> DGLinkType
hidingThm Node
tar (GMorphism -> DGLinkType) -> GMorphism -> DGLinkType
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
lbl
            else if DGLinkType -> Bool
isGlobalDef DGLinkType
lbltype then DGLinkType
globalThm else DGLinkType
localThm)
        DGLinkOrigin
DGLinkProof
      newEdge :: LEdge DGLinkLab
newEdge = (Node
node, Node
target, DGLinkLab
newEdgeLbl)
      in case [LEdge DGLinkLab]
defEdgesToTarget of
      (_, _, dl :: DGLinkLab
dl) : _ | Bool -> Bool
not Bool
isHiding
             -> (DGraph
dgraph, ProofBasis -> EdgeId -> ProofBasis
addEdgeId ProofBasis
proof_basis (EdgeId -> ProofBasis) -> EdgeId -> ProofBasis
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> EdgeId
dgl_id DGLinkLab
dl)
      _ | Node
node Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
target Bool -> Bool -> Bool
&& DGEdgeType -> Bool
isInc (DGLinkLab -> DGEdgeType
getRealDGLinkType DGLinkLab
newEdgeLbl)
               Bool -> Bool -> Bool
&& DGLinkType -> Bool
isGlobalDef DGLinkType
lbltype
             -> (DGraph
dgraph, ProofBasis -> EdgeId -> ProofBasis
addEdgeId ProofBasis
proof_basis (EdgeId -> ProofBasis) -> EdgeId -> ProofBasis
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> EdgeId
dgl_id DGLinkLab
lbl)
      _ -> case LEdge DGLinkLab -> DGraph -> Maybe (LEdge DGLinkLab)
tryToGetEdge LEdge DGLinkLab
newEdge DGraph
dgraph of
        Nothing -> let
          newGraph :: DGraph
newGraph = DGraph -> DGChange -> DGraph
changeDGH DGraph
dgraph (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
newEdge
          finalEdge :: LEdge DGLinkLab
finalEdge = case DGraph -> DGChange
getLastChange DGraph
newGraph of
            InsertEdge final_e :: LEdge DGLinkLab
final_e -> LEdge DGLinkLab
final_e
            _ -> String -> LEdge DGLinkLab
forall a. HasCallStack => String -> a
error "Proofs.Global.globDecompForOneEdgeAux"
          in (DGraph
newGraph, ProofBasis -> EdgeId -> ProofBasis
addEdgeId ProofBasis
proof_basis (EdgeId -> ProofBasis) -> EdgeId -> ProofBasis
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> EdgeId
getEdgeId LEdge DGLinkLab
finalEdge)
        Just e :: LEdge DGLinkLab
e -> (DGraph
dgraph, ProofBasis -> EdgeId -> ProofBasis
addEdgeId ProofBasis
proof_basis (EdgeId -> ProofBasis) -> EdgeId -> ProofBasis
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> EdgeId
getEdgeId LEdge DGLinkLab
e)

globSubsumeFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
globSubsumeFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
globSubsumeFromList ln :: LibName
ln globalThmEdges :: [LEdge DGLinkLab]
globalThmEdges libEnv :: LibEnv
libEnv =
    let dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libEnv
        finalGlobalThmEdges :: [LEdge DGLinkLab]
finalGlobalThmEdges = (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
isUnprovenGlobalThm) [LEdge DGLinkLab]
globalThmEdges
        nextDGraph :: DGraph
nextDGraph = (DGraph -> LEdge DGLinkLab -> DGraph)
-> DGraph -> [LEdge DGLinkLab] -> DGraph
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
            (LibEnv -> DGraph -> LEdge DGLinkLab -> DGraph
globSubsumeAux LibEnv
libEnv) DGraph
dgraph [LEdge DGLinkLab]
finalGlobalThmEdges
    in LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
nextDGraph LibEnv
libEnv

-- | tries to apply global subsumption to all unproven global theorem edges
globSubsume :: LibName -> LibEnv -> LibEnv
globSubsume :: LibName -> LibEnv -> LibEnv
globSubsume ln :: LibName
ln libEnv :: LibEnv
libEnv =
    let dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libEnv
        globalThmEdges :: [LEdge DGLinkLab]
globalThmEdges = DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dgraph
    in LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
globSubsumeFromList LibName
ln [LEdge DGLinkLab]
globalThmEdges LibEnv
libEnv

-- auxiliary function for globSubsume (above) the actual implementation
globSubsumeAux :: LibEnv -> DGraph -> LEdge DGLinkLab -> DGraph
globSubsumeAux :: LibEnv -> DGraph -> LEdge DGLinkLab -> DGraph
globSubsumeAux libEnv :: LibEnv
libEnv dgraph :: DGraph
dgraph ledge :: LEdge DGLinkLab
ledge@(src :: Node
src, tgt :: Node
tgt, edgeLab :: DGLinkLab
edgeLab) =
  let morphism :: GMorphism
morphism = DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
edgeLab
      filteredPaths :: [[LEdge DGLinkLab]]
filteredPaths = GMorphism -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
filterPathsByMorphism GMorphism
morphism ([[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]])
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> a -> b
$ ([LEdge DGLinkLab] -> Bool)
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a. (a -> Bool) -> [a] -> [a]
filter (LEdge DGLinkLab -> [LEdge DGLinkLab] -> Bool
noPath LEdge DGLinkLab
ledge)
                    ([[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]])
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllGlobPathsBetween DGraph
dgraph Node
src Node
tgt
      proofbasis :: ProofBasis
proofbasis = DGraph -> LEdge DGLinkLab -> [[LEdge DGLinkLab]] -> ProofBasis
selectProofBasis DGraph
dgraph LEdge DGLinkLab
ledge [[LEdge DGLinkLab]]
filteredPaths
  in if Bool -> Bool
not (ProofBasis -> Bool
nullProofBasis ProofBasis
proofbasis) Bool -> Bool -> Bool
|| LEdge DGLinkLab -> LibEnv -> DGraph -> Bool
isIdentityEdge LEdge DGLinkLab
ledge LibEnv
libEnv DGraph
dgraph
   then
     let globSubsumeRule :: DGRule
globSubsumeRule = String -> EdgeId -> DGRule
DGRuleWithEdge "Global-Subsumption"
           (EdgeId -> DGRule) -> EdgeId -> DGRule
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> EdgeId
getEdgeId LEdge DGLinkLab
ledge
         newEdge :: LEdge DGLinkLab
newEdge = (Node
src, Node
tgt, DGLinkLab
edgeLab
               { dgl_type :: DGLinkType
dgl_type = ThmLinkStatus -> DGLinkType -> DGLinkType
setProof (DGRule -> ProofBasis -> ThmLinkStatus
Proven DGRule
globSubsumeRule ProofBasis
proofbasis)
                   (DGLinkType -> DGLinkType) -> DGLinkType -> DGLinkType
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
edgeLab
               , dgl_origin :: DGLinkOrigin
dgl_origin = DGLinkOrigin
DGLinkProof })
         newDGraph :: DGraph
newDGraph = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dgraph [LEdge DGLinkLab -> DGChange
DeleteEdge LEdge DGLinkLab
ledge, LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
newEdge]
     in DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dgraph DGRule
globSubsumeRule DGraph
newDGraph
   else DGraph
dgraph