{- |
Module      :
Copyright   :  (c) Cui Jian, Till Mossakowski, Uni Bremen 2002-2006
Description :  simple version of theorem hide shift proof rule
License     :  GPLv2 or higher, see LICENSE.txt

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

simple version of 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.

   it relates to the ticket 13

-}

module Proofs.SimpleTheoremHideShift
  ( theoremHideShift
  , thmHideShift
  , getInComingGlobalUnprovenEdges
  ) where

import Proofs.EdgeUtils

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

import Common.LibName

import qualified Data.Map as Map
import Data.Graph.Inductive.Graph
import Data.Maybe (fromMaybe)

-- | rule name
thmHideShift :: DGRule
thmHideShift :: DGRule
thmHideShift = String -> DGRule
DGRule "TheoremHideShift"

{- | to be exported function.
     firstly it gets all the hiding definition links out of DGraph and
     passes them to theoremHideShiftFromList which does the actual processing
-}
theoremHideShift :: LibName -> LibEnv -> LibEnv
theoremHideShift :: LibName -> LibEnv -> LibEnv
theoremHideShift ln :: LibName
ln proofStatus :: LibEnv
proofStatus =
    let dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
proofStatus
        hidingDefEdges :: [LEdge DGLinkLab]
hidingDefEdges = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
isHidingDef) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dgraph
        newDGraph :: DGraph
newDGraph = (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
theoremHideShiftFromList DGraph
dgraph [LEdge DGLinkLab]
hidingDefEdges
    in LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
newDGraph LibEnv
proofStatus

{- | apply the theorem hide shift with a list of hiding definition links.
     it calls the function for one hiding edge at a time and fills the history
     if necessary.
-}
theoremHideShiftFromList :: DGraph -> LEdge DGLinkLab -> DGraph
theoremHideShiftFromList :: DGraph -> LEdge DGLinkLab -> DGraph
theoremHideShiftFromList dgraph :: DGraph
dgraph e :: LEdge DGLinkLab
e = let
    newDGraph :: DGraph
newDGraph = DGraph -> LEdge DGLinkLab -> DGraph
theoremHideShiftWithOneHidingDefEdge DGraph
dgraph LEdge DGLinkLab
e
    in DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dgraph DGRule
thmHideShift DGraph
newDGraph

{- | apply the rule to one hiding definition link.
     it takes all the related global unproven edges to the given hiding edge
     and passes them together to its auxiliary function.
-}
theoremHideShiftWithOneHidingDefEdge :: DGraph -> LEdge DGLinkLab -> DGraph
theoremHideShiftWithOneHidingDefEdge :: DGraph -> LEdge DGLinkLab -> DGraph
theoremHideShiftWithOneHidingDefEdge dgraph :: DGraph
dgraph e :: LEdge DGLinkLab
e@(_, n :: Node
n, _) =
    (DGraph -> LEdge DGLinkLab -> DGraph)
-> DGraph -> [LEdge DGLinkLab] -> DGraph
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (LEdge DGLinkLab -> DGraph -> LEdge DGLinkLab -> DGraph
theoremHideShiftWithOneHidingDefEdgeAux LEdge DGLinkLab
e) DGraph
dgraph
      ([LEdge DGLinkLab] -> DGraph) -> [LEdge DGLinkLab] -> DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> [LEdge DGLinkLab]
getInComingGlobalUnprovenEdges DGraph
dgraph Node
n

{- | get all the global unproven threorem links which go into the given
     node in the given dgraph
-}
getInComingGlobalUnprovenEdges :: DGraph -> Node -> [LEdge DGLinkLab]
getInComingGlobalUnprovenEdges :: DGraph -> Node -> [LEdge DGLinkLab]
getInComingGlobalUnprovenEdges dgraph :: DGraph
dgraph =
    (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
isUnprovenGlobalThm) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> (Node -> [LEdge DGLinkLab]) -> Node -> [LEdge DGLinkLab]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Node -> [LEdge DGLinkLab]
innDG DGraph
dgraph

{- | it's the main function of this simplified theorem hide shift.
     it applies the rule to a list of global unproven threorem links
     with the related hiding definition link. It contains three steps
     fulfilling the task and is marked below.
-}
theoremHideShiftWithOneHidingDefEdgeAux :: LEdge DGLinkLab -> DGraph
                                        -> LEdge DGLinkLab -> DGraph
theoremHideShiftWithOneHidingDefEdgeAux :: LEdge DGLinkLab -> DGraph -> LEdge DGLinkLab -> DGraph
theoremHideShiftWithOneHidingDefEdgeAux hd :: LEdge DGLinkLab
hd@(hds :: Node
hds, _, _) dgraph :: DGraph
dgraph x :: LEdge DGLinkLab
x@(s :: Node
s, t :: Node
t, lbl :: DGLinkLab
lbl) =
  let
    newMorphism :: GMorphism
newMorphism = GMorphism -> Maybe GMorphism -> GMorphism
forall a. a -> Maybe a -> a
fromMaybe (String -> GMorphism
forall a. HasCallStack => String -> a
error
       "SimpleTheoremHideShift.theoremHideShiftWithOneHidingDefEdgeAux") (Maybe GMorphism -> GMorphism) -> Maybe GMorphism -> GMorphism
forall a b. (a -> b) -> a -> b
$
       [LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath [LEdge DGLinkLab
x, LEdge DGLinkLab
hd]
    newGlobalEdge :: LEdge DGLinkLab
newGlobalEdge = (Node
s, Node
hds, GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink GMorphism
newMorphism DGLinkType
globalThm DGLinkOrigin
DGLinkProof)
    (newDGraph :: DGraph
newDGraph, proofbasis :: ProofBasis
proofbasis) =
      DGraph -> LEdge DGLinkLab -> ProofBasis -> (DGraph, ProofBasis)
tryToInsertEdgeAndSelectProofBasis DGraph
dgraph LEdge DGLinkLab
newGlobalEdge ProofBasis
emptyProofBasis
    -- ------ to insert a proven global theorem link ---------------
    provenEdge :: LEdge DGLinkLab
provenEdge = (Node
s, Node
t, DGLinkLab
lbl
      { dgl_type :: DGLinkType
dgl_type = ThmLinkStatus -> DGLinkType -> DGLinkType
setProof (DGRule -> ProofBasis -> ThmLinkStatus
Proven DGRule
thmHideShift
                              ProofBasis
proofbasis) (DGLinkType -> DGLinkType) -> DGLinkType -> DGLinkType
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lbl
      , dgl_origin :: DGLinkOrigin
dgl_origin = DGLinkOrigin
DGLinkProof })
  in DGraph -> [DGChange] -> DGraph
changesDGH DGraph
newDGraph [LEdge DGLinkLab -> DGChange
DeleteEdge LEdge DGLinkLab
x, LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
provenEdge]

{- | it tries to insert the given edge into the DGraph and selects the
     inserted edge as proof basis if possible.
-}
tryToInsertEdgeAndSelectProofBasis :: DGraph -> LEdge DGLinkLab -> ProofBasis
                                   -> (DGraph, ProofBasis)
tryToInsertEdgeAndSelectProofBasis :: DGraph -> LEdge DGLinkLab -> ProofBasis -> (DGraph, ProofBasis)
tryToInsertEdgeAndSelectProofBasis dgraph :: DGraph
dgraph newEdge :: LEdge DGLinkLab
newEdge proofbasis :: ProofBasis
proofbasis =
    case LEdge DGLinkLab -> DGraph -> Maybe (LEdge DGLinkLab)
tryToGetEdge LEdge DGLinkLab
newEdge DGraph
dgraph of
      Just tempE :: LEdge DGLinkLab
tempE -> (DGraph
dgraph, ProofBasis -> EdgeId -> ProofBasis
addEdgeId ProofBasis
proofbasis (EdgeId -> ProofBasis) -> EdgeId -> ProofBasis
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> EdgeId
getEdgeId LEdge DGLinkLab
tempE)
      Nothing -> let
          tempDGraph :: DGraph
tempDGraph = DGraph -> DGChange -> DGraph
changeDGH DGraph
dgraph (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
newEdge
          tempPB :: ProofBasis
tempPB = case DGraph -> DGChange
getLastChange DGraph
tempDGraph of
            InsertEdge tempE :: LEdge DGLinkLab
tempE -> ProofBasis -> EdgeId -> ProofBasis
addEdgeId ProofBasis
proofbasis (EdgeId -> ProofBasis) -> EdgeId -> ProofBasis
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> EdgeId
getEdgeId LEdge DGLinkLab
tempE
            _ -> String -> ProofBasis
forall a. HasCallStack => String -> a
error
              "SimpleTheoremHideShift.tryToInsertEdgeAndSelectProofBasis"
          in (DGraph
tempDGraph, ProofBasis
tempPB)