Copyright	(c) T.Mossakowski C.Maeder Uni Bremen 2004-2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	hausmann@informatik.uni-bremen.de
Stability	provisional
Portability	portable
Safe Haskell	Safe

CoCASL.AS_CoCASL

Description

Abstract syntax for CoCASL, the coalgebraic extension of CASL Only the added syntax is specified

Documentation

type C_BASIC_SPEC = BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA Source #

type AnModFORM = Annoted (FORMULA C_FORMULA) Source #

data C_BASIC_ITEM Source #

Constructors

CoFree_datatype [Annoted CODATATYPE_DECL] Range
CoSort_gen [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)] Range

Instances

Instances details

Data C_BASIC_ITEM Source #
Instance details Defined in CoCASL.AS_CoCASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> C_BASIC_ITEM -> c C_BASIC_ITEM gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c C_BASIC_ITEM toConstr :: C_BASIC_ITEM -> Constr dataTypeOf :: C_BASIC_ITEM -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c C_BASIC_ITEM) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c C_BASIC_ITEM) gmapT :: (forall b. Data b => b -> b) -> C_BASIC_ITEM -> C_BASIC_ITEM gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> C_BASIC_ITEM -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> C_BASIC_ITEM -> r gmapQ :: (forall d. Data d => d -> u) -> C_BASIC_ITEM -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> C_BASIC_ITEM -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> C_BASIC_ITEM -> m C_BASIC_ITEM gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> C_BASIC_ITEM -> m C_BASIC_ITEM gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> C_BASIC_ITEM -> m C_BASIC_ITEM
Show C_BASIC_ITEM Source #
Instance details Defined in CoCASL.AS_CoCASL Methods showsPrec :: Int -> C_BASIC_ITEM -> ShowS show :: C_BASIC_ITEM -> String showList :: [C_BASIC_ITEM] -> ShowS
Generic C_BASIC_ITEM
Instance details Defined in CoCASL.ATC_CoCASL Associated Types type Rep C_BASIC_ITEM :: Type -> Type Methods from :: C_BASIC_ITEM -> Rep C_BASIC_ITEM x to :: Rep C_BASIC_ITEM x -> C_BASIC_ITEM
GetRange C_BASIC_ITEM Source #
Instance details Defined in CoCASL.AS_CoCASL Methods getRange :: C_BASIC_ITEM -> Range Source # rangeSpan :: C_BASIC_ITEM -> [Pos] Source #
FromJSON C_BASIC_ITEM
Instance details Defined in CoCASL.ATC_CoCASL Methods parseJSON :: Value -> Parser C_BASIC_ITEM parseJSONList :: Value -> Parser [C_BASIC_ITEM]
ToJSON C_BASIC_ITEM
Instance details Defined in CoCASL.ATC_CoCASL Methods toJSON :: C_BASIC_ITEM -> Value toEncoding :: C_BASIC_ITEM -> Encoding toJSONList :: [C_BASIC_ITEM] -> Value toEncodingList :: [C_BASIC_ITEM] -> Encoding
ShATermConvertible C_BASIC_ITEM
Instance details Defined in CoCASL.ATC_CoCASL Methods toShATermAux :: ATermTable -> C_BASIC_ITEM -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [C_BASIC_ITEM] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, C_BASIC_ITEM) fromShATermList' :: Int -> ATermTable -> (ATermTable, [C_BASIC_ITEM])
Pretty C_BASIC_ITEM Source #
Instance details Defined in CoCASL.Print_AS Methods pretty :: C_BASIC_ITEM -> Doc Source # pretties :: [C_BASIC_ITEM] -> Doc Source #
AParsable C_BASIC_ITEM Source #
Instance details Defined in CoCASL.Parse_AS Methods aparser :: AParser st C_BASIC_ITEM Source #
MinSL Bool C_BASIC_ITEM Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods minSL :: C_BASIC_ITEM -> CASL_SL Bool Source #
ProjBasic Bool C_BASIC_ITEM C_SIG_ITEM C_FORMULA Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods projBasicItems :: CASL_SL Bool -> C_BASIC_ITEM -> (Maybe (BASIC_ITEMS C_BASIC_ITEM C_SIG_ITEM C_FORMULA), [SORT]) Source #
Syntax CoCASL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods parsersAndPrinters :: CoCASL -> Map String (PrefixMap -> AParser st C_BASIC_SPEC, C_BASIC_SPEC -> Doc) Source # parse_basic_spec :: CoCASL -> Maybe (PrefixMap -> AParser st C_BASIC_SPEC) Source # parseSingleSymbItem :: CoCASL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: CoCASL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: CoCASL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: CoCASL -> C_BASIC_SPEC -> Item Source # symb_items_name :: CoCASL -> SYMB_ITEMS -> [String] Source #
StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods basic_analysis :: CoCASL -> Maybe ((C_BASIC_SPEC, CSign, GlobalAnnos) -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named CoCASLFORMULA])) Source # sen_analysis :: CoCASL -> Maybe ((C_BASIC_SPEC, CSign, CoCASLFORMULA) -> Result CoCASLFORMULA) Source # extBasicAnalysis :: CoCASL -> IRI -> LibName -> C_BASIC_SPEC -> CSign -> GlobalAnnos -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named CoCASLFORMULA]) Source # stat_symb_map_items :: CoCASL -> CSign -> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: CoCASL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: CoCASL -> Maybe ((CSign, [Named CoCASLFORMULA]) -> C_BASIC_SPEC) Source # ensures_amalgamability :: CoCASL -> ([CASLAmalgOpt], Gr CSign (Int, CoCASLMor), [(Int, CoCASLMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CoCASL -> CoCASLMor -> [Named CoCASLFORMULA] -> Result (CSign, [Named CoCASLFORMULA]) Source # signature_colimit :: CoCASL -> Gr CSign (Int, CoCASLMor) -> Result (CSign, Map Int CoCASLMor) Source # qualify :: CoCASL -> SIMPLE_ID -> LibName -> CoCASLMor -> CSign -> Result (CoCASLMor, [Named CoCASLFORMULA]) Source # symbol_to_raw :: CoCASL -> Symbol -> RawSymbol Source # id_to_raw :: CoCASL -> Id -> RawSymbol Source # matches :: CoCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: CoCASL -> CSign Source # add_symb_to_sign :: CoCASL -> CSign -> Symbol -> Result CSign Source # signature_union :: CoCASL -> CSign -> CSign -> Result CSign Source # signatureDiff :: CoCASL -> CSign -> CSign -> Result CSign Source # intersection :: CoCASL -> CSign -> CSign -> Result CSign Source # final_union :: CoCASL -> CSign -> CSign -> Result CSign Source # morphism_union :: CoCASL -> CoCASLMor -> CoCASLMor -> Result CoCASLMor Source # is_subsig :: CoCASL -> CSign -> CSign -> Bool Source # subsig_inclusion :: CoCASL -> CSign -> CSign -> Result CoCASLMor Source # generated_sign :: CoCASL -> Set Symbol -> CSign -> Result CoCASLMor Source # cogenerated_sign :: CoCASL -> Set Symbol -> CSign -> Result CoCASLMor Source # induced_from_morphism :: CoCASL -> EndoMap RawSymbol -> CSign -> Result CoCASLMor Source # induced_from_to_morphism :: CoCASL -> EndoMap RawSymbol -> ExtSign CSign Symbol -> ExtSign CSign Symbol -> Result CoCASLMor Source # is_transportable :: CoCASL -> CoCASLMor -> Bool Source # is_injective :: CoCASL -> CoCASLMor -> Bool Source # theory_to_taxonomy :: CoCASL -> TaxoGraphKind -> MMiSSOntology -> CSign -> [Named CoCASLFORMULA] -> Result MMiSSOntology Source # corresp2th :: CoCASL -> String -> Bool -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CSign, [Named CoCASLFORMULA], CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: CoCASL -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CSign, CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: CoCASL -> [IRI] -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source #
Logic CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods parse_basic_sen :: CoCASL -> Maybe (C_BASIC_SPEC -> AParser st CoCASLFORMULA) Source # stability :: CoCASL -> Stability Source # data_logic :: CoCASL -> Maybe AnyLogic Source # top_sublogic :: CoCASL -> CoCASL_Sublogics Source # all_sublogics :: CoCASL -> [CoCASL_Sublogics] Source # bottomSublogic :: CoCASL -> Maybe CoCASL_Sublogics Source # sublogicDimensions :: CoCASL -> [[CoCASL_Sublogics]] Source # parseSublogic :: CoCASL -> String -> Maybe CoCASL_Sublogics Source # proj_sublogic_epsilon :: CoCASL -> CoCASL_Sublogics -> CSign -> CoCASLMor Source # provers :: CoCASL -> [Prover CSign CoCASLFORMULA CoCASLMor CoCASL_Sublogics ()] Source # default_prover :: CoCASL -> String Source # cons_checkers :: CoCASL -> [ConsChecker CSign CoCASLFORMULA CoCASL_Sublogics CoCASLMor ()] Source # conservativityCheck :: CoCASL -> [ConservativityChecker CSign CoCASLFORMULA CoCASLMor] Source # empty_proof_tree :: CoCASL -> () Source # syntaxTable :: CoCASL -> CSign -> Maybe SyntaxTable Source # omdoc_metatheory :: CoCASL -> Maybe OMCD Source # export_symToOmdoc :: CoCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: CoCASL -> NameMap Symbol -> CoCASLFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: CoCASL -> SigMap Symbol -> CSign -> [Named CoCASLFORMULA] -> Result [TCElement] Source # omdocToSym :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CoCASLFORMULA)) Source # addOMadtToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [[OmdADT]] -> Result (CSign, [Named CoCASLFORMULA]) Source # addOmdocToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [TCElement] -> Result (CSign, [Named CoCASLFORMULA]) Source # sublogicOfTheo :: CoCASL -> (CSign, [CoCASLFORMULA]) -> CoCASL_Sublogics Source #
Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CoCFOL2IsabelleHOL Methods sourceLogic :: CoCFOL2IsabelleHOL -> CoCASL Source # sourceSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCFOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CoCFOL2IsabelleHOL -> Isabelle Source # mapSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics -> Maybe () Source # map_theory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CoCFOL2IsabelleHOL -> CoCASLMor -> Result IsabelleMorphism Source # map_sentence :: CoCFOL2IsabelleHOL -> CSign -> CoCASLFORMULA -> Result Sentence Source # map_symbol :: CoCFOL2IsabelleHOL -> CSign -> Symbol -> Set () Source # extractModel :: CoCFOL2IsabelleHOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCFOL2IsabelleHOL -> Bool Source # has_model_expansion :: CoCFOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CoCFOL2IsabelleHOL -> Bool Source # constituents :: CoCFOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: CoCFOL2IsabelleHOL -> Bool Source # rps :: CoCFOL2IsabelleHOL -> Bool Source # eps :: CoCFOL2IsabelleHOL -> Bool Source # isGTC :: CoCFOL2IsabelleHOL -> Bool Source #
Comorphism CoCASL2CoSubCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CoCASL2CoSubCFOL Methods sourceLogic :: CoCASL2CoSubCFOL -> CoCASL Source # sourceSublogic :: CoCASL2CoSubCFOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCASL2CoSubCFOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCASL2CoSubCFOL -> Maybe (LibName, String) Source # targetLogic :: CoCASL2CoSubCFOL -> CoCASL Source # mapSublogic :: CoCASL2CoSubCFOL -> CoCASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CoCASL2CoSubCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CoCASL2CoSubCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CoCASL2CoSubCFOL -> CoCASLMor -> Result CoCASLMor Source # map_sentence :: CoCASL2CoSubCFOL -> CSign -> CoCASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CoCASL2CoSubCFOL -> CSign -> Symbol -> Set Symbol Source # extractModel :: CoCASL2CoSubCFOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCASL2CoSubCFOL -> Bool Source # has_model_expansion :: CoCASL2CoSubCFOL -> Bool Source # is_weakly_amalgamable :: CoCASL2CoSubCFOL -> Bool Source # constituents :: CoCASL2CoSubCFOL -> [String] Source # isInclusionComorphism :: CoCASL2CoSubCFOL -> Bool Source # rps :: CoCASL2CoSubCFOL -> Bool Source # eps :: CoCASL2CoSubCFOL -> Bool Source # isGTC :: CoCASL2CoSubCFOL -> Bool Source #
Comorphism CoCASL2CoPCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CoCASL2CoPCFOL Methods sourceLogic :: CoCASL2CoPCFOL -> CoCASL Source # sourceSublogic :: CoCASL2CoPCFOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCASL2CoPCFOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCASL2CoPCFOL -> Maybe (LibName, String) Source # targetLogic :: CoCASL2CoPCFOL -> CoCASL Source # mapSublogic :: CoCASL2CoPCFOL -> CoCASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CoCASL2CoPCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CoCASL2CoPCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CoCASL2CoPCFOL -> CoCASLMor -> Result CoCASLMor Source # map_sentence :: CoCASL2CoPCFOL -> CSign -> CoCASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CoCASL2CoPCFOL -> CSign -> Symbol -> Set Symbol Source # extractModel :: CoCASL2CoPCFOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCASL2CoPCFOL -> Bool Source # has_model_expansion :: CoCASL2CoPCFOL -> Bool Source # is_weakly_amalgamable :: CoCASL2CoPCFOL -> Bool Source # constituents :: CoCASL2CoPCFOL -> [String] Source # isInclusionComorphism :: CoCASL2CoPCFOL -> Bool Source # rps :: CoCASL2CoPCFOL -> Bool Source # eps :: CoCASL2CoPCFOL -> Bool Source # isGTC :: CoCASL2CoPCFOL -> Bool Source #
Comorphism CASL2CoCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2CoCASL Methods sourceLogic :: CASL2CoCASL -> CASL Source # sourceSublogic :: CASL2CoCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2CoCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2CoCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2CoCASL -> CoCASL Source # mapSublogic :: CASL2CoCASL -> CASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CASL2CoCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CASL2CoCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CASL2CoCASL -> CASLMor -> Result CoCASLMor Source # map_sentence :: CASL2CoCASL -> CASLSign -> CASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CASL2CoCASL -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2CoCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2CoCASL -> Bool Source # has_model_expansion :: CASL2CoCASL -> Bool Source # is_weakly_amalgamable :: CASL2CoCASL -> Bool Source # constituents :: CASL2CoCASL -> [String] Source # isInclusionComorphism :: CASL2CoCASL -> Bool Source # rps :: CASL2CoCASL -> Bool Source # eps :: CASL2CoCASL -> Bool Source # isGTC :: CASL2CoCASL -> Bool Source #
type Rep C_BASIC_ITEM
Instance details Defined in CoCASL.ATC_CoCASL type Rep C_BASIC_ITEM = D1 ('MetaData "C_BASIC_ITEM" "CoCASL.AS_CoCASL" "main" 'False) (C1 ('MetaCons "CoFree_datatype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted CODATATYPE_DECL]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "CoSort_gen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

data C_SIG_ITEM Source #

Constructors

CoDatatype_items [Annoted CODATATYPE_DECL] Range

Instances

Instances details

Data C_SIG_ITEM Source #
Instance details Defined in CoCASL.AS_CoCASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> C_SIG_ITEM -> c C_SIG_ITEM gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c C_SIG_ITEM toConstr :: C_SIG_ITEM -> Constr dataTypeOf :: C_SIG_ITEM -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c C_SIG_ITEM) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c C_SIG_ITEM) gmapT :: (forall b. Data b => b -> b) -> C_SIG_ITEM -> C_SIG_ITEM gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> C_SIG_ITEM -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> C_SIG_ITEM -> r gmapQ :: (forall d. Data d => d -> u) -> C_SIG_ITEM -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> C_SIG_ITEM -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> C_SIG_ITEM -> m C_SIG_ITEM gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> C_SIG_ITEM -> m C_SIG_ITEM gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> C_SIG_ITEM -> m C_SIG_ITEM
Show C_SIG_ITEM Source #
Instance details Defined in CoCASL.AS_CoCASL Methods showsPrec :: Int -> C_SIG_ITEM -> ShowS show :: C_SIG_ITEM -> String showList :: [C_SIG_ITEM] -> ShowS
Generic C_SIG_ITEM
Instance details Defined in CoCASL.ATC_CoCASL Associated Types type Rep C_SIG_ITEM :: Type -> Type Methods from :: C_SIG_ITEM -> Rep C_SIG_ITEM x to :: Rep C_SIG_ITEM x -> C_SIG_ITEM
GetRange C_SIG_ITEM Source #
Instance details Defined in CoCASL.AS_CoCASL Methods getRange :: C_SIG_ITEM -> Range Source # rangeSpan :: C_SIG_ITEM -> [Pos] Source #
FromJSON C_SIG_ITEM
Instance details Defined in CoCASL.ATC_CoCASL Methods parseJSON :: Value -> Parser C_SIG_ITEM parseJSONList :: Value -> Parser [C_SIG_ITEM]
ToJSON C_SIG_ITEM
Instance details Defined in CoCASL.ATC_CoCASL Methods toJSON :: C_SIG_ITEM -> Value toEncoding :: C_SIG_ITEM -> Encoding toJSONList :: [C_SIG_ITEM] -> Value toEncodingList :: [C_SIG_ITEM] -> Encoding
ShATermConvertible C_SIG_ITEM
Instance details Defined in CoCASL.ATC_CoCASL Methods toShATermAux :: ATermTable -> C_SIG_ITEM -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [C_SIG_ITEM] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, C_SIG_ITEM) fromShATermList' :: Int -> ATermTable -> (ATermTable, [C_SIG_ITEM])
Pretty C_SIG_ITEM Source #
Instance details Defined in CoCASL.Print_AS Methods pretty :: C_SIG_ITEM -> Doc Source # pretties :: [C_SIG_ITEM] -> Doc Source #
AParsable C_SIG_ITEM Source #
Instance details Defined in CoCASL.Parse_AS Methods aparser :: AParser st C_SIG_ITEM Source #
MinSL Bool C_SIG_ITEM Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods minSL :: C_SIG_ITEM -> CASL_SL Bool Source #
ProjSigItem Bool C_SIG_ITEM C_FORMULA Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods projSigItems :: CASL_SL Bool -> C_SIG_ITEM -> (Maybe (SIG_ITEMS C_SIG_ITEM C_FORMULA), [SORT]) Source #
ProjBasic Bool C_BASIC_ITEM C_SIG_ITEM C_FORMULA Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods projBasicItems :: CASL_SL Bool -> C_BASIC_ITEM -> (Maybe (BASIC_ITEMS C_BASIC_ITEM C_SIG_ITEM C_FORMULA), [SORT]) Source #
Syntax CoCASL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods parsersAndPrinters :: CoCASL -> Map String (PrefixMap -> AParser st C_BASIC_SPEC, C_BASIC_SPEC -> Doc) Source # parse_basic_spec :: CoCASL -> Maybe (PrefixMap -> AParser st C_BASIC_SPEC) Source # parseSingleSymbItem :: CoCASL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: CoCASL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: CoCASL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: CoCASL -> C_BASIC_SPEC -> Item Source # symb_items_name :: CoCASL -> SYMB_ITEMS -> [String] Source #
StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods basic_analysis :: CoCASL -> Maybe ((C_BASIC_SPEC, CSign, GlobalAnnos) -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named CoCASLFORMULA])) Source # sen_analysis :: CoCASL -> Maybe ((C_BASIC_SPEC, CSign, CoCASLFORMULA) -> Result CoCASLFORMULA) Source # extBasicAnalysis :: CoCASL -> IRI -> LibName -> C_BASIC_SPEC -> CSign -> GlobalAnnos -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named CoCASLFORMULA]) Source # stat_symb_map_items :: CoCASL -> CSign -> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: CoCASL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: CoCASL -> Maybe ((CSign, [Named CoCASLFORMULA]) -> C_BASIC_SPEC) Source # ensures_amalgamability :: CoCASL -> ([CASLAmalgOpt], Gr CSign (Int, CoCASLMor), [(Int, CoCASLMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CoCASL -> CoCASLMor -> [Named CoCASLFORMULA] -> Result (CSign, [Named CoCASLFORMULA]) Source # signature_colimit :: CoCASL -> Gr CSign (Int, CoCASLMor) -> Result (CSign, Map Int CoCASLMor) Source # qualify :: CoCASL -> SIMPLE_ID -> LibName -> CoCASLMor -> CSign -> Result (CoCASLMor, [Named CoCASLFORMULA]) Source # symbol_to_raw :: CoCASL -> Symbol -> RawSymbol Source # id_to_raw :: CoCASL -> Id -> RawSymbol Source # matches :: CoCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: CoCASL -> CSign Source # add_symb_to_sign :: CoCASL -> CSign -> Symbol -> Result CSign Source # signature_union :: CoCASL -> CSign -> CSign -> Result CSign Source # signatureDiff :: CoCASL -> CSign -> CSign -> Result CSign Source # intersection :: CoCASL -> CSign -> CSign -> Result CSign Source # final_union :: CoCASL -> CSign -> CSign -> Result CSign Source # morphism_union :: CoCASL -> CoCASLMor -> CoCASLMor -> Result CoCASLMor Source # is_subsig :: CoCASL -> CSign -> CSign -> Bool Source # subsig_inclusion :: CoCASL -> CSign -> CSign -> Result CoCASLMor Source # generated_sign :: CoCASL -> Set Symbol -> CSign -> Result CoCASLMor Source # cogenerated_sign :: CoCASL -> Set Symbol -> CSign -> Result CoCASLMor Source # induced_from_morphism :: CoCASL -> EndoMap RawSymbol -> CSign -> Result CoCASLMor Source # induced_from_to_morphism :: CoCASL -> EndoMap RawSymbol -> ExtSign CSign Symbol -> ExtSign CSign Symbol -> Result CoCASLMor Source # is_transportable :: CoCASL -> CoCASLMor -> Bool Source # is_injective :: CoCASL -> CoCASLMor -> Bool Source # theory_to_taxonomy :: CoCASL -> TaxoGraphKind -> MMiSSOntology -> CSign -> [Named CoCASLFORMULA] -> Result MMiSSOntology Source # corresp2th :: CoCASL -> String -> Bool -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CSign, [Named CoCASLFORMULA], CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: CoCASL -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CSign, CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: CoCASL -> [IRI] -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source #
Logic CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods parse_basic_sen :: CoCASL -> Maybe (C_BASIC_SPEC -> AParser st CoCASLFORMULA) Source # stability :: CoCASL -> Stability Source # data_logic :: CoCASL -> Maybe AnyLogic Source # top_sublogic :: CoCASL -> CoCASL_Sublogics Source # all_sublogics :: CoCASL -> [CoCASL_Sublogics] Source # bottomSublogic :: CoCASL -> Maybe CoCASL_Sublogics Source # sublogicDimensions :: CoCASL -> [[CoCASL_Sublogics]] Source # parseSublogic :: CoCASL -> String -> Maybe CoCASL_Sublogics Source # proj_sublogic_epsilon :: CoCASL -> CoCASL_Sublogics -> CSign -> CoCASLMor Source # provers :: CoCASL -> [Prover CSign CoCASLFORMULA CoCASLMor CoCASL_Sublogics ()] Source # default_prover :: CoCASL -> String Source # cons_checkers :: CoCASL -> [ConsChecker CSign CoCASLFORMULA CoCASL_Sublogics CoCASLMor ()] Source # conservativityCheck :: CoCASL -> [ConservativityChecker CSign CoCASLFORMULA CoCASLMor] Source # empty_proof_tree :: CoCASL -> () Source # syntaxTable :: CoCASL -> CSign -> Maybe SyntaxTable Source # omdoc_metatheory :: CoCASL -> Maybe OMCD Source # export_symToOmdoc :: CoCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: CoCASL -> NameMap Symbol -> CoCASLFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: CoCASL -> SigMap Symbol -> CSign -> [Named CoCASLFORMULA] -> Result [TCElement] Source # omdocToSym :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CoCASLFORMULA)) Source # addOMadtToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [[OmdADT]] -> Result (CSign, [Named CoCASLFORMULA]) Source # addOmdocToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [TCElement] -> Result (CSign, [Named CoCASLFORMULA]) Source # sublogicOfTheo :: CoCASL -> (CSign, [CoCASLFORMULA]) -> CoCASL_Sublogics Source #
Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CoCFOL2IsabelleHOL Methods sourceLogic :: CoCFOL2IsabelleHOL -> CoCASL Source # sourceSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCFOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CoCFOL2IsabelleHOL -> Isabelle Source # mapSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics -> Maybe () Source # map_theory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CoCFOL2IsabelleHOL -> CoCASLMor -> Result IsabelleMorphism Source # map_sentence :: CoCFOL2IsabelleHOL -> CSign -> CoCASLFORMULA -> Result Sentence Source # map_symbol :: CoCFOL2IsabelleHOL -> CSign -> Symbol -> Set () Source # extractModel :: CoCFOL2IsabelleHOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCFOL2IsabelleHOL -> Bool Source # has_model_expansion :: CoCFOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CoCFOL2IsabelleHOL -> Bool Source # constituents :: CoCFOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: CoCFOL2IsabelleHOL -> Bool Source # rps :: CoCFOL2IsabelleHOL -> Bool Source # eps :: CoCFOL2IsabelleHOL -> Bool Source # isGTC :: CoCFOL2IsabelleHOL -> Bool Source #
Comorphism CoCASL2CoSubCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CoCASL2CoSubCFOL Methods sourceLogic :: CoCASL2CoSubCFOL -> CoCASL Source # sourceSublogic :: CoCASL2CoSubCFOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCASL2CoSubCFOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCASL2CoSubCFOL -> Maybe (LibName, String) Source # targetLogic :: CoCASL2CoSubCFOL -> CoCASL Source # mapSublogic :: CoCASL2CoSubCFOL -> CoCASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CoCASL2CoSubCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CoCASL2CoSubCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CoCASL2CoSubCFOL -> CoCASLMor -> Result CoCASLMor Source # map_sentence :: CoCASL2CoSubCFOL -> CSign -> CoCASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CoCASL2CoSubCFOL -> CSign -> Symbol -> Set Symbol Source # extractModel :: CoCASL2CoSubCFOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCASL2CoSubCFOL -> Bool Source # has_model_expansion :: CoCASL2CoSubCFOL -> Bool Source # is_weakly_amalgamable :: CoCASL2CoSubCFOL -> Bool Source # constituents :: CoCASL2CoSubCFOL -> [String] Source # isInclusionComorphism :: CoCASL2CoSubCFOL -> Bool Source # rps :: CoCASL2CoSubCFOL -> Bool Source # eps :: CoCASL2CoSubCFOL -> Bool Source # isGTC :: CoCASL2CoSubCFOL -> Bool Source #
Comorphism CoCASL2CoPCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CoCASL2CoPCFOL Methods sourceLogic :: CoCASL2CoPCFOL -> CoCASL Source # sourceSublogic :: CoCASL2CoPCFOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCASL2CoPCFOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCASL2CoPCFOL -> Maybe (LibName, String) Source # targetLogic :: CoCASL2CoPCFOL -> CoCASL Source # mapSublogic :: CoCASL2CoPCFOL -> CoCASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CoCASL2CoPCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CoCASL2CoPCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CoCASL2CoPCFOL -> CoCASLMor -> Result CoCASLMor Source # map_sentence :: CoCASL2CoPCFOL -> CSign -> CoCASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CoCASL2CoPCFOL -> CSign -> Symbol -> Set Symbol Source # extractModel :: CoCASL2CoPCFOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCASL2CoPCFOL -> Bool Source # has_model_expansion :: CoCASL2CoPCFOL -> Bool Source # is_weakly_amalgamable :: CoCASL2CoPCFOL -> Bool Source # constituents :: CoCASL2CoPCFOL -> [String] Source # isInclusionComorphism :: CoCASL2CoPCFOL -> Bool Source # rps :: CoCASL2CoPCFOL -> Bool Source # eps :: CoCASL2CoPCFOL -> Bool Source # isGTC :: CoCASL2CoPCFOL -> Bool Source #
Comorphism CASL2CoCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2CoCASL Methods sourceLogic :: CASL2CoCASL -> CASL Source # sourceSublogic :: CASL2CoCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2CoCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2CoCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2CoCASL -> CoCASL Source # mapSublogic :: CASL2CoCASL -> CASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CASL2CoCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CASL2CoCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CASL2CoCASL -> CASLMor -> Result CoCASLMor Source # map_sentence :: CASL2CoCASL -> CASLSign -> CASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CASL2CoCASL -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2CoCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2CoCASL -> Bool Source # has_model_expansion :: CASL2CoCASL -> Bool Source # is_weakly_amalgamable :: CASL2CoCASL -> Bool Source # constituents :: CASL2CoCASL -> [String] Source # isInclusionComorphism :: CASL2CoCASL -> Bool Source # rps :: CASL2CoCASL -> Bool Source # eps :: CASL2CoCASL -> Bool Source # isGTC :: CASL2CoCASL -> Bool Source #
type Rep C_SIG_ITEM
Instance details Defined in CoCASL.ATC_CoCASL type Rep C_SIG_ITEM = D1 ('MetaData "C_SIG_ITEM" "CoCASL.AS_CoCASL" "main" 'False) (C1 ('MetaCons "CoDatatype_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted CODATATYPE_DECL]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

data CODATATYPE_DECL Source #

Constructors

CoDatatype_decl SORT [Annoted COALTERNATIVE] Range

Instances

Instances details

Data CODATATYPE_DECL Source #
Instance details Defined in CoCASL.AS_CoCASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CODATATYPE_DECL -> c CODATATYPE_DECL gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CODATATYPE_DECL toConstr :: CODATATYPE_DECL -> Constr dataTypeOf :: CODATATYPE_DECL -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CODATATYPE_DECL) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CODATATYPE_DECL) gmapT :: (forall b. Data b => b -> b) -> CODATATYPE_DECL -> CODATATYPE_DECL gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CODATATYPE_DECL -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CODATATYPE_DECL -> r gmapQ :: (forall d. Data d => d -> u) -> CODATATYPE_DECL -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> CODATATYPE_DECL -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> CODATATYPE_DECL -> m CODATATYPE_DECL gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CODATATYPE_DECL -> m CODATATYPE_DECL gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CODATATYPE_DECL -> m CODATATYPE_DECL
Show CODATATYPE_DECL Source #
Instance details Defined in CoCASL.AS_CoCASL Methods showsPrec :: Int -> CODATATYPE_DECL -> ShowS show :: CODATATYPE_DECL -> String showList :: [CODATATYPE_DECL] -> ShowS
Generic CODATATYPE_DECL
Instance details Defined in CoCASL.ATC_CoCASL Associated Types type Rep CODATATYPE_DECL :: Type -> Type Methods from :: CODATATYPE_DECL -> Rep CODATATYPE_DECL x to :: Rep CODATATYPE_DECL x -> CODATATYPE_DECL
GetRange CODATATYPE_DECL Source #
Instance details Defined in CoCASL.AS_CoCASL Methods getRange :: CODATATYPE_DECL -> Range Source # rangeSpan :: CODATATYPE_DECL -> [Pos] Source #
FromJSON CODATATYPE_DECL
Instance details Defined in CoCASL.ATC_CoCASL Methods parseJSON :: Value -> Parser CODATATYPE_DECL parseJSONList :: Value -> Parser [CODATATYPE_DECL]
ToJSON CODATATYPE_DECL
Instance details Defined in CoCASL.ATC_CoCASL Methods toJSON :: CODATATYPE_DECL -> Value toEncoding :: CODATATYPE_DECL -> Encoding toJSONList :: [CODATATYPE_DECL] -> Value toEncodingList :: [CODATATYPE_DECL] -> Encoding
ShATermConvertible CODATATYPE_DECL
Instance details Defined in CoCASL.ATC_CoCASL Methods toShATermAux :: ATermTable -> CODATATYPE_DECL -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [CODATATYPE_DECL] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, CODATATYPE_DECL) fromShATermList' :: Int -> ATermTable -> (ATermTable, [CODATATYPE_DECL])
Pretty CODATATYPE_DECL Source #
Instance details Defined in CoCASL.Print_AS Methods pretty :: CODATATYPE_DECL -> Doc Source # pretties :: [CODATATYPE_DECL] -> Doc Source #
type Rep CODATATYPE_DECL
Instance details Defined in CoCASL.ATC_CoCASL type Rep CODATATYPE_DECL = D1 ('MetaData "CODATATYPE_DECL" "CoCASL.AS_CoCASL" "main" 'False) (C1 ('MetaCons "CoDatatype_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted COALTERNATIVE]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data COALTERNATIVE Source #

Constructors

Co_construct OpKind (Maybe OP_NAME) [COCOMPONENTS] Range
CoSubsorts [SORT] Range

Instances

Instances details

Data COALTERNATIVE Source #
Instance details Defined in CoCASL.AS_CoCASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> COALTERNATIVE -> c COALTERNATIVE gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c COALTERNATIVE toConstr :: COALTERNATIVE -> Constr dataTypeOf :: COALTERNATIVE -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c COALTERNATIVE) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c COALTERNATIVE) gmapT :: (forall b. Data b => b -> b) -> COALTERNATIVE -> COALTERNATIVE gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> COALTERNATIVE -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> COALTERNATIVE -> r gmapQ :: (forall d. Data d => d -> u) -> COALTERNATIVE -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> COALTERNATIVE -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> COALTERNATIVE -> m COALTERNATIVE gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> COALTERNATIVE -> m COALTERNATIVE gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> COALTERNATIVE -> m COALTERNATIVE
Show COALTERNATIVE Source #
Instance details Defined in CoCASL.AS_CoCASL Methods showsPrec :: Int -> COALTERNATIVE -> ShowS show :: COALTERNATIVE -> String showList :: [COALTERNATIVE] -> ShowS
Generic COALTERNATIVE
Instance details Defined in CoCASL.ATC_CoCASL Associated Types type Rep COALTERNATIVE :: Type -> Type Methods from :: COALTERNATIVE -> Rep COALTERNATIVE x to :: Rep COALTERNATIVE x -> COALTERNATIVE
GetRange COALTERNATIVE Source #
Instance details Defined in CoCASL.AS_CoCASL Methods getRange :: COALTERNATIVE -> Range Source # rangeSpan :: COALTERNATIVE -> [Pos] Source #
FromJSON COALTERNATIVE
Instance details Defined in CoCASL.ATC_CoCASL Methods parseJSON :: Value -> Parser COALTERNATIVE parseJSONList :: Value -> Parser [COALTERNATIVE]
ToJSON COALTERNATIVE
Instance details Defined in CoCASL.ATC_CoCASL Methods toJSON :: COALTERNATIVE -> Value toEncoding :: COALTERNATIVE -> Encoding toJSONList :: [COALTERNATIVE] -> Value toEncodingList :: [COALTERNATIVE] -> Encoding
ShATermConvertible COALTERNATIVE
Instance details Defined in CoCASL.ATC_CoCASL Methods toShATermAux :: ATermTable -> COALTERNATIVE -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [COALTERNATIVE] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, COALTERNATIVE) fromShATermList' :: Int -> ATermTable -> (ATermTable, [COALTERNATIVE])
Pretty COALTERNATIVE Source #
Instance details Defined in CoCASL.Print_AS Methods pretty :: COALTERNATIVE -> Doc Source # pretties :: [COALTERNATIVE] -> Doc Source #
type Rep COALTERNATIVE
Instance details Defined in CoCASL.ATC_CoCASL type Rep COALTERNATIVE = D1 ('MetaData "COALTERNATIVE" "CoCASL.AS_CoCASL" "main" 'False) (C1 ('MetaCons "Co_construct" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpKind) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe OP_NAME))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [COCOMPONENTS]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "CoSubsorts" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SORT]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

data COCOMPONENTS Source #

Constructors

CoSelect [OP_NAME] OP_TYPE Range

Instances

Instances details

Data COCOMPONENTS Source #
Instance details Defined in CoCASL.AS_CoCASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> COCOMPONENTS -> c COCOMPONENTS gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c COCOMPONENTS toConstr :: COCOMPONENTS -> Constr dataTypeOf :: COCOMPONENTS -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c COCOMPONENTS) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c COCOMPONENTS) gmapT :: (forall b. Data b => b -> b) -> COCOMPONENTS -> COCOMPONENTS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> COCOMPONENTS -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> COCOMPONENTS -> r gmapQ :: (forall d. Data d => d -> u) -> COCOMPONENTS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> COCOMPONENTS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> COCOMPONENTS -> m COCOMPONENTS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> COCOMPONENTS -> m COCOMPONENTS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> COCOMPONENTS -> m COCOMPONENTS
Show COCOMPONENTS Source #
Instance details Defined in CoCASL.AS_CoCASL Methods showsPrec :: Int -> COCOMPONENTS -> ShowS show :: COCOMPONENTS -> String showList :: [COCOMPONENTS] -> ShowS
Generic COCOMPONENTS
Instance details Defined in CoCASL.ATC_CoCASL Associated Types type Rep COCOMPONENTS :: Type -> Type Methods from :: COCOMPONENTS -> Rep COCOMPONENTS x to :: Rep COCOMPONENTS x -> COCOMPONENTS
GetRange COCOMPONENTS Source #
Instance details Defined in CoCASL.AS_CoCASL Methods getRange :: COCOMPONENTS -> Range Source # rangeSpan :: COCOMPONENTS -> [Pos] Source #
FromJSON COCOMPONENTS
Instance details Defined in CoCASL.ATC_CoCASL Methods parseJSON :: Value -> Parser COCOMPONENTS parseJSONList :: Value -> Parser [COCOMPONENTS]
ToJSON COCOMPONENTS
Instance details Defined in CoCASL.ATC_CoCASL Methods toJSON :: COCOMPONENTS -> Value toEncoding :: COCOMPONENTS -> Encoding toJSONList :: [COCOMPONENTS] -> Value toEncodingList :: [COCOMPONENTS] -> Encoding
ShATermConvertible COCOMPONENTS
Instance details Defined in CoCASL.ATC_CoCASL Methods toShATermAux :: ATermTable -> COCOMPONENTS -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [COCOMPONENTS] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, COCOMPONENTS) fromShATermList' :: Int -> ATermTable -> (ATermTable, [COCOMPONENTS])
Pretty COCOMPONENTS Source #
Instance details Defined in CoCASL.Print_AS Methods pretty :: COCOMPONENTS -> Doc Source # pretties :: [COCOMPONENTS] -> Doc Source #
type Rep COCOMPONENTS
Instance details Defined in CoCASL.ATC_CoCASL type Rep COCOMPONENTS = D1 ('MetaData "COCOMPONENTS" "CoCASL.AS_CoCASL" "main" 'False) (C1 ('MetaCons "CoSelect" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [OP_NAME]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OP_TYPE) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data MODALITY Source #

Constructors

Simple_mod SIMPLE_ID
Term_mod (TERM C_FORMULA)

Instances

Instances details

Eq MODALITY Source #
Instance details Defined in CoCASL.AS_CoCASL Methods (==) :: MODALITY -> MODALITY -> Bool (/=) :: MODALITY -> MODALITY -> Bool
Data MODALITY Source #
Instance details Defined in CoCASL.AS_CoCASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MODALITY -> c MODALITY gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MODALITY toConstr :: MODALITY -> Constr dataTypeOf :: MODALITY -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MODALITY) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MODALITY) gmapT :: (forall b. Data b => b -> b) -> MODALITY -> MODALITY gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MODALITY -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MODALITY -> r gmapQ :: (forall d. Data d => d -> u) -> MODALITY -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> MODALITY -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> MODALITY -> m MODALITY gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MODALITY -> m MODALITY gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MODALITY -> m MODALITY
Ord MODALITY Source #
Instance details Defined in CoCASL.AS_CoCASL Methods compare :: MODALITY -> MODALITY -> Ordering (<) :: MODALITY -> MODALITY -> Bool (<=) :: MODALITY -> MODALITY -> Bool (>) :: MODALITY -> MODALITY -> Bool (>=) :: MODALITY -> MODALITY -> Bool max :: MODALITY -> MODALITY -> MODALITY min :: MODALITY -> MODALITY -> MODALITY
Show MODALITY Source #
Instance details Defined in CoCASL.AS_CoCASL Methods showsPrec :: Int -> MODALITY -> ShowS show :: MODALITY -> String showList :: [MODALITY] -> ShowS
Generic MODALITY
Instance details Defined in CoCASL.ATC_CoCASL Associated Types type Rep MODALITY :: Type -> Type Methods from :: MODALITY -> Rep MODALITY x to :: Rep MODALITY x -> MODALITY
GetRange MODALITY Source #
Instance details Defined in CoCASL.AS_CoCASL Methods getRange :: MODALITY -> Range Source # rangeSpan :: MODALITY -> [Pos] Source #
FromJSON MODALITY
Instance details Defined in CoCASL.ATC_CoCASL Methods parseJSON :: Value -> Parser MODALITY parseJSONList :: Value -> Parser [MODALITY]
ToJSON MODALITY
Instance details Defined in CoCASL.ATC_CoCASL Methods toJSON :: MODALITY -> Value toEncoding :: MODALITY -> Encoding toJSONList :: [MODALITY] -> Value toEncodingList :: [MODALITY] -> Encoding
ShATermConvertible MODALITY
Instance details Defined in CoCASL.ATC_CoCASL Methods toShATermAux :: ATermTable -> MODALITY -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [MODALITY] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, MODALITY) fromShATermList' :: Int -> ATermTable -> (ATermTable, [MODALITY])
Pretty MODALITY Source #
Instance details Defined in CoCASL.Print_AS Methods pretty :: MODALITY -> Doc Source # pretties :: [MODALITY] -> Doc Source #
type Rep MODALITY
Instance details Defined in CoCASL.ATC_CoCASL type Rep MODALITY = D1 ('MetaData "MODALITY" "CoCASL.AS_CoCASL" "main" 'False) (C1 ('MetaCons "Simple_mod" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SIMPLE_ID)) :+: C1 ('MetaCons "Term_mod" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TERM C_FORMULA))))

data C_FORMULA Source #

Constructors

BoxOrDiamond Bool MODALITY (FORMULA C_FORMULA) Range
CoSort_gen_ax [SORT] [OP_SYMB] Bool

Instances

Instances details

Eq C_FORMULA Source #
Instance details Defined in CoCASL.AS_CoCASL Methods (==) :: C_FORMULA -> C_FORMULA -> Bool (/=) :: C_FORMULA -> C_FORMULA -> Bool
Data C_FORMULA Source #
Instance details Defined in CoCASL.AS_CoCASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> C_FORMULA -> c C_FORMULA gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c C_FORMULA toConstr :: C_FORMULA -> Constr dataTypeOf :: C_FORMULA -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c C_FORMULA) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c C_FORMULA) gmapT :: (forall b. Data b => b -> b) -> C_FORMULA -> C_FORMULA gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> C_FORMULA -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> C_FORMULA -> r gmapQ :: (forall d. Data d => d -> u) -> C_FORMULA -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> C_FORMULA -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> C_FORMULA -> m C_FORMULA gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> C_FORMULA -> m C_FORMULA gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> C_FORMULA -> m C_FORMULA
Ord C_FORMULA Source #
Instance details Defined in CoCASL.AS_CoCASL Methods compare :: C_FORMULA -> C_FORMULA -> Ordering (<) :: C_FORMULA -> C_FORMULA -> Bool (<=) :: C_FORMULA -> C_FORMULA -> Bool (>) :: C_FORMULA -> C_FORMULA -> Bool (>=) :: C_FORMULA -> C_FORMULA -> Bool max :: C_FORMULA -> C_FORMULA -> C_FORMULA min :: C_FORMULA -> C_FORMULA -> C_FORMULA
Show C_FORMULA Source #
Instance details Defined in CoCASL.AS_CoCASL Methods showsPrec :: Int -> C_FORMULA -> ShowS show :: C_FORMULA -> String showList :: [C_FORMULA] -> ShowS
Generic C_FORMULA
Instance details Defined in CoCASL.ATC_CoCASL Associated Types type Rep C_FORMULA :: Type -> Type Methods from :: C_FORMULA -> Rep C_FORMULA x to :: Rep C_FORMULA x -> C_FORMULA
GetRange C_FORMULA Source #
Instance details Defined in CoCASL.AS_CoCASL Methods getRange :: C_FORMULA -> Range Source # rangeSpan :: C_FORMULA -> [Pos] Source #
FromJSON C_FORMULA
Instance details Defined in CoCASL.ATC_CoCASL Methods parseJSON :: Value -> Parser C_FORMULA parseJSONList :: Value -> Parser [C_FORMULA]
ToJSON C_FORMULA
Instance details Defined in CoCASL.ATC_CoCASL Methods toJSON :: C_FORMULA -> Value toEncoding :: C_FORMULA -> Encoding toJSONList :: [C_FORMULA] -> Value toEncodingList :: [C_FORMULA] -> Encoding
ShATermConvertible C_FORMULA
Instance details Defined in CoCASL.ATC_CoCASL Methods toShATermAux :: ATermTable -> C_FORMULA -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [C_FORMULA] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, C_FORMULA) fromShATermList' :: Int -> ATermTable -> (ATermTable, [C_FORMULA])
Pretty C_FORMULA Source #
Instance details Defined in CoCASL.Print_AS Methods pretty :: C_FORMULA -> Doc Source # pretties :: [C_FORMULA] -> Doc Source #
FormExtension C_FORMULA Source #
Instance details Defined in CoCASL.Print_AS Methods isQuantifierLike :: C_FORMULA -> Bool Source # prefixExt :: C_FORMULA -> Doc -> Doc Source #
TermExtension C_FORMULA Source #
Instance details Defined in CoCASL.StatAna Methods freeVarsOfExt :: Sign C_FORMULA e -> C_FORMULA -> VarSet Source # optTermSort :: C_FORMULA -> Maybe SORT Source # sortOfTerm :: C_FORMULA -> SORT Source # termToFormula :: TERM C_FORMULA -> Result (FORMULA C_FORMULA) Source #
TermParser C_FORMULA Source #
Instance details Defined in CoCASL.Parse_AS Methods termParser :: Bool -> AParser st C_FORMULA Source #
ProjForm Bool C_FORMULA Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods projForm :: CASL_SL Bool -> C_FORMULA -> Maybe (FORMULA C_FORMULA) Source #
MinSL Bool C_FORMULA Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods minSL :: C_FORMULA -> CASL_SL Bool Source #
ProjSigItem Bool C_SIG_ITEM C_FORMULA Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods projSigItems :: CASL_SL Bool -> C_SIG_ITEM -> (Maybe (SIG_ITEMS C_SIG_ITEM C_FORMULA), [SORT]) Source #
ProjBasic Bool C_BASIC_ITEM C_SIG_ITEM C_FORMULA Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods projBasicItems :: CASL_SL Bool -> C_BASIC_ITEM -> (Maybe (BASIC_ITEMS C_BASIC_ITEM C_SIG_ITEM C_FORMULA), [SORT]) Source #
Sentences CoCASL CoCASLFORMULA CSign CoCASLMor Symbol Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods map_sen :: CoCASL -> CoCASLMor -> CoCASLFORMULA -> Result CoCASLFORMULA Source # simplify_sen :: CoCASL -> CSign -> CoCASLFORMULA -> CoCASLFORMULA Source # negation :: CoCASL -> CoCASLFORMULA -> Maybe CoCASLFORMULA Source # print_sign :: CoCASL -> CSign -> Doc Source # print_named :: CoCASL -> Named CoCASLFORMULA -> Doc Source # sym_of :: CoCASL -> CSign -> [Set Symbol] Source # mostSymsOf :: CoCASL -> CSign -> [Symbol] Source # symmap_of :: CoCASL -> CoCASLMor -> EndoMap Symbol Source # sym_name :: CoCASL -> Symbol -> Id Source # sym_label :: CoCASL -> Symbol -> Maybe String Source # fullSymName :: CoCASL -> Symbol -> String Source # symKind :: CoCASL -> Symbol -> String Source # symsOfSen :: CoCASL -> CSign -> CoCASLFORMULA -> [Symbol] Source # pair_symbols :: CoCASL -> Symbol -> Symbol -> Result Symbol Source #
Syntax CoCASL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods parsersAndPrinters :: CoCASL -> Map String (PrefixMap -> AParser st C_BASIC_SPEC, C_BASIC_SPEC -> Doc) Source # parse_basic_spec :: CoCASL -> Maybe (PrefixMap -> AParser st C_BASIC_SPEC) Source # parseSingleSymbItem :: CoCASL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: CoCASL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: CoCASL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: CoCASL -> C_BASIC_SPEC -> Item Source # symb_items_name :: CoCASL -> SYMB_ITEMS -> [String] Source #
StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods basic_analysis :: CoCASL -> Maybe ((C_BASIC_SPEC, CSign, GlobalAnnos) -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named CoCASLFORMULA])) Source # sen_analysis :: CoCASL -> Maybe ((C_BASIC_SPEC, CSign, CoCASLFORMULA) -> Result CoCASLFORMULA) Source # extBasicAnalysis :: CoCASL -> IRI -> LibName -> C_BASIC_SPEC -> CSign -> GlobalAnnos -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named CoCASLFORMULA]) Source # stat_symb_map_items :: CoCASL -> CSign -> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: CoCASL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: CoCASL -> Maybe ((CSign, [Named CoCASLFORMULA]) -> C_BASIC_SPEC) Source # ensures_amalgamability :: CoCASL -> ([CASLAmalgOpt], Gr CSign (Int, CoCASLMor), [(Int, CoCASLMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CoCASL -> CoCASLMor -> [Named CoCASLFORMULA] -> Result (CSign, [Named CoCASLFORMULA]) Source # signature_colimit :: CoCASL -> Gr CSign (Int, CoCASLMor) -> Result (CSign, Map Int CoCASLMor) Source # qualify :: CoCASL -> SIMPLE_ID -> LibName -> CoCASLMor -> CSign -> Result (CoCASLMor, [Named CoCASLFORMULA]) Source # symbol_to_raw :: CoCASL -> Symbol -> RawSymbol Source # id_to_raw :: CoCASL -> Id -> RawSymbol Source # matches :: CoCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: CoCASL -> CSign Source # add_symb_to_sign :: CoCASL -> CSign -> Symbol -> Result CSign Source # signature_union :: CoCASL -> CSign -> CSign -> Result CSign Source # signatureDiff :: CoCASL -> CSign -> CSign -> Result CSign Source # intersection :: CoCASL -> CSign -> CSign -> Result CSign Source # final_union :: CoCASL -> CSign -> CSign -> Result CSign Source # morphism_union :: CoCASL -> CoCASLMor -> CoCASLMor -> Result CoCASLMor Source # is_subsig :: CoCASL -> CSign -> CSign -> Bool Source # subsig_inclusion :: CoCASL -> CSign -> CSign -> Result CoCASLMor Source # generated_sign :: CoCASL -> Set Symbol -> CSign -> Result CoCASLMor Source # cogenerated_sign :: CoCASL -> Set Symbol -> CSign -> Result CoCASLMor Source # induced_from_morphism :: CoCASL -> EndoMap RawSymbol -> CSign -> Result CoCASLMor Source # induced_from_to_morphism :: CoCASL -> EndoMap RawSymbol -> ExtSign CSign Symbol -> ExtSign CSign Symbol -> Result CoCASLMor Source # is_transportable :: CoCASL -> CoCASLMor -> Bool Source # is_injective :: CoCASL -> CoCASLMor -> Bool Source # theory_to_taxonomy :: CoCASL -> TaxoGraphKind -> MMiSSOntology -> CSign -> [Named CoCASLFORMULA] -> Result MMiSSOntology Source # corresp2th :: CoCASL -> String -> Bool -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CSign, [Named CoCASLFORMULA], CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: CoCASL -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CSign, CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: CoCASL -> [IRI] -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source #
Logic CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods parse_basic_sen :: CoCASL -> Maybe (C_BASIC_SPEC -> AParser st CoCASLFORMULA) Source # stability :: CoCASL -> Stability Source # data_logic :: CoCASL -> Maybe AnyLogic Source # top_sublogic :: CoCASL -> CoCASL_Sublogics Source # all_sublogics :: CoCASL -> [CoCASL_Sublogics] Source # bottomSublogic :: CoCASL -> Maybe CoCASL_Sublogics Source # sublogicDimensions :: CoCASL -> [[CoCASL_Sublogics]] Source # parseSublogic :: CoCASL -> String -> Maybe CoCASL_Sublogics Source # proj_sublogic_epsilon :: CoCASL -> CoCASL_Sublogics -> CSign -> CoCASLMor Source # provers :: CoCASL -> [Prover CSign CoCASLFORMULA CoCASLMor CoCASL_Sublogics ()] Source # default_prover :: CoCASL -> String Source # cons_checkers :: CoCASL -> [ConsChecker CSign CoCASLFORMULA CoCASL_Sublogics CoCASLMor ()] Source # conservativityCheck :: CoCASL -> [ConservativityChecker CSign CoCASLFORMULA CoCASLMor] Source # empty_proof_tree :: CoCASL -> () Source # syntaxTable :: CoCASL -> CSign -> Maybe SyntaxTable Source # omdoc_metatheory :: CoCASL -> Maybe OMCD Source # export_symToOmdoc :: CoCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: CoCASL -> NameMap Symbol -> CoCASLFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: CoCASL -> SigMap Symbol -> CSign -> [Named CoCASLFORMULA] -> Result [TCElement] Source # omdocToSym :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CoCASLFORMULA)) Source # addOMadtToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [[OmdADT]] -> Result (CSign, [Named CoCASLFORMULA]) Source # addOmdocToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [TCElement] -> Result (CSign, [Named CoCASLFORMULA]) Source # sublogicOfTheo :: CoCASL -> (CSign, [CoCASLFORMULA]) -> CoCASL_Sublogics Source #
Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CoCFOL2IsabelleHOL Methods sourceLogic :: CoCFOL2IsabelleHOL -> CoCASL Source # sourceSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCFOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CoCFOL2IsabelleHOL -> Isabelle Source # mapSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics -> Maybe () Source # map_theory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CoCFOL2IsabelleHOL -> CoCASLMor -> Result IsabelleMorphism Source # map_sentence :: CoCFOL2IsabelleHOL -> CSign -> CoCASLFORMULA -> Result Sentence Source # map_symbol :: CoCFOL2IsabelleHOL -> CSign -> Symbol -> Set () Source # extractModel :: CoCFOL2IsabelleHOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCFOL2IsabelleHOL -> Bool Source # has_model_expansion :: CoCFOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CoCFOL2IsabelleHOL -> Bool Source # constituents :: CoCFOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: CoCFOL2IsabelleHOL -> Bool Source # rps :: CoCFOL2IsabelleHOL -> Bool Source # eps :: CoCFOL2IsabelleHOL -> Bool Source # isGTC :: CoCFOL2IsabelleHOL -> Bool Source #
Comorphism CoCASL2CoSubCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CoCASL2CoSubCFOL Methods sourceLogic :: CoCASL2CoSubCFOL -> CoCASL Source # sourceSublogic :: CoCASL2CoSubCFOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCASL2CoSubCFOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCASL2CoSubCFOL -> Maybe (LibName, String) Source # targetLogic :: CoCASL2CoSubCFOL -> CoCASL Source # mapSublogic :: CoCASL2CoSubCFOL -> CoCASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CoCASL2CoSubCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CoCASL2CoSubCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CoCASL2CoSubCFOL -> CoCASLMor -> Result CoCASLMor Source # map_sentence :: CoCASL2CoSubCFOL -> CSign -> CoCASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CoCASL2CoSubCFOL -> CSign -> Symbol -> Set Symbol Source # extractModel :: CoCASL2CoSubCFOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCASL2CoSubCFOL -> Bool Source # has_model_expansion :: CoCASL2CoSubCFOL -> Bool Source # is_weakly_amalgamable :: CoCASL2CoSubCFOL -> Bool Source # constituents :: CoCASL2CoSubCFOL -> [String] Source # isInclusionComorphism :: CoCASL2CoSubCFOL -> Bool Source # rps :: CoCASL2CoSubCFOL -> Bool Source # eps :: CoCASL2CoSubCFOL -> Bool Source # isGTC :: CoCASL2CoSubCFOL -> Bool Source #
Comorphism CoCASL2CoPCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CoCASL2CoPCFOL Methods sourceLogic :: CoCASL2CoPCFOL -> CoCASL Source # sourceSublogic :: CoCASL2CoPCFOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCASL2CoPCFOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCASL2CoPCFOL -> Maybe (LibName, String) Source # targetLogic :: CoCASL2CoPCFOL -> CoCASL Source # mapSublogic :: CoCASL2CoPCFOL -> CoCASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CoCASL2CoPCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CoCASL2CoPCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CoCASL2CoPCFOL -> CoCASLMor -> Result CoCASLMor Source # map_sentence :: CoCASL2CoPCFOL -> CSign -> CoCASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CoCASL2CoPCFOL -> CSign -> Symbol -> Set Symbol Source # extractModel :: CoCASL2CoPCFOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCASL2CoPCFOL -> Bool Source # has_model_expansion :: CoCASL2CoPCFOL -> Bool Source # is_weakly_amalgamable :: CoCASL2CoPCFOL -> Bool Source # constituents :: CoCASL2CoPCFOL -> [String] Source # isInclusionComorphism :: CoCASL2CoPCFOL -> Bool Source # rps :: CoCASL2CoPCFOL -> Bool Source # eps :: CoCASL2CoPCFOL -> Bool Source # isGTC :: CoCASL2CoPCFOL -> Bool Source #
Comorphism CASL2CoCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2CoCASL Methods sourceLogic :: CASL2CoCASL -> CASL Source # sourceSublogic :: CASL2CoCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2CoCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2CoCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2CoCASL -> CoCASL Source # mapSublogic :: CASL2CoCASL -> CASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CASL2CoCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CASL2CoCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CASL2CoCASL -> CASLMor -> Result CoCASLMor Source # map_sentence :: CASL2CoCASL -> CASLSign -> CASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CASL2CoCASL -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2CoCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2CoCASL -> Bool Source # has_model_expansion :: CASL2CoCASL -> Bool Source # is_weakly_amalgamable :: CASL2CoCASL -> Bool Source # constituents :: CASL2CoCASL -> [String] Source # isInclusionComorphism :: CASL2CoCASL -> Bool Source # rps :: CASL2CoCASL -> Bool Source # eps :: CASL2CoCASL -> Bool Source # isGTC :: CASL2CoCASL -> Bool Source #
type Rep C_FORMULA
Instance details Defined in CoCASL.ATC_CoCASL type Rep C_FORMULA = D1 ('MetaData "C_FORMULA" "CoCASL.AS_CoCASL" "main" 'False) (C1 ('MetaCons "BoxOrDiamond" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MODALITY)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FORMULA C_FORMULA)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "CoSort_gen_ax" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SORT]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [OP_SYMB]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))