Automatic.hs revision 980c2505814d75dc689de1412f4de30b4d96314f
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian MaederModule : $Header$
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian MaederCopyright : (c) Jorina F. Gerken, Mossakowski, L�ttich, Uni Bremen 2002-2006
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiMaintainer : jfgerken@tzi.de
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederStability : provisional
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederPortability : non-portable(Logic)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiautomatic proofs in development graphs.
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder Follows Sect. IV:4.4 of the CASL Reference Manual.
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder T. Mossakowski, S. Autexier and D. Hutter:
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Extending Development Graphs With Hiding.
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Lecture Notes in Computer Science 2029, p. 269-283,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Springer-Verlag 2001.
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskitodo in general:
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiOrder of rule application: try to use local links induced by %implies
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskifor subsumption proofs (such that the %implied formulas need not be
ad270004874ce1d0697fb30d7309f180553bb315Christian MaederIntegrate stuff from Saarbr�cken
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederAdd proof status information
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder what should be in proof status:
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder- proofs of thm links according to rules
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski- cons, def and mono annos, and their proofs
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedermodule Proofs.Automatic (automatic, automaticFromList) where
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport qualified Common.Lib.Map as Map
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport Data.Maybe (fromJust)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski{- todo: implement apply for GlobDecomp and Subsumption
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski the list of DGChage must be constructed in parallel to the
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski new DGraph -}
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiapplyRule :: DGRule -> DGraph -> Maybe ([DGChange],DGraph)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiapplyRule = error "Proofs.hs:applyRule"
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiautomaticFromList :: LIB_NAME -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederautomaticFromList ln ls libEnv=
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let x = automaticRecursiveFromList ln 0 libEnv ls
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder y = localInferenceFromList ln ls x
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder z = mergeHistories 0 2 y
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski in fromJust z
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder{- | automatically applies all rules to the library
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski denoted by the library name of the given proofstatus-}
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederautomatic :: LIB_NAME -> LibEnv -> LibEnv
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiautomatic ln = fromJust . mergeHistories 0 2 .
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski localInference ln . automaticRecursive ln 0
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiautomaticRecursiveFromList :: LIB_NAME -> Int -> LibEnv -> [LEdge DGLinkLab] -> LibEnv
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederautomaticRecursiveFromList ln cnt proofstatus ls =
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski let auxProofstatus = automaticApplyRulesToGoals ln ls proofstatus
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski finalProofstatus = mergeHistories cnt noRulesWithGoals auxProofstatus
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder in case finalProofstatus of
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder Nothing -> proofstatus
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Just p -> automaticRecursiveFromList ln 1 p ls
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski{- | applies the rules recursively until no further changes can be made -}
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiautomaticRecursive :: LIB_NAME -> Int -> LibEnv -> LibEnv
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiautomaticRecursive ln cnt proofstatus =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let auxProofstatus = automaticApplyRules ln proofstatus
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski finalProofstatus = mergeHistories cnt noRules auxProofstatus
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder in case finalProofstatus of
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder Nothing -> proofstatus
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Just p -> automaticRecursive ln 1 p
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- | list of rules to use
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskirules :: [LIB_NAME -> LibEnv -> LibEnv]
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder [automaticHideTheoremShift
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski , globSubsume
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- , theoremHideShift
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | number of rules
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskinoRules :: Int
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskinoRules = length rules
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskirulesWithGoals :: [LIB_NAME -> [LEdge DGLinkLab] -> LibEnv -> LibEnv]
a98fd29a06e80e447af26d898044c23497adbc73Mihai CodescurulesWithGoals =
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu [automaticHideTheoremShiftFromList
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu , locDecompFromList
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski , globDecompFromList
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski , globSubsumeFromList
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskinoRulesWithGoals :: Int
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskinoRulesWithGoals = length rulesWithGoals
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederautomaticApplyRulesToGoals :: LIB_NAME -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiautomaticApplyRulesToGoals ln ls = foldl (.) id $ map (\f -> f ln ls) rulesWithGoals
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- | sequentially applies all rules to the given proofstatus,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski ie to the library denoted by the library name of the proofstatus -}
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederautomaticApplyRules :: LIB_NAME -> LibEnv -> LibEnv
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiautomaticApplyRules ln = foldl (.) id $ map (\ f -> f ln) rules
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- | merges for every library the new history elements
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski to one new history element -}
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedermergeHistories :: Int -> Int -> LibEnv -> Maybe LibEnv
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskimergeHistories cnt lenNewHistory libEnv =
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski let (numChanges,newProofstatus) = mergeHistoriesAux cnt lenNewHistory
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski (Map.keys libEnv) libEnv
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski in if numChanges > 0 then
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Just newProofstatus
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- | auxiliary method for mergeHistories:
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder determined the library names and recursively applies mergeHistory -}
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedermergeHistoriesAux :: Int -> Int -> [LIB_NAME] -> LibEnv -> (Int, LibEnv)
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedermergeHistoriesAux _ _ [] proofstatus = (0, proofstatus)
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedermergeHistoriesAux cnt lenNewHistory (ln:list) proofstatus =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let ps = mergeHistory cnt lenNewHistory ln proofstatus
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder in case ps of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Just newProofstatus -> let
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (i,finalProofstatus) = mergeHistoriesAux cnt lenNewHistory list
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder newProofstatus
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder in (i+1,finalProofstatus)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Nothing -> mergeHistoriesAux cnt lenNewHistory list proofstatus
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder{- | merges the new history elements of a single library
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder to one new history elemebt-}
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedermergeHistory :: Int -> Int -> LIB_NAME -> LibEnv -> Maybe LibEnv
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedermergeHistory cnt lenNewHistory ln proofstatus =
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu let history = lookupHistory ln proofstatus
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (newHistoryPart, oldHistory) = splitAt (lenNewHistory+cnt) history
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder in if null (concatMap snd $ take lenNewHistory newHistoryPart)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder && cnt == 1 then
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let (dgrules, changes) = concatHistoryElems (reverse newHistoryPart)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder newHistoryElem = (dgrules, removeContraryChanges changes)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder newHistory = newHistoryElem:oldHistory
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder in Just $ Map.update (\ c -> Just c { proofHistory = newHistory })
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ln proofstatus
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- | concats the given history elements to one history element-}
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederconcatHistoryElems :: [([DGRule],[DGChange])] -> ([DGRule],[DGChange])
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederconcatHistoryElems [] = ([], [])
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederconcatHistoryElems ((dgrules, changes) : elems) =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (dgrules ++ fst (concatHistoryElems elems),
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder changes ++ snd (concatHistoryElems elems))