Proofs.hs revision 797595aad6dfd626bc1c9df52616f1ac4235c669
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{-# OPTIONS -cpp #-}
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
81d182b21020b815887e9057959228546cf61b6bChristian Maeder{-|
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederModule : $Header$
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederCopyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2004
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
fbb66ee3e170624835b99f7aa91980753cb5b472Christian MaederMaintainer : jfgerken@tzi.de
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederStability : provisional
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederPortability : non-portable(Logic)
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder Proofs in development graphs.
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder Follows Sect. IV:4.4 of the CASL Reference Manual.
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder-}
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder{-
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder References:
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder T. Mossakowski, S. Autexier and D. Hutter:
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder Extending Development Graphs With Hiding.
722e8a91f69209ba0e99bf799c4989801d78cf16Christian Maeder H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder Lecture Notes in Computer Science 2029, p. 269-283,
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder Springer-Verlag 2001.
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedertodo in general:
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederOrder of rule application: try to use local links induced by %implies
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederfor subsumption proofs (such that the %implied formulas need not be
33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maederre-proved)
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaederIntegrate stuff from Saarbr�cken
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaederAdd proof status information
e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder what should be in proof status:
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder- proofs of thm links according to rules
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder- cons, def and mono annos, and their proofs
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maedertodo for Jorina:
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder todo:
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder - bei GlobDecomp hinzuf�gen:
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder zus�tzlich alle Pfade K<--theta-- M --sigma-->N in den aktuellen
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder Knoten N, die mit einem HidingDef anfangen, und danach nur GlobalDef
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder theta ist der Signaturmorphismus des HidingDef's (geht "falsch rum")
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski sigma ist die Komposition der Signaturmorphismen auf dem restl. Pfad
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder f�r jeden solchen Pfad: einen HidingThm theta einf�gen. sigma ist
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder der normale Morphismus (wie bei jedem anderen Link)
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder siehe auch Seite 302 des CASL Reference Manual
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-}
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maedermodule Proofs.Proofs where
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maederimport Options
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maederimport Data.Dynamic
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maederimport Logic.Logic
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Logic.Prover
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maederimport Logic.Grothendieck
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maederimport Logic.Comorphism
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maederimport Static.DevGraph
4cf9b5b0484a15c0f071ef7898cdcc3a44a15429Christian Maederimport Common.Result
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maederimport Common.Lib.Graph
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maederimport Common.Lib.Set (fromList)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maederimport qualified Common.Lib.Map as Map
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maederimport Data.List(nub)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maederimport Data.Maybe
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maederimport Common.Id
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maederimport Common.AS_Annotation
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Syntax.AS_Library
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maederimport Syntax.Print_AS_Library
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder#ifdef UNI_PACKAGE
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maederimport GUI.HTkUtils
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder#endif
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder{-
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder proof status = (DG0,[(R1,DG1),...,(Rn,DGn)])
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder DG0 is the development graph resulting from the static analysis
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder Ri is a list of rules that transforms DGi-1 to DGi
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder With the list of intermediate proof states, one can easily implement
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder an undo operation
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder-}
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maedertype ProofStatus = (GlobalContext,LibEnv,[([DGRule],[DGChange])],DGraph)
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederdata DGRule =
961fc5d08256957f68f245f2723085ced14a0a1fChristian Maeder TheoremHideShift
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder | HideTheoremShift
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder | Borrowing
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | ConsShift
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | DefShift
961fc5d08256957f68f245f2723085ced14a0a1fChristian Maeder | MonoShift
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder | ConsComp
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder | DefComp
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | MonoComp
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | DefToMono
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | MonoToCons
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | FreeIsMono
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | MonoIsFree
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | Composition
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | GlobDecomp (LEdge DGLinkLab) -- edge in the conclusion
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | LocDecomp (LEdge DGLinkLab)
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | LocSubsumption (LEdge DGLinkLab)
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | GlobSubsumption (LEdge DGLinkLab)
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | LocalInference
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | BasicInferendge BasicProof
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | BasicConsInference Edge BasicConsProof
df2a122c5ecd7d995323c3f0754e1a2a4e3dc0a8Christian Maeder deriving (Eq, Show)
df2a122c5ecd7d995323c3f0754e1a2a4e3dc0a8Christian Maeder
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maederdata DGChange = InsertNode (LNode DGNodeLab)
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder | DeleteNode (LNode DGNodeLab)
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | InsertEdge (LEdge DGLinkLab)
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder | DeleteEdge (LEdge DGLinkLab)
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder deriving (Eq,Show)
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maederdata BasicProof =
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder forall lid sublogics
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder basic_spec sentence symb_items symb_map_items
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder sign morphism symbol raw_symbol proof_tree .
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder Logic lid sublogics
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder basic_spec sentence symb_items symb_map_items
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder sign morphism symbol raw_symbol proof_tree =>
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder BasicProof lid (Proof_status proof_tree)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder | Guessed
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder | Conjectured
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder | Handwritten
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
5964438458028e61fdabfa74ca3b4210206cdba6Christian Maederinstance Eq BasicProof where
5964438458028e61fdabfa74ca3b4210206cdba6Christian Maeder Guessed == Guessed = True
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder Conjectured == Conjectured = True
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder Handwritten == Handwritten = True
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder BasicProof lid1 p1 == BasicProof lid2 p2 =
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder coerce lid1 lid2 p1 == Just p2
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederinstance Show BasicProof where
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder show (BasicProof lid1 p1) = show p1
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder show Guessed = "Guessed"
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder show Conjectured = "Conjectured"
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder show Handwritten = "Handwritten"
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder
d48085f765fca838c1d972d2123601997174583dChristian Maederdata BasicConsProof = BasicConsProof -- more detail to be added ...
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder deriving (Eq, Show)
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder{- todo: implement apply for GlobDecomp and Subsumption
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder the list of DGChage must be constructed in parallel to the
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder new DGraph -}
f6fc70956d64365527d77a521a96f54a1cc18f91Christian MaederapplyRule :: DGRule -> DGraph -> Maybe ([DGChange],DGraph)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederapplyRule = error "Proofs.hs:applyRule"
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maederautomatic :: ProofStatus -> ProofStatus
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maederautomatic proofStatus =
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder (globalContext, libEnv, newHistory, dgraph)
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder where
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder (globalContext, libEnv, history, dgraph)
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder = automaticAux proofStatus
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder (newHistoryPart, oldHistory) = splitAt 4 history
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder (rules, changes) = concatHistoryElems (reverse newHistoryPart)
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder newHistoryElem = (rules, removeContraryChanges changes)
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder newHistory = newHistoryElem:oldHistory
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederremoveContraryChanges :: [DGChange] -> [DGChange]
149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian MaederremoveContraryChanges [] = []
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederremoveContraryChanges (change:changes) =
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder if elem contraryChange changes
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder then removeContraryChanges (removeChange contraryChange changes)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder else change:(removeContraryChanges changes)
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder where
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder contraryChange = getContraryChange change
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian MaedergetContraryChange :: DGChange -> DGChange
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian MaedergetContraryChange change =
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder case change of
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder InsertEdge edge -> DeleteEdge edge
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder DeleteEdge edge -> InsertEdge edge
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder InsertNode node -> DeleteNode node
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder DeleteNode node -> InsertNode node
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian Maeder
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaederremoveChange :: DGChange -> [DGChange] -> [DGChange]
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaederremoveChange change changes =
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian Maeder (takeWhile (change /=) changes)
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder ++(tail (dropWhile (change /=) changes))
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederautomaticAux :: ProofStatus -> ProofStatus
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederautomaticAux = locDecomp.locSubsume.globDecomp.globSubsume
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederconcatHistoryElems :: [([DGRule],[DGChange])] -> ([DGRule],[DGChange])
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederconcatHistoryElems [] = ([],[])
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederconcatHistoryElems ((rules,changes):elems) =
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder (rules++(fst (concatHistoryElems elems)),changes++(snd (concatHistoryElems elems)))
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder-- ---------------------
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder-- global decomposition
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder-- ---------------------
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder{- apply rule GlobDecomp to all global theorem links in the current DG
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder current DG = DGm
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder add to proof status the pair ([GlobDecomp e1,...,GlobDecomp en],DGm+1)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder where e1...en are the global theorem links in DGm
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder DGm+1 results from DGm by application of GlobDecomp e1,...,GlobDecomp en -}
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder{- applies global decomposition to all unproven global theorem edges
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder if possible -}
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederglobDecomp :: ProofStatus -> ProofStatus
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederglobDecomp proofStatus@(globalContext,libEnv,history,dgraph) =
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder (globalContext, libEnv, ((finalHistoryElem):history), finalDGraph)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder where
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder globalThmEdges = filter isUnprovenGlobalThm (labEdges dgraph)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder (newDGraph, newHistoryElem) = globDecompAux dgraph globalThmEdges ([],[])
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder (finalDGraph, finalHistoryElem)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder = removeSuperfluousInsertions newDGraph newHistoryElem
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder{- removes all superfluous insertions from the list of changes as well as
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder from the development graph (i.e. insertions of edges that are
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder equivalent to edges or paths resulting from the other insertions) -}
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederremoveSuperfluousInsertions :: DGraph -> ([DGRule],[DGChange])
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder -> (DGraph,([DGRule],[DGChange]))
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaederremoveSuperfluousInsertions dgraph (rules,changes)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder = (newDGraph,(rules,newChanges))
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder where
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder localThms = [edge | (InsertEdge edge)
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder <- filter isLocalThmInsertion changes]
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder (newDGraph, localThmsToInsert)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder = removeSuperfluousEdges dgraph localThms
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder newChanges = (filter (not.isLocalThmInsertion) changes)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder ++ [InsertEdge edge | edge <- localThmsToInsert]
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder{- auxiliary function for globDecomp (above)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder actual implementation -}
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederglobDecompAux :: DGraph -> [LEdge DGLinkLab] -> ([DGRule],[DGChange])
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder -> (DGraph,([DGRule],[DGChange]))
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederglobDecompAux dgraph [] historyElem = (dgraph, historyElem)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederglobDecompAux dgraph (edge:edges) historyElem =
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder globDecompAux newDGraph edges newHistoryElem
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder where
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder (newDGraph, newChanges) = globDecompForOneEdge dgraph edge
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder newHistoryElem = (((GlobDecomp edge):(fst historyElem)),
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder (newChanges++(snd historyElem)))
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder-- applies global decomposition to a single edge
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederglobDecompForOneEdge :: DGraph -> LEdge DGLinkLab -> (DGraph,[DGChange])
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederglobDecompForOneEdge dgraph edge =
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder globDecompForOneEdgeAux dgraph edge [] paths
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder where
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder pathsToSource
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder = getAllLocOrHideGlobDefPathsTo dgraph (getSourceNode edge) []
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder paths = [(node, path++(edge:[]))| (node,path) <- pathsToSource]
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder{- auxiliary funktion for globDecompForOneEdge (above)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder actual implementation -}
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederglobDecompForOneEdgeAux :: DGraph -> LEdge DGLinkLab -> [DGChange] ->
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder [(Node, [LEdge DGLinkLab])] -> (DGraph,[DGChange])
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder{- if the list of paths is empty from the beginning, nothing is done
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder otherwise the unprovenThm edge is replaced by a proven one -}
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederglobDecompForOneEdgeAux dgraph edge@(source,target,edgeLab) changes [] =
if null changes then (dgraph, changes)
else
if isDuplicate provenEdge dgraph changes
then (delLEdge edge dgraph,
((DeleteEdge edge):changes))
else ((insEdge provenEdge (delLEdge edge dgraph)),
((DeleteEdge edge):((InsertEdge provenEdge):changes)))
where
(GlobalThm _ conservativity conservStatus) = (dgl_type edgeLab)
proofBasis = getLabelsOfInsertedEdges changes
provenEdge = (source,
target,
DGLink {dgl_morphism = dgl_morphism edgeLab,
dgl_type =
(GlobalThm (Proven proofBasis)
conservativity conservStatus),
dgl_origin = DGProof}
)
-- for each path an unproven localThm edge is inserted
globDecompForOneEdgeAux dgraph edge@(source,target,edgeLab) changes
((node,path):list) =
if isRedundant newEdge dgraph changes list
then globDecompForOneEdgeAux dgraph edge changes list
else globDecompForOneEdgeAux newGraph edge newChanges list
where
isHiding = not (null path) && isHidingDef (head path)
morphismPath = if isHiding then tail path else path
morphism = case calculateMorphismOfPath morphismPath of
Just morph -> morph
Nothing ->
error "globDecomp: could not determine morphism of new edge"
newEdge = if isHiding then hidingEdge else localEdge
hidingEdge =
(node,
target,
DGLink {dgl_morphism = morphism,
dgl_type = (HidingThm (dgl_morphism (getLabelOfEdge (head path))) (Static.DevGraph.Open)),
dgl_origin = DGProof})
localEdge = (node,
target,
DGLink {dgl_morphism = morphism,
dgl_type = (LocalThm (Static.DevGraph.Open)
None (Static.DevGraph.Open)),
dgl_origin = DGProof}
)
newGraph = insEdge newEdge dgraph
newChanges = ((InsertEdge newEdge):changes)
-- -------------------
-- global subsumption
-- -------------------
-- local debug method
printEdges :: [LEdge DGLinkLab] -> String
printEdges [] = ""
printEdges ((edge@(src,tgt,label)):edges) =
"("++(show src)++", "++(show tgt)++", dgl_type=<<"++(show (dgl_type label))++">>\ndgl_origin=<<"++(show (dgl_origin label))++">>\ndgl_morphism=<<"++(show (dgl_morphism label))++">>)\n\n"++(printEdges edges)
-- applies global subsumption to all unproven global theorem edges if possible
globSubsume :: ProofStatus -> ProofStatus
globSubsume proofStatus@(globalContext,libEnv,history,dGraph) =
(globalContext, libEnv, nextHistoryElem:history, nextDGraph)
where
globalThmEdges = filter isUnprovenGlobalThm (labEdges dGraph)
-- the 'nub' is just a workaround, because some of the edges in the graph
-- do not differ from each other in this represetation - which causes
-- problems on deletion
result = globSubsumeAux libEnv dGraph ([],[]) (nub globalThmEdges)
nextDGraph = fst result
nextHistoryElem = snd result
{- auxiliary function for globSubsume (above)
the actual implementation -}
globSubsumeAux :: LibEnv -> DGraph -> ([DGRule],[DGChange]) ->
[LEdge DGLinkLab] -> (DGraph,([DGRule],[DGChange]))
globSubsumeAux _ dgraph historyElement [] = (dgraph, historyElement)
globSubsumeAux libEnv dgraph (rules,changes) ((ledge@(src,tgt,edgeLab)):list) =
if not (null proofBasis) || isIdentityEdge ledge libEnv dgraph
then
if isDuplicate newEdge dgraph changes then
globSubsumeAux libEnv (delLEdge ledge dgraph)
(newRules,(DeleteEdge ledge):changes) list
else
globSubsumeAux libEnv (insEdge newEdge (delLEdge ledge dgraph))
(newRules,(DeleteEdge ledge):((InsertEdge newEdge):changes)) list
else
globSubsumeAux libEnv dgraph (rules,changes) list
where
morphism = dgl_morphism edgeLab
allPaths = getAllGlobPathsOfMorphismBetween dgraph morphism src tgt
filteredPaths = [path| path <- allPaths, notElem ledge path]
proofBasis = selectProofBasis edgeLab filteredPaths
(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
-- --------------------
-- 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,libEnv,history,dGraph) =
(globalContext, libEnv, nextHistoryElem:history, nextDGraph)
where
localThmEdges = filter isUnprovenLocalThm (labEdges dGraph)
result = locDecompAux libEnv dGraph ([],[]) localThmEdges
nextDGraph = fst result
nextHistoryElem = snd result
{- auxiliary function for locDecomp (above)
actual implementation -}
locDecompAux :: LibEnv -> DGraph -> ([DGRule],[DGChange]) -> [LEdge DGLinkLab]
-> (DGraph,([DGRule],[DGChange]))
locDecompAux libEnv dgraph historyElement [] = (dgraph, historyElement)
locDecompAux libEnv dgraph (rules,changes) ((ledge@(src,tgt,edgeLab)):list) =
if (null proofBasis && not (isIdentityEdge ledge libEnv dgraph))
then
locDecompAux libEnv dgraph (rules,changes) list
else
if isDuplicate newEdge dgraph changes
then locDecompAux libEnv auxGraph
(newRules,(DeleteEdge ledge):changes) list
else locDecompAux libEnv newGraph (newRules,newChanges) list
where
morphism = dgl_morphism edgeLab
allPaths = getAllLocGlobPathsBetween dgraph src tgt
th = computeLocalTheory libEnv dgraph src
pathsWithoutEdgeItself = [path|path <- allPaths, notElem ledge path]
filteredPaths = filterByTranslation th morphism pathsWithoutEdgeItself
proofBasis = selectProofBasis edgeLab filteredPaths
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)
{- compute the theory of a given node.
If this node is a DGRef, the referenced node is looked up first. -}
computeLocalTheory :: LibEnv -> DGraph -> Node -> Maybe G_theory
computeLocalTheory libEnv dgraph node =
if isDGRef nodeLab
then case Map.lookup (dgn_libname nodeLab) libEnv of
Just (_,_,refDgraph) -> computeLocalTheory libEnv refDgraph (dgn_node nodeLab)
Nothing -> Nothing
else toG_theory (dgn_sign nodeLab) (dgn_sens nodeLab)
where nodeLab = lab' (context node dgraph)
{- returns the sentence list of the given node -}
getSignature :: LibEnv -> DGraph -> Node -> Maybe G_sign
getSignature libEnv dgraph node =
if isDGRef nodeLab
then case Map.lookup (dgn_libname nodeLab) libEnv of
Just (_,_,refDgraph) ->
getSignature libEnv refDgraph (dgn_node nodeLab)
Nothing -> Nothing
else Just (dgn_sign nodeLab)
where nodeLab = lab' (context node dgraph)
{- removes all paths from the given list of paths whose morphism does not translate the given sentence list to the same resulting sentence list as the given morphism-}
filterByTranslation :: Maybe G_theory -> GMorphism -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
filterByTranslation maybeTh morphism paths =
case maybeTh of
Just th -> [path| path <- paths, isSameTranslation th morphism path]
Nothing -> []
-- isSameTranslation th morphism (calculateMorphismOfPath path)]
{- checks if the given morphism and the morphism of the given path translate the given sentence list to the same resulting sentence list -}
isSameTranslation :: G_theory -> GMorphism -> [LEdge DGLinkLab] -> Bool
isSameTranslation th morphism path =
case calculateMorphismOfPath path of
Just morphismOfPath ->
translateG_theory morphism th == translateG_theory morphismOfPath th
Nothing -> False
-- ----------------------------------------------
-- local subsumption
-- ----------------------------------------------
-- applies local subsumption to all unproven local theorem edges
locSubsume :: ProofStatus -> ProofStatus
locSubsume proofStatus@(globalContext,libEnv,history,dGraph) =
(globalContext, libEnv, nextHistoryElem:history, nextDGraph)
where
localThmEdges = filter isUnprovenLocalThm (labEdges dGraph)
result = locSubsumeAux libEnv dGraph ([],[]) localThmEdges
nextDGraph = fst result
nextHistoryElem = snd result
-- auxiliary method for locSubsume
locSubsumeAux :: LibEnv -> DGraph -> ([DGRule],[DGChange]) -> [LEdge DGLinkLab]
-> (DGraph,([DGRule],[DGChange]))
locSubsumeAux libEnv dgraph historyElement [] = (dgraph, historyElement)
locSubsumeAux libEnv dgraph (rules,changes) ((ledge@(src,tgt,edgeLab)):list) =
case (getDGNode libEnv dgraph tgt, maybeThSrc) of
(Just (target,_), Just thSrc) ->
case (maybeResult (computeTheory libEnv dgraph target), maybeResult (translateG_theory morphism thSrc)) of
(Just theoryTgt, Just (G_theory lidSrc _ sensSrc)) ->
case maybeResult (coerceTheory lidSrc theoryTgt) of
Nothing -> locSubsumeAux libEnv dgraph (rules,changes) list
Just (_,sentencesTgt) ->
if (all (`elem` sentencesTgt) sensSrc)
then locSubsumeAux libEnv newGraph (newRules,newChanges) list
else locSubsumeAux libEnv dgraph (rules,changes) list
otherwise -> locSubsumeAux libEnv dgraph (rules,changes) list
otherwise -> -- showDiags defaultHetcatsOpts (errSrc++errTgt)
locSubsumeAux libEnv dgraph (rules,changes) list
where
morphism = dgl_morphism edgeLab
maybeThSrc = computeLocalTheory libEnv dgraph src
auxGraph = delLEdge ledge dgraph
(LocalThm _ conservativity conservStatus) = (dgl_type edgeLab)
newEdge = (src,
tgt,
DGLink {dgl_morphism = morphism,
dgl_type =
(LocalThm (Proven [])
conservativity conservStatus),
dgl_origin = DGProof}
)
newGraph = insEdge newEdge auxGraph
newRules = (LocSubsumption ledge):rules
newChanges = (DeleteEdge ledge):((InsertEdge newEdge):changes)
{- if the given node is a DGRef, the referenced node is returned (as a labeled node). Otherwise the node itself is returned (as a labeled node).-}
getDGNode :: LibEnv -> DGraph -> Node -> Maybe (LNode DGNodeLab)
getDGNode libEnv dgraph node =
if isDGRef nodeLab then case Map.lookup (dgn_libname nodeLab) libEnv of
Just (_,_,refDgraph) ->
getDGNode libEnv refDgraph (dgn_node nodeLab)
Nothing -> Nothing
else Just (labNode' contextOfNode)
where contextOfNode = (context node dgraph)
nodeLab = lab' contextOfNode
-- ----------------------------------------------
-- 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
{- 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 edge only
or
that consist of a localDef or hidingDef edge
followed by any number of globalDef edges -}
getAllLocOrHideGlobDefPathsTo :: DGraph -> Node -> [LEdge DGLinkLab]
-> [(Node, [LEdge DGLinkLab])]
getAllLocOrHideGlobDefPathsTo =
getAllGlobDefPathsBeginningWithTypesTo
([isLocalDef, isHidingDef]::[LEdge DGLinkLab -> Bool])
{- 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 = getAllGlobDefPathsBeginningWithTypesTo
([isLocalDef]::[LEdge DGLinkLab -> Bool])
{- (node,path):(locGlobPaths ++
(concat (
[getAllLocGlobDefPathsTo dgraph (getSourceNode edge) path|
(_, path@(edge:edges)) <- globalPaths]))
)
where
inEdges = inn dgraph node
globalEdges = [edge| edge <- filter isGlobalDef inEdges, notElem edge path]
localEdges = [edge| edge <- filter isLocalDef inEdges, notElem edge path]
globalPaths = [(getSourceNode edge, (edge:path))| edge <- globalEdges]
locGlobPaths = [(getSourceNode edge, (edge:path))| edge <- localEdges]
-}
{- returns a list of all paths to the given node
that consist of globalDef edges only
or
that consist of an edge of one of the given types
followed by any number of globalDef edges -}
getAllGlobDefPathsBeginningWithTypesTo :: [LEdge DGLinkLab -> Bool] -> DGraph -> Node -> [LEdge DGLinkLab]
-> [(Node, [LEdge DGLinkLab])]
getAllGlobDefPathsBeginningWithTypesTo types dgraph node path =
(node,path):(typeGlobPaths ++
(concat ( [getAllGlobDefPathsBeginningWithTypesTo
types dgraph (getSourceNode edge) path |
(_, path@(edge:edges)) <- globalPaths])
)
)
where
inEdges = inn dgraph node
globalEdges = [edge| edge <- filter isGlobalDef inEdges, notElem edge path]
edgesOfTypes
= [edge| edge <- filterByTypes types inEdges, notElem edge path]
globalPaths = [(getSourceNode edge, (edge:path))| edge <- globalEdges]
typeGlobPaths = [(getSourceNode edge, (edge:path))| edge <- edgesOfTypes]
{- returns all paths consisting of global edges only
or
of one local edge followed by any number of global edges-}
getAllLocGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllLocGlobPathsBetween dgraph src tgt =
locGlobPaths ++ globPaths
where
outEdges = out dgraph src
locEdges = [(edge,target)|edge@(_,target,_) <-
(filterByTypes [isLocalEdge] outEdges)]
locGlobPaths = (concat [map ([edge]++)
(getAllPathsOfTypesBetween dgraph [isGlobalEdge] node tgt [])|
(edge,node) <- locEdges])
globPaths = getAllPathsOfTypesBetween dgraph [isGlobalEdge] 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 =
[edge| edge <- filterByTypes types inGoingEdges, notElem edge path]
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 ->
resultToMaybe $ compHomInclusion 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
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
isGlobalEdge :: LEdge DGLinkLab -> Bool
isGlobalEdge edge = isGlobalDef edge || isGlobalThm edge
isLocalEdge :: LEdge DGLinkLab -> Bool
isLocalEdge edge = isLocalDef edge || isLocalThm edge
isGlobalThm :: LEdge DGLinkLab -> Bool
isGlobalThm edge = isProvenGlobalThm edge || isUnprovenGlobalThm edge
isLocalThm :: LEdge DGLinkLab -> Bool
isLocalThm edge = isProvenLocalThm edge || isUnprovenLocalThm 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
isHidingDef :: LEdge DGLinkLab -> Bool
isHidingDef (_,_,edgeLab) =
case dgl_type edgeLab of
HidingDef -> True
otherwise -> False
-- ----------------------------------------------------------------------------
-- other methods on edges
-- ----------------------------------------------------------------------------
{- returns true, if an identical edge is already in the graph or marked to be inserted,
false otherwise-}
isDuplicate :: LEdge DGLinkLab -> DGraph -> [DGChange] -> Bool
isDuplicate newEdge dgraph changes =
elem (InsertEdge newEdge) changes || elem newEdge (labEdges dgraph)
{- returns true, if the given edge is duplicate or
if there already exists a parallel path,
which starts with a localThmEdge to one of the startnodes in 'otherNewEdge'
and has the same morphism as the given edge,
false otherwise -}
isRedundant :: LEdge DGLinkLab -> DGraph -> [DGChange]
->[(Node, [LEdge DGLinkLab])] -> Bool
isRedundant newEdge@(src,_,label) dgraph changes otherNewEdges =
isDuplicate newEdge dgraph changes
|| elem (Just (dgl_morphism label)) morphismsOfParallelPaths
where
localThmEdgesToOtherSources =
[outEdge|outEdge@(_,tgt,_) <- out dgraph src,
elem tgt (map fst otherNewEdges)
&& isLocalThm outEdge]
parallelPaths
= concat (map (combineSucceedingEdges otherNewEdges)
localThmEdgesToOtherSources)
morphismsOfParallelPaths = map calculateMorphismOfPath parallelPaths
{- combines the given edge with each of those given paths that start
with the target node of the edge-}
combineSucceedingEdges :: [(Node,[LEdge DGLinkLab])] -> LEdge DGLinkLab
-> [[LEdge DGLinkLab]]
combineSucceedingEdges [] _ = []
combineSucceedingEdges ((src,path):paths) edge@(_,tgt,_) =
if tgt == src
then ((edge:path)):(combineSucceedingEdges paths edge)
else combineSucceedingEdges paths edge
isIdentityEdge :: LEdge DGLinkLab -> LibEnv -> DGraph -> Bool
isIdentityEdge (src,tgt,edgeLab) libEnv dgraph =
if isDGRef nodeLab then
case Map.lookup (dgn_libname nodeLab) libEnv of
Just globContext@(_,_,refDgraph) -> isIdentityEdge (dgn_node nodeLab,tgt,edgeLab) libEnv refDgraph
Nothing -> False
else if src == tgt && (dgl_morphism edgeLab) == (ide Grothendieck (dgn_sign nodeLab)) then True else False
where nodeLab = lab' (context src dgraph)
{- returns the DGLinkLab of the given LEdge -}
getLabelOfEdge :: (LEdge b) -> b
getLabelOfEdge (_,_,label) = label
-- ----------------------------------------------------------------------------
-- 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
-- ---------------------------------------------------------------------------
-- methods for the extension of globDecomp (avoid insertion ofredundant edges)
-- ---------------------------------------------------------------------------
{- returns all paths consisting of local theorem links whose src and tgt nodes
are contained in the given list of nodes -}
localThmPathsBetweenNodes :: DGraph -> [Node] -> [[LEdge DGLinkLab]]
localThmPathsBetweenNodes _ [] = []
localThmPathsBetweenNodes dgraph nodes@(x:xs) =
localThmPathsBetweenNodesAux dgraph nodes nodes
{- auxiliary method for localThmPathsBetweenNodes -}
localThmPathsBetweenNodesAux :: DGraph -> [Node] -> [Node] -> [[LEdge DGLinkLab]]
localThmPathsBetweenNodesAux _ [] _ = []
localThmPathsBetweenNodesAux dgraph (node:srcNodes) tgtNodes =
(concat (map (getAllPathsOfTypeBetween dgraph isUnprovenLocalThm node) tgtNodes))
++ (localThmPathsBetweenNodesAux dgraph srcNodes tgtNodes)
{- combines each of the given paths with matching edges from the given list
(i.e. every edge that has as its source node the tgt node of the path)-}
combinePathsWithEdges :: [[LEdge DGLinkLab]] -> [LEdge DGLinkLab]
-> [[LEdge DGLinkLab]]
combinePathsWithEdges paths edges =
concat (map (combinePathsWithEdge paths) edges)
{- combines the given path with each matching edge from the given list
(i.e. every edge that has as its source node the tgt node of the path)-}
combinePathsWithEdge :: [[LEdge DGLinkLab]] -> LEdge DGLinkLab
-> [[LEdge DGLinkLab]]
combinePathsWithEdge [] _ = []
combinePathsWithEdge (path:paths) edge@(src,_,_) =
case path of
[] -> combinePathsWithEdge paths edge
(x:xs) -> if (getTargetNode (last path)) == src
then (path++[edge]):(combinePathsWithEdge paths edge)
else combinePathsWithEdge paths edge
{- todo: choose a better name for this method...
returns for each of the given paths a pair consisting of the last edge
contained in the path and - as a triple - the src, tgt and morphism of the
complete path
if there is an empty path in the given list or the morphsim cannot be
calculated, it is simply ignored -}
calculateResultingEdges :: [[LEdge DGLinkLab]] -> [(LEdge DGLinkLab,(Node,Node,GMorphism))]
calculateResultingEdges [] = []
calculateResultingEdges (path:paths) =
case path of
[] -> calculateResultingEdges paths
(x:xs) ->
case calculateMorphismOfPath path of
Nothing -> calculateResultingEdges paths
Just morphism -> (last path, (src,tgt,morphism)):(calculateResultingEdges paths)
where src = getSourceNode (head path)
tgt = getTargetNode (last path)
{- removes from the given list every edge for which there is already an
equivalent edge or path (i.e. an edge or path with the same src, tgt and
morphsim) -}
removeSuperfluousEdges :: DGraph -> [LEdge DGLinkLab]
-> (DGraph,[LEdge DGLinkLab])
removeSuperfluousEdges dgraph [] = (dgraph,[])
removeSuperfluousEdges dgraph edges
= removeSuperfluousEdgesAux dgraph edges
(calculateResultingEdges combinedPaths) []
where
localThmPaths
= localThmPathsBetweenNodes dgraph (map (getSourceNode) edges)
combinedPaths = combinePathsWithEdges localThmPaths edges
{- auxiliary method for removeSuperfluousEdges -}
removeSuperfluousEdgesAux :: DGraph -> [LEdge DGLinkLab]
-> [(LEdge DGLinkLab,(Node,Node,GMorphism))]
-> [LEdge DGLinkLab] -> (DGraph,[LEdge DGLinkLab])
removeSuperfluousEdgesAux dgraph [] _ edgesToInsert= (dgraph,edgesToInsert)
removeSuperfluousEdgesAux dgraph ((src,tgt,lab):edges)
resultingEdges edgesToInsert =
if not (null equivalentEdges)
then removeSuperfluousEdgesAux
newDGraph edges newResultingEdges edgesToInsert
else removeSuperfluousEdgesAux
dgraph edges resultingEdges ((src,tgt,lab):edgesToInsert)
where
equivalentEdges
= [e | e <- resultingEdges,(snd e) == (src,tgt,dgl_morphism lab)]
newResultingEdges = [e | e <- resultingEdges,(fst e) /= (src,tgt,lab)]
newDGraph = delLEdge (src,tgt,lab) dgraph
{- returns true, if the given change is an insertion of an local theorem edge,
false otherwise -}
isLocalThmInsertion :: DGChange -> Bool
isLocalThmInsertion change
= case change of
InsertEdge edge -> isLocalThm edge
otherwise -> False
-- --------------------------------------------------------
-- further methods
-- -------------------------------------------------------
-- | Calculate the morphism of a path with given start node
calculateMorphismOfPathWithStart :: DGraph -> LibEnv
-> (Node,[LEdge DGLinkLab])
-> Maybe GMorphism
calculateMorphismOfPathWithStart dg libEnv (n,[]) = do
ctx <- fst $ match n dg
case getDGNode libEnv dg (fst (labNode' ctx)) of
Just dgNode_ctx -> return $ ide Grothendieck (dgn_sign (snd (dgNode_ctx))) -- ??? to simplistic
Nothing -> Nothing
calculateMorphismOfPathWithStart _ _ (_,p) = calculateMorphismOfPath p
-- | Compute the theory of a node (CASL Reference Manual, p. 294, Def. 4.9)
computeTheory :: LibEnv -> DGraph -> Node -> Result G_theory
computeTheory libEnv dg n = do
let paths = reverse $ getAllLocGlobDefPathsTo dg n []
-- reverse needed to have a "bottom up" ordering
mors <- maybeToMonad "Could not calculate morphism of path"
$ mapM (calculateMorphismOfPathWithStart dg libEnv) paths
ths <- maybeToMonad "Could not calculate sentence list of node"
$ mapM (computeLocalTheory libEnv dg . fst) paths
ths' <- mapM (uncurry translateG_theory) $ zip mors ths
th'' <- maybeToMonad "Logic mismatch for theories" $ flatG_theories ths'
return (nubG_theory th'')
-- ---------------
-- basic inference
-- ---------------
getGoals :: LibEnv -> DGraph -> LEdge DGLinkLab -> Result G_l_sentence_list
getGoals libEnv dg (n,_,edge) = do
th <- maybeToMonad ("Could node find node "++show n)
$ computeLocalTheory libEnv dg n
let mor = dgl_morphism edge
fmap sensOf $ translateG_theory mor th
getProvers :: Bool -> LogicGraph -> G_sublogics -> [(G_prover,AnyComorphism)]
getProvers consCheck lg gsub =
if consCheck then
[(G_cons_checker (targetLogic cid) p,Comorphism cid) |
Comorphism cid <- cms,
p <- cons_checkers (targetLogic cid)]
else
[(G_prover (targetLogic cid) p,Comorphism cid) |
Comorphism cid <- cms,
p <- provers (targetLogic cid)]
where cms = findComorphismPaths lg gsub
selectProver :: [(G_prover,AnyComorphism)] -> IOResult (G_prover,AnyComorphism)
selectProver [p] = return p
selectProver [] = resToIORes $ fatal_error "No pover available" nullPos
#ifdef UNI_PACKAGE
selectProver provers = do
sel <- ioToIORes $ listBox
"Choose a translation to a prover-supported logic"
(map (show.snd) provers)
i <- case sel of
Just j -> return j
_ -> resToIORes $ fatal_error "Proofs.Proofs: selection" nullPos
return (provers!!i)
#endif
-- applies basic inference to a given node
basicInferenceNode :: Bool -> LogicGraph -> (LIB_NAME,Node) -> ProofStatus
-> IO (Result ProofStatus)
basicInferenceNode checkCons lg (ln,node)
proofStatus@(globalContext,libEnv,history,dGraph) =
ioresToIO (do
-- compute the theory of the node, and its name
G_theory lid1 sign axs <-
resToIORes $ computeTheory libEnv dGraph node
ctx <- resToIORes
$ maybeToMonad ("Could node find node "++show node)
$ fst $ match node dGraph
let nlab = lab' ctx
nodeName = case nlab of
DGNode _ _ _ _-> dgn_name nlab
DGRef _ _ _ -> dgn_renamed nlab
thName = showPretty (getLIB_ID ln) "_"
++ maybe (show node) (flip showPretty "") nodeName
-- compute the list of proof goals
let inEdges = inn dGraph node
localEdges = filter isUnprovenLocalThm inEdges
goalslist <- if checkCons then return []
else resToIORes $ mapM (getGoals libEnv dGraph) localEdges
G_l_sentence_list lid3 goals <-
if null goalslist then return $ G_l_sentence_list lid1 []
else resToIORes (maybeToMonad
"Logic mismatch for proof goals"
(flatG_l_sentence_list goalslist))
goals1 <- coerce lid1 lid3 goals
-- select a suitable translation and prover
let provers = getProvers checkCons lg $ sublogicOfTh $
(G_theory lid1 sign (axs++goals1))
(prover,Comorphism cid) <- selectProver provers
-- Borrowing: translate theory
let lidS = sourceLogic cid
lidT = targetLogic cid
sign' <- coerce lidS lid1 sign
axs' <- coerce lidS lid1 axs
(sign'',sens'') <- resToIORes $ map_theory cid (sign',axs')
case prover of
G_prover lid4 p -> do
-- Borrowing: translate goal
goals' <- coerce lidS lid3 goals
goals'' <- resToIORes $ mapM (mapNamedM $ map_sentence cid sign') goals'
-- call the prover
p' <- coerce lidT lid4 p
ps <- ioToIORes $ prove p' thName (sign'',sens'') goals''
-- update the development graph
let (nextDGraph, nextHistoryElem) = proveLocalEdges dGraph localEdges
return (globalContext, libEnv, nextHistoryElem:history, nextDGraph)
G_cons_checker lid4 p -> do
incl <- resToIORes $ inclusion lidT (empty_signature lidT) sign''
let mor = TheoryMorphism { t_source = empty_theory lidT,
t_target = (sign'',sens''),
t_morphism = incl }
p' <- coerce lidT lid4 p
ps <- ioToIORes $ cons_check p' thName mor
let nextHistoryElem = ([LocalInference],[])
-- ??? to be implemented
return (globalContext, libEnv, nextHistoryElem:history, dGraph)
)
proveLocalEdges :: DGraph -> [LEdge DGLinkLab] -> (DGraph,([DGRule],[DGChange]))
proveLocalEdges dGraph edges = (nextDGraph,([LocalInference],changes))
where (nextDGraph,(_,changes)) = proveLocalEdgesAux ([],[]) dGraph edges
proveLocalEdgesAux :: ([DGRule],[DGChange]) -> DGraph -> [LEdge DGLinkLab]
-> (DGraph,([DGRule],[DGChange]))
proveLocalEdgesAux historyElem dGraph [] = (dGraph, historyElem)
proveLocalEdgesAux (rules,changes) dGraph ((edge@(src, tgt, edgelab)):edges) =
if True then proveLocalEdgesAux (rules,(DeleteEdge edge):((InsertEdge provenEdge):changes)) (insEdge provenEdge(delLEdge edge dGraph)) edges
else proveLocalEdgesAux (rules,changes) dGraph edges
where
morphism = dgl_morphism edgelab
(LocalThm _ conservativity conservStatus) = (dgl_type edgelab)
proofBasis = [] -- to be implemented
provenEdge = (src,
tgt,
DGLink {dgl_morphism = morphism,
dgl_type =
(LocalThm (Proven proofBasis)
conservativity conservStatus),
dgl_origin = DGProof}
)