{- |

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 "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 ln proofStatus =

let dgraph = lookupDGraph ln proofStatus

hidingDefEdges = filter (liftE isHidingDef) $ labEdgesDG dgraph

newDGraph = foldl theoremHideShiftFromList dgraph hidingDefEdges

in Map.insert ln newDGraph 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 e = let

newDGraph = theoremHideShiftWithOneHidingDefEdge dgraph e

in groupHistory dgraph thmHideShift 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 e@(_, n, _) =

foldl (theoremHideShiftWithOneHidingDefEdgeAux e) dgraph

$ getInComingGlobalUnprovenEdges dgraph 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 =

filter (liftE isUnprovenGlobalThm) . innDG 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 hd@(hds, _, _) dgraph x@(s, t, lbl) =

let

newMorphism = fromMaybe (error

"SimpleTheoremHideShift.theoremHideShiftWithOneHidingDefEdgeAux") $

calculateMorphismOfPath [x, hd]

newGlobalEdge = (s, hds, defDGLink newMorphism globalThm DGLinkProof)

(newDGraph, proofbasis) =

tryToInsertEdgeAndSelectProofBasis dgraph newGlobalEdge emptyProofBasis

-- ------ to insert a proven global theorem link ---------------

provenEdge = (s, t, lbl

{ dgl_type = setProof (Proven thmHideShift

proofbasis) $ dgl_type lbl

, dgl_origin = DGLinkProof })

in changesDGH newDGraph [DeleteEdge x, InsertEdge 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 newEdge proofbasis =

case tryToGetEdge newEdge dgraph of

Just tempE -> (dgraph, addEdgeId proofbasis $ getEdgeId tempE)

Nothing -> let

tempDGraph = changeDGH dgraph $ InsertEdge newEdge

tempPB = case getLastChange tempDGraph of

InsertEdge tempE -> addEdgeId proofbasis $ getEdgeId tempE

_ -> error

"SimpleTheoremHideShift.tryToInsertEdgeAndSelectProofBasis"

in (tempDGraph, tempPB)