{- |

Module : $Header$

Description : theorem hide shift proof rule for development graphs

Copyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : ken@informatik.uni-bremen.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

, convertToNf

, convertNodesToNf

, hasIngoingHidingDef

, computeTheory

, theoremsToAxioms

) where

import Logic.Logic

import Logic.Prover

import Static.GTheory

import Static.DevGraph

import Static.WACocone

import Proofs.EdgeUtils

import Proofs.ComputeColimit

import Proofs.SimpleTheoremHideShift

(thmHideShift, getInComingGlobalUnprovenEdges)

import Common.Id

import Common.LibName

import Common.Result

import Data.Graph.Inductive.Graph as Graph

import qualified Data.Map as Map

import Data.List (nub, sortBy)

import Control.Monad

normalFormRule :: DGRule

normalFormRule = DGRule "NormalForm"

convertNodesToNf :: LIB_NAME -> LibEnv -> Result LibEnv

convertNodesToNf ln libEnv = do

libEnv' <- foldM (convertToNf ln) libEnv $

nodesDG $ lookupDGraph ln libEnv

let oldGraph = lookupDGraph ln libEnv

newGraph = lookupDGraph ln libEnv'

return $ Map.insert ln

(groupHistory oldGraph thmHideShift newGraph) libEnv'

{- | converts the given node to its own normal form -}

convertToNf :: LIB_NAME -> LibEnv -> Node -> Result LibEnv

convertToNf ln libEnv node = do

let dgraph = lookupDGraph ln libEnv

nodelab = labDG dgraph node

case dgn_nf nodelab of

-- here checks if it's already been computed

Just _ -> return libEnv

Nothing ->

case hasIngoingHidingDef libEnv ln node of

False -> -- no hiding, nf is the node itself

-- we need to update the fields

-- dgn_sign and dgn_nf of node

do

let (sign, mor) = (dgn_theory nodelab, Just $ ide $ dgn_sign nodelab)

newLab = (newNodeLab (dgn_name nodelab) DGProof sign){

dgn_nf = Just node,

dgn_sigma = mor,

nodeInfo = nodeInfo nodelab}

chLab = SetNodeLab nodelab (node, newLab)

newGraph = changeDGH dgraph chLab

return $ Map.insert ln

(groupHistory dgraph normalFormRule newGraph) libEnv

True -> case isDGRef nodelab of

True -> do

-- the normal form of the node

-- is a reference to the normal form of the node it references

-- careful: here not refNf, but a new Node which references refN

let refLib = dgn_libname nodelab

refNode = dgn_node nodelab

libEnv' <- convertToNf refLib libEnv refNode

let

refGraph' = lookupDGraph refLib libEnv'

Just refNf = dgn_nf $ labDG refGraph' refNode

-- the normal form just computed ^

refNodelab = labDG refGraph' refNf

-- the label of the normal form ^

nfNode = getNewNodeDG dgraph

-- the new reference node in the old graph ^

NodeName tt _ss _ii = dgn_name nodelab

nfName = mkSimpleId $ "NormalForm" ++ show tt ++ show node

refLab = DGNodeLab{

dgn_name = NodeName nfName (show nfName) 0,

dgn_theory = dgn_theory $ refNodelab,

dgn_nf = Just nfNode,

dgn_sigma = Just $ ide $ dgn_sign refNodelab,

nodeInfo = DGRef{ref_libname = dgn_libname nodelab,

ref_node = refNf},

dgn_lock = Nothing

}

newLab = nodelab{

dgn_nf = Just nfNode,

dgn_sigma = dgn_sigma $ labDG refGraph' $ dgn_node nodelab

}

chLab = SetNodeLab nodelab (node, newLab)

changes = [InsertNode (nfNode, refLab), chLab]

newGraph = changesDGH dgraph changes

return $ Map.insert ln

(groupHistory dgraph normalFormRule newGraph) libEnv'

False -> do

auxProofstatus <- createNfsForPredecessors ln libEnv node

(diagram, g) <- computeDiagram ln auxProofstatus node

let Result _ds res = gWeaklyAmalgamableCocone diagram

case res of

Nothing -> fail "convert to normal form: can't compute cocone"

Just (sign, mmap) -> do

let

-- the new node which will contain the normal form

auxGraph = lookupDGraph ln auxProofstatus

nfNode = getNewNodeDG auxGraph

-- the label of the new node

NodeName tt ss _ii = dgn_name nodelab

nfName = mkSimpleId $ "NormalForm" ++ show tt ++ show node

nfLabel = DGNodeLab{

dgn_name = NodeName nfName ss 0,

dgn_theory = sign,

dgn_nf = Just nfNode, -- is its own nf

dgn_sigma = Just $ ide $ signOf sign, -- id morphism

nodeInfo = DGNode{

node_origin = DGProof,

node_cons_status = Nothing

},

dgn_lock = Nothing

}

-- the new label for node

newLab = (newNodeLab (dgn_name nodelab) DGProof

(dgn_theory nodelab))

{ dgn_nf = Just nfNode,

dgn_sigma = Just $ mmap Map.! (g Map.! node)

}

-- add the nf to the label of node

chLab = SetNodeLab nodelab (node, newLab)

-- insert the new node and add edges from the predecessors

insNNF = InsertNode (nfNode, nfLabel)

makeEdge src tgt m = (src, tgt, DGLink { dgl_morphism = m

, dgl_type = GlobalDef

, dgl_origin = DGLinkProof

, dgl_id = defaultEdgeId

})

insStrMor = map (\ (x, f) -> InsertEdge $ makeEdge x nfNode f)

$ nub $ map (\ (x, y) -> (g Map.! x, y))

$ Map.toList mmap

allChanges = chLab : insNNF : insStrMor

newGraph = changesDGH auxGraph allChanges

return $ Map.insert ln

(groupHistory auxGraph normalFormRule newGraph)

auxProofstatus

{- computes the diagram associated to a node N in a development graph,

adding common origins for multiple occurences of nodes, whenever

needed

-}

computeDiagram :: LIB_NAME -> LibEnv -> Node ->

Result (GDiagram, Map.Map Node Node) -- (D,G)

computeDiagram ln libEnv node =

unfoldedGraph ln libEnv node

-- as described in the paper for now

unfoldedGraph :: LIB_NAME -> LibEnv -> Node ->

Result (GDiagram, Map.Map Node Node)

unfoldedGraph ln libEnv node = do

let dgraph = lookupDGraph ln libEnv

gd = insNode (node, dgn_theory $ labDG dgraph node) empty

g = Map.fromList [(node,node)]

unfoldedGraphAux ln libEnv [node] node (gd, g)

unfoldedGraphAux :: LIB_NAME -> LibEnv -> [Node] -> Node ->

(GDiagram, Map.Map Node Node) ->

Result (GDiagram, Map.Map Node Node)

unfoldedGraphAux ln libEnv nodeList node (gd,g) =

case nodeList of

[] -> return (gd,g)

_ -> do

let dgraph = lookupDGraph ln libEnv

-- defInEdges is list of pairs (n, edges of target g(n))

defInEdges = map (\n -> (n,filter (\e@(s,t,_) -> s /= t &&

liftE (liftOr isGlobalDef isHidingDef) e) $

innDG dgraph $ g Map.! n)) nodeList

-- TO DO: no local links, and why edges with s=t are removed

-- add normal form nodes

-- sources of each edge must be added as new nodes

nodeIds = zip (newNodes (length $ concat $ map snd defInEdges) gd)

$ concatMap (\(n,l) -> map (\x -> (n,x)) l ) defInEdges

newLNodes = zip (map fst nodeIds) $

map (\ (s,_,_) -> dgn_theory $ labDG dgraph s) $

concat $ map snd defInEdges

g0 = Map.fromList $

map (\ (newS, (_newT, (s,_t, _))) -> (newS,s)) nodeIds

morphEdge (n1,(n2, (_, _, el))) =

if isHidingDef $ dgl_type el

then (n2,n1,(x, dgl_morphism el))

else (n1,n2,(x, dgl_morphism el))

where EdgeId x = dgl_id el

newLEdges = map morphEdge nodeIds

gd' = insEdges newLEdges $ insNodes newLNodes gd

g' = Map.union g g0

unfoldedGraphAux ln libEnv (map fst nodeIds) node (gd', g')

{- | creates the normal forms of the predecessors of the given node

-}

createNfsForPredecessors :: LIB_NAME -> LibEnv -> Node -> Result LibEnv

createNfsForPredecessors ln proofstatus node =

foldM (convertToNf ln) proofstatus predecessors

where

dgraph = lookupDGraph ln proofstatus

defInEdges = filter ( \e@(s,_,_) ->

liftE (liftOr isGlobalDef isHidingDef) e

&& node /= s) $ innDG dgraph node

predecessors = map (\ (src,_,_) -> src) defInEdges

{- | returns True, if the given node has at least one directly or

indirectly (ie via an ingoing path of GlobalDef edges)

ingoing HidingDef edge. returns False otherwise

-}

hasIngoingHidingDef :: LibEnv -> LIB_NAME -> Node -> Bool

hasIngoingHidingDef libEnv ln node =

let dgraph = lookupDGraph ln libEnv

nodelab = labDG dgraph node

ingoingEdges = innDG dgraph node

hidingDefEdges = filter (liftE isHidingDef ) ingoingEdges

globalDefEdges = filter (liftE isGlobalDef) ingoingEdges

next = map (\ (s, _, _) -> s) globalDefEdges

isNormalFormNode = case dgn_nf nodelab of

Just n -> node == n

_ -> False

in

if isNormalFormNode then False

else

if isDGRef nodelab then

-- if the referenced node has incoming hiding links

-- then the reference is also treated as with hiding

let DGRef refLib refNode = nodeInfo nodelab

in hasIngoingHidingDef libEnv refLib refNode

else

not (null hidingDefEdges)

|| or (map (hasIngoingHidingDef libEnv ln) next)

------------------------------------------------

-- Theorem hide shift and auxiliaries

-----------------------------------------------

theoremHideShift :: LIB_NAME -> LibEnv -> Result LibEnv

theoremHideShift ln proofStatus =

theoremHideShiftAux ln proofStatus $ nodesDG $ lookupDGraph ln proofStatus

theoremHideShiftAux :: LIB_NAME -> LibEnv -> [Node] -> Result LibEnv

theoremHideShiftAux ln proofStatus nodeList = do

auxProofstatus <- foldM (convertToNf ln) proofStatus $

nodesDG $ lookupDGraph ln proofStatus

let

auxGraph = lookupDGraph ln auxProofstatus

nodesWHiding = filter (hasIngoingHidingDef proofStatus ln) nodeList

-- 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 = concat $

map (getInComingGlobalUnprovenEdges auxGraph) nodesWHiding

newGraph = foldl theoremHideShiftForEdge auxGraph ingoingEdges

return $ Map.insert ln

(groupHistory auxGraph thmHideShift newGraph)

auxProofstatus

theoremHideShiftForEdge :: DGraph -> LEdge DGLinkLab -> DGraph

theoremHideShiftForEdge dg edge@(source, target, edgeLab) =

case maybeResult $ theoremHideShiftForEdgeAux dg edge of

Nothing -> error "theoremHideShiftForEdgeAux"

Just (dg', pbasis) -> let

GlobalThm _ conservativity conservStatus = dgl_type edgeLab

provenEdge = (source, target, edgeLab

{ dgl_type = GlobalThm (Proven thmHideShift pbasis)

conservativity conservStatus

, dgl_origin = DGLinkProof })

in changesDGH dg' [DeleteEdge edge, InsertEdge provenEdge]

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, DGLink{

dgl_morphism = cmor,

dgl_type = GlobalThm LeftOpen None LeftOpen,

dgl_origin = DGLinkProof,

dgl_id = defaultEdgeId

})

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 :: LIB_NAME -> [LNode DGNodeLab] -> LibEnv

-> Result LibEnv

theoremHideShiftFromList ln ls proofStatus =

theoremHideShiftAux ln proofStatus $ map fst ls

----------------------------------------------------

{- compute the theory of a node, using normal forms when available -}

computeTheory :: Bool -> LibEnv -> LIB_NAME -> Node ->

Result (LibEnv, G_theory)

computeTheory useNf libEnv ln n =

let dg = lookupDGraph ln libEnv

nodelab = labDG dg n

isDefLink = liftOr isGlobalDef $ liftOr isLocalDef

$ liftOr isFreeEdge isCofreeEdge

inEdges = filter (liftE isDefLink) $ innDG dg n

localTh = dgn_theory nodelab

in

if isDGRef nodelab then do

let refLn = dgn_libname nodelab

refNode = dgn_node nodelab

(libEnv', refTh) <- computeTheory useNf libEnv refLn refNode

-- local sentences have to be mapped along dgn_sigma if refNode has hiding

localTh' <- if useNf && hasIngoingHidingDef libEnv' refLn refNode then

let dg' = lookupDGraph refLn libEnv'

newLab = labDG dg' refNode

in case dgn_sigma newLab of

Nothing -> return localTh

-- normal form computation failed

Just phi -> translateG_theory phi localTh

else return localTh

joinTh <- joinG_sentences (theoremsToAxioms refTh) localTh'

return (libEnv', joinTh)

else

if useNf && hasIngoingHidingDef libEnv ln n then do

let libEnvRes = convertToNf ln libEnv n

case maybeResult libEnvRes of

Nothing -> computeTheory False libEnv ln n

-- if it fails or colimits are not implemented,

-- use old version

Just libEnv' -> do

let dg' = lookupDGraph ln libEnv'

nodelab' = labDG dg' n

Just nfN = dgn_nf nodelab'

computeTheory False libEnv' ln nfN

-- set flag to False, so compute without checking hiding

-- for normal form node

else do

ths <- mapM (computePathTheory libEnv ln) $ sortBy

(\ (_, _, l1) (_, _, l2) -> compare (dgl_id l2) $ dgl_id l1) inEdges

ths' <- flatG_sentences localTh ths

return (libEnv, ths')

computePathTheory :: LibEnv -> LIB_NAME -> LEdge DGLinkLab -> Result G_theory

computePathTheory libEnv ln e@(src, _, link) = do

th <- if liftE isLocalDef e then computeLocalTheory libEnv ln src

else do

(_, th') <- computeTheory False libEnv ln src

-- because this function is called only when flag is False

return th'

-- translate theory and turn all imported theorems into axioms

translateG_theory (dgl_morphism link) $ theoremsToAxioms th

theoremsToAxioms :: G_theory -> G_theory

theoremsToAxioms (G_theory lid sign ind1 sens ind2) =

G_theory lid sign ind1 (markAsAxiom True sens) ind2