Copyright	(c) A. Tsogias DFKI Bremen 2011
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Alexis.Tsogias@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	Safe

THF.Cons

Description

Data structures and functions used in Logic_THF and HasCASL2THF. Note: Some of the implenentations depend on the THF0 Syntax.

Documentation

data BasicSpecTHF Source #

Constructors

BasicSpecTHF [TPTP_THF]

Instances

Eq BasicSpecTHF Source #
Methods (==) :: BasicSpecTHF -> BasicSpecTHF -> Bool (/=) :: BasicSpecTHF -> BasicSpecTHF -> Bool
Data BasicSpecTHF Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BasicSpecTHF -> c BasicSpecTHF gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BasicSpecTHF toConstr :: BasicSpecTHF -> Constr dataTypeOf :: BasicSpecTHF -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c BasicSpecTHF) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BasicSpecTHF) gmapT :: (forall b. Data b => b -> b) -> BasicSpecTHF -> BasicSpecTHF gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BasicSpecTHF -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BasicSpecTHF -> r gmapQ :: (forall d. Data d => d -> u) -> BasicSpecTHF -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BasicSpecTHF -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BasicSpecTHF -> m BasicSpecTHF gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BasicSpecTHF -> m BasicSpecTHF gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BasicSpecTHF -> m BasicSpecTHF
Ord BasicSpecTHF Source #
Methods compare :: BasicSpecTHF -> BasicSpecTHF -> Ordering (<) :: BasicSpecTHF -> BasicSpecTHF -> Bool (<=) :: BasicSpecTHF -> BasicSpecTHF -> Bool (>) :: BasicSpecTHF -> BasicSpecTHF -> Bool (>=) :: BasicSpecTHF -> BasicSpecTHF -> Bool max :: BasicSpecTHF -> BasicSpecTHF -> BasicSpecTHF min :: BasicSpecTHF -> BasicSpecTHF -> BasicSpecTHF
Show BasicSpecTHF Source #
Methods showsPrec :: Int -> BasicSpecTHF -> ShowS show :: BasicSpecTHF -> String showList :: [BasicSpecTHF] -> ShowS
GetRange BasicSpecTHF Source #
Methods getRange :: BasicSpecTHF -> Range Source # rangeSpan :: BasicSpecTHF -> [Pos] Source #
Syntax THF BasicSpecTHF SymbolTHF () () Source #
Methods parsersAndPrinters :: THF -> Map String (PrefixMap -> AParser st BasicSpecTHF, BasicSpecTHF -> Doc) Source # parse_basic_spec :: THF -> Maybe (PrefixMap -> AParser st BasicSpecTHF) Source # parseSingleSymbItem :: THF -> Maybe (AParser st ()) Source # parse_symb_items :: THF -> Maybe (AParser st ()) Source # parse_symb_map_items :: THF -> Maybe (AParser st ()) Source # toItem :: THF -> BasicSpecTHF -> Item Source # symb_items_name :: THF -> () -> [String] Source #
StaticAnalysis THF BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () Source #
Methods basic_analysis :: THF -> Maybe ((BasicSpecTHF, SignTHF, GlobalAnnos) -> Result (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])) Source # sen_analysis :: THF -> Maybe ((BasicSpecTHF, SignTHF, THFFormula) -> Result THFFormula) Source # extBasicAnalysis :: THF -> IRI -> LibName -> BasicSpecTHF -> SignTHF -> GlobalAnnos -> Result (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula]) Source # stat_symb_map_items :: THF -> SignTHF -> Maybe SignTHF -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: THF -> SignTHF -> [()] -> Result [()] Source # convertTheory :: THF -> Maybe ((SignTHF, [Named THFFormula]) -> BasicSpecTHF) Source # ensures_amalgamability :: THF -> ([CASLAmalgOpt], Gr SignTHF (Int, MorphismTHF), [(Int, MorphismTHF)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: THF -> MorphismTHF -> [Named THFFormula] -> Result (SignTHF, [Named THFFormula]) Source # signature_colimit :: THF -> Gr SignTHF (Int, MorphismTHF) -> Result (SignTHF, Map Int MorphismTHF) Source # qualify :: THF -> SIMPLE_ID -> LibName -> MorphismTHF -> SignTHF -> Result (MorphismTHF, [Named THFFormula]) Source # symbol_to_raw :: THF -> SymbolTHF -> () Source # id_to_raw :: THF -> Id -> () Source # matches :: THF -> SymbolTHF -> () -> Bool Source # empty_signature :: THF -> SignTHF Source # add_symb_to_sign :: THF -> SignTHF -> SymbolTHF -> Result SignTHF Source # signature_union :: THF -> SignTHF -> SignTHF -> Result SignTHF Source # signatureDiff :: THF -> SignTHF -> SignTHF -> Result SignTHF Source # intersection :: THF -> SignTHF -> SignTHF -> Result SignTHF Source # final_union :: THF -> SignTHF -> SignTHF -> Result SignTHF Source # morphism_union :: THF -> MorphismTHF -> MorphismTHF -> Result MorphismTHF Source # is_subsig :: THF -> SignTHF -> SignTHF -> Bool Source # subsig_inclusion :: THF -> SignTHF -> SignTHF -> Result MorphismTHF Source # generated_sign :: THF -> Set SymbolTHF -> SignTHF -> Result MorphismTHF Source # cogenerated_sign :: THF -> Set SymbolTHF -> SignTHF -> Result MorphismTHF Source # induced_from_morphism :: THF -> EndoMap () -> SignTHF -> Result MorphismTHF Source # induced_from_to_morphism :: THF -> EndoMap () -> ExtSign SignTHF SymbolTHF -> ExtSign SignTHF SymbolTHF -> Result MorphismTHF Source # is_transportable :: THF -> MorphismTHF -> Bool Source # is_injective :: THF -> MorphismTHF -> Bool Source # theory_to_taxonomy :: THF -> TaxoGraphKind -> MMiSSOntology -> SignTHF -> [Named THFFormula] -> Result MMiSSOntology Source # corresp2th :: THF -> String -> Bool -> SignTHF -> SignTHF -> [()] -> [()] -> EndoMap SymbolTHF -> EndoMap SymbolTHF -> REL_REF -> Result (SignTHF, [Named THFFormula], SignTHF, SignTHF, EndoMap SymbolTHF, EndoMap SymbolTHF) Source # equiv2cospan :: THF -> SignTHF -> SignTHF -> [()] -> [()] -> Result (SignTHF, SignTHF, SignTHF, EndoMap SymbolTHF, EndoMap SymbolTHF) Source # extract_module :: THF -> [IRI] -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #
Logic THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Methods parse_basic_sen :: THF -> Maybe (BasicSpecTHF -> AParser st THFFormula) Source # stability :: THF -> Stability Source # data_logic :: THF -> Maybe AnyLogic Source # top_sublogic :: THF -> THFSl Source # all_sublogics :: THF -> [THFSl] Source # bottomSublogic :: THF -> Maybe THFSl Source # sublogicDimensions :: THF -> [[THFSl]] Source # parseSublogic :: THF -> String -> Maybe THFSl Source # proj_sublogic_epsilon :: THF -> THFSl -> SignTHF -> MorphismTHF Source # provers :: THF -> [Prover SignTHF THFFormula MorphismTHF THFSl ProofTree] Source # default_prover :: THF -> String Source # cons_checkers :: THF -> [ConsChecker SignTHF THFFormula THFSl MorphismTHF ProofTree] Source # conservativityCheck :: THF -> [ConservativityChecker SignTHF THFFormula MorphismTHF] Source # empty_proof_tree :: THF -> ProofTree Source # syntaxTable :: THF -> SignTHF -> Maybe SyntaxTable Source # omdoc_metatheory :: THF -> Maybe OMCD Source # export_symToOmdoc :: THF -> NameMap SymbolTHF -> SymbolTHF -> String -> Result TCElement Source # export_senToOmdoc :: THF -> NameMap SymbolTHF -> THFFormula -> Result TCorOMElement Source # export_theoryToOmdoc :: THF -> SigMap SymbolTHF -> SignTHF -> [Named THFFormula] -> Result [TCElement] Source # omdocToSym :: THF -> SigMapI SymbolTHF -> TCElement -> String -> Result SymbolTHF Source # omdocToSen :: THF -> SigMapI SymbolTHF -> TCElement -> String -> Result (Maybe (Named THFFormula)) Source # addOMadtToTheory :: THF -> SigMapI SymbolTHF -> (SignTHF, [Named THFFormula]) -> [[OmdADT]] -> Result (SignTHF, [Named THFFormula]) Source # addOmdocToTheory :: THF -> SigMapI SymbolTHF -> (SignTHF, [Named THFFormula]) -> [TCElement] -> Result (SignTHF, [Named THFFormula]) Source # sublogicOfTheo :: THF -> (SignTHF, [THFFormula]) -> THFSl Source #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Methods sourceLogic :: HasCASL2THFP_P -> HasCASL Source # sourceSublogic :: HasCASL2THFP_P -> Sublogic Source # sourceSublogicLossy :: HasCASL2THFP_P -> Sublogic Source # minSourceTheory :: HasCASL2THFP_P -> Maybe (LibName, String) Source # targetLogic :: HasCASL2THFP_P -> THF Source # mapSublogic :: HasCASL2THFP_P -> Sublogic -> Maybe THFSl Source # map_theory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: HasCASL2THFP_P -> Morphism -> Result MorphismTHF Source # map_sentence :: HasCASL2THFP_P -> Env -> Sentence -> Result THFFormula Source # map_symbol :: HasCASL2THFP_P -> Env -> Symbol -> Set SymbolTHF Source # extractModel :: HasCASL2THFP_P -> Env -> ProofTree -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2THFP_P -> Bool Source # has_model_expansion :: HasCASL2THFP_P -> Bool Source # is_weakly_amalgamable :: HasCASL2THFP_P -> Bool Source # constituents :: HasCASL2THFP_P -> [String] Source # isInclusionComorphism :: HasCASL2THFP_P -> Bool Source # rps :: HasCASL2THFP_P -> Bool Source # eps :: HasCASL2THFP_P -> Bool Source #
Comorphism THFP2THF0 THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Methods sourceLogic :: THFP2THF0 -> THF Source # sourceSublogic :: THFP2THF0 -> THFSl Source # sourceSublogicLossy :: THFP2THF0 -> THFSl Source # minSourceTheory :: THFP2THF0 -> Maybe (LibName, String) Source # targetLogic :: THFP2THF0 -> THF Source # mapSublogic :: THFP2THF0 -> THFSl -> Maybe THFSl Source # map_theory :: THFP2THF0 -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: THFP2THF0 -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: THFP2THF0 -> MorphismTHF -> Result MorphismTHF Source # map_sentence :: THFP2THF0 -> SignTHF -> THFFormula -> Result THFFormula Source # map_symbol :: THFP2THF0 -> SignTHF -> SymbolTHF -> Set SymbolTHF Source # extractModel :: THFP2THF0 -> SignTHF -> ProofTree -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP2THF0 -> Bool Source # has_model_expansion :: THFP2THF0 -> Bool Source # is_weakly_amalgamable :: THFP2THF0 -> Bool Source # constituents :: THFP2THF0 -> [String] Source # isInclusionComorphism :: THFP2THF0 -> Bool Source # rps :: THFP2THF0 -> Bool Source # eps :: THFP2THF0 -> Bool Source #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Methods sourceLogic :: THFP_P2HasCASL -> THF Source # sourceSublogic :: THFP_P2HasCASL -> THFSl Source # sourceSublogicLossy :: THFP_P2HasCASL -> THFSl Source # minSourceTheory :: THFP_P2HasCASL -> Maybe (LibName, String) Source # targetLogic :: THFP_P2HasCASL -> HasCASL Source # mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic Source # map_theory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # map_morphism :: THFP_P2HasCASL -> MorphismTHF -> Result Morphism Source # map_sentence :: THFP_P2HasCASL -> SignTHF -> THFFormula -> Result Sentence Source # map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol Source # extractModel :: THFP_P2HasCASL -> SignTHF -> () -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2HasCASL -> Bool Source # has_model_expansion :: THFP_P2HasCASL -> Bool Source # is_weakly_amalgamable :: THFP_P2HasCASL -> Bool Source # constituents :: THFP_P2HasCASL -> [String] Source # isInclusionComorphism :: THFP_P2HasCASL -> Bool Source # rps :: THFP_P2HasCASL -> Bool Source # eps :: THFP_P2HasCASL -> Bool Source #
Comorphism THFP_P2THFP THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Methods sourceLogic :: THFP_P2THFP -> THF Source # sourceSublogic :: THFP_P2THFP -> THFSl Source # sourceSublogicLossy :: THFP_P2THFP -> THFSl Source # minSourceTheory :: THFP_P2THFP -> Maybe (LibName, String) Source # targetLogic :: THFP_P2THFP -> THF Source # mapSublogic :: THFP_P2THFP -> THFSl -> Maybe THFSl Source # map_theory :: THFP_P2THFP -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: THFP_P2THFP -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: THFP_P2THFP -> MorphismTHF -> Result MorphismTHF Source # map_sentence :: THFP_P2THFP -> SignTHF -> THFFormula -> Result THFFormula Source # map_symbol :: THFP_P2THFP -> SignTHF -> SymbolTHF -> Set SymbolTHF Source # extractModel :: THFP_P2THFP -> SignTHF -> ProofTree -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2THFP -> Bool Source # has_model_expansion :: THFP_P2THFP -> Bool Source # is_weakly_amalgamable :: THFP_P2THFP -> Bool Source # constituents :: THFP_P2THFP -> [String] Source # isInclusionComorphism :: THFP_P2THFP -> Bool Source # rps :: THFP_P2THFP -> Bool Source # eps :: THFP_P2THFP -> Bool Source #

data SymbolTHF Source #

Constructors

Symbol
Fields symId :: Constant symName :: Name symType :: SymbolType

Instances

Eq SymbolTHF Source #
Methods (==) :: SymbolTHF -> SymbolTHF -> Bool (/=) :: SymbolTHF -> SymbolTHF -> Bool
Data SymbolTHF Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbolTHF -> c SymbolTHF gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbolTHF toConstr :: SymbolTHF -> Constr dataTypeOf :: SymbolTHF -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c SymbolTHF) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbolTHF) gmapT :: (forall b. Data b => b -> b) -> SymbolTHF -> SymbolTHF gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbolTHF -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbolTHF -> r gmapQ :: (forall d. Data d => d -> u) -> SymbolTHF -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbolTHF -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymbolTHF -> m SymbolTHF gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbolTHF -> m SymbolTHF gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbolTHF -> m SymbolTHF
Ord SymbolTHF Source #
Methods compare :: SymbolTHF -> SymbolTHF -> Ordering (<) :: SymbolTHF -> SymbolTHF -> Bool (<=) :: SymbolTHF -> SymbolTHF -> Bool (>) :: SymbolTHF -> SymbolTHF -> Bool (>=) :: SymbolTHF -> SymbolTHF -> Bool max :: SymbolTHF -> SymbolTHF -> SymbolTHF min :: SymbolTHF -> SymbolTHF -> SymbolTHF
Show SymbolTHF Source #
Methods showsPrec :: Int -> SymbolTHF -> ShowS show :: SymbolTHF -> String showList :: [SymbolTHF] -> ShowS
GetRange SymbolTHF Source #
Methods getRange :: SymbolTHF -> Range Source # rangeSpan :: SymbolTHF -> [Pos] Source #
Sentences THF THFFormula SignTHF MorphismTHF SymbolTHF Source #
Methods map_sen :: THF -> MorphismTHF -> THFFormula -> Result THFFormula Source # simplify_sen :: THF -> SignTHF -> THFFormula -> THFFormula Source # negation :: THF -> THFFormula -> Maybe THFFormula Source # print_sign :: THF -> SignTHF -> Doc Source # print_named :: THF -> Named THFFormula -> Doc Source # sym_of :: THF -> SignTHF -> [Set SymbolTHF] Source # mostSymsOf :: THF -> SignTHF -> [SymbolTHF] Source # symmap_of :: THF -> MorphismTHF -> EndoMap SymbolTHF Source # sym_name :: THF -> SymbolTHF -> Id Source # sym_label :: THF -> SymbolTHF -> Maybe String Source # fullSymName :: THF -> SymbolTHF -> String Source # symKind :: THF -> SymbolTHF -> String Source # symsOfSen :: THF -> SignTHF -> THFFormula -> [SymbolTHF] Source # pair_symbols :: THF -> SymbolTHF -> SymbolTHF -> Result SymbolTHF Source #
Syntax THF BasicSpecTHF SymbolTHF () () Source #
Methods parsersAndPrinters :: THF -> Map String (PrefixMap -> AParser st BasicSpecTHF, BasicSpecTHF -> Doc) Source # parse_basic_spec :: THF -> Maybe (PrefixMap -> AParser st BasicSpecTHF) Source # parseSingleSymbItem :: THF -> Maybe (AParser st ()) Source # parse_symb_items :: THF -> Maybe (AParser st ()) Source # parse_symb_map_items :: THF -> Maybe (AParser st ()) Source # toItem :: THF -> BasicSpecTHF -> Item Source # symb_items_name :: THF -> () -> [String] Source #
StaticAnalysis THF BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () Source #
Methods basic_analysis :: THF -> Maybe ((BasicSpecTHF, SignTHF, GlobalAnnos) -> Result (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])) Source # sen_analysis :: THF -> Maybe ((BasicSpecTHF, SignTHF, THFFormula) -> Result THFFormula) Source # extBasicAnalysis :: THF -> IRI -> LibName -> BasicSpecTHF -> SignTHF -> GlobalAnnos -> Result (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula]) Source # stat_symb_map_items :: THF -> SignTHF -> Maybe SignTHF -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: THF -> SignTHF -> [()] -> Result [()] Source # convertTheory :: THF -> Maybe ((SignTHF, [Named THFFormula]) -> BasicSpecTHF) Source # ensures_amalgamability :: THF -> ([CASLAmalgOpt], Gr SignTHF (Int, MorphismTHF), [(Int, MorphismTHF)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: THF -> MorphismTHF -> [Named THFFormula] -> Result (SignTHF, [Named THFFormula]) Source # signature_colimit :: THF -> Gr SignTHF (Int, MorphismTHF) -> Result (SignTHF, Map Int MorphismTHF) Source # qualify :: THF -> SIMPLE_ID -> LibName -> MorphismTHF -> SignTHF -> Result (MorphismTHF, [Named THFFormula]) Source # symbol_to_raw :: THF -> SymbolTHF -> () Source # id_to_raw :: THF -> Id -> () Source # matches :: THF -> SymbolTHF -> () -> Bool Source # empty_signature :: THF -> SignTHF Source # add_symb_to_sign :: THF -> SignTHF -> SymbolTHF -> Result SignTHF Source # signature_union :: THF -> SignTHF -> SignTHF -> Result SignTHF Source # signatureDiff :: THF -> SignTHF -> SignTHF -> Result SignTHF Source # intersection :: THF -> SignTHF -> SignTHF -> Result SignTHF Source # final_union :: THF -> SignTHF -> SignTHF -> Result SignTHF Source # morphism_union :: THF -> MorphismTHF -> MorphismTHF -> Result MorphismTHF Source # is_subsig :: THF -> SignTHF -> SignTHF -> Bool Source # subsig_inclusion :: THF -> SignTHF -> SignTHF -> Result MorphismTHF Source # generated_sign :: THF -> Set SymbolTHF -> SignTHF -> Result MorphismTHF Source # cogenerated_sign :: THF -> Set SymbolTHF -> SignTHF -> Result MorphismTHF Source # induced_from_morphism :: THF -> EndoMap () -> SignTHF -> Result MorphismTHF Source # induced_from_to_morphism :: THF -> EndoMap () -> ExtSign SignTHF SymbolTHF -> ExtSign SignTHF SymbolTHF -> Result MorphismTHF Source # is_transportable :: THF -> MorphismTHF -> Bool Source # is_injective :: THF -> MorphismTHF -> Bool Source # theory_to_taxonomy :: THF -> TaxoGraphKind -> MMiSSOntology -> SignTHF -> [Named THFFormula] -> Result MMiSSOntology Source # corresp2th :: THF -> String -> Bool -> SignTHF -> SignTHF -> [()] -> [()] -> EndoMap SymbolTHF -> EndoMap SymbolTHF -> REL_REF -> Result (SignTHF, [Named THFFormula], SignTHF, SignTHF, EndoMap SymbolTHF, EndoMap SymbolTHF) Source # equiv2cospan :: THF -> SignTHF -> SignTHF -> [()] -> [()] -> Result (SignTHF, SignTHF, SignTHF, EndoMap SymbolTHF, EndoMap SymbolTHF) Source # extract_module :: THF -> [IRI] -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #
Logic THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Methods parse_basic_sen :: THF -> Maybe (BasicSpecTHF -> AParser st THFFormula) Source # stability :: THF -> Stability Source # data_logic :: THF -> Maybe AnyLogic Source # top_sublogic :: THF -> THFSl Source # all_sublogics :: THF -> [THFSl] Source # bottomSublogic :: THF -> Maybe THFSl Source # sublogicDimensions :: THF -> [[THFSl]] Source # parseSublogic :: THF -> String -> Maybe THFSl Source # proj_sublogic_epsilon :: THF -> THFSl -> SignTHF -> MorphismTHF Source # provers :: THF -> [Prover SignTHF THFFormula MorphismTHF THFSl ProofTree] Source # default_prover :: THF -> String Source # cons_checkers :: THF -> [ConsChecker SignTHF THFFormula THFSl MorphismTHF ProofTree] Source # conservativityCheck :: THF -> [ConservativityChecker SignTHF THFFormula MorphismTHF] Source # empty_proof_tree :: THF -> ProofTree Source # syntaxTable :: THF -> SignTHF -> Maybe SyntaxTable Source # omdoc_metatheory :: THF -> Maybe OMCD Source # export_symToOmdoc :: THF -> NameMap SymbolTHF -> SymbolTHF -> String -> Result TCElement Source # export_senToOmdoc :: THF -> NameMap SymbolTHF -> THFFormula -> Result TCorOMElement Source # export_theoryToOmdoc :: THF -> SigMap SymbolTHF -> SignTHF -> [Named THFFormula] -> Result [TCElement] Source # omdocToSym :: THF -> SigMapI SymbolTHF -> TCElement -> String -> Result SymbolTHF Source # omdocToSen :: THF -> SigMapI SymbolTHF -> TCElement -> String -> Result (Maybe (Named THFFormula)) Source # addOMadtToTheory :: THF -> SigMapI SymbolTHF -> (SignTHF, [Named THFFormula]) -> [[OmdADT]] -> Result (SignTHF, [Named THFFormula]) Source # addOmdocToTheory :: THF -> SigMapI SymbolTHF -> (SignTHF, [Named THFFormula]) -> [TCElement] -> Result (SignTHF, [Named THFFormula]) Source # sublogicOfTheo :: THF -> (SignTHF, [THFFormula]) -> THFSl Source #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Methods sourceLogic :: HasCASL2THFP_P -> HasCASL Source # sourceSublogic :: HasCASL2THFP_P -> Sublogic Source # sourceSublogicLossy :: HasCASL2THFP_P -> Sublogic Source # minSourceTheory :: HasCASL2THFP_P -> Maybe (LibName, String) Source # targetLogic :: HasCASL2THFP_P -> THF Source # mapSublogic :: HasCASL2THFP_P -> Sublogic -> Maybe THFSl Source # map_theory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: HasCASL2THFP_P -> Morphism -> Result MorphismTHF Source # map_sentence :: HasCASL2THFP_P -> Env -> Sentence -> Result THFFormula Source # map_symbol :: HasCASL2THFP_P -> Env -> Symbol -> Set SymbolTHF Source # extractModel :: HasCASL2THFP_P -> Env -> ProofTree -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2THFP_P -> Bool Source # has_model_expansion :: HasCASL2THFP_P -> Bool Source # is_weakly_amalgamable :: HasCASL2THFP_P -> Bool Source # constituents :: HasCASL2THFP_P -> [String] Source # isInclusionComorphism :: HasCASL2THFP_P -> Bool Source # rps :: HasCASL2THFP_P -> Bool Source # eps :: HasCASL2THFP_P -> Bool Source #
Comorphism THFP2THF0 THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Methods sourceLogic :: THFP2THF0 -> THF Source # sourceSublogic :: THFP2THF0 -> THFSl Source # sourceSublogicLossy :: THFP2THF0 -> THFSl Source # minSourceTheory :: THFP2THF0 -> Maybe (LibName, String) Source # targetLogic :: THFP2THF0 -> THF Source # mapSublogic :: THFP2THF0 -> THFSl -> Maybe THFSl Source # map_theory :: THFP2THF0 -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: THFP2THF0 -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: THFP2THF0 -> MorphismTHF -> Result MorphismTHF Source # map_sentence :: THFP2THF0 -> SignTHF -> THFFormula -> Result THFFormula Source # map_symbol :: THFP2THF0 -> SignTHF -> SymbolTHF -> Set SymbolTHF Source # extractModel :: THFP2THF0 -> SignTHF -> ProofTree -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP2THF0 -> Bool Source # has_model_expansion :: THFP2THF0 -> Bool Source # is_weakly_amalgamable :: THFP2THF0 -> Bool Source # constituents :: THFP2THF0 -> [String] Source # isInclusionComorphism :: THFP2THF0 -> Bool Source # rps :: THFP2THF0 -> Bool Source # eps :: THFP2THF0 -> Bool Source #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Methods sourceLogic :: THFP_P2HasCASL -> THF Source # sourceSublogic :: THFP_P2HasCASL -> THFSl Source # sourceSublogicLossy :: THFP_P2HasCASL -> THFSl Source # minSourceTheory :: THFP_P2HasCASL -> Maybe (LibName, String) Source # targetLogic :: THFP_P2HasCASL -> HasCASL Source # mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic Source # map_theory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # map_morphism :: THFP_P2HasCASL -> MorphismTHF -> Result Morphism Source # map_sentence :: THFP_P2HasCASL -> SignTHF -> THFFormula -> Result Sentence Source # map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol Source # extractModel :: THFP_P2HasCASL -> SignTHF -> () -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2HasCASL -> Bool Source # has_model_expansion :: THFP_P2HasCASL -> Bool Source # is_weakly_amalgamable :: THFP_P2HasCASL -> Bool Source # constituents :: THFP_P2HasCASL -> [String] Source # isInclusionComorphism :: THFP_P2HasCASL -> Bool Source # rps :: THFP_P2HasCASL -> Bool Source # eps :: THFP_P2HasCASL -> Bool Source #
Comorphism THFP_P2THFP THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Methods sourceLogic :: THFP_P2THFP -> THF Source # sourceSublogic :: THFP_P2THFP -> THFSl Source # sourceSublogicLossy :: THFP_P2THFP -> THFSl Source # minSourceTheory :: THFP_P2THFP -> Maybe (LibName, String) Source # targetLogic :: THFP_P2THFP -> THF Source # mapSublogic :: THFP_P2THFP -> THFSl -> Maybe THFSl Source # map_theory :: THFP_P2THFP -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: THFP_P2THFP -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: THFP_P2THFP -> MorphismTHF -> Result MorphismTHF Source # map_sentence :: THFP_P2THFP -> SignTHF -> THFFormula -> Result THFFormula Source # map_symbol :: THFP_P2THFP -> SignTHF -> SymbolTHF -> Set SymbolTHF Source # extractModel :: THFP_P2THFP -> SignTHF -> ProofTree -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2THFP -> Bool Source # has_model_expansion :: THFP_P2THFP -> Bool Source # is_weakly_amalgamable :: THFP_P2THFP -> Bool Source # constituents :: THFP_P2THFP -> [String] Source # isInclusionComorphism :: THFP_P2THFP -> Bool Source # rps :: THFP_P2THFP -> Bool Source # eps :: THFP_P2THFP -> Bool Source #

data SymbolType Source #

Constructors

ST_Const Type
ST_Type Kind

Instances

Eq SymbolType Source #
Methods (==) :: SymbolType -> SymbolType -> Bool (/=) :: SymbolType -> SymbolType -> Bool
Data SymbolType Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbolType -> c SymbolType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbolType toConstr :: SymbolType -> Constr dataTypeOf :: SymbolType -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c SymbolType) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbolType) gmapT :: (forall b. Data b => b -> b) -> SymbolType -> SymbolType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbolType -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbolType -> r gmapQ :: (forall d. Data d => d -> u) -> SymbolType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbolType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType
Ord SymbolType Source #
Methods compare :: SymbolType -> SymbolType -> Ordering (<) :: SymbolType -> SymbolType -> Bool (<=) :: SymbolType -> SymbolType -> Bool (>) :: SymbolType -> SymbolType -> Bool (>=) :: SymbolType -> SymbolType -> Bool max :: SymbolType -> SymbolType -> SymbolType min :: SymbolType -> SymbolType -> SymbolType
Show SymbolType Source #
Methods showsPrec :: Int -> SymbolType -> ShowS show :: SymbolType -> String showList :: [SymbolType] -> ShowS

data Type Source #

Constructors

TType
OType
IType
MapType Type Type
ProdType [Type]
CType Constant
SType Token
VType Token
ParType Type

Instances

Eq Type Source #
Methods (==) :: Type -> Type -> Bool (/=) :: Type -> Type -> Bool
Data Type Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type -> c Type gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type toConstr :: Type -> Constr dataTypeOf :: Type -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Type) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type) gmapT :: (forall b. Data b => b -> b) -> Type -> Type gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r gmapQ :: (forall d. Data d => d -> u) -> Type -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Type -> m Type gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type
Ord Type Source #
Methods compare :: Type -> Type -> Ordering (<) :: Type -> Type -> Bool (<=) :: Type -> Type -> Bool (>) :: Type -> Type -> Bool (>=) :: Type -> Type -> Bool max :: Type -> Type -> Type min :: Type -> Type -> Type
Show Type Source #
Methods showsPrec :: Int -> Type -> ShowS show :: Type -> String showList :: [Type] -> ShowS

data Kind Source #

Constructors

Kind

Instances

Eq Kind Source #
Methods (==) :: Kind -> Kind -> Bool (/=) :: Kind -> Kind -> Bool
Data Kind Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Kind -> c Kind gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Kind toConstr :: Kind -> Constr dataTypeOf :: Kind -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Kind) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind) gmapT :: (forall b. Data b => b -> b) -> Kind -> Kind gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r gmapQ :: (forall d. Data d => d -> u) -> Kind -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Kind -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Kind -> m Kind gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Kind -> m Kind gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Kind -> m Kind
Ord Kind Source #
Methods compare :: Kind -> Kind -> Ordering (<) :: Kind -> Kind -> Bool (<=) :: Kind -> Kind -> Bool (>) :: Kind -> Kind -> Bool (>=) :: Kind -> Kind -> Bool max :: Kind -> Kind -> Kind min :: Kind -> Kind -> Kind
Show Kind Source #
Methods showsPrec :: Int -> Kind -> ShowS show :: Kind -> String showList :: [Kind] -> ShowS