Copyright	(c) Till Mossakowski Uni Bremen 2002-2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	till@informatik.uni-bremen.de
Stability	provisional
Portability	non-portable(Logic)
Safe Haskell	None

Static.DevGraph

Contents

types for structured specification analysis
- basic types
methods to check the type of an edge
utility functions
bottom up traversal

Description

Central datastructures for development graphs Follows Sect. IV:4.2 of the CASL Reference Manual.

We also provide functions for constructing and modifying development graphs. However note that these changes need to be propagated to the GUI if they also shall be visible in the displayed development graph.

Synopsis

data NodeSig = NodeSig {
- getNode :: Node
- getSig :: G_sign
}
data MaybeNode
- = JustNode NodeSig
- | EmptyNode AnyLogic
getMaybeNodes :: MaybeNode -> Set Node
newtype Renamed = Renamed RENAMING
data MaybeRestricted
- = NoRestriction
- | Restricted RESTRICTION
data DGOrigin
- = DGEmpty
- | DGBasic
- | DGBasicSpec (Maybe G_basic_spec) G_sign (Set G_symbol)
- | DGExtension
- | DGLogicCoercion
- | DGTranslation Renamed
- | DGUnion
- | DGIntersect
- | DGExtract
- | DGRestriction MaybeRestricted (Set G_symbol)
- | DGRevealTranslation
- | DGFreeOrCofree FreeOrCofree
- | DGLocal
- | DGClosed
- | DGLogicQual
- | DGData
- | DGFormalParams
- | DGVerificationGeneric
- | DGImports
- | DGInst IRI
- | DGFitSpec
- | DGFitView IRI
- | DGProof
- | DGNormalForm Node
- | DGintegratedSCC
- | DGFlattening
- | DGAlignment
- | DGTest
data DGNodeInfo
- = DGNode {
  - node_origin :: DGOrigin
  - node_cons_status :: ConsStatus
  }
- | DGRef {
  - ref_libname :: LibName
  - ref_node :: Node
  }
data DGNodeLab = DGNodeLab {
- dgn_name :: NodeName
- dgn_theory :: G_theory
- globalTheory :: Maybe G_theory
- labelHasHiding :: Bool
- labelHasFree :: Bool
- dgn_nf :: Maybe Node
- dgn_sigma :: Maybe GMorphism
- dgn_freenf :: Maybe Node
- dgn_phi :: Maybe GMorphism
- nodeInfo :: DGNodeInfo
- nodeMod :: NodeMod
- xnode :: Maybe XNode
- dgn_lock :: Maybe (MVar ())
}
isDGRef :: DGNodeLab -> Bool
sensWithKind :: (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool) -> G_theory -> [String]
hasSenKind :: (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool) -> DGNodeLab -> Bool
hasOpenGoals :: DGNodeLab -> Bool
isInternalNode :: DGNodeLab -> Bool
getNodeConsStatus :: DGNodeLab -> ConsStatus
getNodeCons :: DGNodeLab -> Conservativity
getNodeConservativity :: LNode DGNodeLab -> Conservativity
hasOpenNodeConsStatus :: Bool -> DGNodeLab -> Bool
markNodeConsistency :: Conservativity -> String -> DGNodeLab -> DGNodeLab
markNodeConsistent :: String -> DGNodeLab -> DGNodeLab
markNodeInconsistent :: String -> DGNodeLab -> DGNodeLab
getRealDGNodeType :: DGNodeLab -> DGNodeType
newtype Fitted = Fitted [G_mapping]
data DGLinkOrigin
- = SeeTarget
- | SeeSource
- | TEST
- | DGLinkVerif
- | DGImpliesLink
- | DGLinkExtension
- | DGLinkTranslation
- | DGLinkClosedLenv
- | DGLinkImports
- | DGLinkIntersect
- | DGLinkMorph IRI
- | DGLinkInst IRI Fitted
- | DGLinkInstArg IRI
- | DGLinkView IRI Fitted
- | DGLinkAlign IRI
- | DGLinkFitView IRI
- | DGLinkFitViewImp IRI
- | DGLinkProof
- | DGLinkFlatteningUnion
- | DGLinkFlatteningRename
- | DGLinkRefinement IRI
data DGLinkType
- = ScopedLink Scope LinkKind ConsStatus
- | HidingDefLink
- | FreeOrCofreeDefLink FreeOrCofree MaybeNode
- | HidingFreeOrCofreeThm (Maybe FreeOrCofree) Node GMorphism ThmLinkStatus
thmLinkStatus :: DGLinkType -> Maybe ThmLinkStatus
thmProofBasis :: DGLinkType -> ProofBasis
updThmProofBasis :: DGLinkType -> ProofBasis -> DGLinkType
data DGLinkLab = DGLink {
- dgl_morphism :: GMorphism
- dgl_type :: DGLinkType
- dgl_origin :: DGLinkOrigin
- dglPending :: Bool
- dgl_id :: EdgeId
- dglName :: String
}
mkDGLink :: GMorphism -> DGLinkType -> DGLinkOrigin -> String -> EdgeId -> DGLinkLab
nameDGLink :: String -> DGLinkLab -> DGLinkLab
defDGLink :: GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLinkId :: GMorphism -> DGLinkType -> DGLinkOrigin -> EdgeId -> DGLinkLab
globDefLink :: GMorphism -> DGLinkOrigin -> DGLinkLab
getDGLinkType :: DGLinkLab -> String
getHomEdgeType :: Bool -> Bool -> DGLinkType -> DGEdgeTypeModInc
getRealDGLinkType :: DGLinkLab -> DGEdgeType
getProofBasis :: DGLinkLab -> ProofBasis
setProof :: ThmLinkStatus -> DGLinkType -> DGLinkType
isProven :: DGLinkType -> Bool
isGlobalEdge :: DGLinkType -> Bool
isGlobalThm :: DGLinkType -> Bool
isUnprovenGlobalThm :: DGLinkType -> Bool
isLocalThm :: DGLinkType -> Bool
isUnprovenLocalThm :: DGLinkType -> Bool
isUnprovenHidingThm :: DGLinkType -> Bool
isFreeEdge :: DGLinkType -> Bool
isCofreeEdge :: DGLinkType -> Bool
hasOutgoingFreeEdge :: DGraph -> Node -> Bool
data GenSig = GenSig MaybeNode [NodeSig] MaybeNode
getGenSigNodes :: GenSig -> Set Node
data ExtGenSig = ExtGenSig {
- genericity :: GenSig
- extGenBody :: NodeSig
}
getExtGenSigNodes :: ExtGenSig -> Set Node
data ExtViewSig = ExtViewSig NodeSig GMorphism ExtGenSig
getExtViewSigNodes :: ExtViewSig -> Set Node
data UnitSig = UnitSig [NodeSig] NodeSig (Maybe NodeSig)
getUnitSigNodes :: UnitSig -> Set Node
data ImpUnitSigOrSig
- = ImpUnitSig MaybeNode UnitSig
- | Sig NodeSig
type StUnitCtx = Map IRI ImpUnitSigOrSig
emptyStUnitCtx :: StUnitCtx
type RefSigMap = Map IRI RefSig
getSigMapNodes :: RefSigMap -> Set Node
type BStContext = Map IRI RefSig
getBStContextNodes :: BStContext -> Set Node
data RefSig
- = BranchRefSig RTPointer (UnitSig, Maybe BranchSig)
- | ComponentRefSig RTPointer RefSigMap
getRefSigNodes :: RefSig -> Set Node
getPointerFromRef :: RefSig -> RTPointer
setPointerInRef :: RefSig -> RTPointer -> RefSig
setUnitSigInRef :: RefSig -> UnitSig -> RefSig
getUnitSigFromRef :: RefSig -> Result UnitSig
mkRefSigFromUnit :: UnitSig -> RefSig
mkBotSigFromUnit :: UnitSig -> RefSig
data BranchSig
- = UnitSigAsBranchSig UnitSig
- | BranchStaticContext BStContext
getBranchSigNodes :: BranchSig -> Set Node
type RefStUnitCtx = Map IRI RefSig
emptyRefStUnitCtx :: RefStUnitCtx
matchesContext :: RefSigMap -> BStContext -> Bool
equalSigs :: UnitSig -> UnitSig -> Bool
namesMatchCtx :: [IRI] -> BStContext -> RefSigMap -> Bool
modifyCtx :: [IRI] -> RefSigMap -> BStContext -> BStContext
refSigComposition :: RefSig -> RefSig -> Result RefSig
data GlobalEntry
- = SpecEntry ExtGenSig
- | ViewOrStructEntry Bool ExtViewSig
- | ArchOrRefEntry Bool RefSig
- | AlignEntry AlignSig
- | UnitEntry UnitSig
- | NetworkEntry GDiagram
getGlobEntryNodes :: GlobalEntry -> Set Node
data AlignSig
- = AlignMor NodeSig GMorphism NodeSig
- | AlignSpan NodeSig GMorphism NodeSig GMorphism NodeSig
- | WAlign NodeSig GMorphism GMorphism NodeSig GMorphism GMorphism NodeSig NodeSig NodeSig
type GlobalEnv = Map IRI GlobalEntry
getGlobNodes :: GlobalEnv -> Set Node
data DGChange
- = InsertNode (LNode DGNodeLab)
- | DeleteNode (LNode DGNodeLab)
- | InsertEdge (LEdge DGLinkLab)
- | DeleteEdge (LEdge DGLinkLab)
- | SetNodeLab DGNodeLab (LNode DGNodeLab)
data HistElem
- = HistElem DGChange
- | HistGroup DGRule ProofHistory
type ProofHistory = SizedList HistElem
data RTNodeType
- = RTPlain UnitSig
- | RTRef Node
data RTNodeLab = RTNodeLab {
- rtn_type :: RTNodeType
- rtn_name :: String
- rtn_diag :: String
}
data RTLinkType
- = RTRefine
- | RTComp
data RTLinkLab = RTLink {
- rtl_type :: RTLinkType
}
addNodeRT :: DGraph -> UnitSig -> String -> (Node, DGraph)
addSpecNodeRT :: DGraph -> UnitSig -> String -> (Node, DGraph)
updateNodeNameRT :: DGraph -> Node -> Bool -> String -> DGraph
updateSigRT :: DGraph -> Node -> UnitSig -> DGraph
updateNodeNameSpecRT :: DGraph -> Node -> String -> DGraph
addSubTree :: DGraph -> Maybe RTLeaves -> RTPointer -> (DGraph, RTPointer)
copySubTree :: DGraph -> Node -> Maybe Node -> (DGraph, Map Node Node)
copySubTreeN :: DGraph -> [Node] -> Map Node Node -> (DGraph, Map Node Node)
copyNode :: Node -> (DGraph, Map Node Node) -> LNode RTLinkLab -> (DGraph, Map Node Node)
addRefEdgeRT :: DGraph -> Node -> Node -> DGraph
addEdgesToNodeRT :: DGraph -> [Node] -> Node -> DGraph
data DiagNodeLab = DiagNode {
- dn_sig :: NodeSig
- dn_desc :: String
}
data DiagLinkLab = DiagLink {
- dl_morphism :: GMorphism
- dl_number :: Int
}
data Diag = Diagram {
- diagGraph :: Gr DiagNodeLab DiagLinkLab
- numberOfEdges :: Int
}
data DGraph = DGraph {
- globalAnnos :: GlobalAnnos
- optLibDefn :: Maybe LIB_DEFN
- globalEnv :: GlobalEnv
- dgBody :: Gr DGNodeLab DGLinkLab
- currentBaseTheory :: Maybe NodeSig
- refTree :: Gr RTNodeLab RTLinkLab
- specRoots :: Map String [Node]
- nameMap :: MapSet String Node
- archSpecDiags :: Map String Diag
- getNewEdgeId :: EdgeId
- allRefNodes :: Map (LibName, Node) Node
- sigMap :: Map SigId G_sign
- thMap :: Map ThId G_theory
- morMap :: Map MorId G_morphism
- proofHistory :: ProofHistory
- redoHistory :: ProofHistory
}
emptyDG :: DGraph
type LibEnv = Map LibName DGraph
emptyLibEnv :: LibEnv
emptyG_sign :: AnyLogic -> G_sign
getMaybeSig :: MaybeNode -> G_sign
getLogic :: MaybeNode -> AnyLogic
getNodeLogic :: NodeSig -> AnyLogic
dgn_origin :: DGNodeLab -> DGOrigin
dgn_libname :: DGNodeLab -> LibName
dgn_node :: DGNodeLab -> Node
dgn_sign :: DGNodeLab -> G_sign
getDGNodeName :: DGNodeLab -> String
globOrLocTh :: DGNodeLab -> G_theory
newConsNodeInfo :: DGOrigin -> Conservativity -> DGNodeInfo
newNodeInfo :: DGOrigin -> DGNodeInfo
newRefInfo :: LibName -> Node -> DGNodeInfo
newInfoNodeLab :: NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newNodeLab :: NodeName -> DGOrigin -> G_theory -> DGNodeLab
treatNodeLock :: (MVar () -> a) -> DGNodeLab -> a
tryLockLocal :: DGNodeLab -> IO Bool
unlockLocal :: DGNodeLab -> IO ()
hasLock :: DGNodeLab -> Bool
eqDGLinkLabContent :: DGLinkLab -> DGLinkLab -> Bool
eqDGLinkLabById :: DGLinkLab -> DGLinkLab -> Bool
cpIndexMaps :: DGraph -> DGraph -> DGraph
setSigMapDG :: Map SigId G_sign -> DGraph -> DGraph
setThMapDG :: Map ThId G_theory -> DGraph -> DGraph
setMorMapDG :: Map MorId G_morphism -> DGraph -> DGraph
lookupSigMapDG :: SigId -> DGraph -> Maybe G_sign
lookupThMapDG :: ThId -> DGraph -> Maybe G_theory
lookupMorMapDG :: MorId -> DGraph -> Maybe G_morphism
sigMapI :: DGraph -> (Map SigId G_sign, SigId)
thMapI :: DGraph -> (Map ThId G_theory, ThId)
morMapI :: DGraph -> (Map MorId G_morphism, MorId)
lookupGlobalEnvDG :: IRI -> DGraph -> Maybe GlobalEntry
lookupInAllRefNodesDG :: DGNodeInfo -> DGraph -> Maybe Node
lookupNodeByName :: String -> DGraph -> [LNode DGNodeLab]
lookupUniqueNodeByName :: String -> DGraph -> Maybe (LNode DGNodeLab)
filterLocalNodesByName :: String -> DGraph -> [LNode DGNodeLab]
filterRefNodesByName :: String -> LibName -> DGraph -> [LNode DGNodeLab]
lookupLocalNodeByNameInEnv :: LibEnv -> String -> Maybe (DGraph, LNode DGNodeLab)
lookupLocalNodeByName :: LibEnv -> DGraph -> String -> Maybe (DGraph, LNode DGNodeLab)
lookupLocalNode :: LibEnv -> DGraph -> Node -> (DGraph, LNode DGNodeLab)
lookupRefNode :: LibEnv -> LibName -> DGraph -> Node -> (LibName, DGraph, LNode DGNodeLab)
lookupRefNodeM :: LibEnv -> Maybe LibName -> DGraph -> Node -> (Maybe LibName, DGraph, LNode DGNodeLab)
getNewNodeDG :: DGraph -> Node
labNodesDG :: DGraph -> [LNode DGNodeLab]
labEdgesDG :: DGraph -> [LEdge DGLinkLab]
isEmptyDG :: DGraph -> Bool
gelemDG :: Node -> DGraph -> Bool
innDG :: DGraph -> Node -> [LEdge DGLinkLab]
outDG :: DGraph -> Node -> [LEdge DGLinkLab]
nodesDG :: DGraph -> [Node]
labDG :: DGraph -> Node -> DGNodeLab
labRT :: DGraph -> Node -> RTNodeLab
getNameOfNode :: Node -> DGraph -> String
newNodesDG :: Int -> DGraph -> [Node]
safeContextDG :: String -> DGraph -> Node -> Context DGNodeLab DGLinkLab
labelNodeDG :: LNode DGNodeLab -> DGraph -> (DGraph, DGNodeLab)
delNodeDG :: Node -> DGraph -> DGraph
delNodesDG :: [Node] -> DGraph -> DGraph
insNodeDG :: LNode DGNodeLab -> DGraph -> DGraph
insLNodeDG :: LNode DGNodeLab -> DGraph -> DGraph
insNodesDG :: [LNode DGNodeLab] -> DGraph -> DGraph
delLEdgeDG :: LEdge DGLinkLab -> DGraph -> DGraph
insInclEdgeDG :: LogicGraph -> DGraph -> NodeSig -> NodeSig -> Result DGraph
insLEdgeDG :: LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
compareLinks :: DGLinkLab -> DGLinkLab -> Ordering
insLEdgeNubDG :: LEdge DGLinkLab -> DGraph -> DGraph
insEdgeAsIs :: LEdge DGLinkLab -> DGraph -> DGraph
insEdgesDG :: [LEdge DGLinkLab] -> DGraph -> DGraph
mkGraphDG :: [LNode DGNodeLab] -> [LEdge DGLinkLab] -> DGraph -> DGraph
getDGLinksById :: EdgeId -> DGraph -> [LEdge DGLinkLab]
lookupUniqueLink :: MonadFail m => Node -> EdgeId -> DGraph -> m (LEdge DGLinkLab)
initLocking :: DGraph -> LNode DGNodeLab -> IO (DGraph, DGNodeLab)
lookupDGraph :: LibName -> LibEnv -> DGraph
computeLocalTheory :: Monad m => LibEnv -> LibName -> Node -> m G_theory
computeLocalNodeTheory :: Monad m => LibEnv -> DGraph -> Node -> m G_theory
computeLocalLabelTheory :: Monad m => LibEnv -> DGNodeLab -> m G_theory
liftE :: (DGLinkType -> a) -> LEdge DGLinkLab -> a
isGlobalDef :: DGLinkType -> Bool
isLocalDef :: DGLinkType -> Bool
isHidingDef :: DGLinkType -> Bool
isDefEdge :: DGLinkType -> Bool
isLocalEdge :: DGLinkType -> Bool
isHidingEdge :: DGLinkType -> Bool
hidingThm :: Node -> GMorphism -> DGLinkType
globalThm :: DGLinkType
localThm :: DGLinkType
globalConsThm :: Conservativity -> DGLinkType
localConsThm :: Conservativity -> DGLinkType
localOrGlobalThm :: Scope -> Conservativity -> DGLinkType
localOrGlobalDef :: Scope -> Conservativity -> DGLinkType
globalConsDef :: Conservativity -> DGLinkType
globalDef :: DGLinkType
localDef :: DGLinkType
getLinkConsStatus :: DGLinkType -> ConsStatus
getEdgeConsStatus :: DGLinkLab -> ConsStatus
getCons :: DGLinkType -> Conservativity
getConservativity :: LEdge DGLinkLab -> Conservativity
getConservativityOfPath :: [LEdge DGLinkLab] -> Conservativity
getLibDepRel :: LibEnv -> Rel LibName
getTopsortedLibs :: LibEnv -> [LibName]
dependentLibs :: LibName -> LibEnv -> [LibName]
topsortedNodes :: DGraph -> [LNode DGNodeLab]
changedPendingEdges :: DGraph -> [LEdge DGLinkLab]
changedLocalTheorems :: DGraph -> LNode DGNodeLab -> [LEdge DGLinkLab]
duplicateDefEdges :: DGraph -> [Edge]
ensureUniqueNames :: DGraph -> IRI -> Int -> NodeName

types for structured specification analysis

basic types

data NodeSig Source #

Node with signature in a DG

Constructors

NodeSig
Fields getNode :: Node getSig :: G_sign

Instances

Instances details

Eq NodeSig Source #
Instance details Defined in Static.DevGraph Methods (==) :: NodeSig -> NodeSig -> Bool (/=) :: NodeSig -> NodeSig -> Bool
Show NodeSig Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> NodeSig -> ShowS show :: NodeSig -> String showList :: [NodeSig] -> ShowS
Pretty NodeSig Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: NodeSig -> Doc Source # pretties :: [NodeSig] -> Doc Source #
ShATermLG NodeSig Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> NodeSig -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig) Source #

data MaybeNode Source #

NodeSig or possibly the empty sig in a logic (but since we want to avoid lots of vsacuous nodes with empty sig, we do not assign a real node in the DG here)

Constructors

JustNode NodeSig
EmptyNode AnyLogic

Instances

Instances details

Eq MaybeNode Source #
Instance details Defined in Static.DevGraph Methods (==) :: MaybeNode -> MaybeNode -> Bool (/=) :: MaybeNode -> MaybeNode -> Bool
Show MaybeNode Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> MaybeNode -> ShowS show :: MaybeNode -> String showList :: [MaybeNode] -> ShowS
ShATermLG MaybeNode Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> MaybeNode -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, MaybeNode) Source #

getMaybeNodes :: MaybeNode -> Set Node Source #

newtype Renamed Source #

a wrapper for renamings with a trivial Ord instance

Constructors

Renamed RENAMING

Instances

Instances details

Eq Renamed Source #
Instance details Defined in Static.DevGraph Methods (==) :: Renamed -> Renamed -> Bool (/=) :: Renamed -> Renamed -> Bool
Ord Renamed Source #
Instance details Defined in Static.DevGraph Methods compare :: Renamed -> Renamed -> Ordering (<) :: Renamed -> Renamed -> Bool (<=) :: Renamed -> Renamed -> Bool (>) :: Renamed -> Renamed -> Bool (>=) :: Renamed -> Renamed -> Bool max :: Renamed -> Renamed -> Renamed min :: Renamed -> Renamed -> Renamed
Show Renamed Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> Renamed -> ShowS show :: Renamed -> String showList :: [Renamed] -> ShowS
ShATermLG Renamed Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> Renamed -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, Renamed) Source #

data MaybeRestricted Source #

a wrapper for restrictions with a trivial Ord instance

Constructors

NoRestriction
Restricted RESTRICTION

Instances

Instances details

Eq MaybeRestricted Source #
Instance details Defined in Static.DevGraph Methods (==) :: MaybeRestricted -> MaybeRestricted -> Bool (/=) :: MaybeRestricted -> MaybeRestricted -> Bool
Ord MaybeRestricted Source #
Instance details Defined in Static.DevGraph Methods compare :: MaybeRestricted -> MaybeRestricted -> Ordering (<) :: MaybeRestricted -> MaybeRestricted -> Bool (<=) :: MaybeRestricted -> MaybeRestricted -> Bool (>) :: MaybeRestricted -> MaybeRestricted -> Bool (>=) :: MaybeRestricted -> MaybeRestricted -> Bool max :: MaybeRestricted -> MaybeRestricted -> MaybeRestricted min :: MaybeRestricted -> MaybeRestricted -> MaybeRestricted
Show MaybeRestricted Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> MaybeRestricted -> ShowS show :: MaybeRestricted -> String showList :: [MaybeRestricted] -> ShowS
ShATermLG MaybeRestricted Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> MaybeRestricted -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, MaybeRestricted) Source #

data DGOrigin Source #

Data type indicating the origin of nodes and edges in the input language This is not used in the DG calculus, only may be used in the future for reconstruction of input and management of change.

Instances

Instances details

Eq DGOrigin Source #
Instance details Defined in Static.DevGraph Methods (==) :: DGOrigin -> DGOrigin -> Bool (/=) :: DGOrigin -> DGOrigin -> Bool
Ord DGOrigin Source #
Instance details Defined in Static.DevGraph Methods compare :: DGOrigin -> DGOrigin -> Ordering (<) :: DGOrigin -> DGOrigin -> Bool (<=) :: DGOrigin -> DGOrigin -> Bool (>) :: DGOrigin -> DGOrigin -> Bool (>=) :: DGOrigin -> DGOrigin -> Bool max :: DGOrigin -> DGOrigin -> DGOrigin min :: DGOrigin -> DGOrigin -> DGOrigin
Show DGOrigin Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> DGOrigin -> ShowS show :: DGOrigin -> String showList :: [DGOrigin] -> ShowS
Pretty DGOrigin Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: DGOrigin -> Doc Source # pretties :: [DGOrigin] -> Doc Source #
ShATermLG DGOrigin Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> DGOrigin -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGOrigin) Source #

data DGNodeInfo Source #

node content or reference to another library's node

Constructors

DGNode
Fields node_origin :: DGOrigin node_cons_status :: ConsStatus
DGRef
Fields ref_libname :: LibName ref_node :: Node

Instances

Instances details

Eq DGNodeInfo Source #
Instance details Defined in Static.DevGraph Methods (==) :: DGNodeInfo -> DGNodeInfo -> Bool (/=) :: DGNodeInfo -> DGNodeInfo -> Bool
Show DGNodeInfo Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> DGNodeInfo -> ShowS show :: DGNodeInfo -> String showList :: [DGNodeInfo] -> ShowS
Pretty DGNodeInfo Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: DGNodeInfo -> Doc Source # pretties :: [DGNodeInfo] -> Doc Source #
ShATermLG DGNodeInfo Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> DGNodeInfo -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGNodeInfo) Source #

data DGNodeLab Source #

node inscriptions in development graphs. Nothing entries indicate "not computed yet"

Constructors

DGNodeLab
Fields dgn_name :: NodeName dgn_theory :: G_theory globalTheory :: Maybe G_theory labelHasHiding :: Bool labelHasFree :: Bool dgn_nf :: Maybe Node dgn_sigma :: Maybe GMorphism dgn_freenf :: Maybe Node dgn_phi :: Maybe GMorphism nodeInfo :: DGNodeInfo nodeMod :: NodeMod xnode :: Maybe XNode dgn_lock :: Maybe (MVar ())

Instances

Instances details

Show DGNodeLab Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> DGNodeLab -> ShowS show :: DGNodeLab -> String showList :: [DGNodeLab] -> ShowS
Pretty DGNodeLab Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: DGNodeLab -> Doc Source # pretties :: [DGNodeLab] -> Doc Source #
ShATermLG DGNodeLab Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> DGNodeLab -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGNodeLab) Source #

isDGRef :: DGNodeLab -> Bool Source #

sensWithKind :: (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool) -> G_theory -> [String] Source #

hasSenKind :: (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool) -> DGNodeLab -> Bool Source #

hasOpenGoals :: DGNodeLab -> Bool Source #

test if a given node label has local open goals

isInternalNode :: DGNodeLab -> Bool Source #

check if the node has an internal name

getNodeConsStatus :: DGNodeLab -> ConsStatus Source #

getNodeCons :: DGNodeLab -> Conservativity Source #

getNodeConservativity :: LNode DGNodeLab -> Conservativity Source #

returns the Conservativity if the given node has one, otherwise none

hasOpenNodeConsStatus :: Bool -> DGNodeLab -> Bool Source #

test if a node conservativity is open, return input for refs or nodes with normal forms

markNodeConsistency :: Conservativity -> String -> DGNodeLab -> DGNodeLab Source #

markNodeConsistent :: String -> DGNodeLab -> DGNodeLab Source #

markNodeInconsistent :: String -> DGNodeLab -> DGNodeLab Source #

getRealDGNodeType :: DGNodeLab -> DGNodeType Source #

creates a DGNodeType from a DGNodeLab

newtype Fitted Source #

a wrapper for fitting morphisms with a trivial Eq instance

Constructors

Fitted [G_mapping]

Instances

Instances details

Eq Fitted Source #
Instance details Defined in Static.DevGraph Methods (==) :: Fitted -> Fitted -> Bool (/=) :: Fitted -> Fitted -> Bool
Show Fitted Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> Fitted -> ShowS show :: Fitted -> String showList :: [Fitted] -> ShowS
ShATermLG Fitted Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> Fitted -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, Fitted) Source #

data DGLinkOrigin Source #

Instances

Instances details

Eq DGLinkOrigin Source #
Instance details Defined in Static.DevGraph Methods (==) :: DGLinkOrigin -> DGLinkOrigin -> Bool (/=) :: DGLinkOrigin -> DGLinkOrigin -> Bool
Show DGLinkOrigin Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> DGLinkOrigin -> ShowS show :: DGLinkOrigin -> String showList :: [DGLinkOrigin] -> ShowS
Pretty DGLinkOrigin Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: DGLinkOrigin -> Doc Source # pretties :: [DGLinkOrigin] -> Doc Source #
ShATermLG DGLinkOrigin Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> DGLinkOrigin -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGLinkOrigin) Source #

data DGLinkType Source #

Link types of development graphs, Sect. IV:4.2 of the CASL Reference Manual explains them in depth.

Constructors

ScopedLink Scope LinkKind ConsStatus
HidingDefLink
FreeOrCofreeDefLink FreeOrCofree MaybeNode
HidingFreeOrCofreeThm (Maybe FreeOrCofree) Node GMorphism ThmLinkStatus

Instances

Instances details

Eq DGLinkType Source #
Instance details Defined in Static.DevGraph Methods (==) :: DGLinkType -> DGLinkType -> Bool (/=) :: DGLinkType -> DGLinkType -> Bool
Show DGLinkType Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> DGLinkType -> ShowS show :: DGLinkType -> String showList :: [DGLinkType] -> ShowS
Pretty DGLinkType Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: DGLinkType -> Doc Source # pretties :: [DGLinkType] -> Doc Source #
ShATermLG DGLinkType Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> DGLinkType -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGLinkType) Source #

thmLinkStatus :: DGLinkType -> Maybe ThmLinkStatus Source #

extract theorem link status from link type

thmProofBasis :: DGLinkType -> ProofBasis Source #

extract proof basis from link type

updThmProofBasis :: DGLinkType -> ProofBasis -> DGLinkType Source #

data DGLinkLab Source #

link inscriptions in development graphs

Constructors

DGLink
Fields dgl_morphism :: GMorphism dgl_type :: DGLinkType dgl_origin :: DGLinkOrigin dglPending :: Bool dgl_id :: EdgeId dglName :: String

Instances

Instances details

Eq DGLinkLab Source #
Instance details Defined in Static.DevGraph Methods (==) :: DGLinkLab -> DGLinkLab -> Bool (/=) :: DGLinkLab -> DGLinkLab -> Bool
Show DGLinkLab Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> DGLinkLab -> ShowS show :: DGLinkLab -> String showList :: [DGLinkLab] -> ShowS
Pretty DGLinkLab Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: DGLinkLab -> Doc Source # pretties :: [DGLinkLab] -> Doc Source #
ShATermLG DGLinkLab Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> DGLinkLab -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGLinkLab) Source #
Eq (DaVinciArc EdgeValue)
Instance details Defined in Taxonomy.AbstractGraphView Methods (==) :: DaVinciArc EdgeValue -> DaVinciArc EdgeValue -> Bool (/=) :: DaVinciArc EdgeValue -> DaVinciArc EdgeValue -> Bool
Eq (DaVinciArc EdgeValue)
Instance details Defined in GUI.GraphAbstraction Methods (==) :: DaVinciArc EdgeValue -> DaVinciArc EdgeValue -> Bool (/=) :: DaVinciArc EdgeValue -> DaVinciArc EdgeValue -> Bool

mkDGLink :: GMorphism -> DGLinkType -> DGLinkOrigin -> String -> EdgeId -> DGLinkLab Source #

nameDGLink :: String -> DGLinkLab -> DGLinkLab Source #

name a link

defDGLink :: GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab Source #

defDGLinkId :: GMorphism -> DGLinkType -> DGLinkOrigin -> EdgeId -> DGLinkLab Source #

globDefLink :: GMorphism -> DGLinkOrigin -> DGLinkLab Source #

getDGLinkType :: DGLinkLab -> String Source #

describe the link type of the label

getHomEdgeType :: Bool -> Bool -> DGLinkType -> DGEdgeTypeModInc Source #

getRealDGLinkType :: DGLinkLab -> DGEdgeType Source #

creates a DGEdgeType from a DGLinkLab

getProofBasis :: DGLinkLab -> ProofBasis Source #

return the proof basis of the given linklab

setProof :: ThmLinkStatus -> DGLinkType -> DGLinkType Source #

set proof for theorem links

methods to check the type of an edge

isProven :: DGLinkType -> Bool Source #

isGlobalEdge :: DGLinkType -> Bool Source #

isGlobalThm :: DGLinkType -> Bool Source #

isUnprovenGlobalThm :: DGLinkType -> Bool Source #

isLocalThm :: DGLinkType -> Bool Source #

isUnprovenLocalThm :: DGLinkType -> Bool Source #

isUnprovenHidingThm :: DGLinkType -> Bool Source #

isFreeEdge :: DGLinkType -> Bool Source #

isCofreeEdge :: DGLinkType -> Bool Source #

hasOutgoingFreeEdge :: DGraph -> Node -> Bool Source #

types for global environments

data GenSig Source #

import, formal parameters and united signature of formal params

Constructors

GenSig MaybeNode [NodeSig] MaybeNode

Instances

Instances details

Show GenSig Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> GenSig -> ShowS show :: GenSig -> String showList :: [GenSig] -> ShowS
ShATermLG GenSig Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> GenSig -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, GenSig) Source #

getGenSigNodes :: GenSig -> Set Node Source #

data ExtGenSig Source #

genericity and body

Constructors

ExtGenSig
Fields genericity :: GenSig extGenBody :: NodeSig

Instances

Instances details

Show ExtGenSig Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> ExtGenSig -> ShowS show :: ExtGenSig -> String showList :: [ExtGenSig] -> ShowS
Pretty ExtGenSig Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: ExtGenSig -> Doc Source # pretties :: [ExtGenSig] -> Doc Source #
ShATermLG ExtGenSig Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> ExtGenSig -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, ExtGenSig) Source #

getExtGenSigNodes :: ExtGenSig -> Set Node Source #

data ExtViewSig Source #

source, morphism, parameterized target

Constructors

ExtViewSig NodeSig GMorphism ExtGenSig

Instances

Instances details

Show ExtViewSig Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> ExtViewSig -> ShowS show :: ExtViewSig -> String showList :: [ExtViewSig] -> ShowS
Pretty ExtViewSig Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: ExtViewSig -> Doc Source # pretties :: [ExtViewSig] -> Doc Source #
ShATermLG ExtViewSig Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> ExtViewSig -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, ExtViewSig) Source #

getExtViewSigNodes :: ExtViewSig -> Set Node Source #

types for architectural and unit specification analysis (as defined for basic static semantics in Chap. III:5.1)

data UnitSig Source #

Constructors

UnitSig [NodeSig] NodeSig (Maybe NodeSig)

Instances

Instances details

Eq UnitSig Source #
Instance details Defined in Static.DevGraph Methods (==) :: UnitSig -> UnitSig -> Bool (/=) :: UnitSig -> UnitSig -> Bool
Show UnitSig Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> UnitSig -> ShowS show :: UnitSig -> String showList :: [UnitSig] -> ShowS
Pretty UnitSig Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: UnitSig -> Doc Source # pretties :: [UnitSig] -> Doc Source #
ShATermLG UnitSig Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> UnitSig -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, UnitSig) Source #

getUnitSigNodes :: UnitSig -> Set Node Source #

data ImpUnitSigOrSig Source #

Constructors

ImpUnitSig MaybeNode UnitSig
Sig NodeSig

Instances

Instances details

Eq ImpUnitSigOrSig Source #
Instance details Defined in Static.DevGraph Methods (==) :: ImpUnitSigOrSig -> ImpUnitSigOrSig -> Bool (/=) :: ImpUnitSigOrSig -> ImpUnitSigOrSig -> Bool
Show ImpUnitSigOrSig Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> ImpUnitSigOrSig -> ShowS show :: ImpUnitSigOrSig -> String showList :: [ImpUnitSigOrSig] -> ShowS
Pretty ImpUnitSigOrSig Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: ImpUnitSigOrSig -> Doc Source # pretties :: [ImpUnitSigOrSig] -> Doc Source #
ShATermLG ImpUnitSigOrSig Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> ImpUnitSigOrSig -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, ImpUnitSigOrSig) Source #

type StUnitCtx = Map IRI ImpUnitSigOrSig Source #

emptyStUnitCtx :: StUnitCtx Source #

type RefSigMap = Map IRI RefSig Source #

getSigMapNodes :: RefSigMap -> Set Node Source #

type BStContext = Map IRI RefSig Source #

getBStContextNodes :: BStContext -> Set Node Source #

data RefSig Source #

Constructors

BranchRefSig RTPointer (UnitSig, Maybe BranchSig)
ComponentRefSig RTPointer RefSigMap

Instances

Instances details

Eq RefSig Source #
Instance details Defined in Static.DevGraph Methods (==) :: RefSig -> RefSig -> Bool (/=) :: RefSig -> RefSig -> Bool
Show RefSig Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> RefSig -> ShowS show :: RefSig -> String showList :: [RefSig] -> ShowS
Pretty RefSig Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: RefSig -> Doc Source # pretties :: [RefSig] -> Doc Source #
ShATermLG RefSig Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> RefSig -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, RefSig) Source #

getRefSigNodes :: RefSig -> Set Node Source #

getPointerFromRef :: RefSig -> RTPointer Source #

setPointerInRef :: RefSig -> RTPointer -> RefSig Source #

setUnitSigInRef :: RefSig -> UnitSig -> RefSig Source #

getUnitSigFromRef :: RefSig -> Result UnitSig Source #

mkRefSigFromUnit :: UnitSig -> RefSig Source #

mkBotSigFromUnit :: UnitSig -> RefSig Source #

data BranchSig Source #

Constructors

UnitSigAsBranchSig UnitSig
BranchStaticContext BStContext

Instances

Instances details

Eq BranchSig Source #
Instance details Defined in Static.DevGraph Methods (==) :: BranchSig -> BranchSig -> Bool (/=) :: BranchSig -> BranchSig -> Bool
Show BranchSig Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> BranchSig -> ShowS show :: BranchSig -> String showList :: [BranchSig] -> ShowS
ShATermLG BranchSig Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> BranchSig -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, BranchSig) Source #

getBranchSigNodes :: BranchSig -> Set Node Source #

type RefStUnitCtx = Map IRI RefSig Source #

emptyRefStUnitCtx :: RefStUnitCtx Source #

matchesContext :: RefSigMap -> BStContext -> Bool Source #

equalSigs :: UnitSig -> UnitSig -> Bool Source #

namesMatchCtx :: [IRI] -> BStContext -> RefSigMap -> Bool Source #

modifyCtx :: [IRI] -> RefSigMap -> BStContext -> BStContext Source #

refSigComposition :: RefSig -> RefSig -> Result RefSig Source #

data GlobalEntry Source #

an entry of the global environment

Constructors

SpecEntry ExtGenSig
ViewOrStructEntry Bool ExtViewSig
ArchOrRefEntry Bool RefSig
AlignEntry AlignSig
UnitEntry UnitSig
NetworkEntry GDiagram

Instances

Instances details

Show GlobalEntry Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> GlobalEntry -> ShowS show :: GlobalEntry -> String showList :: [GlobalEntry] -> ShowS
Pretty GlobalEntry Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: GlobalEntry -> Doc Source # pretties :: [GlobalEntry] -> Doc Source #
ShATermLG GlobalEntry Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> GlobalEntry -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, GlobalEntry) Source #

getGlobEntryNodes :: GlobalEntry -> Set Node Source #

data AlignSig Source #

Constructors

AlignMor NodeSig GMorphism NodeSig
AlignSpan NodeSig GMorphism NodeSig GMorphism NodeSig
WAlign NodeSig GMorphism GMorphism NodeSig GMorphism GMorphism NodeSig NodeSig NodeSig

Instances

Instances details

Eq AlignSig Source #
Instance details Defined in Static.DevGraph Methods (==) :: AlignSig -> AlignSig -> Bool (/=) :: AlignSig -> AlignSig -> Bool
Show AlignSig Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> AlignSig -> ShowS show :: AlignSig -> String showList :: [AlignSig] -> ShowS
Pretty AlignSig Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: AlignSig -> Doc Source # pretties :: [AlignSig] -> Doc Source #
ShATermLG AlignSig Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> AlignSig -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, AlignSig) Source #

type GlobalEnv = Map IRI GlobalEntry Source #

getGlobNodes :: GlobalEnv -> Set Node Source #

change and history types

data DGChange Source #

the edit operations of the DGraph

Constructors

InsertNode (LNode DGNodeLab)
DeleteNode (LNode DGNodeLab)
InsertEdge (LEdge DGLinkLab)
DeleteEdge (LEdge DGLinkLab)
SetNodeLab DGNodeLab (LNode DGNodeLab)

Instances

Instances details

Show DGChange Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> DGChange -> ShowS show :: DGChange -> String showList :: [DGChange] -> ShowS
Pretty DGChange Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: DGChange -> Doc Source # pretties :: [DGChange] -> Doc Source #
ShATermLG DGChange Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> DGChange -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGChange) Source #

data HistElem Source #

Constructors

HistElem DGChange
HistGroup DGRule ProofHistory

Instances

Instances details

ShATermLG HistElem Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> HistElem -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, HistElem) Source #

type ProofHistory = SizedList HistElem Source #

data RTNodeType Source #

Constructors

RTPlain UnitSig
RTRef Node

Instances

Instances details

Eq RTNodeType Source #
Instance details Defined in Static.DevGraph Methods (==) :: RTNodeType -> RTNodeType -> Bool (/=) :: RTNodeType -> RTNodeType -> Bool
Show RTNodeType Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> RTNodeType -> ShowS show :: RTNodeType -> String showList :: [RTNodeType] -> ShowS
Pretty RTNodeType Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: RTNodeType -> Doc Source # pretties :: [RTNodeType] -> Doc Source #
ShATermLG RTNodeType Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> RTNodeType -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, RTNodeType) Source #

data RTNodeLab Source #

Constructors

RTNodeLab
Fields rtn_type :: RTNodeType rtn_name :: String rtn_diag :: String

Instances

Instances details

Eq RTNodeLab Source #
Instance details Defined in Static.DevGraph Methods (==) :: RTNodeLab -> RTNodeLab -> Bool (/=) :: RTNodeLab -> RTNodeLab -> Bool
Show RTNodeLab Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> RTNodeLab -> ShowS show :: RTNodeLab -> String showList :: [RTNodeLab] -> ShowS
Pretty RTNodeLab Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: RTNodeLab -> Doc Source # pretties :: [RTNodeLab] -> Doc Source #
ShATermLG RTNodeLab Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> RTNodeLab -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, RTNodeLab) Source #

data RTLinkType Source #

Constructors

RTRefine
RTComp

Instances

Instances details

Eq RTLinkType Source #
Instance details Defined in Static.DevGraph Methods (==) :: RTLinkType -> RTLinkType -> Bool (/=) :: RTLinkType -> RTLinkType -> Bool
Show RTLinkType Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> RTLinkType -> ShowS show :: RTLinkType -> String showList :: [RTLinkType] -> ShowS
ShATermLG RTLinkType Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> RTLinkType -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, RTLinkType) Source #

data RTLinkLab Source #

Constructors

RTLink
Fields rtl_type :: RTLinkType

Instances

Instances details

Eq RTLinkLab Source #
Instance details Defined in Static.DevGraph Methods (==) :: RTLinkLab -> RTLinkLab -> Bool (/=) :: RTLinkLab -> RTLinkLab -> Bool
Show RTLinkLab Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> RTLinkLab -> ShowS show :: RTLinkLab -> String showList :: [RTLinkLab] -> ShowS
ShATermLG RTLinkLab Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> RTLinkLab -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, RTLinkLab) Source #

addNodeRT :: DGraph -> UnitSig -> String -> (Node, DGraph) Source #

addSpecNodeRT :: DGraph -> UnitSig -> String -> (Node, DGraph) Source #

updateNodeNameRT :: DGraph -> Node -> Bool -> String -> DGraph Source #

updateSigRT :: DGraph -> Node -> UnitSig -> DGraph Source #

updateNodeNameSpecRT :: DGraph -> Node -> String -> DGraph Source #

addSubTree :: DGraph -> Maybe RTLeaves -> RTPointer -> (DGraph, RTPointer) Source #

copySubTree :: DGraph -> Node -> Maybe Node -> (DGraph, Map Node Node) Source #

copySubTreeN :: DGraph -> [Node] -> Map Node Node -> (DGraph, Map Node Node) Source #

copyNode :: Node -> (DGraph, Map Node Node) -> LNode RTLinkLab -> (DGraph, Map Node Node) Source #

addRefEdgeRT :: DGraph -> Node -> Node -> DGraph Source #

addEdgesToNodeRT :: DGraph -> [Node] -> Node -> DGraph Source #

data DiagNodeLab Source #

Constructors

DiagNode
Fields dn_sig :: NodeSig dn_desc :: String

Instances

Instances details

Show DiagNodeLab Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> DiagNodeLab -> ShowS show :: DiagNodeLab -> String showList :: [DiagNodeLab] -> ShowS
ShATermLG DiagNodeLab Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> DiagNodeLab -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DiagNodeLab) Source #

data DiagLinkLab Source #

Constructors

DiagLink
Fields dl_morphism :: GMorphism dl_number :: Int

Instances

Instances details

Show DiagLinkLab Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> DiagLinkLab -> ShowS show :: DiagLinkLab -> String showList :: [DiagLinkLab] -> ShowS
ShATermLG DiagLinkLab Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> DiagLinkLab -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DiagLinkLab) Source #

data Diag Source #

Constructors

Diagram
Fields diagGraph :: Gr DiagNodeLab DiagLinkLab numberOfEdges :: Int

Instances

Instances details

Show Diag Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> Diag -> ShowS show :: Diag -> String showList :: [Diag] -> ShowS
Pretty Diag Source #
Instance details Defined in Static.ArchDiagram Methods pretty :: Diag -> Doc Source # pretties :: [Diag] -> Doc Source #
ShATermLG Diag Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> Diag -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, Diag) Source #

data DGraph Source #

the actual development graph with auxiliary information. A G_sign should be stored in sigMap under its gSignSelfIdx. The same applies to G_morphism with morMap and gMorphismSelfIdx resp. G_theory with thMap and gTheorySelfIdx.

Constructors

DGraph

Fields

globalAnnos :: GlobalAnnos
global annos of library
optLibDefn :: Maybe LIB_DEFN
globalEnv :: GlobalEnv
name entities (specs, views) of a library
dgBody :: Gr DGNodeLab DGLinkLab
actual DGraph tree
currentBaseTheory :: Maybe NodeSig
refTree :: Gr RTNodeLab RTLinkLab
the refinement tree
specRoots :: Map String [Node]
root nodes for named specs, several for comp ref
nameMap :: MapSet String Node
all nodes by name
archSpecDiags :: Map String Diag
dependency diagrams between units
getNewEdgeId :: EdgeId
edge counter
allRefNodes :: Map (LibName, Node) Node
all DGRef's
sigMap :: Map SigId G_sign
signature map
thMap :: Map ThId G_theory
theory map
morMap :: Map MorId G_morphism
morphism map
proofHistory :: ProofHistory
applied proof steps
redoHistory :: ProofHistory
undone proofs steps

Instances

Instances details

Show DGraph Source #
Instance details Defined in Static.DevGraph Methods showsPrec :: Int -> DGraph -> ShowS show :: DGraph -> String showList :: [DGraph] -> ShowS
Pretty DGraph Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: DGraph -> Doc Source # pretties :: [DGraph] -> Doc Source #
ShATermLG DGraph Source #
Instance details Defined in ATC.DevGraph Methods toShATermLG :: ATermTable -> DGraph -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGraph) Source #

emptyDG :: DGraph Source #

type LibEnv = Map LibName DGraph Source #

emptyLibEnv :: LibEnv Source #

an empty environment

utility functions

for node signatures

emptyG_sign :: AnyLogic -> G_sign Source #

getMaybeSig :: MaybeNode -> G_sign Source #

getLogic :: MaybeNode -> AnyLogic Source #

getNodeLogic :: NodeSig -> AnyLogic Source #

accessing node label

dgn_origin :: DGNodeLab -> DGOrigin Source #

get the origin of a non-reference node (partial)

dgn_libname :: DGNodeLab -> LibName Source #

get the referenced library (partial)

dgn_node :: DGNodeLab -> Node Source #

get the referenced node (partial)

dgn_sign :: DGNodeLab -> G_sign Source #

get the signature of a node's theory (total)

getDGNodeName :: DGNodeLab -> String Source #

gets the name of a development graph node as a string (total)

globOrLocTh :: DGNodeLab -> G_theory Source #

get the global theory of a node or the local one if missing

creating node content and label

newConsNodeInfo :: DGOrigin -> Conservativity -> DGNodeInfo Source #

create node info

newNodeInfo :: DGOrigin -> DGNodeInfo Source #

create default content

newRefInfo :: LibName -> Node -> DGNodeInfo Source #

create a reference node part

newInfoNodeLab :: NodeName -> DGNodeInfo -> G_theory -> DGNodeLab Source #

create a new node label

newNodeLab :: NodeName -> DGOrigin -> G_theory -> DGNodeLab Source #

create a new node label using newNodeInfo and newInfoNodeLab

handle the lock of a node

treatNodeLock :: (MVar () -> a) -> DGNodeLab -> a Source #

wrapper to access the maybe lock

tryLockLocal :: DGNodeLab -> IO Bool Source #

Tries to acquire the local lock. Return False if already acquired.

unlockLocal :: DGNodeLab -> IO () Source #

Releases the local lock.

hasLock :: DGNodeLab -> Bool Source #

checks if locking MVar is initialized

edge label equalities

eqDGLinkLabContent :: DGLinkLab -> DGLinkLab -> Bool Source #

equality without comparing the edge ids

eqDGLinkLabById :: DGLinkLab -> DGLinkLab -> Bool Source #

equality comparing ids only

setting index maps

cpIndexMaps :: DGraph -> DGraph -> DGraph Source #

setSigMapDG :: Map SigId G_sign -> DGraph -> DGraph Source #

setThMapDG :: Map ThId G_theory -> DGraph -> DGraph Source #

setMorMapDG :: Map MorId G_morphism -> DGraph -> DGraph Source #

looking up in index maps

lookupSigMapDG :: SigId -> DGraph -> Maybe G_sign Source #

lookupThMapDG :: ThId -> DGraph -> Maybe G_theory Source #

lookupMorMapDG :: MorId -> DGraph -> Maybe G_morphism Source #

getting index maps and their maximal index

sigMapI :: DGraph -> (Map SigId G_sign, SigId) Source #

thMapI :: DGraph -> (Map ThId G_theory, ThId) Source #

morMapI :: DGraph -> (Map MorId G_morphism, MorId) Source #

lookup other graph parts

lookupGlobalEnvDG :: IRI -> DGraph -> Maybe GlobalEntry Source #

lookupInAllRefNodesDG :: DGNodeInfo -> DGraph -> Maybe Node Source #

lookup a reference node for a given libname and node

lookup nodes by their names or other properties

lookupNodeByName :: String -> DGraph -> [LNode DGNodeLab] Source #

lookup a node in the graph by its name, using showName to convert nodenames.

lookupUniqueNodeByName :: String -> DGraph -> Maybe (LNode DGNodeLab) Source #

filterLocalNodesByName :: String -> DGraph -> [LNode DGNodeLab] Source #

filters all local nodes in the graph by their names, using showName to convert nodenames. See also lookupNodeByName.

filterRefNodesByName :: String -> LibName -> DGraph -> [LNode DGNodeLab] Source #

filter all ref nodes in the graph by their names, using showName to convert nodenames. See also lookupNodeByName.

lookupLocalNodeByNameInEnv :: LibEnv -> String -> Maybe (DGraph, LNode DGNodeLab) Source #

Given a LibEnv we search each DGraph in it for a (maybe referenced) node with the given name. We return the labeled node and the Graph where this node resides as local node. See also lookupLocalNode.

lookupLocalNodeByName :: LibEnv -> DGraph -> String -> Maybe (DGraph, LNode DGNodeLab) Source #

We search only the given DGraph for a (maybe referenced) node with the given name. We return the labeled node and the Graph where this node resides as local node. See also lookupLocalNode.

lookupLocalNode :: LibEnv -> DGraph -> Node -> (DGraph, LNode DGNodeLab) Source #

Given a Node and a DGraph we follow the node to the graph where it is defined as a local node.

lookupRefNode :: LibEnv -> LibName -> DGraph -> Node -> (LibName, DGraph, LNode DGNodeLab) Source #

Given a Node and a DGraph we follow the node to the graph where it is defined .

lookupRefNodeM :: LibEnv -> Maybe LibName -> DGraph -> Node -> (Maybe LibName, DGraph, LNode DGNodeLab) Source #

accessing the actual graph

getNewNodeDG :: DGraph -> Node Source #

get the next available node id

labNodesDG :: DGraph -> [LNode DGNodeLab] Source #

get all the nodes

labEdgesDG :: DGraph -> [LEdge DGLinkLab] Source #

get all the edges

isEmptyDG :: DGraph -> Bool Source #

checks if a DG is empty or not.

gelemDG :: Node -> DGraph -> Bool Source #

checks if a given node belongs to a given DG

innDG :: DGraph -> Node -> [LEdge DGLinkLab] Source #

get all the incoming ledges of the given node in a given DG

outDG :: DGraph -> Node -> [LEdge DGLinkLab] Source #

get all the outgoing ledges of the given node in a given DG

nodesDG :: DGraph -> [Node] Source #

get all the nodes of the given DG

labDG :: DGraph -> Node -> DGNodeLab Source #

tries to get the label of the given node in a given DG

labRT :: DGraph -> Node -> RTNodeLab Source #

tries to get the label of the given node in a given RT

getNameOfNode :: Node -> DGraph -> String Source #

get the name of a node from the number of node

newNodesDG :: Int -> DGraph -> [Node] Source #

gets the given number of new node-ids in a given DG.

safeContextDG :: String -> DGraph -> Node -> Context DGNodeLab DGLinkLab Source #

get the context and throw input string as error message

manipulate graph

labelNodeDG :: LNode DGNodeLab -> DGraph -> (DGraph, DGNodeLab) Source #

sets the node with new label and returns the new graph and the old label

delNodeDG :: Node -> DGraph -> DGraph Source #

delete the node out of the given DG

delNodesDG :: [Node] -> DGraph -> DGraph Source #

delete a list of nodes out of the given DG

insNodeDG :: LNode DGNodeLab -> DGraph -> DGraph Source #

insert a new node into given DGraph

insLNodeDG :: LNode DGNodeLab -> DGraph -> DGraph Source #

inserts a lnode into a given DG

insNodesDG :: [LNode DGNodeLab] -> DGraph -> DGraph Source #

insert a new node with the given node content into a given DGraph

delLEdgeDG :: LEdge DGLinkLab -> DGraph -> DGraph Source #

delete a labeled edge out of the given DG

insInclEdgeDG :: LogicGraph -> DGraph -> NodeSig -> NodeSig -> Result DGraph Source #

inserts an edge between two nodes, labelled with inclusion

insLEdgeDG :: LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph) Source #

insert a labeled edge into a given DG, return possibly new id of edge

compareLinks :: DGLinkLab -> DGLinkLab -> Ordering Source #

insLEdgeNubDG :: LEdge DGLinkLab -> DGraph -> DGraph Source #

tries to insert a labeled edge into a given DG, but if this edge already exists, then does nothing.

insEdgeAsIs :: LEdge DGLinkLab -> DGraph -> DGraph Source #

inserts a new edge into the DGraph using it's own edgeId. ATTENTION: the caller must ensure that an edgeId is not used twice

insEdgesDG :: [LEdge DGLinkLab] -> DGraph -> DGraph Source #

insert a list of labeled edge into a given DG

mkGraphDG :: [LNode DGNodeLab] -> [LEdge DGLinkLab] -> DGraph -> DGraph Source #

merge a list of lnodes and ledges into a given DG

getDGLinksById :: EdgeId -> DGraph -> [LEdge DGLinkLab] Source #

get links by id (inefficiently)

lookupUniqueLink :: MonadFail m => Node -> EdgeId -> DGraph -> m (LEdge DGLinkLab) Source #

find a unique link given its source node and edgeId

top-level functions

initLocking :: DGraph -> LNode DGNodeLab -> IO (DGraph, DGNodeLab) Source #

initializes the MVar for locking if nessesary

lookupDGraph :: LibName -> LibEnv -> DGraph Source #

returns the DGraph that belongs to the given library name

computeLocalTheory :: Monad m => LibEnv -> LibName -> Node -> m G_theory Source #

compute the theory of a given node. If this node is a DGRef, the referenced node is looked up first.

computeLocalNodeTheory :: Monad m => LibEnv -> DGraph -> Node -> m G_theory Source #

computeLocalLabelTheory :: Monad m => LibEnv -> DGNodeLab -> m G_theory Source #

test link types

liftE :: (DGLinkType -> a) -> LEdge DGLinkLab -> a Source #

isGlobalDef :: DGLinkType -> Bool Source #

isLocalDef :: DGLinkType -> Bool Source #

isHidingDef :: DGLinkType -> Bool Source #

isDefEdge :: DGLinkType -> Bool Source #

isLocalEdge :: DGLinkType -> Bool Source #

isHidingEdge :: DGLinkType -> Bool Source #

create link types

hidingThm :: Node -> GMorphism -> DGLinkType Source #

globalThm :: DGLinkType Source #

localThm :: DGLinkType Source #

globalConsThm :: Conservativity -> DGLinkType Source #

localConsThm :: Conservativity -> DGLinkType Source #

localOrGlobalThm :: Scope -> Conservativity -> DGLinkType Source #

localOrGlobalDef :: Scope -> Conservativity -> DGLinkType Source #

globalConsDef :: Conservativity -> DGLinkType Source #

globalDef :: DGLinkType Source #

localDef :: DGLinkType Source #

link conservativity

getLinkConsStatus :: DGLinkType -> ConsStatus Source #

getEdgeConsStatus :: DGLinkLab -> ConsStatus Source #

getCons :: DGLinkType -> Conservativity Source #

getConservativity :: LEdge DGLinkLab -> Conservativity Source #

returns the Conservativity if the given edge has one, otherwise none

getConservativityOfPath :: [LEdge DGLinkLab] -> Conservativity Source #

returns the conservativity of the given path

bottom up traversal

getLibDepRel :: LibEnv -> Rel LibName Source #

Creates a LibName relation wrt dependencies via reference nodes

getTopsortedLibs :: LibEnv -> [LibName] Source #

dependentLibs :: LibName -> LibEnv -> [LibName] Source #

Get imported libs in topological order, i.e. lib(s) without imports first. The input lib-name will be last

topsortedNodes :: DGraph -> [LNode DGNodeLab] Source #

changedPendingEdges :: DGraph -> [LEdge DGLinkLab] Source #

changedLocalTheorems :: DGraph -> LNode DGNodeLab -> [LEdge DGLinkLab] Source #

duplicateDefEdges :: DGraph -> [Edge] Source #

ensureUniqueNames :: DGraph -> IRI -> Int -> NodeName Source #

DGEmpty
DGBasic
DGBasicSpec (Maybe G_basic_spec) G_sign (Set G_symbol)
DGExtension
DGLogicCoercion
DGTranslation Renamed
DGUnion
DGIntersect
DGExtract
DGRestriction MaybeRestricted (Set G_symbol)
DGRevealTranslation
DGFreeOrCofree FreeOrCofree
DGLocal
DGClosed
DGLogicQual
DGData
DGFormalParams
DGVerificationGeneric
DGImports
DGInst IRI
DGFitSpec
DGFitView IRI
DGProof
DGNormalForm Node
DGintegratedSCC
DGFlattening
DGAlignment
DGTest

SeeTarget
SeeSource
TEST
DGLinkVerif
DGImpliesLink
DGLinkExtension
DGLinkTranslation
DGLinkClosedLenv
DGLinkImports
DGLinkIntersect
DGLinkMorph IRI
DGLinkInst IRI Fitted
DGLinkInstArg IRI
DGLinkView IRI Fitted
DGLinkAlign IRI
DGLinkFitView IRI
DGLinkFitViewImp IRI
DGLinkProof
DGLinkFlatteningUnion
DGLinkFlatteningRename
DGLinkRefinement IRI