446N/A{-# LANGUAGE RankNTypes #-}
446N/ADescription : functions for changing a development graphs
446N/ACopyright : (c) Christian Maeder, DFKI GmbH 2009
446N/AMaintainer : Christian.Maeder@dfki.de
446N/APortability : non-portable(Logic)
446N/Afunctions to manipulate a development graph for change management
446N/AAll of the following functions may fail, therefore the result type should
446N/Anot be taken literally, but maybe changed to some monadic result type.
446N/AAlso all functions modify an development graph when the are successful, which
446N/Amay be captured by some form of a state monad.
4865N/A-- * deleting and adding nodes
4865N/AIf a node is deleted all in- and outgoing links will be lost. This is intended
4865N/Afor ingoing definitions links. The targets of outgoing definitions links (aka
4865N/A"depending nodes") need to me marked as "reduced".
4865N/Atheorem links from A to B state that all sentences in A can be proven by the
4865N/Aaxioms (and proven theorems) from B (note the reversal). This means the
4865N/Asentences of A are translated and moved to B as theorems (to be proven) by
4865N/Aremoving ingoing theorem links means: we loose properties of B, which is no
5073N/Aproblem since we delete B. (If we just delete the theorem link we must inform
5073N/Adepending nodes that fewer axioms are now available. Since a proof for the
4865N/Alink will be lost other proofs in depending nodes may become invalid.)
4865N/Aremoving outgoing (local) theorem links means: target nodes may contain theorems
4865N/Afrom the source node that need to be deleted, too. So these nodes are
4865N/A"reduced" (fewer theorems only). (We do not keep even valid theorems, if we
4865N/AThe node to be deleted may have been subject to global decomposition. So
4865N/Aoutgoing global theorems of depending nodes may get a deleted edge-id in
4865N/Atheir proof-basis, that should be deleted, too.
4865N/AOutgoing theorem links of source nodes that have definition links to the
4865N/Atarget node to be deleted may be theorem links created by global decomposition
4865N/Awhich should be deleted, too.
4865N/ASo, when deleting a node, let's delete the edges in reverse order of their
4865N/A - (outgoing) local theorem links (with reversal of "local-inference")
4865N/A whose corresponding global theorem link has only this local theorem link
4865N/A - sentences in targets are removed (or the target is deleted node anyway)
4865N/A (if the local theorem was proven)
4865N/A - corresponding global theorem links become unproven again and loose
4865N/A their proof basis (or are deleted together with the node)
4865N/A - unproven global theorem links (with reversal of "global-decomposition")
4865N/A - the proof basis of other proven global theorem links with the same
4865N/A target is reduced and marked as incomplete (since a corresponding local
4865N/A theorem link and the definition link is not deleted yet).
4865N/A - so proven global theorems links are removed after removing the links in
4865N/A - outgoing definition links
4865N/A - target nodes need to be marked as reduced (outgoing global theorem links
4865N/A (Proofs relying on imported axioms become invalid, provided the sentence
4865N/A are still well-formed in the reduced signature)
4865N/A this just marks the current node as reduced which will be deleted later
4865N/ALater on reduced nodes need to be re-computed possibly causing depending nodes
4865N/Ato become reduced. Incomplete global theorem links need to be completed (by
5061N/AIf the node index is unknown then auxiliary functions (or a mapping between
5061N/Anode names and node indices) can be supplied to delete nodes by name. -}
5061N/AdeleteDGNode :: Node -> DGraph -> Result DGraph
5061N/AdeleteDGNode t dg = case fst . match t $ dgBody dg of
5061N/A Just (ins, _, nl, outs) -> case dgn_nf nl of
4865N/A deleteDGNode t $ changeDGH dg2 $ SetNodeLab nl
4865N/A (t, nl { dgn_nf = Nothing, dgn_sigma = Nothing })
4865N/A Nothing -> case dgn_freenf nl of
4865N/A deleteDGNode t $ changeDGH dg2 $ SetNodeLab nl
4865N/A (t, nl { dgn_freenf = Nothing, dgn_phi = Nothing })
4865N/A if null $ ins ++ outs then return $ changeDGH dg $ DeleteNode (t, nl)
4865N/A dg2 <- foldM (\ dgx (el, sr) -> delDGLink (Just sr) t (dgl_id el) dgx)
4865N/A dg3 <- foldM (\ dgx (el, rt) -> delDGLink (Just t) rt (dgl_id el) dgx)
4865N/A _ -> justWarn dg $ "node not in graph: " ++ show t
4865N/A{- | add a node supplying the necessary information.
5073N/AWe should allow to add a node without knowing its final signature. We just
5073N/Aknow the 'XNode' information. Later on definition and theorem links may be
4865N/Aadded. Only after all ingoing definition links (and their sources) are known
4865N/Awe can compute the actual signature (and theory).
4865N/AThe node index will be new and returned. The name should be unique. The theory
4865N/Ais a closed signature plus local sentences. The origin could be anything (to
4865N/Abe added yet), but for basic specs it is the list of the newly introduced
4865N/AThe required conservativity is some value from
5061N/AReference nodes can not be added this way. Also the references and morphisms
5061N/Ato normal forms for hiding or free links cannot be set this way. So further
5061N/AaddDGNode :: NodeName -> G_theory -> DGOrigin -> Conservativity -> DGraph
5061N/AaddDGNode nn th o cs dg = let
4865N/A nl = newInfoNodeLab nn inf th
4865N/A in case lookupNodeByName sn dg of
4865N/A [] -> return (changeDGH dg $ InsertNode (n, nl), n)
4865N/A ns -> fail $ "node name '" ++ sn
4865N/A ++ "' already defined in graph for node(s): "
4865N/A-- | Maybe a function to rename nodes is desirable
4865N/ArenameNode :: Node -> NodeName -> DGraph -> Result DGraph
4865N/A in case lookupNodeByName sn dg of
4744N/A [] -> return $ changeDGH dg $ SetNodeLab nl (n, nl { dgn_name = nn })
4744N/A ns -> fail $ "node name '" ++ sn
4865N/A ++ "' already defined in graph for node(s): "
4744N/A-- * deleting and adding links
4865N/A{- | delete a link given the source and target node by index and the edge-id.
4744N/AEdge-ids are globally unique, but locating source and target nodes would be
4865N/AGetting the edge-id if only source node name, target
4744N/Anode name, link type, possibly an origin, and the link morphism is given,
4744N/ALocal theorem links are proven by moving sentences from the source to target
4744N/Anode and changing them to theorems. So if such a proven local theorem link is
4744N/Aremoved the target node needs to be reduced, too.
4744N/Atarget nodes of definition links are "reduced" (see deleteDGNode)
4865N/AdelDGLink :: Maybe Node -> Node -> EdgeId -> DGraph -> Result DGraph
4865N/A (ins, _, nl, loopsAndOuts) = safeContextDG "delDGLink" dg t
4865N/A loops = filter ((== t) . snd) loopsAndOuts
4744N/A in case partition ((== i) . dgl_id . fst) allIns of
4744N/A ([], _) -> justWarn dg $ "link not found: " ++ show (t, i)
4744N/A unless (null os) $ justWarn ()
4865N/A $ "ambiguous link: " ++ shows (t, i) " other sources are: "
4865N/A $ "non-matching source node: " ++ show (s, t, i)
4865N/A _ -> let delE dg' = return $ changeDGH dg' $ DeleteEdge (s, t, lbl)
4865N/A -- links proven by current link
4865N/A gs = filter (edgeInProofBasis i . getProofBasis . fst) rs
4865N/A dgCh = changeDGH dg $ SetNodeLab nl (t, updNodeMod delSymMod nl)
4744N/A ScopedLink lOrG lk _ -> case lOrG of
4744N/A ThmLink (Proven (DGRuleLocalInference renms) _) -> do
4744N/A nl2 <- deleteDGNodeSens (\ nSen -> not (isAxiom nSen)
4744N/A && senAttr nSen `elem` map snd renms) nl
4744N/A return $ updDGNodeLab dg nl (t, nl2)
4744N/A -- find global link(s) that contain(s) the edge-id as proof-basis
4744N/A let dg3 = invalDGLinkProofs dg2 $ map (\ (l, sr) -> (sr, t, l)) gs
4744N/A pB = proofBasisOfThmLinkStatus pst
4744N/A {- delete all links created by global decomposition,
4744N/A (this may delete also manually inserted theorem links!)
4744N/A all links have the same target. -}
4744N/A filter ((`edgeInProofBasis` pB) . dgl_id . fst) rs
4744N/A in if null createdLinks then
4744N/A let dg3 = invalDGLinkProofs dg
4744N/A $ map (\ (l, sr) -> (sr, t, l)) gs
4744N/A dg2 <- foldM (\ dgx (el, sr) ->
4865N/A delDGLink (Just sr) t (dgl_id el) dgx) dg createdLinks
4865N/A HidingFreeOrCofreeThm {} -> delE dg
4865N/A {- just delete the theorem link, we don't know what links can be
4865N/A in the proof basis by the shifting rules -}
4865N/A _ -> delDef -- delete other def links
4865N/AupdNodeMod :: NodeMod -> DGNodeLab -> DGNodeLab
4865N/AupdNodeMod m nl = nl { nodeMod = mergeNodeMod m $ nodeMod nl }
4865N/A -> DGNodeLab -- ^ old label
4865N/A -> LNode DGNodeLab -- ^ node with new label
4865N/A dg0 = changeDGH dg $ SetNodeLab l n
4865N/A in togglePending dg0 $ changedLocalTheorems dg0 n
4865N/AdeleteDGNodeSens :: (forall a . Named a -> Bool) -> DGNodeLab
4865N/AdeleteDGNodeSens p nl = case dgn_theory nl of
4865N/A G_theory lid s si sens _ ->
4865N/A chg | all isAxiom es = delAxMod
4865N/A | all (not . isAxiom) es = delThMod
4865N/A then justWarn nl $ "no sentence deleted in: " ++ getDGNodeName nl
4865N/A else return $ updNodeMod chg $ nl
4865N/A { dgn_theory = G_theory lid s si rest startThId }
4865N/AinvalidateDGLinkProof :: DGLinkLab -> DGLinkLab
4865N/AinvalidateDGLinkProof el = el { dgl_type = setProof LeftOpen $ dgl_type el }
4865N/AinvalDGLinkProof :: LEdge DGLinkLab -> [DGChange]
4865N/AinvalDGLinkProof e@(s, t, l) =
4865N/A [DeleteEdge e, InsertEdge (s, t, invalidateDGLinkProof l)]
4865N/AinvalDGLinkProofs :: DGraph -> [LEdge DGLinkLab] -> DGraph
4865N/AinvalDGLinkProofs dg = changesDGH dg . concatMap invalDGLinkProof
4865N/A{- | add a link supplying the necessary information.
4865N/AMorphisms do not store source and target signatures. Only the source signature
4865N/Ais taken from the node. The induced signature of the morphism will be a
4865N/Asubsignature of the target signature.
4865N/A- adding an (unproven) global theorem link:
4865N/A this states that more theorems are supposed to hold in target nodes.
4744N/A- adding a global definition link:
4744N/A - the signature of the target is enlarged (Proofs remain valid).
4744N/A - proven outgoing global theorem links for new ingoing definition links may
4744N/A become unproven and incomplete
4865N/A - outgoing local theorem links for new ingoing definition links add proof
4865N/A obligations the target nodes of the local theorem links.
4744N/A Additional theorems need to be moved or we mark the proven local theorem
4865N/AThe link type may also contain a conservativity and isn't easy to set up for
4865N/Afree and hiding links. The origin is again basically for documentation
4865N/AThe returned edge-id will be new or an edge-id may be supplied as input. -}
4865N/AaddDGLink :: Node -> Node -> GMorphism -> DGLinkType -> DGLinkOrigin -> DGraph
4865N/A{- | Do we need functions to modify links?
4865N/AYes, later, for example, if a conservativity as part of the link type should
4865N/ASome link types contain proof information that needs to be kept up-to-date.
4865N/AFor example, a global theorem link will (after decomposition) refer to a local
4865N/Atheorem link and maybe another global theorem link. A local theorem link will
4865N/A(after local inference) refer to (possibly renamed) theorems in the target
4865N/AMaybe some more thoughts are needed to decide which link type information may
4865N/Abe set or changed explicitely and which information should be adjusted
4865N/AmodifyDGLinkType :: Node -> Node -> EdgeId -> DGLinkType -> DGraph -> DGraph
4865N/AmodifyDGLinkType = undefined
4865N/AIf the link morphism should change, this most likely (but not necessarily)
4865N/Ainvolves signature changes of the source or target node (or both nodes).
4865N/AIn the latter case, either the old link was invalidated before, by changing
4865N/Athe signature of the source or target node, or the modification of the link
4865N/Awill invalidate the contents of the source or target.
4865N/AInstead of tricky morphism changes it may be better to simply delete old edges
4865N/Aand nodes and reinsert new nodes and edges propagating some old attributes. -}
4865N/AmodifyDGLinkMorphism :: Node -> Node -> EdgeId -> GMorphism -> DGraph -> DGraph
4865N/AmodifyDGLinkMorphism = undefined
4865N/A-- | Modifying the documenting link origin should also be possible.
4865N/AmodifyDGLinkOrigin :: Node -> Node -> EdgeId -> DGLinkOrigin -> DGraph -> DGraph
4865N/AmodifyDGLinkOrigin = undefined
4865N/A-- * modifying the signature of a node
4744N/A{- | replace the signature of a node.
4744N/AThis function should be used as basis to add or delete symbols from a node.
4744N/AChanging the signature means that the codomain of incoming and the domain of
4744N/Aoutgoing links change. Therefore we would invalidate all attached links and
4865N/Aexpect further link morphism modifications to adjust these links.
4744N/AIf the signature is not enlarged some local sentences may become invalid.
4865N/ATherefore the class logic must supply a checking function that takes a
4744N/Asignature and a sentence and checks if the sentence is still well-formed
4865N/Aaccording to the given signature. A logic specific implementation my choose to
4865N/Afirst extract all symbols from a sentence and compare it to the set of
4865N/Asignature symbols. (Extracting symbols from sentences is no method of the
4865N/ASince there are functions to remove sentences explicitely, we leave it to the
4865N/Auser to remove sentences first before reducing or changing the signature and
4865N/Asimply fail if invalid sentences are left! -}
4865N/AsetSignature :: Node -> G_sign -> DGraph -> DGraph
4865N/A{- | delete symbols from a node's signature.
4865N/ADeleting symbols is a special case of setting a node's signature. The new
4865N/Asignature is computed using the method for the co-generated signature that is
4865N/Aalso used when symbols are hidden.
4865N/AIt is only checked that the symbol set difference of the new and old signature
4865N/Acorresponds to the supplied symbol set. (Alternatively it could be checked if
4865N/Athe new signature is a sub-signature of the old one.)
4865N/AThe target nodes of outgoing definition links will be adjusted according to
4865N/Athe reduced closed signature automatically.
4865N/AInvalid sentences should have been removed before.
4865N/AThis function can be easily extended to delete raw symbol via the logic
4865N/Aspecific matching between raw and signature symbols. -}
4865N/A{- | extending a node's signature.
4865N/AAdding symbols requires the new signature directly supplied as argument, since
4865N/Athe class logic supplies no way to extend a signature by a given set of
4865N/Asymbols. In fact symbols can only be extracted from a given signature.
4865N/AIt is only checked if the old signature is a sub-signature of the new one.
4865N/ASentences are not checked, because fully analyzed sentences are expected to
4865N/Aremain well-formed in an enlarged signature, although re-parsing and
4865N/Atype-checking may fail for the syntactic representation of these sentences.
4865N/AIt is, however, possible to extend a given signature by a basic spec as
4865N/Ahappens for usual spec extensions, but note that the basic analysis may also
4865N/Ayield sentences that might need to be added separately.
4865N/AAgain target nodes of outgoing definition links will be adjusted
4865N/AextendSignature :: Node -> G_sign -> DGraph -> DGraph
4744N/A-- * modifying local sentences of a node
4744N/ALocal sentences have been either directly added or have been inserted by
4865N/Alocal inference. Sentences inserted by local inference should not be
4865N/Amanipulated at the target node but only at the original source. But maybe it
4744N/Ashould be possible to delete such sentences explicitly to match the
4865N/Acorresponding deletion of the proven local theorem link? Alternatively a
4744N/Afunction to undo a local inference step could be applied.
4865N/AAll sentences are uniquely named. User given duplicate names or missing names
4865N/Aare removed by generating unique names.
4865N/AIf additional sentences are added by local inference they may be
4865N/Arenamed to ensure unique names. The renaming is stored to keep the
4865N/Acorrespondence to the original sentences.
4865N/AThe global theory of node should be computed if needed but is cached for
4865N/Aefficiency reason. It contains all sentences as axioms along incoming
4865N/Adefinition links. All these axioms may be used to prove a theorem, assuming
4865N/Athat the used axioms are valid in their original theory.
4865N/ASo a change of a sentence may invalidate proofs in nodes reachable via theorem
4865N/A{- | delete the sentences that fulfill the given predicate.
4865N/AShould this function fail if the predicate does not determine a unique
4865N/Asentence? Surely, simply all sentences could be deleted fulfilling the
4865N/Apredicate (possibly none). -}
4865N/AdeleteSentence :: Node -> (Named GSentence -> Bool) -> DGraph -> Result DGraph
4865N/A{- | delete a sentence by name
4865N/AThis is a more efficient version of deleting a single sentence. All sentences
4865N/Aof one node have a unique name, but it may be a generated name that the user
4865N/AOnly sentences not inserted by local inference can be deleted.
4865N/AdeleteSentenceByName :: Node -> String -> DGraph -> DGraph
4865N/AdeleteSentenceByName = undefined
4865N/AThe unproven named sentence given as argument is added as new sentence. The
4865N/Aname must be different from those of all other sentences, including those
4865N/Ainserted by local inference.
4865N/AAdding axioms will not invalidate proofs (if the logic is monotone), but the
4865N/Aaddition may trigger the addition of theorems in a neighbor node if linked to
4865N/Avia a proven local theorem link. Theorems are not propagated further.
4744N/ASentences can not be added with some old proof, that could be retried by the
4744N/AaddSentence :: Node -> Named GSentence -> DGraph -> DGraph
4744N/A{- | It may be desirable to rename sentences or change there role (axiom or
4865N/Atheorem) and even to invalid but keep an old proof. -}
4744N/AchangeSentence :: Node -> (Named GSentence -> Named GSentence) -> DGraph