{- |

Module : $Header$

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