{-# 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