fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu{-|

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuModule : $Header$

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuCopyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2004

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : hets@tzi.de

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuStability : provisional

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuPortability : non-portable(Logic)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu Proofs in development graphs.

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu Follows Sect. IV:4.4 of the CASL Reference Manual.

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu-}

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu{-

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu References:

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu T. Mossakowski, S. Autexier and D. Hutter:

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu Extending Development Graphs With Hiding.

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu Lecture Notes in Computer Science 2029, p. 269-283,

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu Springer-Verlag 2001.

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescutodo:

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuIntegrate stuff from Saarbr�cken

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuAdd proof status information

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu what should be in proof status:

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu- proofs of thm links according to rules

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu- cons, def and mono annos, and their proofs

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu-}

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescumodule Proofs.Proofs where

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescuimport Logic.Logic

da955132262baab309a50fdffe228c9efe68251dCui Jianimport Logic.Prover

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescuimport Logic.Grothendieck

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescuimport Static.DevGraph

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescuimport Common.Result

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescuimport Common.Lib.Graph

da955132262baab309a50fdffe228c9efe68251dCui Jianimport List(nub)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescuimport Common.Id

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu{- proof status = (DG0,[(R1,DG1),...,(Rn,DGn)])

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu DG0 is the development graph resulting from the static analysis

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu Ri is a list of rules that transforms DGi-1 to DGi

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu With the list of intermediate proof states, one can easily implement

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu an undo operation

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu-}

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescutype ProofStatus = (GlobalContext,[([DGRule],[DGChange])],DGraph)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

da955132262baab309a50fdffe228c9efe68251dCui Jiandata DGRule =

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu TheoremHideShift

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | HideTheoremShift

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | Borrowing

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | ConsShift

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | DefShift

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | MonoShift

da955132262baab309a50fdffe228c9efe68251dCui Jian | ConsComp

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | DefComp

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | MonoComp

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | DefToMono

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | MonoToCons

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | FreeIsMono

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | MonoIsFree

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | Composition

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | GlobDecomp (LEdge DGLinkLab) -- edge in the conclusion

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | LocDecomp (LEdge DGLinkLab)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | GlobSubsumption (LEdge DGLinkLab)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | LocalInference

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | BasicInference Edge BasicProof

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | BasicConsInference Edge BasicConsProof

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescudata DGChange = InsertNode (LNode DGNodeLab)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | DeleteNode Node

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | InsertEdge (LEdge DGLinkLab)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | DeleteEdge (LEdge DGLinkLab)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

2df3a08c43f067ba532151ade20b1e4e2d2efd90Mihai Codescudata BasicProof =

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder forall lid sublogics

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu basic_spec sentence symb_items symb_map_items

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign morphism symbol raw_symbol proof_tree .

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu Logic lid sublogics

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu basic_spec sentence symb_items symb_map_items

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign morphism symbol raw_symbol proof_tree =>

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu BasicProof lid (Proof_status sentence proof_tree)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | Guessed

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | Conjectured

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu | Handwritten

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescudata BasicConsProof = BasicConsProof -- more detail to be added ...

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu{- todo: implement apply for GlobDecomp and Subsumption

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu the list of DGChage must be constructed in parallel to the

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu new DGraph -}

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuapplyRule :: DGRule -> DGraph -> Maybe ([DGChange],DGraph)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuapplyRule = error "Proofs.hs:applyRule"

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

da955132262baab309a50fdffe228c9efe68251dCui Jian-- ---------------------

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu-- global decomposition

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu-- ---------------------

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu{- apply rule GlobDecomp to all global theorem links in the current DG

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu current DG = DGm

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu add to proof status the pair ([GlobDecomp e1,...,GlobDecomp en],DGm+1)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu where e1...en are the global theorem links in DGm

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu DGm+1 results from DGm by application of GlobDecomp e1,...,GlobDecomp en -}

da955132262baab309a50fdffe228c9efe68251dCui Jian

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu{- applies global decomposition to all unproven global theorem edges

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu if possible -}

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuglobDecomp :: ProofStatus -> ProofStatus

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuglobDecomp proofStatus@(globalContext,history,dgraph) =

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu (globalContext, ((newHistoryElem):history), newDgraph)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu where

da955132262baab309a50fdffe228c9efe68251dCui Jian globalThmEdges = filter isUnprovenGlobalThm (labEdges dgraph)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu (newDgraph, newHistoryElem) = globDecompAux dgraph globalThmEdges ([],[])

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

2df3a08c43f067ba532151ade20b1e4e2d2efd90Mihai Codescu{- auxiliary function for globDecomp (above)

2df3a08c43f067ba532151ade20b1e4e2d2efd90Mihai Codescu actual implementation -}

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuglobDecompAux :: DGraph -> [LEdge DGLinkLab] -> ([DGRule],[DGChange])

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu -> (DGraph,([DGRule],[DGChange]))

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuglobDecompAux dgraph [] historyElem = (dgraph, historyElem)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuglobDecompAux dgraph (edge:edges) historyElem =

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu globDecompAux newDGraph edges newHistoryElem

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu where

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder (newDGraph, newChanges) = globDecompForOneEdge dgraph edge

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder newHistoryElem =

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu if null newChanges then historyElem

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu else (((GlobDecomp edge):(fst historyElem)),

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu (newChanges++(snd historyElem)))

da955132262baab309a50fdffe228c9efe68251dCui Jian

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu-- applies global decomposition to a single edge

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuglobDecompForOneEdge :: DGraph -> LEdge DGLinkLab -> (DGraph,[DGChange])

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuglobDecompForOneEdge dgraph edge =

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu globDecompForOneEdgeAux dgraph edge [] paths

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu where

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu pathsToSource = getAllLocGlobDefPathsTo dgraph (getSourceNode edge) []

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu paths = [(node, path++(edge:[]))| (node,path) <- pathsToSource]

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu{- auxiliary funktion for globDecompForOneEdge (above)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu actual implementation -}

da955132262baab309a50fdffe228c9efe68251dCui JianglobDecompForOneEdgeAux :: DGraph -> LEdge DGLinkLab -> [DGChange] ->

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu [(Node, [LEdge DGLinkLab])] -> (DGraph,[DGChange])

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu{- if the list of paths is empty from the beginning, nothing is done

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu otherwise the unprovenThm edge is replaced by a proven one -}

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuglobDecompForOneEdgeAux dgraph edge@(source,target,edgeLab) changes [] =

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu if null changes then (dgraph, [])

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu else ((insEdge provenEdge (delLEdge edge dgraph)),

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu ((DeleteEdge edge):((InsertEdge provenEdge):changes)))

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

da955132262baab309a50fdffe228c9efe68251dCui Jian where

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu (GlobalThm _ conservativity conservStatus) = (dgl_type edgeLab)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu proofBasis = getLabelsOfInsertedEdges changes

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu provenEdge = (source,

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu target,

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu DGLink {dgl_morphism = dgl_morphism edgeLab,

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu dgl_type =

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu (GlobalThm (Proven proofBasis)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu conservativity conservStatus),

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu dgl_origin = DGProof}

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu )

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu-- for each path an unproven localThm edge is inserted

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuglobDecompForOneEdgeAux dgraph edge@(source,target,edgeLab) changes

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu ((node,path):list) =

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu globDecompForOneEdgeAux newGraph edge newChanges list

da955132262baab309a50fdffe228c9efe68251dCui Jian

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu where

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu morphism = case calculateMorphismOfPath path of

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu Just morph -> morph

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu Nothing ->

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu error "globDecomp: could not determine morphism of new edge"

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu newEdge = (node,

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu target,

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu DGLink {dgl_morphism = morphism,

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu dgl_type = (LocalThm (Static.DevGraph.Open)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu None (Static.DevGraph.Open)),

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu dgl_origin = DGProof}

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu )

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu newGraph = insEdge newEdge dgraph

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu newChanges = ((InsertEdge newEdge):changes)

2df3a08c43f067ba532151ade20b1e4e2d2efd90Mihai Codescu

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

da955132262baab309a50fdffe228c9efe68251dCui Jian-- -------------------

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu-- global subsumption

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder-- -------------------

da955132262baab309a50fdffe228c9efe68251dCui Jian

da955132262baab309a50fdffe228c9efe68251dCui Jian-- applies global subsumption to all unproven global theorem edges if possible

da955132262baab309a50fdffe228c9efe68251dCui JianglobSubsume :: ProofStatus -> ProofStatus

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuglobSubsume proofStatus@(globalContext,history,dGraph) =

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu (globalContext, nextHistoryElem:history, nextDGraph)

fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu

where

globalThmEdges = filter isUnprovenGlobalThm (labEdges dGraph)

result = globSubsumeAux dGraph ([],[]) globalThmEdges

nextDGraph = fst result

nextHistoryElem = snd result

{- auxiliary function for globSubsume (above)

the actual implementation -}

globSubsumeAux :: DGraph -> ([DGRule],[DGChange]) -> [LEdge DGLinkLab]

-> (DGraph,([DGRule],[DGChange]))

globSubsumeAux dgraph historyElement [] = (dgraph, historyElement)

globSubsumeAux dgraph (rules,changes) ((ledge@(src,tgt,edgeLab)):list) =

if null proofBasis

then

globSubsumeAux dgraph (rules,changes) list

else

globSubsumeAux (insEdge newEdge (delLEdge ledge dgraph)) (newRules,newChanges) list

where

morphism = dgl_morphism edgeLab

allPaths = getAllGlobPathsOfMorphismBetween dgraph morphism src tgt

proofBasis = selectProofBasis edgeLab allPaths

(GlobalThm _ conservativity conservStatus) = (dgl_type edgeLab)

newEdge = (src,

tgt,

DGLink {dgl_morphism = morphism,

dgl_type = (GlobalThm (Proven proofBasis)

conservativity conservStatus),

dgl_origin = DGProof}

)

newRules = (GlobSubsumption ledge):rules

newChanges = (DeleteEdge ledge):((InsertEdge newEdge):changes)

{- returns the DGLinkLab of the given LEdge -}

getLabelOfEdge :: (LEdge b) -> b

getLabelOfEdge (_,_,label) = label

-- --------------------

-- local decomposition

-- --------------------

{- a merge of the rules local subsumption, local decomposition I and

local decomposition II -}

-- applies this merge of rules to all unproven localThm edges if possible

locDecomp :: ProofStatus -> ProofStatus

locDecomp proofStatus@(globalContext,history,dGraph) =

(globalContext, nextHistoryElem:history, nextDGraph)

where

localThmEdges = filter isUnprovenLocalThm (labEdges dGraph)

result = locDecompAux dGraph ([],[]) localThmEdges

nextDGraph = fst result

nextHistoryElem = snd result

{- auxiliary function for locDecomp (above)

actual implementation -}

locDecompAux :: DGraph -> ([DGRule],[DGChange]) -> [LEdge DGLinkLab]

-> (DGraph,([DGRule],[DGChange]))

locDecompAux dgraph historyElement [] = (dgraph, historyElement)

locDecompAux dgraph (rules,changes) ((ledge@(src,tgt,edgeLab)):list) =

if null proofBasis

then

globSubsumeAux dgraph (rules,changes) list

else

globSubsumeAux newGraph (newRules,newChanges) list

where

morphism = dgl_morphism edgeLab

allPaths = getAllThmDefPathsOfMorphismBetween dgraph morphism src tgt

-- getAllProvenLocGlobPathsOfMorphismBetween dgraph morphism source target

proofBasis = selectProofBasis edgeLab allPaths

auxGraph = delLEdge ledge dgraph

(LocalThm _ conservativity conservStatus) = (dgl_type edgeLab)

newEdge = (src,

tgt,

DGLink {dgl_morphism = morphism,

dgl_type =

(LocalThm (Proven proofBasis)

conservativity conservStatus),

dgl_origin = DGProof}

)

newGraph = insEdge newEdge auxGraph

newRules = (LocDecomp ledge):rules

newChanges = (DeleteEdge ledge):((InsertEdge newEdge):changes)

-- ----------------------------------------------

-- methods that calculate paths of certain types

-- ----------------------------------------------

{- returns a list of all proven global paths of the given morphism between

the given source and target node-}

getAllGlobPathsOfMorphismBetween :: DGraph -> GMorphism -> Node -> Node

-> [[LEdge DGLinkLab]]

getAllGlobPathsOfMorphismBetween dgraph morphism src tgt =

filterPathsByMorphism morphism allPaths

where

allPaths = getAllGlobPathsBetween dgraph src tgt

{- Benutzung dieser Methode derzeit auskommentiert - wird wahrscheinlich weggeschmissen -}

{- returns a list of all proven loc-glob paths of the given morphism between

the given source and target node -}

{-getAllProvenLocGlobPathsOfMorphismBetween :: DGraph -> GMorphism -> Node

-> Node -> [[LEdge DGLinkLab]]

getAllProvenLocGlobPathsOfMorphismBetween dgraph morphism src tgt =

filterPathsByMorphism morphism allPaths

where

allPaths = getAllProvenLocGlobPathsBetween dgraph src tgt

-}

{- returns all paths from the given list whose morphism is equal to the

given one-}

filterPathsByMorphism :: GMorphism -> [[LEdge DGLinkLab]]

-> [[LEdge DGLinkLab]]

filterPathsByMorphism morphism paths =

[path| path <- paths, (calculateMorphismOfPath path) == (Just morphism)]

{- returns a list of all paths to the given node

that consist of globalDef edges only

or

that consist of a localDef edge followed by any number of globalDef edges -}

getAllLocGlobDefPathsTo :: DGraph -> Node -> [LEdge DGLinkLab]

-> [(Node, [LEdge DGLinkLab])]

getAllLocGlobDefPathsTo dgraph node path =

(node,path):(locGlobPaths ++

(concat (

[getAllLocGlobDefPathsTo dgraph (getSourceNode edge) path|

(_, path@(edge:edges)) <- globalPaths]))

)

where

inEdges = inn dgraph node

globalEdges = filter isGlobalDef inEdges

localEdges = filter isLocalDef inEdges

globalPaths = [(getSourceNode edge, (edge:path))| edge <- globalEdges]

locGlobPaths = [(getSourceNode edge, (edge:path))| edge <- localEdges]

{- Benutzung dieser Methode derzeit auskommentiert - wird wahrscheinlich weggeschmissen -}

{- returns all paths consisting of globalDef and proven global thm edges only

or

of one localDef or proven local thm followed by any number of globalDef or

proven global thm edges-}

{- getAllProvenLocGlobPathsBetween :: DGraph -> Node -> Node

-> [[LEdge DGLinkLab]]

getAllProvenLocGlobPathsBetween dgraph src tgt =

getAllLocGlobPathsOfTypesBetween dgraph src tgt

[isLocalDef,isProvenLocalThm] [isGlobalDef,isProvenGlobalThm] -}

{- Benutzung dieser Methode derzeit auskommentiert - wird wahrscheinlich weggeschmissen -}

{- returns all paths consisting only of edges of the types in the snd list

or

of one edge of one of the types of the fst list followed by any number

of edges of the types of the snd list -}

{- getAllLocGlobPathsOfTypesBetween :: DGraph -> Node -> Node -> [LEdge DGLinkLab -> Bool] -> [LEdge DGLinkLab -> Bool] -> [[LEdge DGLinkLab]]

getAllLocGlobPathsOfTypesBetween dgraph src tgt locTypes globTypes =

locGlobPaths ++ globPaths

where

outEdges = out dgraph src

locEdges = [(edge,getTargetNode edge)|edge <-

(filterByTypes locTypes outEdges)]

locGlobPaths = (concat [map ([edge]++)

(getAllPathsOfTypesBetween dgraph globTypes node tgt [])|

(edge,node) <- locEdges])

globPaths = getAllProvenGlobPathsBetween dgraph src tgt

-}

{- returns all paths of globalDef edges or globalThm edges

between the given source and target node -}

getAllGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]

getAllGlobPathsBetween dgraph src tgt =

getAllPathsOfTypesBetween dgraph [isGlobalDef,isGlobalThm] src tgt []

{- gets all paths consisting of local/global thm/def edges

of the given morphism -}

getAllThmDefPathsOfMorphismBetween :: DGraph -> GMorphism -> Node -> Node

-> [[LEdge DGLinkLab]]

getAllThmDefPathsOfMorphismBetween dgraph morphism src tgt =

filterPathsByMorphism morphism allPaths

where

allPaths = getAllPathsOfTypesBetween dgraph types src tgt []

types =

[isGlobalThm,

isProvenLocalThm,

isProvenLocalThm,

isUnprovenLocalThm,

isGlobalDef,

isLocalDef]

{- returns all paths of globalDef edges between the given source and

target node -}

getAllGlobDefPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]

getAllGlobDefPathsBetween dgraph src tgt =

getAllPathsOfTypeBetween dgraph isGlobalDef src tgt

{- returns all paths consiting of edges of the given type between the

given node -}

getAllPathsOfTypeBetween :: DGraph -> (LEdge DGLinkLab -> Bool) -> Node

-> Node -> [[LEdge DGLinkLab]]

getAllPathsOfTypeBetween dgraph isType src tgt =

getAllPathsOfTypesBetween dgraph (isType:[]) src tgt []

{- returns all paths consisting of edges of the given types between

the given nodes -}

getAllPathsOfTypesBetween :: DGraph -> [LEdge DGLinkLab -> Bool] -> Node

-> Node -> [LEdge DGLinkLab]

-> [[LEdge DGLinkLab]]

getAllPathsOfTypesBetween dgraph types src tgt path =

[edge:path| edge <- edgesFromSrc]

++ (concat

[getAllPathsOfTypesBetween dgraph types src nextTgt (edge:path)|

(edge,nextTgt) <- nextStep] )

where

inGoingEdges = inn dgraph tgt

edgesOfTypes = filterByTypes types inGoingEdges

edgesFromSrc =

[edge| edge@(source,_,_) <- edgesOfTypes, source == src]

nextStep =

[(edge, source)| edge@(source,_,_) <- edgesOfTypes, source /= src]

-- removes all edges that are not of the given types

filterByTypes :: [LEdge DGLinkLab -> Bool] -> [LEdge DGLinkLab]

-> [LEdge DGLinkLab]

filterByTypes [] edges = []

filterByTypes (isType:typeChecks) edges =

(filter isType edges)++(filterByTypes typeChecks edges)

-- --------------------------------------

-- methods to determine or get morphisms

-- --------------------------------------

-- determines the morphism of a given path

calculateMorphismOfPath :: [LEdge DGLinkLab] -> Maybe GMorphism

calculateMorphismOfPath [] = Nothing

calculateMorphismOfPath path@((src,tgt,edgeLab):furtherPath) =

case maybeMorphismOfFurtherPath of

Nothing -> if null furtherPath then Just morphism else Nothing

Just morphismOfFurtherPath ->

comp Grothendieck morphism morphismOfFurtherPath

where

morphism = dgl_morphism edgeLab

maybeMorphismOfFurtherPath = calculateMorphismOfPath furtherPath

-- ------------------------------------

-- methods to get the nodes of an edge

-- ------------------------------------

getSourceNode :: LEdge DGLinkLab -> Node

getSourceNode (source,_,_) = source

{- Benutzung derzeit auskommentiert ... -}

{-getTargetNode :: LEdge DGLinkLab -> Node

getTargetNode (_,target,_) = target -}

-- -------------------------------------

-- methods to check the type of an edge

-- -------------------------------------

isProven :: LEdge DGLinkLab -> Bool

isProven edge = isGlobalDef edge || isLocalDef edge

|| isProvenGlobalThm edge || isProvenLocalThm edge

isGlobalThm :: LEdge DGLinkLab -> Bool

isGlobalThm edge = isProvenGlobalThm edge || isUnprovenGlobalThm edge

isProvenGlobalThm :: LEdge DGLinkLab -> Bool

isProvenGlobalThm (_,_,edgeLab) =

case dgl_type edgeLab of

(GlobalThm (Proven _) _ _) -> True

otherwise -> False

isUnprovenGlobalThm :: LEdge DGLinkLab -> Bool

isUnprovenGlobalThm (_,_,edgeLab) =

case dgl_type edgeLab of

(GlobalThm Static.DevGraph.Open _ _) -> True

otherwise -> False

isProvenLocalThm :: LEdge DGLinkLab -> Bool

isProvenLocalThm (_,_,edgeLab) =

case dgl_type edgeLab of

(LocalThm (Proven _) _ _) -> True

otherwise -> False

isUnprovenLocalThm :: LEdge DGLinkLab -> Bool

isUnprovenLocalThm (_,_,edgeLab) =

case dgl_type edgeLab of

(LocalThm (Static.DevGraph.Open) _ _) -> True

otherwise -> False

isGlobalDef :: LEdge DGLinkLab -> Bool

isGlobalDef (_,_,edgeLab) =

case dgl_type edgeLab of

GlobalDef -> True

otherwise -> False

isLocalDef :: LEdge DGLinkLab -> Bool

isLocalDef (_,_,edgeLab) =

case dgl_type edgeLab of

LocalDef -> True

otherwise -> False

-- ----------------------------------------------------------------------------

-- methods to determine the labels of the inserted edges in the given dgchange

-- ----------------------------------------------------------------------------

{- filters the list of changes for insertions of edges and returns the label

of one of these; or Nothing if no insertion was found -}

getLabelsOfInsertedEdges :: [DGChange] -> [DGLinkLab]

getLabelsOfInsertedEdges changes =

[label | (_,_,label) <- getInsertedEdges changes]

{- returns all insertions of edges from the given list of changes -}

getInsertedEdges :: [DGChange] -> [LEdge DGLinkLab]

getInsertedEdges [] = []

getInsertedEdges (change:list) =

case change of

(InsertEdge edge) -> edge:(getInsertedEdges list)

otherwise -> getInsertedEdges list

-- ----------------------------------------

-- methods to check and select proof basis

-- ----------------------------------------

{- determines all proven paths in the given list and tries to selet a

proof basis from these (s. selectProofBasisAux);

if this fails the same is done for the rest of the given paths, i.e.

for the unproven ones -}

selectProofBasis :: DGLinkLab -> [[LEdge DGLinkLab]] -> [DGLinkLab]

selectProofBasis label paths =

if null provenProofBasis then selectProofBasisAux label unprovenPaths

else provenProofBasis

where

provenPaths = filterProvenPaths paths

provenProofBasis = selectProofBasisAux label provenPaths

unprovenPaths = [path | path <- paths, notElem path provenPaths]

{- selects the first path that does not form a proof cycle with the given

label (if such a path exits) and returns the labels of its edges -}

selectProofBasisAux :: DGLinkLab -> [[LEdge DGLinkLab]] -> [DGLinkLab]

selectProofBasisAux _ [] = []

selectProofBasisAux label (path:list) =

if notProofCycle label path then nub (calculateProofBasis path)

else selectProofBasisAux label list

{- calculates the proofBasis of the given path,

i.e. the list of all DGLinkLabs the proofs of the edges contained in the path

are based on, plus the DGLinkLabs of the edges themselves;

duplicates are not removed here, but in the calling method

selectProofBasisAux -}

calculateProofBasis :: [LEdge DGLinkLab] -> [DGLinkLab]

calculateProofBasis [] = []

calculateProofBasis ((_,_,lab):edges) =

lab:((getProofBasis lab)++(calculateProofBasis edges))

{- returns the proofBasis contained in the given DGLinkLab -}

getProofBasis :: DGLinkLab -> [DGLinkLab]

getProofBasis lab =

case dgl_type lab of

(GlobalThm (Proven proofBasis) _ _) -> proofBasis

(LocalThm (Proven proofBasis) _ _) -> proofBasis

_ -> []

{- returns all proven paths from the given list -}

filterProvenPaths :: [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]

filterProvenPaths [] = []

filterProvenPaths (path:list) =

if (and [isProven edge| edge <- path]) then path:(filterProvenPaths list)

else filterProvenPaths list

{- opposite of isProofCycle -}

notProofCycle :: DGLinkLab -> [LEdge DGLinkLab] -> Bool

notProofCycle label = not.(isProofCycle label)

{- checks if the given label is contained in the ProofBasis of one of the

edges of the given path -}

isProofCycle :: DGLinkLab -> [LEdge DGLinkLab] -> Bool

isProofCycle _ [] = False

isProofCycle label (edge:path) =

if (elemOfProofBasis label edge) then True else (isProofCycle label path)

{- checks if the given label is contained in the ProofBasis of the given

edge -}

elemOfProofBasis :: DGLinkLab -> (LEdge DGLinkLab) -> Bool

elemOfProofBasis label (_,_,dglink) =

case dgl_type dglink of

(GlobalThm (Proven proofBasis) _ _) -> elem label proofBasis

(LocalThm (Proven proofBasis) _ _) -> elem label proofBasis

_ -> False

sensOfNode :: DGraph -> DGNodeLab -> G_l_sentence_list

sensOfNode dg (DGNode {dgn_sens = sens}) = sens

sensOfNode dg _ = undefined -- ??? to simplistic

-- | Calculate the morphism of a path with given start node

calculateMorphismOfPathWithStart :: DGraph -> (Node,[LEdge DGLinkLab])

-> Maybe GMorphism

calculateMorphismOfPathWithStart dg (n,[]) = do

ctx <- fst $ match n dg

return $ ide Grothendieck (dgn_sign (lab' ctx)) -- ??? to simplistic

calculateMorphismOfPathWithStart _ (_,p) = calculateMorphismOfPath p

-- | Compute the theory of a node (CASL Reference Manual, p. 294, Def. 4.9)

computeTheory :: DGraph -> Node -> Result (G_sign,G_l_sentence_list)

computeTheory dg n = do

ctx <- maybeToResult nullPos ("Could node find node "++show n)

$ fst $ match n dg

let nlab = lab' ctx

paths = getAllLocGlobDefPathsTo dg n []

mors <- maybeToResult nullPos "Could not calculate morphism of path"

$ sequence $ map (calculateMorphismOfPathWithStart dg) paths

ctxs <- maybeToResult nullPos "Could not find start node of path"

$ sequence $ map (fst . flip match dg . fst) paths

let sens = map (sensOfNode dg . lab') ctxs

sens' <- maybeToResult nullPos "Could not translate sentences"

$ sequence

$ map (resultToMaybe . uncurry translateG_l_sentence_list)

$ zip mors sens

sens'' <- maybeToResult nullPos "Logic mismatch for sentences"

$ flatG_l_sentence_list sens'

return (dgn_sign nlab,sens'') -- ??? dgn_sign too simplistic