{- |
Module      :  ./Proofs/Local.hs
Description :  local proof rules for development graphs
Copyright   :  (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable(Logic)

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

{-

Order of rule application: try to use local links induced by %implies
for subsumption proofs (such that the %implied formulas need not be
re-proved)

-}

module Proofs.Local
    ( localInference
    , locDecomp
    , locDecompFromList
    , localInferenceFromList
    ) where

import Proofs.EdgeUtils
import Proofs.StatusUtils

import Logic.Grothendieck
import Logic.Prover

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

import Common.AS_Annotation
import Common.LibName
import Common.Result
import qualified Common.OrderedMap as OMap

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

-- | local decomposition
locDecompFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
locDecompFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
locDecompFromList ln :: LibName
ln localThmEdges :: [LEdge DGLinkLab]
localThmEdges libEnv :: LibEnv
libEnv =
   let dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libEnv
       finalLocalThmEdges :: [LEdge DGLinkLab]
finalLocalThmEdges = (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
isUnprovenLocalThm) [LEdge DGLinkLab]
localThmEdges
       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 -> LibName -> DGraph -> LEdge DGLinkLab -> DGraph
locDecompAux LibEnv
libEnv LibName
ln) DGraph
dgraph [LEdge DGLinkLab]
finalLocalThmEdges
   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

-- | local decomposition for all edges
locDecomp :: LibName -> LibEnv -> LibEnv
locDecomp :: LibName -> LibEnv -> LibEnv
locDecomp ln :: LibName
ln libEnv :: LibEnv
libEnv =
    let dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libEnv
        localThmEdges :: [LEdge DGLinkLab]
localThmEdges = DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dgraph
    in LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
locDecompFromList LibName
ln [LEdge DGLinkLab]
localThmEdges LibEnv
libEnv

{- auxiliary function for locDecomp (above)
   actual implementation -}
locDecompAux :: LibEnv -> LibName -> DGraph -> LEdge DGLinkLab -> DGraph
locDecompAux :: LibEnv -> LibName -> DGraph -> LEdge DGLinkLab -> DGraph
locDecompAux libEnv :: LibEnv
libEnv ln :: LibName
ln 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
    allPaths :: [[LEdge DGLinkLab]]
allPaths = DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllLocGlobPathsBetween DGraph
dgraph Node
src Node
tgt
    th :: Maybe G_theory
th = LibEnv -> LibName -> Node -> Maybe G_theory
forall (m :: * -> *).
Monad m =>
LibEnv -> LibName -> Node -> m G_theory
computeLocalTheory LibEnv
libEnv LibName
ln Node
src
    pathsWithoutEdgeItself :: [[LEdge DGLinkLab]]
pathsWithoutEdgeItself = ([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]]
allPaths
    filteredPaths :: [[LEdge DGLinkLab]]
filteredPaths = Maybe G_theory
-> GMorphism -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
filterByTranslation Maybe G_theory
th GMorphism
morphism [[LEdge DGLinkLab]]
pathsWithoutEdgeItself
    proofbasis :: ProofBasis
proofbasis = DGraph -> LEdge DGLinkLab -> [[LEdge DGLinkLab]] -> ProofBasis
selectProofBasis DGraph
dgraph LEdge DGLinkLab
ledge [[LEdge DGLinkLab]]
filteredPaths
    auxGraph :: DGraph
auxGraph = DGraph -> DGChange -> DGraph
changeDGH DGraph
dgraph (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGChange
DeleteEdge LEdge DGLinkLab
ledge
    locDecompRule :: DGRule
locDecompRule = String -> EdgeId -> DGRule
DGRuleWithEdge "Local-Decomposition" (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
locDecompRule 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 })
    newGraph :: DGraph
newGraph = LEdge DGLinkLab -> DGraph -> DGraph
insertDGLEdge LEdge DGLinkLab
newEdge DGraph
auxGraph
    in if Bool -> Bool
not (LEdge DGLinkLab -> LibEnv -> DGraph -> Bool
isIdentityEdge LEdge DGLinkLab
ledge LibEnv
libEnv DGraph
dgraph) Bool -> Bool -> Bool
&& ProofBasis -> Bool
nullProofBasis ProofBasis
proofbasis
     then DGraph
dgraph else
     DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dgraph DGRule
locDecompRule DGraph
newGraph


{- | removes all paths from the given list of paths whose morphism does
not translate the given sentence list to the same resulting sentence
list as the given morphism. -}
filterByTranslation :: Maybe G_theory -> GMorphism -> [[LEdge DGLinkLab]]
                    -> [[LEdge DGLinkLab]]
filterByTranslation :: Maybe G_theory
-> GMorphism -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
filterByTranslation maybeTh :: Maybe G_theory
maybeTh morphism :: GMorphism
morphism paths :: [[LEdge DGLinkLab]]
paths =
  case Maybe G_theory
maybeTh of
    Just th :: G_theory
th -> ([LEdge DGLinkLab] -> Bool)
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a. (a -> Bool) -> [a] -> [a]
filter (G_theory -> GMorphism -> [LEdge DGLinkLab] -> Bool
isSameTranslation G_theory
th GMorphism
morphism) [[LEdge DGLinkLab]]
paths
    Nothing -> []

{- | checks if the given morphism and the morphism of the given path
translate the given sentence list to the same resulting sentence list. -}
isSameTranslation :: G_theory -> GMorphism -> [LEdge DGLinkLab] -> Bool
isSameTranslation :: G_theory -> GMorphism -> [LEdge DGLinkLab] -> Bool
isSameTranslation th :: G_theory
th morphism :: GMorphism
morphism path :: [LEdge DGLinkLab]
path =
  case [LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath [LEdge DGLinkLab]
path of
      Just morphismOfPath :: GMorphism
morphismOfPath ->
         Result G_theory -> Maybe G_theory
forall a. Result a -> Maybe a
maybeResult (GMorphism -> G_theory -> Result G_theory
translateG_theory GMorphism
morphism G_theory
th) Maybe G_theory -> Maybe G_theory -> Bool
forall a. Eq a => a -> a -> Bool
==
                     Result G_theory -> Maybe G_theory
forall a. Result a -> Maybe a
maybeResult (GMorphism -> G_theory -> Result G_theory
translateG_theory GMorphism
morphismOfPath G_theory
th)
      Nothing -> Bool
False

-- | local inference
localInferenceFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
localInferenceFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
localInferenceFromList ln :: LibName
ln localThmEdges :: [LEdge DGLinkLab]
localThmEdges libEnv :: LibEnv
libEnv =
    LibName -> LibEnv -> DGraph -> [LEdge DGLinkLab] -> LibEnv
localInferenceFromAux LibName
ln LibEnv
libEnv (LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libEnv) [LEdge DGLinkLab]
localThmEdges

localInferenceFromAux :: LibName -> LibEnv -> DGraph -> [LEdge DGLinkLab]
  -> LibEnv
localInferenceFromAux :: LibName -> LibEnv -> DGraph -> [LEdge DGLinkLab] -> LibEnv
localInferenceFromAux ln :: LibName
ln libEnv :: LibEnv
libEnv dgraph :: DGraph
dgraph localThmEdges :: [LEdge DGLinkLab]
localThmEdges =
   let finalLocalThmEdges :: [LEdge DGLinkLab]
finalLocalThmEdges = (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
isUnprovenLocalThm) [LEdge DGLinkLab]
localThmEdges
       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
localInferenceAux LibEnv
libEnv) DGraph
dgraph [LEdge DGLinkLab]
finalLocalThmEdges
   in LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln (LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories LibEnv
libEnv LibName
ln DGraph
nextDGraph) LibEnv
libEnv

-- | local inference for all edges
localInference :: LibName -> LibEnv -> LibEnv
localInference :: LibName -> LibEnv -> LibEnv
localInference ln :: LibName
ln libEnv :: LibEnv
libEnv =
    let dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libEnv
        localThmEdges :: [LEdge DGLinkLab]
localThmEdges = DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dgraph
    in LibName -> LibEnv -> DGraph -> [LEdge DGLinkLab] -> LibEnv
localInferenceFromAux LibName
ln LibEnv
libEnv DGraph
dgraph [LEdge DGLinkLab]
localThmEdges

-- auxiliary method for localInference
localInferenceAux :: LibEnv -> DGraph -> LEdge DGLinkLab -> DGraph
localInferenceAux :: LibEnv -> DGraph -> LEdge DGLinkLab -> DGraph
localInferenceAux 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
    maybeThSrc :: Maybe G_theory
maybeThSrc = LibEnv -> DGraph -> Node -> Maybe G_theory
forall (m :: * -> *).
Monad m =>
LibEnv -> DGraph -> Node -> m G_theory
computeLocalNodeTheory LibEnv
libEnv DGraph
dgraph Node
src
    oldContents :: DGNodeLab
oldContents = DGraph -> Node -> DGNodeLab
labDG DGraph
dgraph Node
tgt
    in case Maybe G_theory
maybeThSrc of
    Just thSrc :: G_theory
thSrc ->
      case (LibEnv -> DGraph -> Node -> Maybe G_theory
forall (m :: * -> *).
Monad m =>
LibEnv -> DGraph -> Node -> m G_theory
computeLocalNodeTheory LibEnv
libEnv DGraph
dgraph Node
tgt,
                        Result G_theory -> Maybe G_theory
forall a. Result a -> Maybe a
maybeResult (Result G_theory -> Maybe G_theory)
-> Result G_theory -> Maybe G_theory
forall a b. (a -> b) -> a -> b
$ GMorphism -> G_theory -> Result G_theory
translateG_theory GMorphism
morphism G_theory
thSrc) of
        (Just th :: G_theory
th@(G_theory lidTgt :: lid
lidTgt syn :: Maybe IRI
syn sig :: ExtSign sign symbol
sig ind :: SigId
ind sensTgt :: ThSens sentence (AnyComorphism, BasicProof)
sensTgt _),
              Just (G_theory lidSrc :: lid
lidSrc _ _ _ sentensSrc :: ThSens sentence (AnyComorphism, BasicProof)
sentensSrc _)) ->
          case Result (ThSens sentence (AnyComorphism, BasicProof))
-> Maybe (ThSens sentence (AnyComorphism, BasicProof))
forall a. Result a -> Maybe a
maybeResult (lid
-> lid
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> Result (ThSens sentence (AnyComorphism, BasicProof))
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *) b.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m, Typeable b) =>
lid1
-> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
coerceThSens lid
lidSrc lid
lidTgt "" ThSens sentence (AnyComorphism, BasicProof)
sentensSrc) of
            Nothing -> DGraph
dgraph
            Just sensSrc :: ThSens sentence (AnyComorphism, BasicProof)
sensSrc ->
              -- check if all source axioms are also axioms in the target
              let goals :: ThSens sentence (AnyComorphism, BasicProof)
goals = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom ThSens sentence (AnyComorphism, BasicProof)
sensSrc
                  goals' :: ThSens sentence (AnyComorphism, BasicProof)
goals' = ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall a b. Ord a => ThSens a b -> ThSens a b
markAsGoal ThSens sentence (AnyComorphism, BasicProof)
goals
                  noGoals :: Bool
noGoals = ThSens sentence (AnyComorphism, BasicProof) -> Bool
forall k a. Map k a -> Bool
Map.null ThSens sentence (AnyComorphism, BasicProof)
goals'
                  (newSens :: ThSens sentence (AnyComorphism, BasicProof)
newSens, renms :: [(String, String)]
renms) = ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
-> (ThSens sentence (AnyComorphism, BasicProof),
    [(String, String)])
forall a b.
(Ord a, Eq b) =>
ThSens a b -> ThSens a b -> (ThSens a b, [(String, String)])
joinSensAux ThSens sentence (AnyComorphism, BasicProof)
sensTgt ThSens sentence (AnyComorphism, BasicProof)
goals'
                  provenSens :: ThSens sentence (AnyComorphism, BasicProof)
provenSens = lid
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
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
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
proveSens lid
lidTgt ThSens sentence (AnyComorphism, BasicProof)
newSens
                  pendingGoals :: Bool
pendingGoals =
                    (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus
                         (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> (String
    -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> String
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> Maybe (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
forall a. a -> Maybe a -> a
fromMaybe (String -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
forall a. HasCallStack => String -> a
error "localInferenceAux")
                         (Maybe (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
 -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> (String
    -> Maybe
         (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))))
-> String
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
 -> ThSens sentence (AnyComorphism, BasicProof)
 -> Maybe
      (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))))
-> ThSens sentence (AnyComorphism, BasicProof)
-> String
-> Maybe (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
forall a b c. (a -> b -> c) -> b -> a -> c
flip String
-> ThSens sentence (AnyComorphism, BasicProof)
-> Maybe (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
forall (m :: * -> *) k a.
(MonadFail m, Ord k) =>
k -> OMap k a -> m a
OMap.lookup ThSens sentence (AnyComorphism, BasicProof)
provenSens)
                        ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, String) -> String
forall a b. (a, b) -> b
snd [(String, String)]
renms
                  newTh :: G_theory
newTh = if Bool
noGoals then G_theory
th else
                    lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> 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
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lidTgt Maybe IRI
syn ExtSign sign symbol
sig SigId
ind ThSens sentence (AnyComorphism, BasicProof)
provenSens ThId
startThId
                  newContents :: DGNodeLab
newContents = DGNodeLab
oldContents { dgn_theory :: G_theory
dgn_theory = G_theory
newTh }
                  locInferRule :: DGRule
locInferRule = [(String, String)] -> DGRule
DGRuleLocalInference [(String, String)]
renms
                  newLab :: DGLinkLab
newLab = DGLinkLab
edgeLab
                    { dgl_type :: DGLinkType
dgl_type = ThmLinkStatus -> DGLinkType -> DGLinkType
setProof (DGRule -> ProofBasis -> ThmLinkStatus
Proven DGRule
locInferRule ProofBasis
emptyProofBasis)
                        (DGLinkType -> DGLinkType) -> DGLinkType -> DGLinkType
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
edgeLab
                    , dgl_origin :: DGLinkOrigin
dgl_origin = DGLinkOrigin
DGLinkProof
                    , dglPending :: Bool
dglPending = Bool
pendingGoals }
                  newEdge :: LEdge DGLinkLab
newEdge = (Node
src, Node
tgt, DGLinkLab
newLab)
                  newGraph0 :: DGraph
newGraph0 = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dgraph
                     ([DGChange] -> DGraph) -> [DGChange] -> DGraph
forall a b. (a -> b) -> a -> b
$ (if Bool
noGoals then [] else
                         [DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
oldContents (Node
tgt, DGNodeLab
newContents)])
                         [DGChange] -> [DGChange] -> [DGChange]
forall a. [a] -> [a] -> [a]
++ [LEdge DGLinkLab -> DGChange
DeleteEdge LEdge DGLinkLab
ledge, LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
newEdge]
                  newGraph :: DGraph
newGraph =
                    DGraph -> [LEdge DGLinkLab] -> DGraph
togglePending DGraph
newGraph0 ([LEdge DGLinkLab] -> DGraph) -> [LEdge DGLinkLab] -> DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> [LEdge DGLinkLab]
changedPendingEdges DGraph
newGraph0
              in DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dgraph DGRule
locInferRule DGraph
newGraph
        _ -> DGraph
dgraph
    _ -> DGraph
dgraph