Automatic.hs revision ad270004874ce1d0697fb30d7309f180553bb315
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederDescription : automatic proofs in the development graph calculus
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Jorina F. Gerken, Mossakowski, L�ttich, Uni Bremen 2002-2006
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : jfgerken@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : non-portable(Logic)
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maederautomatic proofs in development graphs.
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder Follows Sect. IV:4.4 of the CASL Reference Manual.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder T. Mossakowski, S. Autexier and D. Hutter:
a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maeder Extending Development Graphs With Hiding.
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich Lecture Notes in Computer Science 2029, p. 269-283,
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder Springer-Verlag 2001.
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maedertodo in general:
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian MaederOrder of rule application: try to use local links induced by %implies
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichfor subsumption proofs (such that the %implied formulas need not be
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederIntegrate stuff from Saarbr�cken
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian MaederAdd proof status information
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder what should be in proof status:
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder- proofs of thm links according to rules
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder- cons, def and mono annos, and their proofs
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maedermodule Proofs.Automatic (automatic, automaticFromList) where
05a62e84edac8c64de04f8349dee418598d216b9Christian Maederimport qualified Data.Map as Map
1cd4f6541984962658add5cfaa9f28a93879881bChristian Maederimport Data.Maybe (fromJust)
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder{- todo: implement apply for GlobDecomp and Subsumption
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder the list of DGChage must be constructed in parallel to the
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder new DGraph -}
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederapplyRule :: DGRule -> DGraph -> Maybe ([DGChange],DGraph)
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederapplyRule = error "Proofs.hs:applyRule"
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian MaederautomaticFromList :: LIB_NAME -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian MaederautomaticFromList ln ls libEnv=
b5da047a9a875dec3f968b6c0df96af326f90fa9Alexis Tsogias let x = automaticRecursiveFromList ln 0 libEnv ls
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder y = localInferenceFromList ln ls x
6a2dad705deefd1b7a7e09b84fd2d75f2213be47Christian Maeder z = mergeHistories 0 2 y
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder in fromJust z
014dc30f64ec25e4790cca987d4d1e6635430510Christian Maeder{- | automatically applies all rules to the library
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich denoted by the library name of the given proofstatus-}
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maederautomatic :: LIB_NAME -> LibEnv -> LibEnv
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maederautomatic ln = fromJust . mergeHistories 0 2 .
feca1d35123d8c31aee238c9ce79947b0bf65494Christian Maeder localInference ln . automaticRecursive ln 0
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian MaederautomaticRecursiveFromList :: LIB_NAME -> Int -> LibEnv -> [LEdge DGLinkLab] -> LibEnv
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian MaederautomaticRecursiveFromList ln cnt proofstatus ls =
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder let auxProofstatus = automaticApplyRulesToGoals ln ls proofstatus rulesWithGoals
23ffcc44ca8612feccbd8fda63fa5be7ab5f9dc3Christian Maeder finalProofstatus = mergeHistories cnt noRulesWithGoals auxProofstatus
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder in case finalProofstatus of
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder Nothing -> proofstatus
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just p -> automaticRecursiveFromList ln 1 p ls
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder{- | applies the rules recursively until no further changes can be made -}
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederautomaticRecursive :: LIB_NAME -> Int -> LibEnv -> LibEnv
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederautomaticRecursive ln cnt proofstatus =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let auxProofstatus = automaticApplyRules ln proofstatus
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder finalProofstatus = mergeHistories cnt noRules auxProofstatus
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder in case finalProofstatus of
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Nothing -> proofstatus
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Just p -> automaticRecursive ln 1 p
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- | list of rules to use
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederrules :: [LIB_NAME -> LibEnv -> LibEnv]
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder [automaticHideTheoremShift
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder , globSubsume
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder -- , theoremHideShift
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian Maeder-- | number of rules
b363eb04791e7f735633b9b4088502c2bc50ebfcChristian MaedernoRules :: Int
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian MaedernoRules = length rules
2d130d212db7208777ca896a7ecad619a8944971Christian MaederrulesWithGoals :: [LIB_NAME -> [LEdge DGLinkLab] -> LibEnv -> LibEnv]
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederrulesWithGoals =
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder [automaticHideTheoremShiftFromList
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder , locDecompFromList
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , globDecompFromList
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , globSubsumeFromList
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedernoRulesWithGoals :: Int
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedernoRulesWithGoals = length rulesWithGoals
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian MaederautomaticApplyRulesToGoals :: LIB_NAME -> [LEdge DGLinkLab] -> LibEnv ->
dc679edd4ca027663212afdf00926ae2ce19b555Christian Maeder ([LIB_NAME -> [LEdge DGLinkLab] -> LibEnv -> LibEnv])
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederautomaticApplyRulesToGoals ln ls libEnv ll=
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder f:l-> let nwLibEnv= f ln ls libEnv
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder nwGoalList = createAllGoalsList ln nwLibEnv
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder updateList = extractGoals ls nwGoalList
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder in automaticApplyRulesToGoals ln updateList nwLibEnv l
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder{- | sequentially applies all rules to the given proofstatus,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ie to the library denoted by the library name of the proofstatus -}
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian MaederautomaticApplyRules :: LIB_NAME -> LibEnv -> LibEnv
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaederautomaticApplyRules ln = foldl (.) id $ map (\ f -> f ln) rules
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder{- | merges for every library the new history elements
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder to one new history element -}
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedermergeHistories :: Int -> Int -> LibEnv -> Maybe LibEnv
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedermergeHistories cnt lenNewHistory libEnv =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let (numChanges,newProofstatus) = mergeHistoriesAux cnt lenNewHistory
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (Map.keys libEnv) libEnv
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder in if numChanges > 0 then
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Just newProofstatus
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder{- | auxiliary method for mergeHistories:
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder determined the library names and recursively applies mergeHistory -}
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaedermergeHistoriesAux :: Int -> Int -> [LIB_NAME] -> LibEnv -> (Int, LibEnv)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedermergeHistoriesAux _ _ [] proofstatus = (0, proofstatus)
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian MaedermergeHistoriesAux cnt lenNewHistory (ln:list) proofstatus =
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder let ps = mergeHistory cnt lenNewHistory ln proofstatus
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder in case ps of
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder Just newProofstatus -> let
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian Maeder (i,finalProofstatus) = mergeHistoriesAux cnt lenNewHistory list
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder newProofstatus
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder in (i+1,finalProofstatus)
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maeder Nothing -> mergeHistoriesAux cnt lenNewHistory list proofstatus
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder{- | merges the new history elements of a single library
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder to one new history elemebt-}
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedermergeHistory :: Int -> Int -> LIB_NAME -> LibEnv -> Maybe LibEnv
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaedermergeHistory cnt lenNewHistory ln proofstatus =
8d178ae08a52d61379e6b8074f61646499bc88bbChristian Maeder let history = lookupHistory ln proofstatus
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder (newHistoryPart, oldHistory) = splitAt (lenNewHistory+cnt) history
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder in if null (concatMap snd $ take lenNewHistory newHistoryPart)
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder && cnt == 1 then
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder let (dgrules, changes) = concatHistoryElems (reverse newHistoryPart)
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder newHistoryElem = (dgrules, removeContraryChanges changes)
59138b404f12352d103eeffbeaeb3957b90e75fdChristian Maeder newHistory = newHistoryElem:oldHistory
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder in Just $ Map.update (\ c -> Just c { proofHistory = newHistory })
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder ln proofstatus
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder{- | concats the given history elements to one history element-}
10883d13973c46cac98964b66ace7a52b2d059abChristian MaederconcatHistoryElems :: [([DGRule],[DGChange])] -> ([DGRule],[DGChange])
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian MaederconcatHistoryElems [] = ([], [])
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederconcatHistoryElems ((dgrules, changes) : elems) =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder (dgrules ++ fst (concatHistoryElems elems),
0e5b095a19790411e5352fa7cf57cb0388e70472Christian Maeder changes ++ snd (concatHistoryElems elems))