| Copyright | (c) Till Mossakowski and Uni Bremen 2003-2006 |
|---|---|
| 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 CASL (heterogeneous) structured specifications Follows the verfication semantic rules in Chap. IV:4.7 of the CASL Reference Manual.
- anaSpec :: Bool -> LogicGraph -> LibName -> DGraph -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC -> Range -> Result (SPEC, NodeSig, DGraph)
- anaSpecTop :: Conservativity -> Bool -> LogicGraph -> LibName -> DGraph -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC -> Range -> Result (SPEC, NodeSig, DGraph)
- anaUnion :: Bool -> LogicGraph -> 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
Documentation
anaSpec :: Bool -> LogicGraph -> LibName -> DGraph -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC -> Range -> Result (SPEC, NodeSig, DGraph)
analyze a SPEC. The Bool Parameter determines if incoming symbols shall be ignored. The options are needed to check: shall only the structure be analysed?
anaSpecTop :: Conservativity -> Bool -> LogicGraph -> LibName -> DGraph -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC -> Range -> Result (SPEC, NodeSig, DGraph)
anaUnion :: Bool -> LogicGraph -> 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
insLink :: DGraph -> GMorphism -> DGLinkType -> DGLinkOrigin -> Node -> Node -> DGraph
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
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