4751N/ACopyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2004
4751N/AMaintainer : jfgerken@tzi.de
4751N/APortability : non-portable(Logic)
4751N/A local proofs in development graphs.
4751N/A Follows Sect. IV:4.4 of the CASL Reference Manual.
4751N/AOrder of rule application: try to use local links induced by %implies
4751N/Afor subsumption proofs (such that the %implied formulas need not be
4751N/A{- a merge of the rules local subsumption, local decomposition I and
4751N/A-- applies this merge of rules to all unproven localThm edges if possible
4751N/AlocDecomp :: ProofStatus -> IO ProofStatus
4751N/AlocDecomp proofStatus@(ln,libEnv,_) = do
4751N/A let dgraph = lookupDGraph ln proofStatus
4751N/A localThmEdges = filter isUnprovenLocalThm (labEdges dgraph)
4751N/A result = locDecompAux libEnv ln dgraph ([],[]) localThmEdges
4751N/A nextHistoryElem = snd result
4751N/A = mkResultProofStatus proofStatus nextDGraph nextHistoryElem
4751N/A{- auxiliary function for locDecomp (above)
4751N/AlocDecompAux :: LibEnv -> LIB_NAME -> DGraph -> ([DGRule],[DGChange]) -> [LEdge DGLinkLab]
4751N/A -> (DGraph,([DGRule],[DGChange]))
4751N/AlocDecompAux _ _ dgraph historyElement [] = (dgraph, historyElement)
4751N/AlocDecompAux libEnv ln dgraph (rules,changes) ((ledge@(src,tgt,edgeLab)):list) =
4751N/A if (null proofBasis && not (isIdentityEdge ledge libEnv dgraph))
4751N/A locDecompAux libEnv ln dgraph (rules,changes) list
4751N/A if isDuplicate newEdge dgraph changes
4751N/A then locDecompAux libEnv ln auxGraph
4751N/A (newRules,(DeleteEdge ledge):changes) list
4751N/A else locDecompAux libEnv ln newGraph (newRules,newChanges) list
4751N/A morphism = dgl_morphism edgeLab
4751N/A allPaths = getAllLocGlobPathsBetween dgraph src tgt
4751N/A th = computeLocalTheory libEnv dgraph src
4751N/A pathsWithoutEdgeItself = [path|path <- allPaths, notElem ledge path]
4751N/A filteredPaths = filterByTranslation th morphism pathsWithoutEdgeItself
4751N/A proofBasis = selectProofBasis edgeLab filteredPaths
4751N/A auxGraph = delLEdge ledge dgraph
4751N/A (LocalThm _ conservativity conservStatus) = (dgl_type edgeLab)
4751N/A DGLink {dgl_morphism = morphism,
4751N/A (LocalThm (Proven (LocDecomp ledge) proofBasis)
4751N/A conservativity conservStatus),
4751N/A newGraph = insEdge newEdge auxGraph
4751N/A newRules = (LocDecomp ledge):rules
4751N/A newChanges = (DeleteEdge ledge):((InsertEdge newEdge):changes)
4751N/A{- removes all paths from the given list of paths whose morphism does not translate the given sentence list to the same resulting sentence list as the given morphism-}
4751N/AfilterByTranslation :: Maybe G_theory -> GMorphism -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
4751N/AfilterByTranslation maybeTh morphism paths =
4751N/A Just th -> [path| path <- paths, isSameTranslation th morphism path]
4751N/A-- isSameTranslation th morphism (calculateMorphismOfPath path)]
4751N/A{- checks if the given morphism and the morphism of the given path translate the given sentence list to the same resulting sentence list -}
4751N/AisSameTranslation :: G_theory -> GMorphism -> [LEdge DGLinkLab] -> Bool
4751N/AisSameTranslation th morphism path =
4751N/A case calculateMorphismOfPath path of
4751N/A translateG_theory morphism th == translateG_theory morphismOfPath th
4751N/A-- ----------------------------------------------
4751N/A-- ----------------------------------------------
4751N/A-- applies local subsumption to all unproven local theorem edges
4751N/AlocSubsume :: ProofStatus -> IO ProofStatus
4751N/AlocSubsume proofStatus@(ln,libEnv,_) = do
4751N/A let dgraph = lookupDGraph ln proofStatus
4751N/A localThmEdges = filter isUnprovenLocalThm (labEdges dgraph)
4751N/A result = locSubsumeAux libEnv ln dgraph ([],[]) localThmEdges
4751N/A nextHistoryElem = snd result
4751N/A = mkResultProofStatus proofStatus nextDGraph nextHistoryElem
4751N/A-- auxiliary method for locSubsume
4751N/AlocSubsumeAux :: LibEnv -> LIB_NAME -> DGraph -> ([DGRule],[DGChange]) -> [LEdge DGLinkLab]
4751N/A -> (DGraph,([DGRule],[DGChange]))
4751N/AlocSubsumeAux _ _ dgraph historyElement [] = (dgraph, historyElement)
4751N/AlocSubsumeAux libEnv ln dgraph (rules,changes) ((ledge@(src,tgt,edgeLab)):list) =
4751N/A case (getDGNode libEnv dgraph tgt, maybeThSrc) of
4751N/A (Just (target,_), Just thSrc) ->
4751N/A case (maybeResult (computeTheory libEnv ln dgraph target), maybeResult (translateG_theory morphism thSrc)) of
4751N/A (Just theoryTgt, Just (G_theory lidSrc _ sensSrc)) ->
4751N/A case maybeResult (coerceTheory lidSrc theoryTgt) of
4751N/A Nothing -> locSubsumeAux libEnv ln dgraph (rules,changes) list
4751N/A if (all (`elem` sentencesTgt) sensSrc)
4751N/A then locSubsumeAux libEnv ln newGraph (newRules,newChanges) list
4751N/A else locSubsumeAux libEnv ln dgraph (rules,changes) list
4751N/A _ -> locSubsumeAux libEnv ln dgraph (rules,changes) list
4751N/A _ -> -- showDiags defaultHetcatsOpts (errSrc++errTgt)
4751N/A locSubsumeAux libEnv ln dgraph (rules,changes) list
4751N/A morphism = dgl_morphism edgeLab
4751N/A maybeThSrc = computeLocalTheory libEnv dgraph src
4751N/A auxGraph = delLEdge ledge dgraph
4751N/A (LocalThm _ conservativity conservStatus) = (dgl_type edgeLab)
4751N/A DGLink {dgl_morphism = morphism,
4751N/A (LocalThm (Proven (LocSubsumption ledge) [])
4751N/A conservativity conservStatus),
4751N/A newGraph = insEdge newEdge auxGraph
4751N/A newRules = (LocSubsumption ledge):rules
4751N/A newChanges = (DeleteEdge ledge):((InsertEdge newEdge):changes)