3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher{- |

3441d0c2d11aea0c39b009751a1898333c009674Stephen GallagherModule : $Header$

3441d0c2d11aea0c39b009751a1898333c009674Stephen GallagherDescription : global proof rules for development graphs

3441d0c2d11aea0c39b009751a1898333c009674Stephen GallagherCopyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006

3441d0c2d11aea0c39b009751a1898333c009674Stephen GallagherLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher

3441d0c2d11aea0c39b009751a1898333c009674Stephen GallagherMaintainer : ken@informatik.uni-bremen.de

3441d0c2d11aea0c39b009751a1898333c009674Stephen GallagherStability : provisional

3441d0c2d11aea0c39b009751a1898333c009674Stephen GallagherPortability : non-portable(DevGraph)

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagherglobal proof rules for development graphs.

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher Follows Sect. IV:4.4 of the CASL Reference Manual.

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher-}

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallaghermodule Proofs.Global

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher ( globSubsume

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher , globDecomp

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher , globDecompAux -- for Test.hs

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher , globDecompFromList

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher , globSubsumeFromList

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher ) where

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagherimport Data.Graph.Inductive.Graph

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagherimport qualified Data.Map as Map

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagherimport Data.List

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagherimport Static.GTheory

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagherimport Static.DevGraph

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagherimport Common.LibName

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagherimport Common.Utils

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher

1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barriaimport Proofs.EdgeUtils

1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barriaimport Proofs.StatusUtils

1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria

3441d0c2d11aea0c39b009751a1898333c009674Stephen GallagherglobDecompRule :: LEdge DGLinkLab -> DGRule

3441d0c2d11aea0c39b009751a1898333c009674Stephen GallagherglobDecompRule = DGRuleWithEdge "Global-Decomposition"

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher{- apply rule GlobDecomp to all global theorem links in the current DG

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher current DG = DGm

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher add to proof status the pair ([GlobDecomp e1,...,GlobDecomp en],DGm+1)

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher where e1...en are the global theorem links in DGm

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher DGm+1 results from DGm by application of GlobDecomp e1,...,GlobDecomp en -}

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher

1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria

1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria{- | applies global decomposition to the list of edges given (global

1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria theorem edges) if possible, if empty list is given then to all

1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria unproven global theorems.

1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria Notice: (for ticket 5, which solves the problem across library border)

1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria 1. before the actual global decomposition is applied, the whole DGraph is

1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria updated firstly by calling the function updateDGraph.

1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria 2. The changes of the update action should be added as the head of the

1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria history.

1b171c456ff901ab622e44bcfd213f7de86fd787Ariel Barria-}

1b171c456ff901ab622e44bcfd213f7de86fd787Ariel BarriaglobDecompFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv

3441d0c2d11aea0c39b009751a1898333c009674Stephen GallagherglobDecompFromList ln globalThmEdges proofStatus =

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher let dgraph = lookupDGraph ln proofStatus

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher finalGlobalThmEdges = filter (liftE isUnprovenGlobalThm) globalThmEdges

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher auxGraph = foldl (updateDGraph proofStatus) dgraph

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher $ nubOrd $ map (\ (src, _, _) -> src) finalGlobalThmEdges

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher newDGraph = foldl globDecompAux auxGraph finalGlobalThmEdges

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher in Map.insert ln newDGraph proofStatus

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher{- | update the given DGraph with source nodes of all global unproven

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher links.

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher The idea is, to expand the given DGraph by adding all the referenced

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher nodes related to the given source nodes in other libraries and the

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher corresponding links as well.

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher If a certain node is a referenced node and not expanded yet, then its

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher parents will be found by calling getRefParents.

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher These parents will be added into current DGraph using updateDGraphAux

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher-}

3441d0c2d11aea0c39b009751a1898333c009674Stephen GallagherupdateDGraph :: LibEnv -> DGraph

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher -> Node -- source nodes of all global unproven links

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher -> DGraph

3441d0c2d11aea0c39b009751a1898333c009674Stephen GallagherupdateDGraph le dg x =

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher {- checks if it is an unexpanded referenced node

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher the function lookupInRefNodesDG only checks the

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher nodes which are not expanded. -}

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher case lookupInRefNodesDG x dg of

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher Just (refl, refn) ->

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher let

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher parents = getRefParents le refl refn

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher {- important for those, who's doing redo/undo function:

7800c9da75ad0dc3b4a530b15adce86d6c4f26e5Lukas Slebodnik notice that if the node is expanded, then it should be

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher deleted out of the unexpanded map using

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher deleteFromRefNodesDG -}

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher auxDG = foldl (updateDGraphAux le x refl)

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher dg parents

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher in auxDG

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher _ -> dg

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher{- | get all the parents, namely the related referenced nodes and the links

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher between them and the present to be expanded node.

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher-}

3441d0c2d11aea0c39b009751a1898333c009674Stephen GallaghergetRefParents :: LibEnv -> LibName

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher -> Node -- the present to be expanded node

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher -> [(LNode DGNodeLab, [DGLinkLab])]

3441d0c2d11aea0c39b009751a1898333c009674Stephen GallaghergetRefParents le refl refn =

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher let

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher {- get the previous objects to the current one -}

3441d0c2d11aea0c39b009751a1898333c009674Stephen Gallagher dg = lookupDGraph refl le

pres = innDG dg refn

in modifyPs dg 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 :: DGraph -> [LEdge DGLinkLab] -> [(LNode DGNodeLab, [DGLinkLab])]

modifyPs dg ls =

map

(\ (n, x) -> ((n, labDG dg n), x))

$ modifyPsAux ls

where

modifyPsAux :: Ord a => [(a, t, b)] -> [(a, [b])]

modifyPsAux l =

Map.toList $ Map.fromListWith (++) [(k, [v]) | (k, _, v) <- l ]

{- | the actual update function to insert a list of related parents to the

present to be expanded node.

It inserts the related referenced node firstly by calling addParentNode.

Then it inserts the related links by calling addParentLinks

Notice that nodes have to be added firstly, so that the links can be

connected to the inserted nodes ;), especially by adding to the change

list.

-}

updateDGraphAux :: LibEnv -> Node -- the present to be expanded node

-> LibName -> DGraph -> (LNode DGNodeLab, [DGLinkLab])

-> DGraph

updateDGraphAux libenv n refl dg (pnl, pls) =

let

(auxDG, newN) = addParentNode libenv dg refl pnl

in addParentLinks auxDG newN n pls

{- | add the given parent node into the current dgraph

-}

addParentNode :: LibEnv -> DGraph -> LibName

-> LNode DGNodeLab -- the referenced parent node

-> (DGraph, Node)

addParentNode libenv dg refl (refn, oldNodelab) =

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.

-}

(nodelab, newRefl, newRefn) = if isDGRef oldNodelab then

let

tempRefl = dgn_libname oldNodelab

tempRefn = dgn_node oldNodelab

originDG = lookupDGraph tempRefl libenv

in

(labDG originDG tempRefn, tempRefl, tempRefn)

else (oldNodelab, refl, 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 = case dgn_theory nodelab of

G_theory lid sig ind _ _ -> noSensGTheory lid sig ind

refInfo = newRefInfo newRefl newRefn

newRefNode = (newInfoNodeLab (dgn_name nodelab) refInfo newGTh)

{ globalTheory = globalTheory nodelab }

in

-- checks if this node exists in the current dg, if so, nothing needs to be

-- done.

case lookupInAllRefNodesDG refInfo dg of

Nothing -> let newN = getNewNodeDG dg in

( changeDGH (addToRefNodesDG newN refInfo dg)

$ InsertNode (newN, newRefNode)

, newN)

Just extN -> (dg, extN)

{- | add a list of links between the given two node ids.

-}

addParentLinks :: DGraph -> Node -> Node -> [DGLinkLab] -> DGraph

addParentLinks dg src tgt ls =

let oldLinks = map (\ (_, _, l) -> l)

$ filter (\ (s, _, _) -> s == src) $ innDG dg tgt

newLinks = map (\ l -> l

{ dgl_id = defaultEdgeId

, dgl_type = invalidateProof $ dgl_type l }) ls

in if null oldLinks then

changesDGH dg $ map (\ l -> InsertEdge (src, tgt, l)) newLinks

else dg -- assume ingoing links are already properly set

{- applies global decomposition to all unproven global theorem edges

if possible -}

globDecomp :: LibName -> LibEnv -> LibEnv

globDecomp ln proofStatus =

let dgraph = lookupDGraph ln proofStatus

globalThmEdges = labEdgesDG dgraph

in

globDecompFromList ln globalThmEdges proofStatus

{- auxiliary function for globDecomp (above)

actual implementation -}

globDecompAux :: DGraph -> LEdge DGLinkLab -> DGraph

globDecompAux dgraph edge =

let newDGraph = globDecompForOneEdge dgraph edge

in groupHistory dgraph (globDecompRule edge) newDGraph

-- applies global decomposition to a single edge

globDecompForOneEdge :: DGraph -> LEdge DGLinkLab -> DGraph

globDecompForOneEdge dgraph edge@(source, target, edgeLab) = let

defEdgesToSource = [e | e@(_, _, lbl) <- innDG dgraph source,

isDefEdge (dgl_type lbl)]

paths = map (\e -> [e, edge]) defEdgesToSource ++ [[edge]]

-- why not? [edge] : map ...

(newGr, proof_basis) = foldl

(globDecompForOneEdgeAux target) (dgraph, emptyProofBasis) paths

provenEdge = (source, target, edgeLab

{ dgl_type = setProof (Proven (globDecompRule edge) proof_basis)

$ dgl_type edgeLab

, dgl_origin = DGLinkProof })

in changesDGH newGr [DeleteEdge edge, InsertEdge 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 target (dgraph, proof_basis) path =

case path of

[] -> error "globDecompForOneEdgeAux"

(node, _, lbl) : rpath -> let

lbltype = dgl_type lbl

isHiding = isHidingDef lbltype

morphismPath = if isHiding then rpath else path

morphism = case calculateMorphismOfPath morphismPath of

Just morph -> morph

Nothing -> error "globDecomp: could not determine morphism of new edge"

newEdgeLbl = DGLink

{ dgl_morphism = morphism

, dgl_type = if isHiding then hidingThm $ dgl_morphism lbl

else if isGlobalDef lbltype then globalThm else localThm

, dgl_origin = DGLinkProof

, dgl_id = defaultEdgeId }

newEdge = (node, target, newEdgeLbl)

in if node == target && isInc (getRealDGLinkType newEdgeLbl)

&& isGlobalDef lbltype

then (dgraph, addEdgeId proof_basis $ dgl_id lbl)

else case tryToGetEdge newEdge dgraph of

Nothing -> let

newGraph = changeDGH dgraph $ InsertEdge newEdge

finalEdge = case getLastChange newGraph of

InsertEdge final_e -> final_e

_ -> error "Proofs.Global.globDecompForOneEdgeAux"

in (newGraph, addEdgeId proof_basis $ getEdgeId finalEdge)

Just e -> (dgraph, addEdgeId proof_basis $ getEdgeId e)

globSubsumeFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv

globSubsumeFromList ln globalThmEdges libEnv =

let dgraph = lookupDGraph ln libEnv

finalGlobalThmEdges = filter (liftE isUnprovenGlobalThm) globalThmEdges

nextDGraph = foldl

(globSubsumeAux libEnv) dgraph finalGlobalThmEdges

in Map.insert ln nextDGraph libEnv

-- | tries to apply global subsumption to all unproven global theorem edges

globSubsume :: LibName -> LibEnv -> LibEnv

globSubsume ln libEnv =

let dgraph = lookupDGraph ln libEnv

globalThmEdges = labEdgesDG dgraph

in globSubsumeFromList ln globalThmEdges libEnv

{- auxiliary function for globSubsume (above) the actual implementation -}

globSubsumeAux :: LibEnv -> DGraph -> LEdge DGLinkLab -> DGraph

globSubsumeAux libEnv dgraph ledge@(src, tgt, edgeLab) =

let morphism = dgl_morphism edgeLab

filteredPaths = filterPathsByMorphism morphism $ filter (noPath ledge)

$ getAllGlobPathsBetween dgraph src tgt

proofbasis = selectProofBasis dgraph ledge filteredPaths

in if not (nullProofBasis proofbasis) || isIdentityEdge ledge libEnv dgraph

then

let globSubsumeRule = DGRuleWithEdge "Global-Subsumption" ledge

newEdge = (src, tgt, edgeLab

{ dgl_type = setProof (Proven globSubsumeRule proofbasis)

$ dgl_type edgeLab

, dgl_origin = DGLinkProof })

newDGraph = changesDGH dgraph [DeleteEdge ledge, InsertEdge newEdge]

in groupHistory dgraph globSubsumeRule newDGraph

else dgraph