CoCASL.StatAna

Description

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