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

COL.AS_COL

Description

Abstract syntax for COL extension of CASL Only the added syntax is specified

Documentation

type COL_BASIC_SPEC = BASIC_SPEC () COL_SIG_ITEM () Source #

data COL_SIG_ITEM Source #

Constructors

Constructor_items [Annoted Id] Range
Observer_items [Annoted (Id, Maybe Int)] Range

Instances

Instances details

Eq COL_SIG_ITEM Source #
Instance details Defined in COL.AS_COL Methods (==) :: COL_SIG_ITEM -> COL_SIG_ITEM -> Bool (/=) :: COL_SIG_ITEM -> COL_SIG_ITEM -> Bool
Data COL_SIG_ITEM Source #
Instance details Defined in COL.AS_COL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> COL_SIG_ITEM -> c COL_SIG_ITEM gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c COL_SIG_ITEM toConstr :: COL_SIG_ITEM -> Constr dataTypeOf :: COL_SIG_ITEM -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c COL_SIG_ITEM) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c COL_SIG_ITEM) gmapT :: (forall b. Data b => b -> b) -> COL_SIG_ITEM -> COL_SIG_ITEM gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> COL_SIG_ITEM -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> COL_SIG_ITEM -> r gmapQ :: (forall d. Data d => d -> u) -> COL_SIG_ITEM -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> COL_SIG_ITEM -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> COL_SIG_ITEM -> m COL_SIG_ITEM gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> COL_SIG_ITEM -> m COL_SIG_ITEM gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> COL_SIG_ITEM -> m COL_SIG_ITEM
Show COL_SIG_ITEM Source #
Instance details Defined in COL.AS_COL Methods showsPrec :: Int -> COL_SIG_ITEM -> ShowS show :: COL_SIG_ITEM -> String showList :: [COL_SIG_ITEM] -> ShowS
Generic COL_SIG_ITEM
Instance details Defined in COL.ATC_COL Associated Types type Rep COL_SIG_ITEM :: Type -> Type Methods from :: COL_SIG_ITEM -> Rep COL_SIG_ITEM x to :: Rep COL_SIG_ITEM x -> COL_SIG_ITEM
GetRange COL_SIG_ITEM Source #
Instance details Defined in COL.AS_COL Methods getRange :: COL_SIG_ITEM -> Range Source # rangeSpan :: COL_SIG_ITEM -> [Pos] Source #
FromJSON COL_SIG_ITEM
Instance details Defined in COL.ATC_COL Methods parseJSON :: Value -> Parser COL_SIG_ITEM parseJSONList :: Value -> Parser [COL_SIG_ITEM]
ToJSON COL_SIG_ITEM
Instance details Defined in COL.ATC_COL Methods toJSON :: COL_SIG_ITEM -> Value toEncoding :: COL_SIG_ITEM -> Encoding toJSONList :: [COL_SIG_ITEM] -> Value toEncodingList :: [COL_SIG_ITEM] -> Encoding
ShATermConvertible COL_SIG_ITEM
Instance details Defined in COL.ATC_COL Methods toShATermAux :: ATermTable -> COL_SIG_ITEM -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [COL_SIG_ITEM] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, COL_SIG_ITEM) fromShATermList' :: Int -> ATermTable -> (ATermTable, [COL_SIG_ITEM])
Pretty COL_SIG_ITEM Source #
Instance details Defined in COL.Print_AS Methods pretty :: COL_SIG_ITEM -> Doc Source # pretties :: [COL_SIG_ITEM] -> Doc Source #
AParsable COL_SIG_ITEM Source #
Instance details Defined in COL.Parse_AS Methods aparser :: AParser st COL_SIG_ITEM Source #
Syntax COL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in COL.Logic_COL Methods parsersAndPrinters :: COL -> Map String (PrefixMap -> AParser st C_BASIC_SPEC, C_BASIC_SPEC -> Doc) Source # parse_basic_spec :: COL -> Maybe (PrefixMap -> AParser st C_BASIC_SPEC) Source # parseSingleSymbItem :: COL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: COL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: COL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: COL -> C_BASIC_SPEC -> Item Source # symb_items_name :: COL -> SYMB_ITEMS -> [String] Source #
StaticAnalysis COL C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol Source #
Instance details Defined in COL.Logic_COL Methods basic_analysis :: COL -> Maybe ((C_BASIC_SPEC, CSign, GlobalAnnos) -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA])) Source # sen_analysis :: COL -> Maybe ((C_BASIC_SPEC, CSign, COLFORMULA) -> Result COLFORMULA) Source # extBasicAnalysis :: COL -> IRI -> LibName -> C_BASIC_SPEC -> CSign -> GlobalAnnos -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA]) Source # stat_symb_map_items :: COL -> CSign -> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: COL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: COL -> Maybe ((CSign, [Named COLFORMULA]) -> C_BASIC_SPEC) Source # ensures_amalgamability :: COL -> ([CASLAmalgOpt], Gr CSign (Int, COLMor), [(Int, COLMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: COL -> COLMor -> [Named COLFORMULA] -> Result (CSign, [Named COLFORMULA]) Source # signature_colimit :: COL -> Gr CSign (Int, COLMor) -> Result (CSign, Map Int COLMor) Source # qualify :: COL -> SIMPLE_ID -> LibName -> COLMor -> CSign -> Result (COLMor, [Named COLFORMULA]) Source # symbol_to_raw :: COL -> Symbol -> RawSymbol Source # id_to_raw :: COL -> Id -> RawSymbol Source # matches :: COL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: COL -> CSign Source # add_symb_to_sign :: COL -> CSign -> Symbol -> Result CSign Source # signature_union :: COL -> CSign -> CSign -> Result CSign Source # signatureDiff :: COL -> CSign -> CSign -> Result CSign Source # intersection :: COL -> CSign -> CSign -> Result CSign Source # final_union :: COL -> CSign -> CSign -> Result CSign Source # morphism_union :: COL -> COLMor -> COLMor -> Result COLMor Source # is_subsig :: COL -> CSign -> CSign -> Bool Source # subsig_inclusion :: COL -> CSign -> CSign -> Result COLMor Source # generated_sign :: COL -> Set Symbol -> CSign -> Result COLMor Source # cogenerated_sign :: COL -> Set Symbol -> CSign -> Result COLMor Source # induced_from_morphism :: COL -> EndoMap RawSymbol -> CSign -> Result COLMor Source # induced_from_to_morphism :: COL -> EndoMap RawSymbol -> ExtSign CSign Symbol -> ExtSign CSign Symbol -> Result COLMor Source # is_transportable :: COL -> COLMor -> Bool Source # is_injective :: COL -> COLMor -> Bool Source # theory_to_taxonomy :: COL -> TaxoGraphKind -> MMiSSOntology -> CSign -> [Named COLFORMULA] -> Result MMiSSOntology Source # corresp2th :: COL -> String -> Bool -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CSign, [Named COLFORMULA], CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: COL -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CSign, CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: COL -> [IRI] -> (CSign, [Named COLFORMULA]) -> Result (CSign, [Named COLFORMULA]) Source #
Logic COL () C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol () Source #
Instance details Defined in COL.Logic_COL Methods parse_basic_sen :: COL -> Maybe (C_BASIC_SPEC -> AParser st COLFORMULA) Source # stability :: COL -> Stability Source # data_logic :: COL -> Maybe AnyLogic Source # top_sublogic :: COL -> () Source # all_sublogics :: COL -> [()] Source # bottomSublogic :: COL -> Maybe () Source # sublogicDimensions :: COL -> [[()]] Source # parseSublogic :: COL -> String -> Maybe () Source # proj_sublogic_epsilon :: COL -> () -> CSign -> COLMor Source # provers :: COL -> [Prover CSign COLFORMULA COLMor () ()] Source # default_prover :: COL -> String Source # cons_checkers :: COL -> [ConsChecker CSign COLFORMULA () COLMor ()] Source # conservativityCheck :: COL -> [ConservativityChecker CSign COLFORMULA COLMor] Source # empty_proof_tree :: COL -> () Source # syntaxTable :: COL -> CSign -> Maybe SyntaxTable Source # omdoc_metatheory :: COL -> Maybe OMCD Source # export_symToOmdoc :: COL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: COL -> NameMap Symbol -> COLFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: COL -> SigMap Symbol -> CSign -> [Named COLFORMULA] -> Result [TCElement] Source # omdocToSym :: COL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: COL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named COLFORMULA)) Source # addOMadtToTheory :: COL -> SigMapI Symbol -> (CSign, [Named COLFORMULA]) -> [[OmdADT]] -> Result (CSign, [Named COLFORMULA]) Source # addOmdocToTheory :: COL -> SigMapI Symbol -> (CSign, [Named COLFORMULA]) -> [TCElement] -> Result (CSign, [Named COLFORMULA]) Source # sublogicOfTheo :: COL -> (CSign, [COLFORMULA]) -> () Source #
type Rep COL_SIG_ITEM
Instance details Defined in COL.ATC_COL type Rep COL_SIG_ITEM = D1 ('MetaData "COL_SIG_ITEM" "COL.AS_COL" "main" 'False) (C1 ('MetaCons "Constructor_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted Id]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Observer_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (Id, Maybe Int)]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

constructorS :: String Source #

constructorsS :: String Source #

observerS :: String Source #

observersS :: String Source #

col_reserved_words :: [String] Source #