hets/Proofs/Local.hs

	Local.hs revision 9603ad7198b72e812688ad7970e4eac4b553837a
e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski{- |
0095c7efbddd0ffeed6aaf8ec015346be161d819Till MossakowskiModule      :  $Header$
0095c7efbddd0ffeed6aaf8ec015346be161d819Till MossakowskiCopyright   :  (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2004
e687bd70d6e6c98d82b239e01fef4a60de6739f4Till MossakowskiLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill MossakowskiMaintainer  :  jfgerken@tzi.de
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill MossakowskiStability   :  provisional
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill MossakowskiPortability :  non-portable(Logic)
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskilocal proofs in development graphs.
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski   Follows Sect. IV:4.4 of the CASL Reference Manual.
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski-}
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski{-
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill MossakowskiOrder of rule application: try to use local links induced by %implies
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskifor subsumption proofs (such that the %implied formulas need not be
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskire-proved)
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski-}
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskimodule Proofs.Local (localInference, locDecomp) where
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Logic.Grothendieck
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Static.DevGraph
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Static.DGToSpec
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Common.Result
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Logic.Prover
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Common.Utils
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport qualified Common.Lib.Map as Map
e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowskiimport qualified Common.OrderedMap as OMap
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescuimport Data.Graph.Inductive.Graph
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescuimport Data.Maybe
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescuimport Proofs.EdgeUtils
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescuimport Proofs.StatusUtils
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescuimport Syntax.AS_Library
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescu
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescu-- --------------------
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescu-- local decomposition
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescu-- --------------------
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescu
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescu{- a merge of the rules local subsumption, local decomposition I and
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescu   local decomposition II -}
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescu-- applies this merge of rules to all unproven localThm edges if possible
37bca994f215449238dd0c8308a94a83ae184d38Mihai CodesculocDecomp ::  ProofStatus -> ProofStatus
37bca994f215449238dd0c8308a94a83ae184d38Mihai CodesculocDecomp proofStatus@(ln,libEnv,_) =
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescu  let dgraph = lookupDGraph ln proofStatus
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescu      localThmEdges = filter isUnprovenLocalThm (labEdges dgraph)
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescu      (nextDGraph, nextHistoryElem) =
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescu          locDecompAux libEnv ln dgraph ([],[]) localThmEdges
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescu  in mkResultProofStatus proofStatus nextDGraph nextHistoryElem
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescu
37bca994f215449238dd0c8308a94a83ae184d38Mihai Codescu{- auxiliary function for locDecomp (above)
e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski   actual implementation -}
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill MossakowskilocDecompAux :: LibEnv -> LIB_NAME -> DGraph -> ([DGRule],[DGChange])
be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski             -> [LEdge DGLinkLab] -> (DGraph,([DGRule],[DGChange]))
da955132262baab309a50fdffe228c9efe68251dCui JianlocDecompAux _ _ dgraph historyElement [] = (dgraph, historyElement)
e687bd70d6e6c98d82b239e01fef4a60de6739f4Till MossakowskilocDecompAux libEnv ln dgraph (rules,changes)
e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski                 (ledge@(src, tgt, edgeLab) : list) =
e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski  if (null proofBasis && not (isIdentityEdge ledge libEnv dgraph))
7474388b4c2236f8ab2327289555000268c7901aTill Mossakowski     then
7474388b4c2236f8ab2327289555000268c7901aTill Mossakowski       locDecompAux libEnv ln dgraph (rules, changes) list
7474388b4c2236f8ab2327289555000268c7901aTill Mossakowski     else
7474388b4c2236f8ab2327289555000268c7901aTill Mossakowski       if isDuplicate newEdge dgraph changes
7474388b4c2236f8ab2327289555000268c7901aTill Mossakowski          then locDecompAux libEnv ln auxGraph
e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski                 (newRules, DeleteEdge ledge : changes) list
da955132262baab309a50fdffe228c9efe68251dCui Jian       else locDecompAux libEnv ln newGraph (newRules,newChanges) list
e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski
8d6aa4bda97770cc79cf96de3c0f9dfa4d7d7aafChristian Maeder  where
99249aeda5fac6f8f0b2316ca357bac898af1928Christian Maeder    morphism = dgl_morphism edgeLab
e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski    allPaths = getAllLocGlobPathsBetween dgraph src tgt
e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski    th = computeLocalTheory libEnv (ln, src)
4918e2f622cfb96f9a57b7617cd18ca7e4f8b5d4Christian Maeder    pathsWithoutEdgeItself = [ path | path <- allPaths, notElem ledge path ]
    filteredPaths = filterByTranslation th morphism pathsWithoutEdgeItself
    proofBasis = selectProofBasis ledge filteredPaths
    auxGraph = delLEdge ledge dgraph
    (LocalThm _ conservativity conservStatus) = (dgl_type edgeLab)
    newEdge = (src,
               tgt,
               DGLink {dgl_morphism = morphism,
                       dgl_type =
                         (LocalThm (Proven (LocDecomp ledge) proofBasis)
                          conservativity conservStatus),
                       dgl_origin = DGProof}
               )
    newGraph = insEdge newEdge auxGraph
    newRules =  LocDecomp ledge : rules
    newChanges = DeleteEdge ledge : InsertEdge newEdge : changes


{- | 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 -> [path| path <- paths, isSameTranslation th morphism path]
    Nothing -> []
--     isSameTranslation th morphism (calculateMorphismOfPath path)]

{- | 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 ->
         translateG_theory morphism th == translateG_theory morphismOfPath th
      Nothing -> False

-- ----------------------------------------------
-- local subsumption
-- ----------------------------------------------

-- applies local subsumption to all unproven local theorem edges
localInference :: ProofStatus -> ProofStatus
localInference proofStatus@(ln,libEnv,_) =
  let dgraph = lookupDGraph ln proofStatus
      localThmEdges = filter isUnprovenLocalThm (labEdges dgraph)
      (nextDGraph, nextHistoryElem) =
          localInferenceAux libEnv ln dgraph ([],[]) localThmEdges
  in mkResultProofStatus proofStatus nextDGraph nextHistoryElem

-- auxiliary method for localInference
localInferenceAux :: LibEnv -> LIB_NAME -> DGraph -> ([DGRule],[DGChange])
                  -> [LEdge DGLinkLab] -> (DGraph,([DGRule],[DGChange]))
localInferenceAux _ _ dgraph historyElement [] = (dgraph, historyElement)
localInferenceAux libEnv ln dgraph (rules, changes)
                      (ledge@(src,tgt,edgeLab) : list) =
  case maybeThSrc of
    Just thSrc ->
      case (maybeResult (computeTheory libEnv (ln, tgt)),
                        maybeResult (translateG_theory morphism thSrc)) of
        (Just (G_theory lidTgt _ sensTgt), Just (G_theory lidSrc _ sensSrc)) ->
          case maybeResult (coerceThSens lidTgt lidSrc "" sensTgt) of
            Nothing -> localInferenceAux libEnv ln dgraph (rules,changes) list
            Just sentencesTgt ->
              -- check if all source axioms are also axioms in the target
              let goals = OMap.filter isAxiom sensSrc
                           OMap.\\ sentencesTgt
                  goals' = markAsGoal goals
                  newTh = case (dgn_theory oldContents) of
                          G_theory lid sig sens ->
                           case coerceThSens lidSrc lid "" goals' of
                             Nothing -> G_theory lid sig sens
                             Just goals'' ->
                                 G_theory lid sig (sens `joinSens` goals'')
             in if OMap.null goals
                then
                 let newEdge = (src, tgt, newLab)
                     newGraph = insEdge newEdge auxGraph
                     newChanges = changes ++
                                  [DeleteEdge ledge, InsertEdge newEdge]
                 in localInferenceAux libEnv ln newGraph
                        (newRules,newChanges) list
                else
                 let n = getNewNode auxGraph
                     newNode = (n, oldContents{dgn_theory = newTh})
                     newList = map (replaceNode tgt n) list
                     (newGraph,changes') = adoptEdges
                                           (insNode newNode $ auxGraph) tgt n
                     newEdge = (src, n, newLab)
                     newGraph' = insEdge newEdge  $  delNode tgt $ newGraph
                     newLibEnv = Map.adjust adjMap ln libEnv
                     adjMap (annos, env, _dg) = (annos,env,newGraph')
                     newChanges = changes ++ DeleteEdge ledge :
                                    InsertNode newNode : changes' ++
                                    [DeleteNode oldNode,InsertEdge newEdge]
                 in localInferenceAux newLibEnv ln newGraph'
                        (newRules,newChanges) newList
        _ -> localInferenceAux libEnv ln dgraph (rules,changes) list
    _ -> localInferenceAux libEnv ln dgraph (rules,changes) list
  where
    morphism = dgl_morphism edgeLab
    maybeThSrc = computeLocalTheory libEnv (ln, src)
    auxGraph = delLEdge ledge dgraph
    (LocalThm _ conservativity conservStatus) = (dgl_type edgeLab)
    newLab = DGLink {dgl_morphism = morphism,
                       dgl_type =
                         (LocalThm (Proven (LocInference ledge) [])
                          conservativity conservStatus),
                       dgl_origin = DGProof}
    newRules = (LocInference ledge):rules
    oldNode = labNode' (safeContext "localInferenceAux" dgraph tgt)
    (_,oldContents) = oldNode
    replaceNode from to (src',tgt',labl) =
       (replaceNodeAux from to src', replaceNodeAux from to tgt',labl)
    replaceNodeAux from to n = if n==from then to else n