Local.hs revision 446dc91e74430884802bd5cb367e369f6d9902c7
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederModule : $Header$
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederCopyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2004
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederMaintainer : jfgerken@tzi.de
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiStability : provisional
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederPortability : non-portable(Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederlocal proofs in development graphs.
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder Follows Sect. IV:4.4 of the CASL Reference Manual.
93fa7e4374de6e37328e752991a698bf03032c75Christian MaederOrder of rule application: try to use local links induced by %implies
93fa7e4374de6e37328e752991a698bf03032c75Christian Maederfor subsumption proofs (such that the %implied formulas need not be
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maedermodule Proofs.Local (localInference, locDecomp) where
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport qualified Common.Lib.Map as Map
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maederimport qualified Common.OrderedMap as OMap
62198789c7cb57cac13399055515921c0fe3483fChristian Maeder-- --------------------
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder-- local decomposition
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder-- --------------------
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder{- a merge of the rules local subsumption, local decomposition I and
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder local decomposition II -}
62198789c7cb57cac13399055515921c0fe3483fChristian Maeder-- applies this merge of rules to all unproven localThm edges if possible
a255351561838b3743d03c1629d335cfb8b83804Christian MaederlocDecomp :: ProofStatus -> ProofStatus
9963c741a47c42d2dedc6e4589c1b197129a6239Christian MaederlocDecomp proofStatus@(ln,libEnv,_) =
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder let dgraph = lookupDGraph ln proofStatus
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian Maeder localThmEdges = filter isUnprovenLocalThm (labEdges dgraph)
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian Maeder (nextDGraph, nextHistoryElem) =
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder locDecompAux libEnv ln dgraph ([],[]) localThmEdges
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian Maeder in mkResultProofStatus proofStatus nextDGraph nextHistoryElem
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder{- auxiliary function for locDecomp (above)
b502963581a463467939d578b211cb7a173c5428Christian Maeder actual implementation -}
906f0b21e2dc78ee4f37f879518be018a0204cd9Christian MaederlocDecompAux :: LibEnv -> LIB_NAME -> DGraph -> ([DGRule],[DGChange])
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder -> [LEdge DGLinkLab] -> (DGraph,([DGRule],[DGChange]))
a255351561838b3743d03c1629d335cfb8b83804Christian MaederlocDecompAux _ _ dgraph historyElement [] = (dgraph, historyElement)
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaederlocDecompAux libEnv ln dgraph (rules,changes)
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder (ledge@(src, tgt, edgeLab) : list) =
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder if (null proofBasis && not (isIdentityEdge ledge libEnv dgraph))
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder locDecompAux libEnv ln dgraph (rules, changes) list
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder if isDuplicate newEdge dgraph changes
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder then locDecompAux libEnv ln auxGraph
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder (newRules, DeleteEdge ledge : changes) list
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder else locDecompAux libEnv ln newGraph (newRules,newChanges) list
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder morphism = dgl_morphism edgeLab
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder allPaths = getAllLocGlobPathsBetween dgraph src tgt
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder th = computeLocalTheory libEnv (ln, src)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder pathsWithoutEdgeItself = [ path | path <- allPaths, notElem ledge path ]
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder filteredPaths = filterByTranslation th morphism pathsWithoutEdgeItself
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski proofBasis = selectProofBasis ledge filteredPaths
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder auxGraph = delLEdge ledge dgraph
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder (LocalThm _ conservativity conservStatus) = (dgl_type edgeLab)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder newEdge = (src,
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder DGLink {dgl_morphism = morphism,
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (LocalThm (Proven (LocDecomp ledge) proofBasis)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder conservativity conservStatus),
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski dgl_origin = DGProof}
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder newGraph = insEdge newEdge auxGraph
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder newRules = LocDecomp ledge : rules
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski newChanges = DeleteEdge ledge : InsertEdge newEdge : changes
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski{- | removes all paths from the given list of paths whose morphism does
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maedernot translate the given sentence list to the same resulting sentence
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskilist as the given morphism. -}
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaederfilterByTranslation :: Maybe G_theory -> GMorphism -> [[LEdge DGLinkLab]]
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder -> [[LEdge DGLinkLab]]
9963c741a47c42d2dedc6e4589c1b197129a6239Christian MaederfilterByTranslation maybeTh morphism paths =
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski case maybeTh of
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder Just th -> [path| path <- paths, isSameTranslation th morphism path]
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder Nothing -> []
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder-- isSameTranslation th morphism (calculateMorphismOfPath path)]
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder{- | checks if the given morphism and the morphism of the given path
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskitranslate the given sentence list to the same resulting sentence list. -}
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiisSameTranslation :: G_theory -> GMorphism -> [LEdge DGLinkLab] -> Bool
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiisSameTranslation th morphism path =
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder case calculateMorphismOfPath path of
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder Just morphismOfPath ->
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski translateG_theory morphism th == translateG_theory morphismOfPath th
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Nothing -> False
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder-- ----------------------------------------------
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder-- local subsumption
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- ----------------------------------------------
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder-- applies local subsumption to all unproven local theorem edges
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaederlocalInference :: ProofStatus -> ProofStatus
9963c741a47c42d2dedc6e4589c1b197129a6239Christian MaederlocalInference proofStatus@(ln,libEnv,_) =
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder let dgraph = lookupDGraph ln proofStatus
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder localThmEdges = filter isUnprovenLocalThm (labEdges dgraph)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder (nextDGraph, nextHistoryElem) =
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder localInferenceAux libEnv ln dgraph ([],[]) localThmEdges
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder in mkResultProofStatus proofStatus nextDGraph nextHistoryElem
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder-- auxiliary method for localInference
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian MaederlocalInferenceAux :: LibEnv -> LIB_NAME -> DGraph -> ([DGRule],[DGChange])
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder -> [LEdge DGLinkLab] -> (DGraph,([DGRule],[DGChange]))
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian MaederlocalInferenceAux _ _ dgraph historyElement [] = (dgraph, historyElement)
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian MaederlocalInferenceAux libEnv ln dgraph (rules, changes)
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder (ledge@(src,tgt,edgeLab) : list) =
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder case maybeThSrc of
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Just thSrc ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder case (maybeResult (computeTheory libEnv (ln, tgt)),
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder maybeResult (translateG_theory morphism thSrc)) of
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder (Just (G_theory lidTgt _ sensTgt), Just (G_theory lidSrc _ sensSrc)) ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder case maybeResult (coerceThSens lidTgt lidSrc "" sensTgt) of
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder Nothing -> localInferenceAux libEnv ln dgraph (rules,changes) list
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder Just sentencesTgt ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder -- check if all source axioms are also axioms in the target
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let goals = OMap.filter isAxiom sensSrc
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder `diffSens` sentencesTgt
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder goals' = markAsGoal goals
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder newTh = case (dgn_theory oldContents) of
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder G_theory lid sig sens ->
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder case coerceThSens lidSrc lid "" goals' of
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Nothing -> G_theory lid sig sens
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Just goals'' ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder G_theory lid sig (sens `joinSens` goals'')
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let newEdge = (src, tgt, newLab)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder newGraph = insEdge newEdge auxGraph
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder newChanges = changes ++
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder [DeleteEdge ledge, InsertEdge newEdge]
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder in localInferenceAux libEnv ln newGraph
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (newRules,newChanges) list
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let n = getNewNode auxGraph
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder newNode = (n, oldContents{dgn_theory = newTh})
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder newList = map (replaceNode tgt n) list
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder (newGraph,changes') = adoptEdges
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (insNode newNode $ auxGraph) tgt n
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder newEdge = (if src==tgt then n else src, n, newLab)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder newGraph' = insEdge newEdge $ delNode tgt $ newGraph
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder newLibEnv = Map.adjust adjMap ln libEnv
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder adjMap (annos, env, _dg) = (annos,env,newGraph')
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder newChanges = changes ++ DeleteEdge ledge :
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder InsertNode newNode : changes' ++
95936ba3a6577d40aae065aafac4147f5a308782Christian Maeder [DeleteNode oldNode,InsertEdge newEdge]
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder in localInferenceAux newLibEnv ln newGraph'
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (newRules,newChanges) newList
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder _ -> localInferenceAux libEnv ln dgraph (rules,changes) list
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder _ -> localInferenceAux libEnv ln dgraph (rules,changes) list
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder morphism = dgl_morphism edgeLab
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder maybeThSrc = computeLocalTheory libEnv (ln, src)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder auxGraph = delLEdge ledge dgraph
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder (LocalThm _ conservativity conservStatus) = (dgl_type edgeLab)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder newLab = DGLink {dgl_morphism = morphism,
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder (LocalThm (Proven (LocInference ledge) [])
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder conservativity conservStatus),
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder dgl_origin = DGProof}
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder newRules = (LocInference ledge):rules
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder oldNode = labNode' (safeContext "localInferenceAux" dgraph tgt)
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder (_,oldContents) = oldNode
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder replaceNode from to (src',tgt',labl) =
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder (replaceNodeAux from to src', replaceNodeAux from to tgt',labl)
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder replaceNodeAux from to n = if n==from then to else n