Automatic.hs revision c208973c890b8f993297720fd0247bc7481d4304
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederDescription : automatic proofs in the development graph calculus
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Jorina F. Gerken, Mossakowski, Luettich, Uni Bremen 2002-2006
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : Christian.Maeder@dfki.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.
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maedermodule Proofs.Automatic (automatic, automaticFromList) where
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport qualified Common.Lib.SizedList as SizedList
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport qualified Data.Map as Map
3dde4051c307b609159a097f08a05108fdd036efJonathan von SchroederautomaticFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
3dde4051c307b609159a097f08a05108fdd036efJonathan von SchroederautomaticFromList ln ls libEnv =
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder let x = automaticRecursiveFromList ln libEnv ls
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder y = localInferenceFromList ln ls x
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaedernoChange :: LibEnv -> LibEnv -> Bool
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaedernoChange oldLib newLib = and $ Map.elems $ Map.intersectionWith
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder (\ a b -> SizedList.null . snd $ splitHistory a b) oldLib newLib
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederautomaticRecursiveFromList :: LibName -> LibEnv -> [LEdge DGLinkLab]
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian MaederautomaticRecursiveFromList ln proofstatus ls =
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder let auxProofstatus = automaticApplyRulesToGoals ln ls proofstatus
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maeder rulesWithGoals
734257b9ea9fcaa18d4e3627f54f5295a99aa1f7Felix Gabriel Mance in if noChange proofstatus auxProofstatus then auxProofstatus
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder else automaticRecursiveFromList ln auxProofstatus ls
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder{- | automatically applies all rules to the library
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder denoted by the library name of the given proofstatus-}
014dc30f64ec25e4790cca987d4d1e6635430510Christian Maederautomatic :: LibName -> LibEnv -> LibEnv
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettichautomatic ln le = let nLib = localInference ln $ automaticRecursive 49 ln le in
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder groupHistory odg (DGRule "automatic") ndg) le nLib
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder{- | applies the rules recursively until no further changes can be made -}
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaederautomaticRecursive :: Int -> LibName -> LibEnv -> LibEnv
f5c0884429b01e74c6e658ded921fb2e16dfb478Christian MaederautomaticRecursive count ln proofstatus =
db675e8302ddb0d6528088ce68f5e98a00e890e3Christian Maeder let auxProofstatus = automaticApplyRules ln proofstatus
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder in if noChange proofstatus auxProofstatus || count < 1 then auxProofstatus
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder else automaticRecursive (count - 1) ln auxProofstatus
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian MaederwrapTheoremHideShift :: LibName -> LibEnv -> LibEnv
23ffcc44ca8612feccbd8fda63fa5be7ab5f9dc3Christian MaederwrapTheoremHideShift ln libEnv =
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder case maybeResult $ theoremHideShift ln libEnv of
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder Nothing -> libEnv
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just libEnv' -> libEnv'
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | list of rules to use
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederrules :: [LibName -> LibEnv -> LibEnv]
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder [ automaticHideTheoremShift
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , wrapTheoremHideShift
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederrulesWithGoals :: [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv]
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederrulesWithGoals =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder [automaticHideTheoremShiftFromList
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , locDecompFromList
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , globDecompFromList
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , globSubsumeFromList
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederautomaticApplyRulesToGoals :: LibName -> [LEdge DGLinkLab] -> LibEnv ->
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich ([LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv])
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederautomaticApplyRulesToGoals ln ls libEnv ll=
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder f:l-> let nwLibEnv= f ln ls libEnv
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder dgraph = lookupDGraph ln nwLibEnv
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder updateList = filter
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder (\(_,_,lp) ->
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder case thmLinkStatus
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder $ dgl_type lp of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just LeftOpen -> True
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder $ labEdgesDG dgraph
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder in automaticApplyRulesToGoals ln updateList nwLibEnv l
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder{- | sequentially applies all rules to the given proofstatus,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ie to the library denoted by the library name of the proofstatus -}
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederautomaticApplyRules :: LibName -> LibEnv -> LibEnv
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederautomaticApplyRules ln = foldl (.) id $ map (\ f -> f ln) rules