Proofs.hs revision 788dd403da4203e895e15892ef7fa48129617d30
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Till Mossakowski
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski Proofs in development graphs.
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder T. Mossakowski, S. Autexier and D. Hutter:
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Extending Development Graphs With Hiding.
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder Lecture Notes in Computer Science 2029, p. 269-283,
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski Springer-Verlag 2001.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder CASL Proof calculus. In: CASL reference manual, part IV.
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederIntegrate stuff from Saarbr�cken
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederAdd proof status information
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder what should be in proof status:
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder- proofs of thm links according to rules
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder- cons, def and mono annos, and their proofs
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder{- proof status = (DG0,[(R1,DG1),...,(Rn,DGn)])
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder DG0 is the development graph resulting from the static analysis
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder Ri is a list of rules that transforms DGi-1 to DGi
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder With the list of intermediate proof states, one can easily implement
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder an undo operation
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maedertype ProofStatus = (GlobalContext,[([DGRule],[DGChange])],DGraph)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder TheoremHideShift
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder | HideTheoremShift
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder | Composition
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder | GlobDecomp (LEdge DGLinkLab) -- edge in the conclusion
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder | LocDecompII
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder | GlobSubsumption (LEdge DGLinkLab)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder | LocSubsumption (LEdge DGLinkLab)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder | LocalInference
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | BasicInference Edge BasicProof
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder | BasicConsInference Edge BasicConsProof
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederdata DGChange = InsertNode (LNode DGNodeLab)
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder | DeleteNode Node
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder | InsertEdge (LEdge DGLinkLab)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder | DeleteEdge (LEdge DGLinkLab)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederdata BasicProof =
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski forall lid sublogics
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang basic_spec sentence symb_items symb_map_items
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder sign morphism symbol raw_symbol proof_tree .
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder Logic lid sublogics
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder basic_spec sentence symb_items symb_map_items
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder sign morphism symbol raw_symbol proof_tree =>
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang BasicProof lid (Proof_status sentence proof_tree)
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder | Conjectured
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder | Handwritten
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskidata BasicConsProof = BasicConsProof -- more detail to be added ...
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{- todo: implement apply for GlobDecomp and Subsumption
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder the list of DGChage must be constructed in parallel to the
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder new DGraph -}
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian MaederapplyRule :: DGRule -> DGraph -> Maybe ([DGChange],DGraph)
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus LuettichapplyRule = error "Proofs.hs:applyRule"
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich-- ---------------------
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- global decomposition
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- ---------------------
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu{- apply rule GlobDecomp to all global theorem links in the current DG
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder current DG = DGm
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder add to proof status the pair ([GlobDecomp e1,...,GlobDecomp en],DGm+1)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder where e1...en are the global theorem links in DGm
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder DGm+1 results from DGm by application of GlobDecomp e1,...,GlobDecomp en -}
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder{- applies global decomposition to all unproven global theorem edges
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder if possible -}
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederglobDecomp :: ProofStatus -> ProofStatus
1a38107941725211e7c3f051f7a8f5e12199f03acmaederglobDecomp proofStatus@(globalContext,history,dgraph) =
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder if null (snd newHistoryElem) then proofStatus
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder else (globalContext, ((newHistoryElem):history), newDgraph)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder globalThmEdges = filter isUnprovenGlobalThm (labEdges dgraph)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder (newDgraph, newHistoryElem) = globDecompAux dgraph globalThmEdges ([],[])
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder{- auxiliary function for globDecomp (above)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder actual implementation -}
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederglobDecompAux :: DGraph -> [LEdge DGLinkLab] -> ([DGRule],[DGChange])
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder -> (DGraph,([DGRule],[DGChange]))
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederglobDecompAux dgraph [] historyElem = (dgraph, historyElem)
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederglobDecompAux dgraph (edge:edges) historyElem =
e6dccba746efe07338d3107fed512e713fd50b28Christian Maeder globDecompAux newDGraph edges newHistoryElem
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder (newDGraph, newChanges) = globDecompForOneEdge dgraph edge
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder newHistoryElem =
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder if null newChanges then historyElem
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder else (((GlobDecomp edge):(fst historyElem)),
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder (newChanges++(snd historyElem)))
9a6779c8495854bdf36e4a87f98f095e8d0a6e45Christian Maeder-- applies global decomposition to a single edge
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaederglobDecompForOneEdge :: DGraph -> LEdge DGLinkLab -> (DGraph,[DGChange])
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaederglobDecompForOneEdge dgraph edge =
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder globDecompForOneEdgeAux dgraph edge [] paths
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder pathsToSource = getAllLocGlobDefPathsTo dgraph (getSourceNode edge) []
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder paths = [(node, path++(edge:[]))| (node,path) <- pathsToSource]
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder{- auxiliary funktion for globDecompForOneEdge (above)
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder actual implementation -}
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaederglobDecompForOneEdgeAux :: DGraph -> LEdge DGLinkLab -> [DGChange] ->
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder [(Node, [LEdge DGLinkLab])] -> (DGraph,[DGChange])
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder{- if the list of paths is empty from the beginning, nothing is done
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder otherwise the unprovenThm edge is replaced by a proven one -}
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaederglobDecompForOneEdgeAux dgraph edge@(source,target,edgeLab) changes [] =
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder if null changes then (dgraph, [])
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder else ((insEdge provenEdge (delLEdge edge dgraph)),
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder ((DeleteEdge edge):((InsertEdge provenEdge):changes)))
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder (GlobalThm _ conservativity) = (dgl_type edgeLab)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder provenEdge = (source,
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder DGLink {dgl_morphism = dgl_morphism edgeLab,
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder dgl_type = (GlobalThm True conservativity),
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder dgl_origin = DGProof}
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- for each path an unproven localThm edge is inserted
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederglobDecompForOneEdgeAux dgraph edge@(source,target,edgeLab) changes
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder ((node,path):list) =
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder globDecompForOneEdgeAux newGraph edge newChanges list
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder morphism = case calculateMorphismOfPath path of
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Just morph -> morph
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder error "globDecomp: could not determine morphism of new edge"
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder (GlobalThm _ conservativity) = (dgl_type edgeLab)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder newEdge = (node,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski DGLink {dgl_morphism = morphism,
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder dgl_type = (LocalThm False conservativity),
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_origin = DGProof}
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski newGraph = insEdge newEdge dgraph
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder newChanges = ((InsertEdge newEdge):changes)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- -------------------
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- global subsumption
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder-- -------------------
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder-- applies global subsumption to all unproven global theorem edges if possible
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederglobSubsume :: ProofStatus -> ProofStatus
26d11a256b1433604a3dbc69913b520fff7586acChristian MaederglobSubsume proofStatus@(globalContext,history,dGraph) =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder if null (snd nextHistoryElem) then proofStatus
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else (globalContext, nextHistoryElem:history, nextDGraph)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder globalThmEdges = filter isUnprovenGlobalThm (labEdges dGraph)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder result = globSubsumeAux dGraph ([],[]) globalThmEdges
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder nextDGraph = fst result
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder nextHistoryElem = snd result
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder{- auxiliary function for globSubsume (above)
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder the actual implementation -}
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaederglobSubsumeAux :: DGraph -> ([DGRule],[DGChange]) -> [LEdge DGLinkLab]
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder -> (DGraph,([DGRule],[DGChange]))
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaederglobSubsumeAux dGraph historyElement [] = (dGraph, historyElement)
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaederglobSubsumeAux dGraph (rules,changes) ((ledge@(source,target,edgeLab)):list) = if existsProvenPathOfMorphismBetween dGraph morphism source target
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder globSubsumeAux newGraph (newRules,newChanges) list
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder globSubsumeAux dGraph (rules,changes) list
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder morphism = dgl_morphism edgeLab
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder auxGraph = delLEdge ledge dGraph
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (GlobalThm _ conservativity) = (dgl_type edgeLab)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder newEdge = (source,
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski DGLink {dgl_morphism = morphism,
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder dgl_type = (GlobalThm True conservativity),
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder dgl_origin = DGProof}
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder newGraph = insEdge newEdge auxGraph
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder newRules = (GlobSubsumption ledge):rules
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder newChanges = (DeleteEdge ledge):((InsertEdge newEdge):changes)
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder-- ------------------
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz-- local subsumption
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder-- ------------------
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz{- the same as globSubsume, but for the rule LocSubsumption -}
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder-- applies local Subsumption to all unproven localThm edges if possible
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaederlocSubsume :: ProofStatus -> ProofStatus
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaederlocSubsume proofStatus@(globalContext,history,dGraph) =
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder if null (snd nextHistoryElem) then proofStatus
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder else (globalContext, nextHistoryElem:history, nextDGraph)
4e3c46a1ca40d50a045342c5fab25b5db4fa9a87Christian Maeder localThmEdges = filter isUnprovenLocalThm (labEdges dGraph)
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder result = locSubsumeAux dGraph ([],[]) localThmEdges
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder nextDGraph = fst result
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz nextHistoryElem = snd result
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz{- auxiliary function for locSubsume (above)
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz actual implementation -}
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzlocSubsumeAux :: DGraph -> ([DGRule],[DGChange]) -> [LEdge DGLinkLab]
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> (DGraph,([DGRule],[DGChange]))
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederlocSubsumeAux dgraph historyElement [] = (dgraph, historyElement)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederlocSubsumeAux dgraph (rules,changes) ((ledge@(source,target,edgeLab)):list) =
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder if existsLocGlobDefPathOfMorphismBetween dgraph morphism source target
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder globSubsumeAux newGraph (newRules,newChanges) list
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder globSubsumeAux dgraph (rules,changes) list
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder morphism = dgl_morphism edgeLab
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder auxGraph = delLEdge ledge dgraph
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder (LocalThm _ conservativity) = (dgl_type edgeLab)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder newEdge = (source,
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder DGLink {dgl_morphism = morphism,
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder dgl_type = (LocalThm True conservativity),
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder dgl_origin = DGProof}
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder newGraph = insEdge newEdge auxGraph
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder newRules = (LocSubsumption ledge):rules
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder newChanges = (DeleteEdge ledge):((InsertEdge newEdge):changes)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder-- -----------------------------------------------------------------------
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder-- methods that check if paths of certain types exist between given nodes
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder-- -----------------------------------------------------------------------
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder{- checks if there is a path of globalDef edges or proven globalThm edges
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder with the given morphism between the given source and target node -}
568da6120906d5283c4322114eee10f24ea8dd6dChristian MaederexistsProvenPathOfMorphismBetween :: DGraph -> GMorphism -> Node -> Node
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederexistsProvenPathOfMorphismBetween dgraph morphism src tgt =
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder -- @@@ zum Testen: not (null (concat allDefPathsBetween))
4e144aa4be1f50519f8fa377a7883edfbc76d406Christian Maeder elem morphism filteredMorphismsOfProvenPaths
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder allPaths = getAllProvenPathsBetween dgraph src tgt
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder ([]::[LEdge DGLinkLab])
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder morphismsOfPaths = map calculateMorphismOfPath allPaths
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder filteredMorphismsOfProvenPaths = getFilteredMorphisms morphismsOfPaths
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder{- checks if a path consisting of globalDef edges only
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder or consisting of a localDef edge followed by any number of globalDef edges
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder exists between the given nodes -}
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederexistsLocGlobDefPathOfMorphismBetween :: DGraph -> GMorphism -> Node -> Node
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederexistsLocGlobDefPathOfMorphismBetween dgraph morphism src tgt =
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder elem morphism filteredMorphismsOfLocGlobDefPaths
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder allPaths = getAllLocGlobDefPathsBetween dgraph src tgt
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder morphismsOfPaths =
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder map calculateMorphismOfPath allPaths
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder filteredMorphismsOfLocGlobDefPaths =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski getFilteredMorphisms morphismsOfPaths
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- ----------------------------------------------
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- methods that calculate paths of certain types
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder-- ----------------------------------------------
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- @@@ this method is not used at the momen!! @@@
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder{- returns a list of all paths to the given node
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder that consist of globalDef edges or proven global theorems only
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder that consist of a localDef/proven local theorem edge followed by
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder any number of globalDef/proven global theorem edges -}
99476ac2689c74251219db4782e57fe713a24a52Christian MaedergetAllProvenLocGlobPathsTo :: DGraph -> Node -> [LEdge DGLinkLab]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> [(Node, [LEdge DGLinkLab])]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedergetAllProvenLocGlobPathsTo dgraph node path =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (node,path):(locGlobPaths ++
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder [getAllProvenLocGlobPathsTo dgraph (getSourceNode edge) path|
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (_, path@(edge:edges)) <- globalPaths]))
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder inEdges = inn dgraph node
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder globalEdges = (filter isGlobalDef inEdges)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ++ (filter isProvenGlobalThm inEdges)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder localEdges = (filter isLocalDef inEdges)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ++ (filter isProvenLocalThm inEdges)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder globalPaths = [(getSourceNode edge, (edge:path))| edge <- globalEdges]
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder locGlobPaths = [(getSourceNode edge, (edge:path))| edge <- localEdges]
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder{- returns a list of all paths to the given node
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder that consist of globalDef edges only
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder that consist of a localDef edge followed by any number of globalDef edges -}
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedergetAllLocGlobDefPathsTo :: DGraph -> Node -> [LEdge DGLinkLab]
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> [(Node, [LEdge DGLinkLab])]
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedergetAllLocGlobDefPathsTo dgraph node path =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (node,path):(locGlobPaths ++
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder [getAllLocGlobDefPathsTo dgraph (getSourceNode edge) path|
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (_, path@(edge:edges)) <- globalPaths]))
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder inEdges = inn dgraph node
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder globalEdges = filter isGlobalDef inEdges
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder localEdges = filter isLocalDef inEdges
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder globalPaths = [(getSourceNode edge, (edge:path))| edge <- globalEdges]
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder locGlobPaths = [(getSourceNode edge, (edge:path))| edge <- localEdges]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder{- returns all paths of globalDef edges or proven globalThm edges
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski between the given source and target node -}
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedergetAllProvenPathsBetween :: DGraph -> Node -> Node -> [LEdge DGLinkLab]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> [[LEdge DGLinkLab]]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedergetAllProvenPathsBetween dgraph src tgt path =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder getAllPathsOfTypesBetween dgraph [isGlobalDef,isProvenGlobalThm] src tgt []
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder{- returns all paths of globalDef edges between the given source and
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder target node -}
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedergetAllDefPathsBetween :: DGraph -> Node -> Node -> [LEdge DGLinkLab]
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -> [[LEdge DGLinkLab]]
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedergetAllDefPathsBetween dgraph src tgt path =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder getAllPathsOfTypeBetween dgraph isGlobalDef src tgt
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder{- returns all paths consiting of edges of the given type between the
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder given node -}
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedergetAllPathsOfTypeBetween :: DGraph -> (LEdge DGLinkLab -> Bool) -> Node
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder -> Node -> [[LEdge DGLinkLab]]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedergetAllPathsOfTypeBetween dgraph isType src tgt =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder getAllPathsOfTypesBetween dgraph (isType:[]) src tgt []
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder{- returns all paths consisting of edges of the given types between
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder the given nodes -}
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedergetAllPathsOfTypesBetween :: DGraph -> [LEdge DGLinkLab -> Bool] -> Node
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> Node -> [LEdge DGLinkLab]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> [[LEdge DGLinkLab]]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedergetAllPathsOfTypesBetween dgraph types src tgt path =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder [edge:path| edge <- edgesFromSrc]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder [getAllPathsOfTypesBetween dgraph types src nextTgt (edge:path)|
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (edge,nextTgt) <- nextStep] )
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder inGoingEdges = inn dgraph tgt
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder edgesOfTypes = filterByTypes types inGoingEdges
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder edgesFromSrc =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder [edge| edge@(source,_,_) <- edgesOfTypes, source == src]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder [(edge, source)| edge@(source,_,_) <- edgesOfTypes, source /= src]
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder{- returns a list of all paths between the given nodes
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder that consist only of globalDef edges
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder that consist of a localDef edge followed by any number of globalDef edges -}
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedergetAllLocGlobDefPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedergetAllLocGlobDefPathsBetween dgraph src tgt = globDefPaths ++ locGlobDefPaths
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder globDefPaths = getAllDefPathsBetween dgraph src tgt ([]::[LEdge DGLinkLab])
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder outEdges = out dgraph src
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder nextStep = [(edge,getTargetNode edge) | edge <- outEdges]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder [(edge,getAllDefPathsBetween dgraph node tgt ([]::[LEdge DGLinkLab]))|
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (edge, node) <- nextStep]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder locGlobDefPaths =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder concat [addToAll edge paths | (edge, paths) <- pathEnds]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder-- adds the given element at the front of all lists in the given list
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederaddToAll :: a -> [[a]] -> [[a]]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaederaddToAll _ [] = []
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaederaddToAll element (list:lists) = (element:list):(addToAll element lists)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- removes all edges that are not of the given types
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaederfilterByTypes :: [LEdge DGLinkLab -> Bool] -> [LEdge DGLinkLab]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> [LEdge DGLinkLab]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaederfilterByTypes [] edges = edges
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaederfilterByTypes (isType:typeChecks) edges =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (filter isType edges)++(filterByTypes typeChecks edges)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- --------------------------------------
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- methods to determine or get morphisms
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder-- --------------------------------------
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder-- determines the morphism of a given path
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaedercalculateMorphismOfPath :: [LEdge DGLinkLab] -> Maybe GMorphism
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaedercalculateMorphismOfPath [] = error "getMorphismOfPath: empty path"
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedercalculateMorphismOfPath path@((src,tgt,edgeLab):furtherPath) =
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder case maybeMorphismOfFurtherPath of
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Nothing -> Nothing
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Just morphismOfFurtherPath ->
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder comp Grothendieck morphism morphismOfFurtherPath
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder morphism = dgl_morphism edgeLab
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder maybeMorphismOfFurtherPath = calculateMorphismOfPath furtherPath
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder{- removes the "Nothing"s from a list of Maybe GMorphism
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder returns the remaining elements as plain GMorphisms -}
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaedergetFilteredMorphisms :: [Maybe GMorphism] -> [GMorphism]
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaedergetFilteredMorphisms morphisms =
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder [morph| (Just morph) <- filter isValidMorphism morphisms]
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder-- returns True if the given Maybe GMorphisms is not "Nothing"
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederisValidMorphism :: Maybe GMorphism -> Bool
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederisValidMorphism morphism =
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder case morphism of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Nothing -> False
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder otherwise -> True
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder-- ------------------------------------
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder-- methods to get the nodes of an edge
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder-- ------------------------------------
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaedergetSourceNode :: LEdge DGLinkLab -> Node
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaedergetSourceNode (source,_,_) = source
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaedergetTargetNode :: LEdge DGLinkLab -> Node
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedergetTargetNode (_,target,_) = target
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder-- -------------------------------------
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder-- methods to check the type of an edge
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder-- -------------------------------------
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian MaederisProvenGlobalThm :: LEdge DGLinkLab -> Bool
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian MaederisProvenGlobalThm (_,_,edgeLab) =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder case dgl_type edgeLab of
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder (GlobalThm True _) -> True
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder otherwise -> False
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederisUnprovenGlobalThm :: LEdge DGLinkLab -> Bool
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederisUnprovenGlobalThm (_,_,edgeLab) =
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder case dgl_type edgeLab of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (GlobalThm False _) -> True
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder otherwise -> False
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederisProvenLocalThm :: LEdge DGLinkLab -> Bool
4072adb8c5d2c86123e8e1c1918263968f187829Christian MaederisProvenLocalThm (_,_,edgeLab) =
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder case dgl_type edgeLab of
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder (LocalThm True _) -> True
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder otherwise -> False
4072adb8c5d2c86123e8e1c1918263968f187829Christian MaederisUnprovenLocalThm :: LEdge DGLinkLab -> Bool
4072adb8c5d2c86123e8e1c1918263968f187829Christian MaederisUnprovenLocalThm (_,_,edgeLab) =
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder case dgl_type edgeLab of
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder (LocalThm False _) -> True
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder otherwise -> False
4072adb8c5d2c86123e8e1c1918263968f187829Christian MaederisGlobalDef :: LEdge DGLinkLab -> Bool
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian MaederisGlobalDef (_,_,edgeLab) =
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder case dgl_type edgeLab of
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder GlobalDef -> True
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder otherwise -> False
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian MaederisLocalDef :: LEdge DGLinkLab -> Bool
5e46b572ed576c0494768998b043d9d340594122Till MossakowskiisLocalDef (_,_,edgeLab) =
74d9a385499bf903b24848dff450a153f525bda7Christian Maeder case dgl_type edgeLab of
da5f197255c3e060416a2aa34cc94e7bf42365e3Christian Maeder LocalDef -> True
da5f197255c3e060416a2aa34cc94e7bf42365e3Christian Maeder otherwise -> False