{- |
Module : ./Proofs/Local.hs
Description : local proof rules for development graphs
Copyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006
License : GPLv2 or higher, see LICENSE.txt
Maintainer : till@informatik.uni-bremen.de
Stability : provisional
Portability : non-portable(Logic)
local proof rules for development graphs
Follows Sect. IV:4.4 of the CASL Reference Manual.
-}
{-
Order of rule application: try to use local links induced by %implies
for subsumption proofs (such that the %implied formulas need not be
re-proved)
-}
module Proofs.Local
( localInference
, locDecomp
, locDecompFromList
, localInferenceFromList
) where
import Proofs.EdgeUtils
import Proofs.StatusUtils
import Logic.Grothendieck
import Logic.Prover
import Static.GTheory
import Static.DevGraph
import Static.DgUtils
import Static.History
import Static.ComputeTheory
import Common.AS_Annotation
import Common.LibName
import Common.Result
import qualified Common.OrderedMap as OMap
import Data.Graph.Inductive.Graph
import qualified Data.Map as Map
import Data.Maybe
-- | local decomposition
locDecompFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
locDecompFromList ln localThmEdges libEnv =
let dgraph = lookupDGraph ln libEnv
finalLocalThmEdges = filter (liftE isUnprovenLocalThm) localThmEdges
nextDGraph = foldl (locDecompAux libEnv ln) dgraph finalLocalThmEdges
in Map.insert ln nextDGraph libEnv
-- | local decomposition for all edges
locDecomp :: LibName -> LibEnv -> LibEnv
locDecomp ln libEnv =
let dgraph = lookupDGraph ln libEnv
localThmEdges = labEdgesDG dgraph
in locDecompFromList ln localThmEdges libEnv
{- auxiliary function for locDecomp (above)
actual implementation -}
locDecompAux :: LibEnv -> LibName -> DGraph -> LEdge DGLinkLab -> DGraph
locDecompAux libEnv ln dgraph ledge@(src, tgt, edgeLab) = let
morphism = dgl_morphism edgeLab
allPaths = getAllLocGlobPathsBetween dgraph src tgt
th = computeLocalTheory libEnv ln src
pathsWithoutEdgeItself = filter (noPath ledge) allPaths
filteredPaths = filterByTranslation th morphism pathsWithoutEdgeItself
proofbasis = selectProofBasis dgraph ledge filteredPaths
auxGraph = changeDGH dgraph $ DeleteEdge ledge
locDecompRule = DGRuleWithEdge "Local-Decomposition" $ getEdgeId ledge
newEdge = (src, tgt, edgeLab
{ dgl_type = setProof (Proven locDecompRule proofbasis)
$ dgl_type edgeLab
, dgl_origin = DGLinkProof })
newGraph = insertDGLEdge newEdge auxGraph
in if not (isIdentityEdge ledge libEnv dgraph) && nullProofBasis proofbasis
then dgraph else
groupHistory dgraph locDecompRule newGraph
{- | 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. -}
filterByTranslation :: Maybe G_theory -> GMorphism -> [[LEdge DGLinkLab]]
-> [[LEdge DGLinkLab]]
filterByTranslation maybeTh morphism paths =
case maybeTh of
Just th -> filter (isSameTranslation th morphism) paths
Nothing -> []
{- | checks if the given morphism and the morphism of the given path
translate the given sentence list to the same resulting sentence list. -}
isSameTranslation :: G_theory -> GMorphism -> [LEdge DGLinkLab] -> Bool
isSameTranslation th morphism path =
case calculateMorphismOfPath path of
Just morphismOfPath ->
maybeResult (translateG_theory morphism th) ==
maybeResult (translateG_theory morphismOfPath th)
Nothing -> False
-- | local inference
localInferenceFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
localInferenceFromList ln localThmEdges libEnv =
localInferenceFromAux ln libEnv (lookupDGraph ln libEnv) localThmEdges
localInferenceFromAux :: LibName -> LibEnv -> DGraph -> [LEdge DGLinkLab]
-> LibEnv
localInferenceFromAux ln libEnv dgraph localThmEdges =
let finalLocalThmEdges = filter (liftE isUnprovenLocalThm) localThmEdges
nextDGraph = foldl (localInferenceAux libEnv) dgraph finalLocalThmEdges
in Map.insert ln (computeDGraphTheories libEnv ln nextDGraph) libEnv
-- | local inference for all edges
localInference :: LibName -> LibEnv -> LibEnv
localInference ln libEnv =
let dgraph = lookupDGraph ln libEnv
localThmEdges = labEdgesDG dgraph
in localInferenceFromAux ln libEnv dgraph localThmEdges
-- auxiliary method for localInference
localInferenceAux :: LibEnv -> DGraph -> LEdge DGLinkLab -> DGraph
localInferenceAux libEnv dgraph ledge@(src, tgt, edgeLab) = let
morphism = dgl_morphism edgeLab
maybeThSrc = computeLocalNodeTheory libEnv dgraph src
oldContents = labDG dgraph tgt
in case maybeThSrc of
Just thSrc ->
case (computeLocalNodeTheory libEnv dgraph tgt,
maybeResult $ translateG_theory morphism thSrc) of
(Just th@(G_theory lidTgt syn sig ind sensTgt _),
Just (G_theory lidSrc _ _ _ sentensSrc _)) ->
case maybeResult (coerceThSens lidSrc lidTgt "" sentensSrc) of
Nothing -> dgraph
Just sensSrc ->
-- check if all source axioms are also axioms in the target
let goals = OMap.filter isAxiom sensSrc
goals' = markAsGoal goals
noGoals = Map.null goals'
(newSens, renms) = joinSensAux sensTgt goals'
provenSens = proveSens lidTgt newSens
pendingGoals =
any (not . isProvenSenStatus
. fromMaybe (error "localInferenceAux")
. flip OMap.lookup provenSens)
$ map snd renms
newTh = if noGoals then th else
G_theory lidTgt syn sig ind provenSens startThId
newContents = oldContents { dgn_theory = newTh }
locInferRule = DGRuleLocalInference renms
newLab = edgeLab
{ dgl_type = setProof (Proven locInferRule emptyProofBasis)
$ dgl_type edgeLab
, dgl_origin = DGLinkProof
, dglPending = pendingGoals }
newEdge = (src, tgt, newLab)
newGraph0 = changesDGH dgraph
$ (if noGoals then [] else
[SetNodeLab oldContents (tgt, newContents)])
++ [DeleteEdge ledge, InsertEdge newEdge]
newGraph =
togglePending newGraph0 $ changedPendingEdges newGraph0
in groupHistory dgraph locInferRule newGraph
_ -> dgraph
_ -> dgraph