{- |
Module : ./Proofs/Automatic.hs
Description : automatic proofs in the development graph calculus
Copyright : (c) Jorina F. Gerken, Mossakowski, Luettich, Uni Bremen 2002-2006
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : non-portable(Logic)
automatic proofs in development graphs.
Follows Sect. IV:4.4 of the CASL Reference Manual.
-}
{-
References:
T. Mossakowski, S. Autexier and D. Hutter:
Extending Development Graphs With Hiding.
H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
Lecture Notes in Computer Science 2029, p. 269-283,
Springer-Verlag 2001.
-}
module Proofs.Automatic (automatic, automaticFromList) where
import Proofs.Global
import Proofs.Local
import Proofs.HideTheoremShift
import Proofs.TheoremHideShift
import Static.DevGraph
import Static.DgUtils
import Static.History
import Common.LibName
import qualified Common.Lib.SizedList as SizedList
import qualified Data.Map as Map
import Data.Maybe (fromMaybe)
import Data.Graph.Inductive.Graph
import Common.Result
automaticFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
automaticFromList ln ls libEnv =
let x = automaticRecursiveFromList ln libEnv ls
y = localInferenceFromList ln ls x
in y
noChange :: LibEnv -> LibEnv -> Bool
noChange oldLib newLib = and $ Map.elems $ Map.intersectionWith
(\ a b -> SizedList.null . snd $ splitHistory a b) oldLib newLib
automaticRecursiveFromList :: LibName -> LibEnv -> [LEdge DGLinkLab]
-> LibEnv
automaticRecursiveFromList ln proofstatus ls =
let auxProofstatus = automaticApplyRulesToGoals ln ls proofstatus
rulesWithGoals
in if noChange proofstatus auxProofstatus then auxProofstatus
else automaticRecursiveFromList ln auxProofstatus ls
{- | automatically applies all rules to the library
denoted by the library name of the given proofstatus -}
automatic :: LibName -> LibEnv -> LibEnv
automatic ln le = let nLib = localInference ln $ automaticRecursive 49 ln le in
Map.intersectionWith (\ odg ndg ->
groupHistory odg (DGRule "automatic") ndg) le nLib
-- | applies the rules recursively until no further changes can be made
automaticRecursive :: Int -> LibName -> LibEnv -> LibEnv
automaticRecursive count ln proofstatus =
let auxProofstatus = automaticApplyRules ln proofstatus
in if noChange proofstatus auxProofstatus || count < 1 then auxProofstatus
else automaticRecursive (count - 1) ln auxProofstatus
wrapTheoremHideShift :: LibName -> LibEnv -> LibEnv
wrapTheoremHideShift ln libEnv = fromMaybe libEnv
(maybeResult $ theoremHideShift ln libEnv)
-- | list of rules to use
rules :: [LibName -> LibEnv -> LibEnv]
rules =
[ automaticHideTheoremShift
, globDecomp
, wrapTheoremHideShift
]
rulesWithGoals :: [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv]
rulesWithGoals =
[automaticHideTheoremShiftFromList
, locDecompFromList
, globDecompFromList
, globSubsumeFromList
]
automaticApplyRulesToGoals :: LibName -> [LEdge DGLinkLab] -> LibEnv ->
[LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv] -> LibEnv
automaticApplyRulesToGoals ln ls libEnv ll =
case ll of
[] -> libEnv
f : l -> let nwLibEnv = f ln ls libEnv
dgraph = lookupDGraph ln nwLibEnv
updateList = filter
(\ (_, _, lp) ->
case thmLinkStatus
$ dgl_type lp of
Just LeftOpen -> True
_ -> False) $ labEdgesDG dgraph
in automaticApplyRulesToGoals ln updateList nwLibEnv l
{- | sequentially applies all rules to the given proofstatus,
ie to the library denoted by the library name of the proofstatus -}
automaticApplyRules :: LibName -> LibEnv -> LibEnv
automaticApplyRules ln = foldl (.) id $ map (\ f -> f ln) rules