content: {- |
  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 ln = return .
    Map.adjust (\ dg -> theoremHideShiftAux (labNodesDG dg) dg) ln
  
  {- | assume that the normal forms a commputed already.
  return Nothing if nothing changed -}
  theoremHideShiftAux :: [LNode DGNodeLab] -> DGraph -> DGraph
  theoremHideShiftAux ns dg = let
    nodesWHiding = map fst $ filter
             (\ (_, lbl) -> labelHasHiding lbl && isJust (dgn_nf lbl)
             && isJust (dgn_sigma lbl)) 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 = concatMap (getInComingGlobalUnprovenEdges dg) nodesWHiding
    in foldl theoremHideShiftForEdge dg ingoingEdges
  
  theoremHideShiftForEdge :: DGraph -> LEdge DGLinkLab -> DGraph
  theoremHideShiftForEdge dg edge@(source, target, edgeLab) =
    case maybeResult $ theoremHideShiftForEdgeAux dg edge of
     Nothing -> error "theoremHideShiftForEdgeAux"
     Just (dg', pbasis) -> let
      provenEdge = (source, target, edgeLab
          { dgl_type = setProof (Proven thmHideShift pbasis) $ dgl_type edgeLab
          , dgl_origin = DGLinkProof
          , dgl_id = defaultEdgeId })
      in insertDGLEdge provenEdge $ changeDGH dg' $ DeleteEdge edge
  
  theoremHideShiftForEdgeAux :: DGraph -> LEdge DGLinkLab
                             -> Result (DGraph, ProofBasis)
  theoremHideShiftForEdgeAux dg (sn, tn, llab) = do
    let tlab = labDG dg tn
        Just nfNode = dgn_nf tlab
        phi = dgl_morphism llab
        Just muN = dgn_sigma tlab
    cmor <- comp phi muN
    let newEdge = (sn, nfNode, defDGLink cmor globalThm DGLinkProof)
    case tryToGetEdge newEdge dg of
          Nothing -> let
            newGraph = changeDGH dg $ InsertEdge newEdge
            finalEdge = case getLastChange newGraph of
              InsertEdge final_e -> final_e
              _ -> error "Proofs.Global.globDecompForOneEdgeAux"
            in return
                (newGraph, addEdgeId emptyProofBasis $ getEdgeId finalEdge)
          Just e -> return (dg, addEdgeId emptyProofBasis $ getEdgeId e)
  
  theoremHideShiftFromList :: LibName -> [LNode DGNodeLab] -> LibEnv
                           -> Result LibEnv
  theoremHideShiftFromList ln ls =
    return . Map.adjust (theoremHideShiftAux ls) ln
  