| Copyright | (c) Till Mossakowski Uni Bremen 2004-2005 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | hausmann@informatik.uni-bremen.de |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
CoCASL.StatAna
Contents
Description
static analysis for CoCASL
Synopsis
- type CSign = Sign C_FORMULA CoCASLSign
- basicCoCASLAnalysis :: (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA, Sign C_FORMULA CoCASLSign, GlobalAnnos) -> Result (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA, ExtSign (Sign C_FORMULA CoCASLSign) Symbol, [Named (FORMULA C_FORMULA)])
- co_sen_analysis :: (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA, CSign, FORMULA C_FORMULA) -> Result (FORMULA C_FORMULA)
- ana_CMix :: Mix C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
- ids_C_BASIC_ITEM :: C_BASIC_ITEM -> IdSets
- ids_C_SIG_ITEM :: C_SIG_ITEM -> IdSets
- ids_CODATATYPE_DECL :: CODATATYPE_DECL -> (Set Id, Set Id)
- ids_COALTERNATIVE :: COALTERNATIVE -> (Set Id, Set Id)
- ids_COCOMPONENTS :: COCOMPONENTS -> Set Id
- data CoRecord a b c d = CoRecord {
- foldBoxOrDiamond :: C_FORMULA -> Bool -> d -> a -> Range -> c
- foldCoSort_gen_ax :: C_FORMULA -> [SORT] -> [OP_SYMB] -> Bool -> c
- foldTerm_mod :: MODALITY -> b -> d
- foldSimple_mod :: MODALITY -> SIMPLE_ID -> d
- foldC_Formula :: Record C_FORMULA a b -> CoRecord a b c d -> C_FORMULA -> c
- foldModality :: Record C_FORMULA a b -> CoRecord a b c d -> MODALITY -> d
- mapCoRecord :: CoRecord (FORMULA C_FORMULA) (TERM C_FORMULA) C_FORMULA MODALITY
- constCoRecord :: ([a] -> a) -> a -> CoRecord a a a a
- mapC_FORMULA :: C_FORMULA -> C_FORMULA
- resolveMODALITY :: MixResolve MODALITY
- resolveC_FORMULA :: MixResolve C_FORMULA
- minExpForm :: Min C_FORMULA CoCASLSign
- ana_C_SIG_ITEM :: Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
- isCoConsAlt :: COALTERNATIVE -> Bool
- getCoSubsorts :: COALTERNATIVE -> [SORT]
- ana_CODATATYPE_DECL :: GenKind -> CODATATYPE_DECL -> State CSign [Component]
- getCoConsType :: SORT -> COALTERNATIVE -> (Maybe Id, OpType, [COCOMPONENTS])
- getCoCompType :: SORT -> COCOMPONENTS -> [(Id, OpType)]
- coselForms :: (Maybe Id, OpType, [COCOMPONENTS]) -> [Named (FORMULA f)]
- coselForms1 :: String -> (Maybe Id, OpType, [COCOMPONENTS]) -> (Maybe (Id, TERM f), [VAR_DECL], [(Maybe Id, OpType)])
- comakeDisjToSort :: (Maybe Id, OpType, [COCOMPONENTS]) -> SORT -> Maybe (Named (FORMULA f))
- comakeInjective :: (Maybe Id, OpType, [COCOMPONENTS]) -> Maybe (Named (FORMULA f))
- comakeDisjoint :: [(Maybe Id, OpType, [COCOMPONENTS])] -> [Named (FORMULA f)]
- comakeDisj :: (Maybe Id, OpType, [COCOMPONENTS]) -> (Maybe Id, OpType, [COCOMPONENTS]) -> Maybe (Named (FORMULA f))
- ana_COALTERNATIVE :: SORT -> Annoted COALTERNATIVE -> State CSign (Maybe (Component, Set Component))
- ana_COCOMPONENTS :: SORT -> COCOMPONENTS -> State CSign ([Component], [Component])
- ana_C_BASIC_ITEM :: Ana C_BASIC_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
- toCoSortGenAx :: Range -> Bool -> GenAx -> State CSign ()
- ana_CoGenerated :: Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign -> Ana ([GenAx], [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]) C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
- getCoGenSig :: SIG_ITEMS C_SIG_ITEM C_FORMULA -> GenAx
- getCoDataGenSig :: [Annoted CODATATYPE_DECL] -> GenAx
Documentation
basicCoCASLAnalysis :: (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA, Sign C_FORMULA CoCASLSign, GlobalAnnos) -> Result (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA, ExtSign (Sign C_FORMULA CoCASLSign) Symbol, [Named (FORMULA C_FORMULA)]) Source #
co_sen_analysis :: (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA, CSign, FORMULA C_FORMULA) -> Result (FORMULA C_FORMULA) Source #
ids_C_SIG_ITEM :: C_SIG_ITEM -> IdSets Source #
ids_CODATATYPE_DECL :: CODATATYPE_DECL -> (Set Id, Set Id) Source #
ids_COALTERNATIVE :: COALTERNATIVE -> (Set Id, Set Id) Source #
ids_COCOMPONENTS :: COCOMPONENTS -> Set Id Source #
data CoRecord a b c d Source #
Constructors
| CoRecord | |
Fields
| |
constCoRecord :: ([a] -> a) -> a -> CoRecord a a a a Source #
mapC_FORMULA :: C_FORMULA -> C_FORMULA Source #
isCoConsAlt :: COALTERNATIVE -> Bool Source #
getCoSubsorts :: COALTERNATIVE -> [SORT] Source #
ana_CODATATYPE_DECL :: GenKind -> CODATATYPE_DECL -> State CSign [Component] Source #
return list of constructors
getCoConsType :: SORT -> COALTERNATIVE -> (Maybe Id, OpType, [COCOMPONENTS]) Source #
getCoCompType :: SORT -> COCOMPONENTS -> [(Id, OpType)] Source #
coselForms :: (Maybe Id, OpType, [COCOMPONENTS]) -> [Named (FORMULA f)] Source #
coselForms1 :: String -> (Maybe Id, OpType, [COCOMPONENTS]) -> (Maybe (Id, TERM f), [VAR_DECL], [(Maybe Id, OpType)]) Source #
comakeDisjToSort :: (Maybe Id, OpType, [COCOMPONENTS]) -> SORT -> Maybe (Named (FORMULA f)) Source #
comakeInjective :: (Maybe Id, OpType, [COCOMPONENTS]) -> Maybe (Named (FORMULA f)) Source #
comakeDisjoint :: [(Maybe Id, OpType, [COCOMPONENTS])] -> [Named (FORMULA f)] Source #
comakeDisj :: (Maybe Id, OpType, [COCOMPONENTS]) -> (Maybe Id, OpType, [COCOMPONENTS]) -> Maybe (Named (FORMULA f)) Source #
ana_COALTERNATIVE :: SORT -> Annoted COALTERNATIVE -> State CSign (Maybe (Component, Set Component)) Source #
return the constructor and the set of total selectors
ana_COCOMPONENTS :: SORT -> COCOMPONENTS -> State CSign ([Component], [Component]) Source #
return total and partial selectors
ana_CoGenerated :: Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign -> Ana ([GenAx], [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]) C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign Source #
getCoDataGenSig :: [Annoted CODATATYPE_DECL] -> GenAx Source #