{- |
Module      :  ./Proofs/TheoremHideShift.hs
Description :  theorem hide shift proof rule for development graphs
Copyright   :  (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(Logic)

theorem hide shift proof rule for development graphs
   Follows Sect. IV:4.4 of the CASL Reference Manual.
-}

{-
   References:

   T. Mossakowski, S. Autexier and D. Hutter:
   Extending Development Graphs With Hiding.
   H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
   Lecture Notes in Computer Science 2029, p. 269-283,
   Springer-Verlag 2001.
-}

module Proofs.TheoremHideShift
    ( theoremHideShift
    , theoremHideShiftFromList
    ) where

import Logic.Logic

import Static.DevGraph
import Static.DgUtils
import Static.History

import Proofs.EdgeUtils
import Proofs.SimpleTheoremHideShift
  (thmHideShift, getInComingGlobalUnprovenEdges)

import Common.LibName
import Common.Result

import Data.Graph.Inductive.Graph as Graph
import qualified Data.Map as Map
import Data.Maybe

{- ----------------------------------------------
Theorem hide shift and  auxiliaries
--------------------------------------------- -}

theoremHideShift :: LibName -> LibEnv -> Result LibEnv
theoremHideShift :: LibName -> LibEnv -> Result LibEnv
theoremHideShift ln :: LibName
ln = LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> Result LibEnv)
-> (LibEnv -> LibEnv) -> LibEnv -> Result LibEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  (DGraph -> DGraph) -> LibName -> LibEnv -> LibEnv
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (\ dg :: DGraph
dg -> [LNode DGNodeLab] -> DGraph -> DGraph
theoremHideShiftAux (DGraph -> [LNode DGNodeLab]
labNodesDG DGraph
dg) DGraph
dg) LibName
ln

{- | assume that the normal forms a commputed already.
return Nothing if nothing changed -}
theoremHideShiftAux :: [LNode DGNodeLab] -> DGraph -> DGraph
theoremHideShiftAux :: [LNode DGNodeLab] -> DGraph -> DGraph
theoremHideShiftAux ns :: [LNode DGNodeLab]
ns dg :: DGraph
dg = let
  nodesWHiding :: [Node]
nodesWHiding = (LNode DGNodeLab -> Node) -> [LNode DGNodeLab] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map LNode DGNodeLab -> Node
forall a b. (a, b) -> a
fst ([LNode DGNodeLab] -> [Node]) -> [LNode DGNodeLab] -> [Node]
forall a b. (a -> b) -> a -> b
$ (LNode DGNodeLab -> Bool) -> [LNode DGNodeLab] -> [LNode DGNodeLab]
forall a. (a -> Bool) -> [a] -> [a]
filter
           (\ (_, lbl :: DGNodeLab
lbl) -> DGNodeLab -> Bool
labelHasHiding DGNodeLab
lbl Bool -> Bool -> Bool
&& Maybe Node -> Bool
forall a. Maybe a -> Bool
isJust (DGNodeLab -> Maybe Node
dgn_nf DGNodeLab
lbl)
           Bool -> Bool -> Bool
&& Maybe GMorphism -> Bool
forall a. Maybe a -> Bool
isJust (DGNodeLab -> Maybe GMorphism
dgn_sigma DGNodeLab
lbl)) [LNode DGNodeLab]
ns
     {- all nodes with incoming hiding links
     all the theorem links entering these nodes
     have to replaced by theorem links with the same origin
     but pointing to the normal form of the former target node -}
  ingoingEdges :: [LEdge DGLinkLab]
ingoingEdges = (Node -> [LEdge DGLinkLab]) -> [Node] -> [LEdge DGLinkLab]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DGraph -> Node -> [LEdge DGLinkLab]
getInComingGlobalUnprovenEdges DGraph
dg) [Node]
nodesWHiding
  in (DGraph -> LEdge DGLinkLab -> DGraph)
-> DGraph -> [LEdge DGLinkLab] -> DGraph
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DGraph -> LEdge DGLinkLab -> DGraph
theoremHideShiftForEdge DGraph
dg [LEdge DGLinkLab]
ingoingEdges

theoremHideShiftForEdge :: DGraph -> LEdge DGLinkLab -> DGraph
theoremHideShiftForEdge :: DGraph -> LEdge DGLinkLab -> DGraph
theoremHideShiftForEdge dg :: DGraph
dg edge :: LEdge DGLinkLab
edge@(source :: Node
source, target :: Node
target, edgeLab :: DGLinkLab
edgeLab) =
  case Result (DGraph, ProofBasis) -> Maybe (DGraph, ProofBasis)
forall a. Result a -> Maybe a
maybeResult (Result (DGraph, ProofBasis) -> Maybe (DGraph, ProofBasis))
-> Result (DGraph, ProofBasis) -> Maybe (DGraph, ProofBasis)
forall a b. (a -> b) -> a -> b
$ DGraph -> LEdge DGLinkLab -> Result (DGraph, ProofBasis)
theoremHideShiftForEdgeAux DGraph
dg LEdge DGLinkLab
edge of
   Nothing -> [Char] -> DGraph
forall a. HasCallStack => [Char] -> a
error "theoremHideShiftForEdgeAux"
   Just (dg' :: DGraph
dg', pbasis :: ProofBasis
pbasis) -> let
    provenEdge :: LEdge DGLinkLab
provenEdge = (Node
source, Node
target, DGLinkLab
edgeLab
        { dgl_type :: DGLinkType
dgl_type = ThmLinkStatus -> DGLinkType -> DGLinkType
setProof (DGRule -> ProofBasis -> ThmLinkStatus
Proven DGRule
thmHideShift ProofBasis
pbasis) (DGLinkType -> DGLinkType) -> DGLinkType -> DGLinkType
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
edgeLab
        , dgl_origin :: DGLinkOrigin
dgl_origin = DGLinkOrigin
DGLinkProof
        , dgl_id :: EdgeId
dgl_id = EdgeId
defaultEdgeId })
    in LEdge DGLinkLab -> DGraph -> DGraph
insertDGLEdge LEdge DGLinkLab
provenEdge (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> DGChange -> DGraph
changeDGH DGraph
dg' (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGChange
DeleteEdge LEdge DGLinkLab
edge

theoremHideShiftForEdgeAux :: DGraph -> LEdge DGLinkLab
                           -> Result (DGraph, ProofBasis)
theoremHideShiftForEdgeAux :: DGraph -> LEdge DGLinkLab -> Result (DGraph, ProofBasis)
theoremHideShiftForEdgeAux dg :: DGraph
dg (sn :: Node
sn, tn :: Node
tn, llab :: DGLinkLab
llab) = do
  let tlab :: DGNodeLab
tlab = DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
tn
      Just nfNode :: Node
nfNode = DGNodeLab -> Maybe Node
dgn_nf DGNodeLab
tlab
      phi :: GMorphism
phi = DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
llab
      Just muN :: GMorphism
muN = DGNodeLab -> Maybe GMorphism
dgn_sigma DGNodeLab
tlab
  GMorphism
cmor <- GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp GMorphism
phi GMorphism
muN
  let newEdge :: LEdge DGLinkLab
newEdge = (Node
sn, Node
nfNode, GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink GMorphism
cmor DGLinkType
globalThm DGLinkOrigin
DGLinkProof)
  case LEdge DGLinkLab -> DGraph -> Maybe (LEdge DGLinkLab)
tryToGetEdge LEdge DGLinkLab
newEdge DGraph
dg of
        Nothing -> let
          newGraph :: DGraph
newGraph = DGraph -> DGChange -> DGraph
changeDGH DGraph
dg (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
newEdge
          finalEdge :: LEdge DGLinkLab
finalEdge = case DGraph -> DGChange
getLastChange DGraph
newGraph of
            InsertEdge final_e :: LEdge DGLinkLab
final_e -> LEdge DGLinkLab
final_e
            _ -> [Char] -> LEdge DGLinkLab
forall a. HasCallStack => [Char] -> a
error "Proofs.Global.globDecompForOneEdgeAux"
          in (DGraph, ProofBasis) -> Result (DGraph, ProofBasis)
forall (m :: * -> *) a. Monad m => a -> m a
return
              (DGraph
newGraph, ProofBasis -> EdgeId -> ProofBasis
addEdgeId ProofBasis
emptyProofBasis (EdgeId -> ProofBasis) -> EdgeId -> ProofBasis
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> EdgeId
getEdgeId LEdge DGLinkLab
finalEdge)
        Just e :: LEdge DGLinkLab
e -> (DGraph, ProofBasis) -> Result (DGraph, ProofBasis)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dg, ProofBasis -> EdgeId -> ProofBasis
addEdgeId ProofBasis
emptyProofBasis (EdgeId -> ProofBasis) -> EdgeId -> ProofBasis
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> EdgeId
getEdgeId LEdge DGLinkLab
e)

theoremHideShiftFromList :: LibName -> [LNode DGNodeLab] -> LibEnv
                         -> Result LibEnv
theoremHideShiftFromList :: LibName -> [LNode DGNodeLab] -> LibEnv -> Result LibEnv
theoremHideShiftFromList ln :: LibName
ln ls :: [LNode DGNodeLab]
ls =
  LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> Result LibEnv)
-> (LibEnv -> LibEnv) -> LibEnv -> Result LibEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DGraph -> DGraph) -> LibName -> LibEnv -> LibEnv
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust ([LNode DGNodeLab] -> DGraph -> DGraph
theoremHideShiftAux [LNode DGNodeLab]
ls) LibName
ln