{-# LANGUAGE RankNTypes #-}
{- |
Module : ./Static/ChangeGraph.hs
Description : functions for changing a development graphs
Copyright : (c) Christian Maeder, DFKI GmbH 2009
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : non-portable(Logic)
functions to manipulate a development graph for change management
All of the following functions may fail, therefore the result type should
not be taken literally, but maybe changed to some monadic result type.
Also all functions modify an development graph when the are successful, which
may be captured by some form of a state monad.
-}
module Static.ChangeGraph where
import Static.DgUtils
import Static.GTheory
import Static.DevGraph
import Static.History
import Logic.Grothendieck
import Common.AS_Annotation
import Common.Consistency
import qualified Common.OrderedMap as OMap
import Common.Result
import Data.Graph.Inductive.Graph as Graph
import qualified Data.Set as Set
import Data.List
import Control.Monad
-- * deleting and adding nodes
{- | delete a node.
If a node is deleted all in- and outgoing links will be lost. This is intended
for ingoing definitions links. The targets of outgoing definitions links (aka
"depending nodes") need to me marked as "reduced".
theorem links from A to B state that all sentences in A can be proven by the
axioms (and proven theorems) from B (note the reversal). This means the
sentences of A are translated and moved to B as theorems (to be proven) by
"local inference".
removing ingoing theorem links means: we loose properties of B, which is no
problem since we delete B. (If we just delete the theorem link we must inform
depending nodes that fewer axioms are now available. Since a proof for the
link will be lost other proofs in depending nodes may become invalid.)
removing outgoing (local) theorem links means: target nodes may contain theorems
from the source node that need to be deleted, too. So these nodes are
"reduced" (fewer theorems only). (We do not keep even valid theorems, if we
are told to delete them.)
The node to be deleted may have been subject to global decomposition. So
outgoing global theorems of depending nodes may get a deleted edge-id in
their proof-basis, that should be deleted, too.
Outgoing theorem links of source nodes that have definition links to the
target node to be deleted may be theorem links created by global decomposition
which should be deleted, too.
So, when deleting a node, let's delete the edges in reverse order of their
creation. remove:
- (outgoing) local theorem links (with reversal of "local-inference")
whose corresponding global theorem link has only this local theorem link
as proof basis.
- sentences in targets are removed (or the target is deleted node anyway)
(if the local theorem was proven)
- corresponding global theorem links become unproven again and loose
their proof basis (or are deleted together with the node)
- unproven global theorem links (with reversal of "global-decomposition")
- the proof basis of other proven global theorem links with the same
target is reduced and marked as incomplete (since a corresponding local
theorem link and the definition link is not deleted yet).
- so proven global theorems links are removed after removing the links in
their proof basis first
- outgoing definition links
- target nodes need to be marked as reduced (outgoing global theorem links
may become complete again)
(Proofs relying on imported axioms become invalid, provided the sentence
are still well-formed in the reduced signature)
- ingoing definition links
this just marks the current node as reduced which will be deleted later
Later on reduced nodes need to be re-computed possibly causing depending nodes
to become reduced. Incomplete global theorem links need to be completed (by
the user).
If the node index is unknown then auxiliary functions (or a mapping between
node names and node indices) can be supplied to delete nodes by name. -}
deleteDGNode :: Node -> DGraph -> Result DGraph
deleteDGNode t dg = case fst . match t $ dgBody dg of
Just (ins, _, nl, outs) -> case dgn_nf nl of
Just n -> do
dg2 <- deleteDGNode n dg
deleteDGNode t $ changeDGH dg2 $ SetNodeLab nl
(t, nl { dgn_nf = Nothing, dgn_sigma = Nothing })
Nothing -> case dgn_freenf nl of
Just n -> do
dg2 <- deleteDGNode n dg
deleteDGNode t $ changeDGH dg2 $ SetNodeLab nl
(t, nl { dgn_freenf = Nothing, dgn_phi = Nothing })
Nothing ->
if null $ ins ++ outs then return $ changeDGH dg $ DeleteNode (t, nl)
else do
dg2 <- foldM (\ dgx (el, sr) -> delDGLink (Just sr) t (dgl_id el) dgx)
dg ins
dg3 <- foldM (\ dgx (el, rt) -> delDGLink (Just t) rt (dgl_id el) dgx)
dg2 outs
deleteDGNode t dg3
_ -> justWarn dg $ "node not in graph: " ++ show t
{- | add a node supplying the necessary information.
We should allow to add a node without knowing its final signature. We just
know the 'XNode' information. Later on definition and theorem links may be
added. Only after all ingoing definition links (and their sources) are known
we can compute the actual signature (and theory).
The node index will be new and returned. The name should be unique. The theory
is a closed signature plus local sentences. The origin could be anything (to
be added yet), but for basic specs it is the list of the newly introduced
symbols.
The required conservativity is some value from
`Common.Consistency.Conservativity' like usually 'None' or 'Cons'.
Reference nodes can not be added this way. Also the references and morphisms
to normal forms for hiding or free links cannot be set this way. So further
function are needed. -}
addDGNode :: NodeName -> G_theory -> DGOrigin -> Conservativity -> DGraph
-> Result (DGraph, Node)
addDGNode nn th o cs dg = let
n = getNewNodeDG dg
inf = newConsNodeInfo o cs
sn = showName nn
nl = newInfoNodeLab nn inf th
in case lookupNodeByName sn dg of
[] -> return (changeDGH dg $ InsertNode (n, nl), n)
ns -> fail $ "node name '" ++ sn
++ "' already defined in graph for node(s): "
++ show (map fst ns)
-- | Maybe a function to rename nodes is desirable
renameNode :: Node -> NodeName -> DGraph -> Result DGraph
renameNode n nn dg = let
sn = showName nn
nl = labDG dg n
in case lookupNodeByName sn dg of
[] -> return $ changeDGH dg $ SetNodeLab nl (n, nl { dgn_name = nn })
ns -> fail $ "node name '" ++ sn
++ "' already defined in graph for node(s): "
++ show (map fst ns)
-- * deleting and adding links
{- | delete a link given the source and target node by index and the edge-id.
Edge-ids are globally unique, but locating source and target nodes would be
inefficient if not given.
Getting the edge-id if only source node name, target
node name, link type, possibly an origin, and the link morphism is given,
needs auxiliary functions.
Edge-ids maybe reused.
Local theorem links are proven by moving sentences from the source to target
node and changing them to theorems. So if such a proven local theorem link is
removed the target node needs to be reduced, too.
target nodes of definition links are "reduced" (see deleteDGNode)
-}
delDGLink :: Maybe Node -> Node -> EdgeId -> DGraph -> Result DGraph
delDGLink ms t i dg = let
(ins, _, nl, loopsAndOuts) = safeContextDG "delDGLink" dg t
loops = filter ((== t) . snd) loopsAndOuts
allIns = loops ++ ins
in case partition ((== i) . dgl_id . fst) allIns of
([], _) -> justWarn dg $ "link not found: " ++ show (t, i)
((lbl, s) : os, rs) -> do
unless (null os) $ justWarn ()
$ "ambiguous link: " ++ shows (t, i) " other sources are: "
++ show (map snd os)
case ms of
Just sr | sr /= s -> fail
$ "non-matching source node: " ++ show (s, t, i)
++ " given: " ++ show sr
_ -> let delE dg' = return $ changeDGH dg' $ DeleteEdge (s, t, lbl)
-- links proven by current link
gs = filter (edgeInProofBasis i . getProofBasis . fst) rs
dgCh = changeDGH dg $ SetNodeLab nl (t, updNodeMod delSymMod nl)
delDef = delE dgCh
in case dgl_type lbl of
ScopedLink lOrG lk _ -> case lOrG of
Local -> do
dg2 <- case lk of
ThmLink (Proven (DGRuleLocalInference renms) _) -> do
nl2 <- deleteDGNodeSens (\ nSen -> not (isAxiom nSen)
&& senAttr nSen `elem` map snd renms) nl
return $ updDGNodeLab dg nl (t, nl2)
_ -> return dg
-- find global link(s) that contain(s) the edge-id as proof-basis
let dg3 = invalDGLinkProofs dg2 $ map (\ (l, sr) -> (sr, t, l)) gs
delE dg3
Global -> case lk of
ThmLink pst -> let
pB = proofBasisOfThmLinkStatus pst
{- delete all links created by global decomposition,
(this may delete also manually inserted theorem links!)
all links have the same target. -}
createdLinks =
filter ((`edgeInProofBasis` pB) . dgl_id . fst) rs
in if null createdLinks then
let dg3 = invalDGLinkProofs dg
$ map (\ (l, sr) -> (sr, t, l)) gs
in delE dg3
else do
dg2 <- foldM (\ dgx (el, sr) ->
delDGLink (Just sr) t (dgl_id el) dgx) dg createdLinks
delDGLink ms t i dg2
DefLink -> delDef
HidingFreeOrCofreeThm {} -> delE dg
{- just delete the theorem link, we don't know what links can be
in the proof basis by the shifting rules -}
_ -> delDef -- delete other def links
updNodeMod :: NodeMod -> DGNodeLab -> DGNodeLab
updNodeMod m nl = nl { nodeMod = mergeNodeMod m $ nodeMod nl }
updDGNodeLab :: DGraph
-> DGNodeLab -- ^ old label
-> LNode DGNodeLab -- ^ node with new label
-> DGraph
updDGNodeLab dg l n = let
dg0 = changeDGH dg $ SetNodeLab l n
in togglePending dg0 $ changedLocalTheorems dg0 n
deleteDGNodeSens :: (forall a . Named a -> Bool) -> DGNodeLab
-> Result DGNodeLab
deleteDGNodeSens p nl = case dgn_theory nl of
G_theory lid s si sens _ ->
case OMap.partitionWithKey (\ n -> p . reName (const n)) sens of
(del, rest) -> let
es = OMap.elems del
chg | all isAxiom es = delAxMod
| all (not . isAxiom) es = delThMod
| otherwise = delSenMod
in if OMap.null del
then justWarn nl $ "no sentence deleted in: " ++ getDGNodeName nl
else return $ updNodeMod chg $ nl
{ dgn_theory = G_theory lid s si rest startThId }
invalidateDGLinkProof :: DGLinkLab -> DGLinkLab
invalidateDGLinkProof el = el { dgl_type = setProof LeftOpen $ dgl_type el }
invalDGLinkProof :: LEdge DGLinkLab -> [DGChange]
invalDGLinkProof e@(s, t, l) =
[DeleteEdge e, InsertEdge (s, t, invalidateDGLinkProof l)]
invalDGLinkProofs :: DGraph -> [LEdge DGLinkLab] -> DGraph
invalDGLinkProofs dg = changesDGH dg . concatMap invalDGLinkProof
{- | add a link supplying the necessary information.
Morphisms do not store source and target signatures. Only the source signature
is taken from the node. The induced signature of the morphism will be a
subsignature of the target signature.
- adding an (unproven) global theorem link:
this states that more theorems are supposed to hold in target nodes.
- adding a global definition link:
- the signature of the target is enlarged (Proofs remain valid).
- proven outgoing global theorem links for new ingoing definition links may
become unproven and incomplete
- outgoing local theorem links for new ingoing definition links add proof
obligations the target nodes of the local theorem links.
Additional theorems need to be moved or we mark the proven local theorem
link as incomplete.
The link type may also contain a conservativity and isn't easy to set up for
free and hiding links. The origin is again basically for documentation
purposes.
The returned edge-id will be new or an edge-id may be supplied as input. -}
addDGLink :: Node -> Node -> GMorphism -> DGLinkType -> DGLinkOrigin -> DGraph
-> (DGraph, EdgeId)
addDGLink = undefined
-- * modifying links
{- | Do we need functions to modify links?
Yes, later, for example, if a conservativity as part of the link type should
be set or changed.
Some link types contain proof information that needs to be kept up-to-date.
For example, a global theorem link will (after decomposition) refer to a local
theorem link and maybe another global theorem link. A local theorem link will
(after local inference) refer to (possibly renamed) theorems in the target
node.
Maybe some more thoughts are needed to decide which link type information may
be set or changed explicitely and which information should be adjusted
automatically. -}
modifyDGLinkType :: Node -> Node -> EdgeId -> DGLinkType -> DGraph -> DGraph
modifyDGLinkType = undefined
{- |
If the link morphism should change, this most likely (but not necessarily)
involves signature changes of the source or target node (or both nodes).
In the latter case, either the old link was invalidated before, by changing
the signature of the source or target node, or the modification of the link
will invalidate the contents of the source or target.
Instead of tricky morphism changes it may be better to simply delete old edges
and nodes and reinsert new nodes and edges propagating some old attributes. -}
modifyDGLinkMorphism :: Node -> Node -> EdgeId -> GMorphism -> DGraph -> DGraph
modifyDGLinkMorphism = undefined
-- | Modifying the documenting link origin should also be possible.
modifyDGLinkOrigin :: Node -> Node -> EdgeId -> DGLinkOrigin -> DGraph -> DGraph
modifyDGLinkOrigin = undefined
-- * modifying the signature of a node
{- | replace the signature of a node.
This function should be used as basis to add or delete symbols from a node.
Changing the signature means that the codomain of incoming and the domain of
outgoing links change. Therefore we would invalidate all attached links and
expect further link morphism modifications to adjust these links.
If the signature is not enlarged some local sentences may become invalid.
Therefore the class logic must supply a checking function that takes a
signature and a sentence and checks if the sentence is still well-formed
according to the given signature. A logic specific implementation my choose to
first extract all symbols from a sentence and compare it to the set of
signature symbols. (Extracting symbols from sentences is no method of the
class logic.)
Since there are functions to remove sentences explicitely, we leave it to the
user to remove sentences first before reducing or changing the signature and
simply fail if invalid sentences are left! -}
setSignature :: Node -> G_sign -> DGraph -> DGraph
setSignature = undefined
{- | delete symbols from a node's signature.
Deleting symbols is a special case of setting a node's signature. The new
signature is computed using the method for the co-generated signature that is
also used when symbols are hidden.
It is only checked that the symbol set difference of the new and old signature
corresponds to the supplied symbol set. (Alternatively it could be checked if
the new signature is a sub-signature of the old one.)
The target nodes of outgoing definition links will be adjusted according to
the reduced closed signature automatically.
Invalid sentences should have been removed before.
This function can be easily extended to delete raw symbol via the logic
specific matching between raw and signature symbols. -}
deleteSymbols :: Node -> Set.Set G_symbol -> DGraph -> DGraph
deleteSymbols = undefined
{- | extending a node's signature.
Adding symbols requires the new signature directly supplied as argument, since
the class logic supplies no way to extend a signature by a given set of
symbols. In fact symbols can only be extracted from a given signature.
It is only checked if the old signature is a sub-signature of the new one.
Sentences are not checked, because fully analyzed sentences are expected to
remain well-formed in an enlarged signature, although re-parsing and
type-checking may fail for the syntactic representation of these sentences.
It is, however, possible to extend a given signature by a basic spec as
happens for usual spec extensions, but note that the basic analysis may also
yield sentences that might need to be added separately.
Again target nodes of outgoing definition links will be adjusted
automatically. -}
extendSignature :: Node -> G_sign -> DGraph -> DGraph
extendSignature = undefined
-- * modifying local sentences of a node
{- | a logic independent sentence data type, yet missing in Logic.Grothendieck
Local sentences have been either directly added or have been inserted by
local inference. Sentences inserted by local inference should not be
manipulated at the target node but only at the original source. But maybe it
should be possible to delete such sentences explicitly to match the
corresponding deletion of the proven local theorem link? Alternatively a
function to undo a local inference step could be applied.
All sentences are uniquely named. User given duplicate names or missing names
are removed by generating unique names.
If additional sentences are added by local inference they may be
renamed to ensure unique names. The renaming is stored to keep the
correspondence to the original sentences.
The global theory of node should be computed if needed but is cached for
efficiency reason. It contains all sentences as axioms along incoming
definition links. All these axioms may be used to prove a theorem, assuming
that the used axioms are valid in their original theory.
So a change of a sentence may invalidate proofs in nodes reachable via theorem
or definition links. -}
data GSentence = GSentence
{- | delete the sentences that fulfill the given predicate.
Should this function fail if the predicate does not determine a unique
sentence? Surely, simply all sentences could be deleted fulfilling the
predicate (possibly none). -}
deleteSentence :: Node -> (Named GSentence -> Bool) -> DGraph -> Result DGraph
deleteSentence = undefined
{- | delete a sentence by name
This is a more efficient version of deleting a single sentence. All sentences
of one node have a unique name, but it may be a generated name that the user
needs to look up.
Only sentences not inserted by local inference can be deleted.
-}
deleteSentenceByName :: Node -> String -> DGraph -> DGraph
deleteSentenceByName = undefined
{- | add a sentence.
The unproven named sentence given as argument is added as new sentence. The
name must be different from those of all other sentences, including those
inserted by local inference.
Adding axioms will not invalidate proofs (if the logic is monotone), but the
addition may trigger the addition of theorems in a neighbor node if linked to
via a proven local theorem link. Theorems are not propagated further.
Sentences can not be added with some old proof, that could be retried by the
corresponding prover. -}
addSentence :: Node -> Named GSentence -> DGraph -> DGraph
addSentence = undefined
{- | It may be desirable to rename sentences or change there role (axiom or
theorem) and even to invalid but keep an old proof. -}
changeSentence :: Node -> (Named GSentence -> Named GSentence) -> DGraph
-> DGraph
changeSentence = undefined