{-|

Module : $Header$

Copyright : (c) Till Mossakowski, Uni Bremen 2002-2004

Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

Maintainer : till@tzi.de

Stability : provisional

Portability : non-portable(Logic)

Central data structure for development graphs.

Follows Sect. IV:4.2 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.

T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:

CASL Proof calculus. In: CASL reference manual, part IV.

Available from http://www.cofi.info

todo:

Integrate stuff from Saarbr�cken

Should AS be stored in GloblaContext as well?

-}

module Static.DevGraph where

import Logic.Logic

import Logic.Grothendieck

import Logic.Prover

import Syntax.AS_Library

import Common.GlobalAnnotations

import Data.Graph.Inductive.Graph

import qualified Data.Graph.Inductive.Tree as Tree

import qualified Common.Lib.Map as Map

import qualified Common.Lib.Set as Set

import Common.Id

import Common.PrettyPrint

import Common.PPUtils

import Common.Result

import Common.Lib.Pretty

getNewNode :: Tree.Gr a b -> Node

getNewNode g = case newNodes 1 g of

[n] -> n

_ -> error "Static.DevGraph.getNewNode"

-- * Types for structured specification analysis

-- ??? Some info about the theorems already proved for a node

-- should be added

-- or should it be kept separately?

-- what about open theorems of a node???

type NODE_NAME = (SIMPLE_ID, String, Int)

data DGNodeLab = DGNode {

dgn_name :: NODE_NAME,

dgn_sign :: G_sign,

dgn_sens :: G_l_sentence_list,

dgn_nf :: Maybe Node,

dgn_sigma :: Maybe GMorphism,

dgn_origin :: DGOrigin

}

| DGRef {

dgn_renamed :: NODE_NAME,

dgn_libname :: LIB_NAME,

dgn_node :: Node,

dgn_nf :: Maybe Node,

dgn_sigma :: Maybe GMorphism

} deriving (Show,Eq)

isInternalNode :: DGNodeLab -> Bool

isInternalNode (DGNode n _ _ _ _ _) = isInternal n

isInternalNode _ = False

-- gets the name of a development graph node as a string

getDGNodeName :: DGNodeLab -> String

getDGNodeName (DGNode n _ _ _ _ _) = showName n

getDGNodeName (DGRef n _ _ _ _) = showName n

emptyName :: NODE_NAME

emptyName = (mkSimpleId "","",0)

showInt :: Int -> String

showInt i = if i==0 then "" else show i

showName :: NODE_NAME -> String

showName (n,s,i) = show n ++ if ext=="" then "" else "_"++ext

where ext = s ++ showInt i

makeName :: SIMPLE_ID -> NODE_NAME

makeName n = (n,"",0)

getName :: NODE_NAME -> SIMPLE_ID

getName (n,_,_) = n

makeMaybeName :: Maybe SIMPLE_ID -> NODE_NAME

makeMaybeName Nothing = emptyName

makeMaybeName (Just n) = makeName n

inc :: NODE_NAME -> NODE_NAME

inc (n,s,i) = (n,s,i+1)

isInternal :: NODE_NAME -> Bool

isInternal (_,s,i) = (i/=0) || s/=""

extName :: String -> NODE_NAME -> NODE_NAME

extName s (n,s1,i) = (n,s1++showInt i++s,0)

isDGRef :: DGNodeLab -> Bool

isDGRef (DGNode _ _ _ _ _ _) = False

isDGRef (DGRef _ _ _ _ _) = True

locallyEmpty :: DGNodeLab -> Bool

locallyEmpty (DGNode _ (G_sign lid sigma) (G_l_sentence_list _ sens) _ _ _) =

is_subsig lid sigma (empty_signature lid) && null sens

locallyEmpty (DGRef _ _ _ _ _) = True

data DGLinkLab = DGLink {

-- dgl_name :: String,

-- dgl_src, dgl_tar :: DGNodeLab, -- already in graph structure

dgl_morphism :: GMorphism,

dgl_type :: DGLinkType,

dgl_origin :: DGOrigin }

deriving (Eq,Show)

instance PrettyPrint DGLinkLab where

printText0 ga l = printText0 ga (dgl_morphism l)

<+> ptext (show (dgl_type l))

<+> printText0 ga (dgl_origin l)

data DGRule =

TheoremHideShift

| HideTheoremShift (LEdge DGLinkLab)

| Borrowing

| ConsShift

| DefShift

| MonoShift

| ConsComp

| DefComp

| MonoComp

| DefToMono

| MonoToCons

| FreeIsMono

| MonoIsFree

| Composition

| GlobDecomp (LEdge DGLinkLab) -- edge in the conclusion

| LocDecomp (LEdge DGLinkLab)

| LocSubsumption (LEdge DGLinkLab)

| GlobSubsumption (LEdge DGLinkLab)

| LocalInference

| BasicInference BasicProof

| BasicConsInference Edge BasicConsProof

deriving (Eq, Show)

data BasicProof =

forall lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree .

Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

BasicProof lid (Proof_status proof_tree)

| Guessed

| Conjectured

| Handwritten

instance Eq BasicProof where

Guessed == Guessed = True

Conjectured == Conjectured = True

Handwritten == Handwritten = True

BasicProof lid1 p1 == BasicProof lid2 p2 =

coerce lid1 lid2 p1 == Just p2

_ == _ = False

instance Show BasicProof where

show (BasicProof _ p1) = show p1

show Guessed = "Guessed"

show Conjectured = "Conjectured"

show Handwritten = "Handwritten"

data BasicConsProof = BasicConsProof -- more detail to be added ...

deriving (Eq, Show)

data ThmLinkStatus = Static.DevGraph.Open

| Proven DGRule [DGLinkLab] deriving (Eq, Show)

data DGLinkType = LocalDef

| GlobalDef

| HidingDef

| FreeDef NodeSig -- the "parameter" node

| CofreeDef NodeSig -- the "parameter" node

| LocalThm ThmLinkStatus Conservativity ThmLinkStatus

-- ??? Some more proof information is needed here

-- (proof tree, ...)

| GlobalThm ThmLinkStatus Conservativity ThmLinkStatus

| HidingThm GMorphism ThmLinkStatus

| FreeThm GMorphism Bool

-- DGLink S1 S2 m2 (DGLinkType m1 p) n

-- corresponds to a span of morphisms

-- S1 <--m1-- S --m2--> S2

deriving (Eq,Show)

data Conservativity = None | Cons | Mono | Def

deriving (Eq,Ord)

instance Show Conservativity where

show None = ""

show Cons = "Cons"

show Mono = "Mono"

show Def = "Def"

data DGOrigin = DGBasic | DGExtension | DGTranslation | DGUnion | DGHiding

| DGRevealing | DGRevealTranslation | DGFree | DGCofree

| DGLocal | DGClosed | DGClosedLenv | DGLogicQual | DGLogicQualLenv

| DGData

| DGFormalParams | DGImports | DGSpecInst SIMPLE_ID | DGFitSpec

| DGView SIMPLE_ID | DGFitView SIMPLE_ID | DGFitViewImp SIMPLE_ID

| DGFitViewA SIMPLE_ID | DGFitViewAImp SIMPLE_ID | DGProof

deriving (Eq,Show)

type DGraph = Tree.Gr DGNodeLab DGLinkLab

data NodeSig = NodeSig (Node,G_sign) | EmptyNode AnyLogic

deriving (Eq,Show)

instance PrettyPrint NodeSig where

printText0 ga (EmptyNode _) = ptext "<empty NodeSig>"

printText0 ga (NodeSig(n,sig)) =

ptext "node" <+> printText0 ga n <> ptext ":" <> printText0 ga sig

getNode (NodeSig (n,sigma)) = Just n

getNode (EmptyNode _) = Nothing

emptyG_sign :: AnyLogic -> G_sign

emptyG_sign (Logic lid) = G_sign lid (empty_signature lid)

getSig (NodeSig (n,sigma)) = sigma

getSig (EmptyNode l) = emptyG_sign l

getNodeAndSig (NodeSig (n,sigma)) = Just (n,sigma)

getNodeAndSig (EmptyNode _) = Nothing

getLogic (NodeSig (n,G_sign lid _)) = Logic lid

getLogic (EmptyNode l) = l

-- | Create a node that represents a union of signatures

nodeSigUnion :: LogicGraph -> DGraph -> [NodeSig] -> DGOrigin -> Result (NodeSig, DGraph)

nodeSigUnion lgraph dg nodeSigs orig =

do sigUnion@(G_sign lid _) <- gsigManyUnion lgraph (map getSig nodeSigs)

let nodeContents = DGNode {dgn_name = emptyName,

dgn_sign = sigUnion,

dgn_sens = G_l_sentence_list lid [],

dgn_nf = Nothing,

dgn_sigma = Nothing,

dgn_origin = orig }

node = getNewNode dg

dg' = insNode (node, nodeContents) dg

inslink dgres nsig = do dg <- dgres

case getNode nsig of

Nothing -> return dg

Just n -> do incl <- ginclusion lgraph (getSig nsig) sigUnion

return (insEdge (n, node, DGLink {dgl_morphism = incl,

dgl_type = GlobalDef,

dgl_origin = orig }) dg)

dg'' <- foldl inslink (return dg') nodeSigs

return (NodeSig (node, sigUnion), dg'')

-- | Extend the development graph with given morphism originating

-- from given NodeSig

extendDGraph :: DGraph -- ^ the development graph to be extended

-> NodeSig -- ^ the NodeSig from which the morphism originates

-> GMorphism -- ^ the morphism to be inserted

-> DGOrigin

-> Result (NodeSig, DGraph)

-- ^ returns 1. the target signature of the morphism and 2. the resulting DGraph

extendDGraph _ n@(EmptyNode _) _ _ =

do fail "Internal error: \

\trying to add a morphism originating from an empty node"

extendDGraph dg (NodeSig (n, G_sign lid _)) morph orig =

let targetSig = cod Grothendieck morph

nodeContents = DGNode {dgn_name = emptyName,

dgn_sign = targetSig,

dgn_sens = G_l_sentence_list lid [],

dgn_nf = Nothing,

dgn_sigma = Nothing,

dgn_origin = orig}

linkContents = DGLink {dgl_morphism = morph,

dgl_type = GlobalDef, -- TODO: other type

dgl_origin = orig}

node = getNewNode dg

dg' = insNode (node, nodeContents) dg

dg'' = insEdge (n, node, linkContents) dg'

in do return (NodeSig (node, targetSig), dg'')

-- | Extend the development graph with given morphism pointing to

-- given NodeSig

extendDGraphRev :: DGraph -- ^ the development graph to be extended

-> NodeSig -- ^ the NodeSig to which the morphism points

-> GMorphism -- ^ the morphism to be inserted

-> DGOrigin

-> Result (NodeSig, DGraph)

-- ^ returns 1. the source signature of the morphism and 2. the resulting DGraph

extendDGraphRev _ n@(EmptyNode _) _ _ =

do fail "Internal error: \

\trying to add a morphism pointing to an empty node"

extendDGraphRev dg (NodeSig (n, G_sign lid _)) morph orig =

let sourceSig = dom Grothendieck morph

nodeContents = DGNode {dgn_name = emptyName,

dgn_sign = sourceSig,

dgn_sens = G_l_sentence_list lid [],

dgn_nf = Nothing,

dgn_sigma = Nothing,

dgn_origin = orig}

linkContents = DGLink {dgl_morphism = morph,

dgl_type = GlobalDef, -- TODO: other type

dgl_origin = orig}

node = getNewNode dg

dg' = insNode (node, nodeContents) dg

dg'' = insEdge (node, n, linkContents) dg'

in do return (NodeSig (node, sourceSig), dg'')

data ExtNodeSig = ExtNodeSig (Node,G_ext_sign) | ExtEmptyNode AnyLogic

deriving (Eq,Show)

instance PrettyPrint ExtNodeSig where

printText0 ga (ExtEmptyNode _) = ptext "<empty NodeSig>"

printText0 ga (ExtNodeSig(n,sig)) =

ptext "node" <+> printText0 ga n <> ptext ":" <> printText0 ga sig

getExtNode (NodeSig (n,sigma)) = Just n

getExtNode (EmptyNode _) = Nothing

getExtSig (ExtNodeSig (n,sigma)) = sigma

getExtSig (ExtEmptyNode (Logic lid)) =

G_ext_sign lid (empty_signature lid) Set.empty

getExtNodeAndSig (ExtNodeSig (n,sigma)) = Just (n,sigma)

getExtNodeAndSig (ExtEmptyNode _) = Nothing

getExtLogic (ExtNodeSig (_,G_ext_sign lid _ _)) = Logic lid

getExtLogic (ExtEmptyNode l) = l

-- import, formal parameters, united signature of formal params, body

type ExtGenSig = (NodeSig,[NodeSig],G_sign,NodeSig)

-- source, morphism, parameterized target

type ExtViewSig = (NodeSig,GMorphism,ExtGenSig)

-- * Types for architectural and unit specification analysis

-- (as defined for basic static semantics in Chap. III:5.1)

type ParUnitSig = ([NodeSig], NodeSig)

data UnitSig = Unit_sig NodeSig

| Par_unit_sig ParUnitSig

deriving (Show, Eq)

emptyUnitSig :: AnyLogic -> UnitSig

emptyUnitSig l = Unit_sig (EmptyNode l)

type ImpUnitSig = (NodeSig, UnitSig)

data ImpUnitSigOrSig = Imp_unit_sig ImpUnitSig

| Sig NodeSig

deriving (Show, Eq)

type StUnitCtx = Map.Map SIMPLE_ID ImpUnitSigOrSig

emptyStUnitCtx :: StUnitCtx

emptyStUnitCtx = Map.empty

type ArchSig = (StUnitCtx, UnitSig)

-- * Types for global and library environments

data GlobalEntry = SpecEntry ExtGenSig

| ViewEntry ExtViewSig

| ArchEntry ArchSig

| UnitEntry UnitSig

| RefEntry deriving (Show,Eq)

type GlobalEnv = Map.Map SIMPLE_ID GlobalEntry

type GlobalContext = (GlobalAnnos,GlobalEnv,DGraph)

type LibEnv = Map.Map LIB_NAME GlobalContext

emptyLibEnv :: LibEnv

emptyLibEnv = Map.empty

instance PrettyPrint DGOrigin where

printText0 _ origin = case origin of

DGBasic -> ptext "basic specification"

DGExtension -> ptext "extension"

DGTranslation -> ptext "translation"

DGUnion -> ptext "union"

DGHiding -> ptext "hiding"

DGRevealing -> ptext "revealing"

DGRevealTranslation -> ptext "translation part of a revealing"

DGFree -> ptext "free specification"

DGCofree -> ptext "cofree specification"

DGLocal -> ptext "local specification"

DGClosed -> ptext "closed specification"

DGClosedLenv -> ptext "closed specification (inclusion of local environment)"

DGFormalParams -> ptext "formal parameters of a generic specification"

DGImports -> ptext "imports of a generic specification"

DGSpecInst n -> ptext ("instantiation of "++showPretty n "")

DGFitSpec -> ptext "fittig specification"

DGView n -> ptext ("view "++showPretty n "")

DGFitView n -> ptext ("fitting view "++showPretty n "")

DGFitViewImp n -> ptext ("fitting view (imports) "++showPretty n "")

DGFitViewA n -> ptext ("fitting view (actual parameters) "++showPretty n "")

DGFitViewAImp n -> ptext ("fitting view (imports and actual parameters) "++showPretty n "")

DGProof -> ptext "constructed within a proof"