| Copyright | (c) Till Mossakowski and Uni Magdeburg 2003-2016 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | till@informatik.uni-bremen.de |
| Stability | provisional |
| Portability | non-portable (imports Logic.Grothendieck) |
| Safe Haskell | None |
Static.AnalysisStructured
Description
Static analysis of DOL OMS and networks and CASL (heterogeneous) structured specifications Follows the semantics of DOL OMS and networks, DOL OMG standard, clauses 10.2.2 and 10.2.3
Synopsis
- anaSpec :: Bool -> Bool -> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC -> Range -> Result (SPEC, NodeSig, DGraph)
- anaSpecTop :: Conservativity -> Bool -> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC -> Range -> Result (SPEC, NodeSig, DGraph)
- anaUnion :: Bool -> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> [Annoted SPEC] -> Range -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
- anaIntersect :: Bool -> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> [Annoted SPEC] -> Range -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
- anaSublogic :: HetcatsOpts -> LogicDescr -> LibName -> DGraph -> LibEnv -> LogicGraph -> Result (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
- getSpecAnnos :: Range -> Annoted a -> Result (Conservativity, Bool)
- anaRenaming :: LogicGraph -> MaybeNode -> G_sign -> HetcatsOpts -> RENAMING -> Result GMorphism
- anaRestriction :: LogicGraph -> G_sign -> G_sign -> HetcatsOpts -> RESTRICTION -> Result (GMorphism, Maybe GMorphism)
- partitionGmaps :: [G_mapping] -> ([G_mapping], [G_mapping])
- homogenizeGM :: AnyLogic -> [G_mapping] -> Result G_symb_map_items_list
- anaGmaps :: LogicGraph -> HetcatsOpts -> Range -> G_sign -> G_sign -> [G_mapping] -> Result G_morphism
- insGSig :: DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
- insLink :: DGraph -> GMorphism -> DGLinkType -> DGLinkOrigin -> Node -> Node -> DGraph
- extendMorphism :: Bool -> G_sign -> G_sign -> G_sign -> G_morphism -> Result (G_sign, G_morphism)
- insGTheory :: DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
- expCurie :: GlobalAnnos -> ExpOverrides -> IRI -> Maybe IRI
- expCurieR :: GlobalAnnos -> ExpOverrides -> IRI -> Result IRI
- expandCurieByPath :: FilePath -> IRI -> Maybe IRI
- type ExpOverrides = Map IRI FilePath
- notFoundError :: String -> IRI -> Result a
- prefixErrorIRI :: IRI -> Result a
- networkDiagram :: DGraph -> [LABELED_ONTO_OR_INTPR_REF] -> [IRI] -> ([Node], [(Node, Node, DGLinkLab)])
Documentation
anaSpec :: Bool -> Bool -> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC -> Range -> Result (SPEC, NodeSig, DGraph) Source #
analyze a SPEC. The first Bool Parameter determines if incoming symbols shall be ignored while the second determines if the nodes should be optimized away for specifications without parameters. The options are needed to check: shall only the structure be analysed?
anaSpecTop :: Conservativity -> Bool -> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC -> Range -> Result (SPEC, NodeSig, DGraph) Source #
anaUnion :: Bool -> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> [Annoted SPEC] -> Range -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph) Source #
anaIntersect :: Bool -> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> [Annoted SPEC] -> Range -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph) Source #
anaSublogic :: HetcatsOpts -> LogicDescr -> LibName -> DGraph -> LibEnv -> LogicGraph -> Result (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph) Source #
getSpecAnnos :: Range -> Annoted a -> Result (Conservativity, Bool) Source #
anaRenaming :: LogicGraph -> MaybeNode -> G_sign -> HetcatsOpts -> RENAMING -> Result GMorphism Source #
anaRestriction :: LogicGraph -> G_sign -> G_sign -> HetcatsOpts -> RESTRICTION -> Result (GMorphism, Maybe GMorphism) Source #
homogenizeGM :: AnyLogic -> [G_mapping] -> Result G_symb_map_items_list Source #
anaGmaps :: LogicGraph -> HetcatsOpts -> Range -> G_sign -> G_sign -> [G_mapping] -> Result G_morphism Source #
insLink :: DGraph -> GMorphism -> DGLinkType -> DGLinkOrigin -> Node -> Node -> DGraph Source #
Arguments
| :: Bool | check sharing (False for lambda expressions) |
| -> G_sign | formal parameter |
| -> G_sign | body |
| -> G_sign | actual parameter |
| -> G_morphism | fitting morphism |
| -> Result (G_sign, G_morphism) |
expCurie :: GlobalAnnos -> ExpOverrides -> IRI -> Maybe IRI Source #
expCurieR :: GlobalAnnos -> ExpOverrides -> IRI -> Result IRI Source #
expandCurieByPath :: FilePath -> IRI -> Maybe IRI Source #
type ExpOverrides = Map IRI FilePath Source #
notFoundError :: String -> IRI -> Result a Source #
prefixErrorIRI :: IRI -> Result a Source #
networkDiagram :: DGraph -> [LABELED_ONTO_OR_INTPR_REF] -> [IRI] -> ([Node], [(Node, Node, DGLinkLab)]) Source #
build the diagram of a network specified as a list of network elements to be added | and a list of network elements to be removed