25f72e2845c89a153ca9d3279d7feccbc912524ematthewDescription : automatic proofs in the development graph calculus
25f72e2845c89a153ca9d3279d7feccbc912524ematthewCopyright : (c) Jorina F. Gerken, Mossakowski, Luettich, Uni Bremen 2002-2006
25f72e2845c89a153ca9d3279d7feccbc912524ematthewLicense : GPLv2 or higher, see LICENSE.txt
25f72e2845c89a153ca9d3279d7feccbc912524ematthewMaintainer : Christian.Maeder@dfki.de
25f72e2845c89a153ca9d3279d7feccbc912524ematthewStability : provisional
25f72e2845c89a153ca9d3279d7feccbc912524ematthewPortability : non-portable(Logic)
25f72e2845c89a153ca9d3279d7feccbc912524ematthewautomatic proofs in development graphs.
25f72e2845c89a153ca9d3279d7feccbc912524ematthew Follows Sect. IV:4.4 of the CASL Reference Manual.
25f72e2845c89a153ca9d3279d7feccbc912524ematthew References:
25f72e2845c89a153ca9d3279d7feccbc912524ematthew T. Mossakowski, S. Autexier and D. Hutter:
25f72e2845c89a153ca9d3279d7feccbc912524ematthew Extending Development Graphs With Hiding.
25f72e2845c89a153ca9d3279d7feccbc912524ematthew H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
25f72e2845c89a153ca9d3279d7feccbc912524ematthew Lecture Notes in Computer Science 2029, p. 269-283,
25f72e2845c89a153ca9d3279d7feccbc912524ematthew Springer-Verlag 2001.
25f72e2845c89a153ca9d3279d7feccbc912524ematthewmodule Proofs.Automatic (automatic, automaticFromList) where
25f72e2845c89a153ca9d3279d7feccbc912524ematthewimport qualified Common.Lib.SizedList as SizedList
b01d258c572743c78c89899e0a49199bac91a7dfmatthewimport qualified Data.Map as Map
25f72e2845c89a153ca9d3279d7feccbc912524ematthewimport Data.Maybe (fromMaybe)
25f72e2845c89a153ca9d3279d7feccbc912524ematthewautomaticFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
25f72e2845c89a153ca9d3279d7feccbc912524ematthewautomaticFromList ln ls libEnv =
25f72e2845c89a153ca9d3279d7feccbc912524ematthew let x = automaticRecursiveFromList ln libEnv ls
25f72e2845c89a153ca9d3279d7feccbc912524ematthew y = localInferenceFromList ln ls x
25f72e2845c89a153ca9d3279d7feccbc912524ematthewnoChange :: LibEnv -> LibEnv -> Bool
25f72e2845c89a153ca9d3279d7feccbc912524ematthewnoChange oldLib newLib = and $ Map.elems $ Map.intersectionWith
25f72e2845c89a153ca9d3279d7feccbc912524ematthew (\ a b -> SizedList.null . snd $ splitHistory a b) oldLib newLib
25f72e2845c89a153ca9d3279d7feccbc912524ematthewautomaticRecursiveFromList :: LibName -> LibEnv -> [LEdge DGLinkLab]
25f72e2845c89a153ca9d3279d7feccbc912524ematthewautomaticRecursiveFromList ln proofstatus ls =
25f72e2845c89a153ca9d3279d7feccbc912524ematthew let auxProofstatus = automaticApplyRulesToGoals ln ls proofstatus
25f72e2845c89a153ca9d3279d7feccbc912524ematthew rulesWithGoals
25f72e2845c89a153ca9d3279d7feccbc912524ematthew in if noChange proofstatus auxProofstatus then auxProofstatus
25f72e2845c89a153ca9d3279d7feccbc912524ematthew else automaticRecursiveFromList ln auxProofstatus ls
25f72e2845c89a153ca9d3279d7feccbc912524ematthew{- | automatically applies all rules to the library
25f72e2845c89a153ca9d3279d7feccbc912524ematthew denoted by the library name of the given proofstatus -}
25f72e2845c89a153ca9d3279d7feccbc912524ematthewautomatic :: LibName -> LibEnv -> LibEnv
25f72e2845c89a153ca9d3279d7feccbc912524ematthewautomatic ln le = let nLib = localInference ln $ automaticRecursive 49 ln le in
25f72e2845c89a153ca9d3279d7feccbc912524ematthew groupHistory odg (DGRule "automatic") ndg) le nLib
25f72e2845c89a153ca9d3279d7feccbc912524ematthew-- | applies the rules recursively until no further changes can be made
a5b9f8fb834b1b2208e59a2fa76714bd91a5f147violetteautomaticRecursive :: Int -> LibName -> LibEnv -> LibEnv
8890d0c686adc8442c156956735470bf289ba2d8markautomaticRecursive count ln proofstatus =
8890d0c686adc8442c156956735470bf289ba2d8mark let auxProofstatus = automaticApplyRules ln proofstatus
8890d0c686adc8442c156956735470bf289ba2d8mark in if noChange proofstatus auxProofstatus || count < 1 then auxProofstatus
8890d0c686adc8442c156956735470bf289ba2d8mark else automaticRecursive (count - 1) ln auxProofstatus
8890d0c686adc8442c156956735470bf289ba2d8markwrapTheoremHideShift :: LibName -> LibEnv -> LibEnv
8890d0c686adc8442c156956735470bf289ba2d8markwrapTheoremHideShift ln libEnv = fromMaybe libEnv
8890d0c686adc8442c156956735470bf289ba2d8mark (maybeResult $ theoremHideShift ln libEnv)
8890d0c686adc8442c156956735470bf289ba2d8mark-- | list of rules to use
8890d0c686adc8442c156956735470bf289ba2d8markrules :: [LibName -> LibEnv -> LibEnv]
8890d0c686adc8442c156956735470bf289ba2d8mark [ automaticHideTheoremShift
8890d0c686adc8442c156956735470bf289ba2d8mark , globDecomp
8890d0c686adc8442c156956735470bf289ba2d8mark , wrapTheoremHideShift
8890d0c686adc8442c156956735470bf289ba2d8markrulesWithGoals :: [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv]
8890d0c686adc8442c156956735470bf289ba2d8markrulesWithGoals =
25f72e2845c89a153ca9d3279d7feccbc912524ematthew [automaticHideTheoremShiftFromList
25f72e2845c89a153ca9d3279d7feccbc912524ematthew , locDecompFromList
28a3ff3fa0d3b5e1c774217425cf609cc6339df7matthew , globDecompFromList
51607ea01068c9047391e4c8b46bc9dbd0edb7fdmark , globSubsumeFromList
88f6ec0f4b21d5a6cb75c06e759d83855c47a20fmarkautomaticApplyRulesToGoals :: LibName -> [LEdge DGLinkLab] -> LibEnv ->
b59eee423e33565718e0b8e0e816fa7cd9c80bc3mark [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv] -> LibEnv
51607ea01068c9047391e4c8b46bc9dbd0edb7fdmarkautomaticApplyRulesToGoals ln ls libEnv ll =
51607ea01068c9047391e4c8b46bc9dbd0edb7fdmark case ll of
88f6ec0f4b21d5a6cb75c06e759d83855c47a20fmark [] -> libEnv
1b97dd0336bf4b2a68c96174fc2da6cacc3bb5fdmark f : l -> let nwLibEnv = f ln ls libEnv
51607ea01068c9047391e4c8b46bc9dbd0edb7fdmark dgraph = lookupDGraph ln nwLibEnv
88f6ec0f4b21d5a6cb75c06e759d83855c47a20fmark updateList = filter
51607ea01068c9047391e4c8b46bc9dbd0edb7fdmark (\ (_, _, lp) ->
cc354d5672bc5cb5bba3bf49b6bf953e2021d7d3mark case thmLinkStatus
cc354d5672bc5cb5bba3bf49b6bf953e2021d7d3mark $ dgl_type lp of
cc354d5672bc5cb5bba3bf49b6bf953e2021d7d3mark Just LeftOpen -> True
cc354d5672bc5cb5bba3bf49b6bf953e2021d7d3mark _ -> False) $ labEdgesDG dgraph
51607ea01068c9047391e4c8b46bc9dbd0edb7fdmark in automaticApplyRulesToGoals ln updateList nwLibEnv l
51607ea01068c9047391e4c8b46bc9dbd0edb7fdmark{- | sequentially applies all rules to the given proofstatus,
cc354d5672bc5cb5bba3bf49b6bf953e2021d7d3mark ie to the library denoted by the library name of the proofstatus -}
cc354d5672bc5cb5bba3bf49b6bf953e2021d7d3markautomaticApplyRules :: LibName -> LibEnv -> LibEnv
51607ea01068c9047391e4c8b46bc9dbd0edb7fdmarkautomaticApplyRules ln = foldl (.) id $ map (\ f -> f ln) rules