Copyright	(c) Christian Maeder DFKI Uni Bremen 2009
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	non-portable (imports Logic.Logic)
Safe Haskell	None

DMU.Logic_DMU

Description

dummy instance of class Logic for DMU

Documentation

data DMU Source #

Constructors

DMU

Instances

Instances details

Show DMU Source #
Instance details Defined in DMU.Logic_DMU Methods showsPrec :: Int -> DMU -> ShowS show :: DMU -> String showList :: [DMU] -> ShowS
Language DMU Source #
Instance details Defined in DMU.Logic_DMU Methods language_name :: DMU -> String Source # description :: DMU -> String Source #
Syntax DMU Text () () () Source #
Instance details Defined in DMU.Logic_DMU Methods parsersAndPrinters :: DMU -> Map String (PrefixMap -> AParser st Text, Text -> Doc) Source # parse_basic_spec :: DMU -> Maybe (PrefixMap -> AParser st Text) Source # parseSingleSymbItem :: DMU -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_items :: DMU -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: DMU -> Maybe (PrefixMap -> AParser st ()) Source # toItem :: DMU -> Text -> Item Source # symb_items_name :: DMU -> () -> [String] Source #
Comorphism DMU2OWL2 DMU () Text () () () Text (DefaultMorphism Text) () () () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source #
Instance details Defined in OWL2.DMU2OWL2 Methods sourceLogic :: DMU2OWL2 -> DMU Source # sourceSublogic :: DMU2OWL2 -> () Source # sourceSublogicLossy :: DMU2OWL2 -> () Source # minSourceTheory :: DMU2OWL2 -> Maybe (LibName, String) Source # targetLogic :: DMU2OWL2 -> OWL2 Source # mapSublogic :: DMU2OWL2 -> () -> Maybe ProfSub Source # map_theory :: DMU2OWL2 -> (Text, [Named ()]) -> Result (Sign, [Named Axiom]) Source # mapMarkedTheory :: DMU2OWL2 -> (Text, [Named ()]) -> Result (Sign, [Named Axiom]) Source # map_morphism :: DMU2OWL2 -> DefaultMorphism Text -> Result OWLMorphism Source # map_sentence :: DMU2OWL2 -> Text -> () -> Result Axiom Source # map_symbol :: DMU2OWL2 -> Text -> () -> Set Entity Source # extractModel :: DMU2OWL2 -> Text -> ProofTree -> Result (Text, [Named ()]) Source # is_model_transportable :: DMU2OWL2 -> Bool Source # has_model_expansion :: DMU2OWL2 -> Bool Source # is_weakly_amalgamable :: DMU2OWL2 -> Bool Source # constituents :: DMU2OWL2 -> [String] Source # isInclusionComorphism :: DMU2OWL2 -> Bool Source # rps :: DMU2OWL2 -> Bool Source # eps :: DMU2OWL2 -> Bool Source # isGTC :: DMU2OWL2 -> Bool Source #
Logic DMU () Text () () () Text (DefaultMorphism Text) () () () Source #
Instance details Defined in DMU.Logic_DMU Methods parse_basic_sen :: DMU -> Maybe (Text -> AParser st ()) Source # stability :: DMU -> Stability Source # data_logic :: DMU -> Maybe AnyLogic Source # top_sublogic :: DMU -> () Source # all_sublogics :: DMU -> [()] Source # bottomSublogic :: DMU -> Maybe () Source # sublogicDimensions :: DMU -> [[()]] Source # parseSublogic :: DMU -> String -> Maybe () Source # proj_sublogic_epsilon :: DMU -> () -> Text -> DefaultMorphism Text Source # provers :: DMU -> [Prover Text () (DefaultMorphism Text) () ()] Source # default_prover :: DMU -> String Source # cons_checkers :: DMU -> [ConsChecker Text () () (DefaultMorphism Text) ()] Source # conservativityCheck :: DMU -> [ConservativityChecker Text () (DefaultMorphism Text)] Source # empty_proof_tree :: DMU -> () Source # syntaxTable :: DMU -> Text -> Maybe SyntaxTable Source # omdoc_metatheory :: DMU -> Maybe OMCD Source # export_symToOmdoc :: DMU -> NameMap () -> () -> String -> Result TCElement Source # export_senToOmdoc :: DMU -> NameMap () -> () -> Result TCorOMElement Source # export_theoryToOmdoc :: DMU -> SigMap () -> Text -> [Named ()] -> Result [TCElement] Source # omdocToSym :: DMU -> SigMapI () -> TCElement -> String -> Result () Source # omdocToSen :: DMU -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source # addOMadtToTheory :: DMU -> SigMapI () -> (Text, [Named ()]) -> [[OmdADT]] -> Result (Text, [Named ()]) Source # addOmdocToTheory :: DMU -> SigMapI () -> (Text, [Named ()]) -> [TCElement] -> Result (Text, [Named ()]) Source # sublogicOfTheo :: DMU -> (Text, [()]) -> () Source #
StaticAnalysis DMU Text () () () Text (DefaultMorphism Text) () () Source #
Instance details Defined in DMU.Logic_DMU Methods basic_analysis :: DMU -> Maybe ((Text, Text, GlobalAnnos) -> Result (Text, ExtSign Text (), [Named ()])) Source # sen_analysis :: DMU -> Maybe ((Text, Text, ()) -> Result ()) Source # extBasicAnalysis :: DMU -> IRI -> LibName -> Text -> Text -> GlobalAnnos -> Result (Text, ExtSign Text (), [Named ()]) Source # stat_symb_map_items :: DMU -> Text -> Maybe Text -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: DMU -> Text -> [()] -> Result [()] Source # convertTheory :: DMU -> Maybe ((Text, [Named ()]) -> Text) Source # ensures_amalgamability :: DMU -> ([CASLAmalgOpt], Gr Text (Int, DefaultMorphism Text), [(Int, DefaultMorphism Text)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: DMU -> DefaultMorphism Text -> [Named ()] -> Result (Text, [Named ()]) Source # signature_colimit :: DMU -> Gr Text (Int, DefaultMorphism Text) -> Result (Text, Map Int (DefaultMorphism Text)) Source # qualify :: DMU -> SIMPLE_ID -> LibName -> DefaultMorphism Text -> Text -> Result (DefaultMorphism Text, [Named ()]) Source # symbol_to_raw :: DMU -> () -> () Source # id_to_raw :: DMU -> Id -> () Source # matches :: DMU -> () -> () -> Bool Source # empty_signature :: DMU -> Text Source # add_symb_to_sign :: DMU -> Text -> () -> Result Text Source # signature_union :: DMU -> Text -> Text -> Result Text Source # signatureDiff :: DMU -> Text -> Text -> Result Text Source # intersection :: DMU -> Text -> Text -> Result Text Source # final_union :: DMU -> Text -> Text -> Result Text Source # morphism_union :: DMU -> DefaultMorphism Text -> DefaultMorphism Text -> Result (DefaultMorphism Text) Source # is_subsig :: DMU -> Text -> Text -> Bool Source # subsig_inclusion :: DMU -> Text -> Text -> Result (DefaultMorphism Text) Source # generated_sign :: DMU -> Set () -> Text -> Result (DefaultMorphism Text) Source # cogenerated_sign :: DMU -> Set () -> Text -> Result (DefaultMorphism Text) Source # induced_from_morphism :: DMU -> EndoMap () -> Text -> Result (DefaultMorphism Text) Source # induced_from_to_morphism :: DMU -> EndoMap () -> ExtSign Text () -> ExtSign Text () -> Result (DefaultMorphism Text) Source # is_transportable :: DMU -> DefaultMorphism Text -> Bool Source # is_injective :: DMU -> DefaultMorphism Text -> Bool Source # theory_to_taxonomy :: DMU -> TaxoGraphKind -> MMiSSOntology -> Text -> [Named ()] -> Result MMiSSOntology Source # corresp2th :: DMU -> String -> Bool -> Text -> Text -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Text, [Named ()], Text, Text, EndoMap (), EndoMap ()) Source # equiv2cospan :: DMU -> Text -> Text -> [()] -> [()] -> Result (Text, Text, Text, EndoMap (), EndoMap ()) Source # extract_module :: DMU -> [IRI] -> (Text, [Named ()]) -> Result (Text, [Named ()]) Source #
Sentences DMU () Text (DefaultMorphism Text) () Source #
Instance details Defined in DMU.Logic_DMU Methods map_sen :: DMU -> DefaultMorphism Text -> () -> Result () Source # simplify_sen :: DMU -> Text -> () -> () Source # negation :: DMU -> () -> Maybe () Source # print_sign :: DMU -> Text -> Doc Source # print_named :: DMU -> Named () -> Doc Source # sym_of :: DMU -> Text -> [Set ()] Source # mostSymsOf :: DMU -> Text -> [()] Source # symmap_of :: DMU -> DefaultMorphism Text -> EndoMap () Source # sym_name :: DMU -> () -> Id Source # sym_label :: DMU -> () -> Maybe String Source # fullSymName :: DMU -> () -> String Source # symKind :: DMU -> () -> String Source # symsOfSen :: DMU -> Text -> () -> [()] Source # pair_symbols :: DMU -> () -> () -> Result () Source #

newtype Text Source #

Constructors

Text
Fields fromText :: String

Instances

Instances details

Eq Text Source #
Instance details Defined in DMU.Logic_DMU Methods (==) :: Text -> Text -> Bool (/=) :: Text -> Text -> Bool
Ord Text Source #
Instance details Defined in DMU.Logic_DMU Methods compare :: Text -> Text -> Ordering (<) :: Text -> Text -> Bool (<=) :: Text -> Text -> Bool (>) :: Text -> Text -> Bool (>=) :: Text -> Text -> Bool max :: Text -> Text -> Text min :: Text -> Text -> Text
Show Text Source #
Instance details Defined in DMU.Logic_DMU Methods showsPrec :: Int -> Text -> ShowS show :: Text -> String showList :: [Text] -> ShowS
Generic Text Source #
Instance details Defined in DMU.Logic_DMU Associated Types type Rep Text :: Type -> Type Methods from :: Text -> Rep Text x to :: Rep Text x -> Text
Semigroup Text Source #
Instance details Defined in DMU.Logic_DMU Methods (<>) :: Text -> Text -> Text # sconcat :: NonEmpty Text -> Text stimes :: Integral b => b -> Text -> Text
Monoid Text Source #
Instance details Defined in DMU.Logic_DMU Methods mempty :: Text mappend :: Text -> Text -> Text mconcat :: [Text] -> Text
GetRange Text Source #
Instance details Defined in DMU.Logic_DMU Methods getRange :: Text -> Range Source # rangeSpan :: Text -> [Pos] Source #
ShATermConvertible Text Source #
Instance details Defined in DMU.Logic_DMU Methods toShATermAux :: ATermTable -> Text -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Text] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Text) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Text])
Pretty Text Source #
Instance details Defined in DMU.Logic_DMU Methods pretty :: Text -> Doc Source # pretties :: [Text] -> Doc Source #
Syntax DMU Text () () () Source #
Instance details Defined in DMU.Logic_DMU Methods parsersAndPrinters :: DMU -> Map String (PrefixMap -> AParser st Text, Text -> Doc) Source # parse_basic_spec :: DMU -> Maybe (PrefixMap -> AParser st Text) Source # parseSingleSymbItem :: DMU -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_items :: DMU -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: DMU -> Maybe (PrefixMap -> AParser st ()) Source # toItem :: DMU -> Text -> Item Source # symb_items_name :: DMU -> () -> [String] Source #
Comorphism DMU2OWL2 DMU () Text () () () Text (DefaultMorphism Text) () () () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source #
Instance details Defined in OWL2.DMU2OWL2 Methods sourceLogic :: DMU2OWL2 -> DMU Source # sourceSublogic :: DMU2OWL2 -> () Source # sourceSublogicLossy :: DMU2OWL2 -> () Source # minSourceTheory :: DMU2OWL2 -> Maybe (LibName, String) Source # targetLogic :: DMU2OWL2 -> OWL2 Source # mapSublogic :: DMU2OWL2 -> () -> Maybe ProfSub Source # map_theory :: DMU2OWL2 -> (Text, [Named ()]) -> Result (Sign, [Named Axiom]) Source # mapMarkedTheory :: DMU2OWL2 -> (Text, [Named ()]) -> Result (Sign, [Named Axiom]) Source # map_morphism :: DMU2OWL2 -> DefaultMorphism Text -> Result OWLMorphism Source # map_sentence :: DMU2OWL2 -> Text -> () -> Result Axiom Source # map_symbol :: DMU2OWL2 -> Text -> () -> Set Entity Source # extractModel :: DMU2OWL2 -> Text -> ProofTree -> Result (Text, [Named ()]) Source # is_model_transportable :: DMU2OWL2 -> Bool Source # has_model_expansion :: DMU2OWL2 -> Bool Source # is_weakly_amalgamable :: DMU2OWL2 -> Bool Source # constituents :: DMU2OWL2 -> [String] Source # isInclusionComorphism :: DMU2OWL2 -> Bool Source # rps :: DMU2OWL2 -> Bool Source # eps :: DMU2OWL2 -> Bool Source # isGTC :: DMU2OWL2 -> Bool Source #
Logic DMU () Text () () () Text (DefaultMorphism Text) () () () Source #
Instance details Defined in DMU.Logic_DMU Methods parse_basic_sen :: DMU -> Maybe (Text -> AParser st ()) Source # stability :: DMU -> Stability Source # data_logic :: DMU -> Maybe AnyLogic Source # top_sublogic :: DMU -> () Source # all_sublogics :: DMU -> [()] Source # bottomSublogic :: DMU -> Maybe () Source # sublogicDimensions :: DMU -> [[()]] Source # parseSublogic :: DMU -> String -> Maybe () Source # proj_sublogic_epsilon :: DMU -> () -> Text -> DefaultMorphism Text Source # provers :: DMU -> [Prover Text () (DefaultMorphism Text) () ()] Source # default_prover :: DMU -> String Source # cons_checkers :: DMU -> [ConsChecker Text () () (DefaultMorphism Text) ()] Source # conservativityCheck :: DMU -> [ConservativityChecker Text () (DefaultMorphism Text)] Source # empty_proof_tree :: DMU -> () Source # syntaxTable :: DMU -> Text -> Maybe SyntaxTable Source # omdoc_metatheory :: DMU -> Maybe OMCD Source # export_symToOmdoc :: DMU -> NameMap () -> () -> String -> Result TCElement Source # export_senToOmdoc :: DMU -> NameMap () -> () -> Result TCorOMElement Source # export_theoryToOmdoc :: DMU -> SigMap () -> Text -> [Named ()] -> Result [TCElement] Source # omdocToSym :: DMU -> SigMapI () -> TCElement -> String -> Result () Source # omdocToSen :: DMU -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source # addOMadtToTheory :: DMU -> SigMapI () -> (Text, [Named ()]) -> [[OmdADT]] -> Result (Text, [Named ()]) Source # addOmdocToTheory :: DMU -> SigMapI () -> (Text, [Named ()]) -> [TCElement] -> Result (Text, [Named ()]) Source # sublogicOfTheo :: DMU -> (Text, [()]) -> () Source #
StaticAnalysis DMU Text () () () Text (DefaultMorphism Text) () () Source #
Instance details Defined in DMU.Logic_DMU Methods basic_analysis :: DMU -> Maybe ((Text, Text, GlobalAnnos) -> Result (Text, ExtSign Text (), [Named ()])) Source # sen_analysis :: DMU -> Maybe ((Text, Text, ()) -> Result ()) Source # extBasicAnalysis :: DMU -> IRI -> LibName -> Text -> Text -> GlobalAnnos -> Result (Text, ExtSign Text (), [Named ()]) Source # stat_symb_map_items :: DMU -> Text -> Maybe Text -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: DMU -> Text -> [()] -> Result [()] Source # convertTheory :: DMU -> Maybe ((Text, [Named ()]) -> Text) Source # ensures_amalgamability :: DMU -> ([CASLAmalgOpt], Gr Text (Int, DefaultMorphism Text), [(Int, DefaultMorphism Text)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: DMU -> DefaultMorphism Text -> [Named ()] -> Result (Text, [Named ()]) Source # signature_colimit :: DMU -> Gr Text (Int, DefaultMorphism Text) -> Result (Text, Map Int (DefaultMorphism Text)) Source # qualify :: DMU -> SIMPLE_ID -> LibName -> DefaultMorphism Text -> Text -> Result (DefaultMorphism Text, [Named ()]) Source # symbol_to_raw :: DMU -> () -> () Source # id_to_raw :: DMU -> Id -> () Source # matches :: DMU -> () -> () -> Bool Source # empty_signature :: DMU -> Text Source # add_symb_to_sign :: DMU -> Text -> () -> Result Text Source # signature_union :: DMU -> Text -> Text -> Result Text Source # signatureDiff :: DMU -> Text -> Text -> Result Text Source # intersection :: DMU -> Text -> Text -> Result Text Source # final_union :: DMU -> Text -> Text -> Result Text Source # morphism_union :: DMU -> DefaultMorphism Text -> DefaultMorphism Text -> Result (DefaultMorphism Text) Source # is_subsig :: DMU -> Text -> Text -> Bool Source # subsig_inclusion :: DMU -> Text -> Text -> Result (DefaultMorphism Text) Source # generated_sign :: DMU -> Set () -> Text -> Result (DefaultMorphism Text) Source # cogenerated_sign :: DMU -> Set () -> Text -> Result (DefaultMorphism Text) Source # induced_from_morphism :: DMU -> EndoMap () -> Text -> Result (DefaultMorphism Text) Source # induced_from_to_morphism :: DMU -> EndoMap () -> ExtSign Text () -> ExtSign Text () -> Result (DefaultMorphism Text) Source # is_transportable :: DMU -> DefaultMorphism Text -> Bool Source # is_injective :: DMU -> DefaultMorphism Text -> Bool Source # theory_to_taxonomy :: DMU -> TaxoGraphKind -> MMiSSOntology -> Text -> [Named ()] -> Result MMiSSOntology Source # corresp2th :: DMU -> String -> Bool -> Text -> Text -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Text, [Named ()], Text, Text, EndoMap (), EndoMap ()) Source # equiv2cospan :: DMU -> Text -> Text -> [()] -> [()] -> Result (Text, Text, Text, EndoMap (), EndoMap ()) Source # extract_module :: DMU -> [IRI] -> (Text, [Named ()]) -> Result (Text, [Named ()]) Source #
Sentences DMU () Text (DefaultMorphism Text) () Source #
Instance details Defined in DMU.Logic_DMU Methods map_sen :: DMU -> DefaultMorphism Text -> () -> Result () Source # simplify_sen :: DMU -> Text -> () -> () Source # negation :: DMU -> () -> Maybe () Source # print_sign :: DMU -> Text -> Doc Source # print_named :: DMU -> Named () -> Doc Source # sym_of :: DMU -> Text -> [Set ()] Source # mostSymsOf :: DMU -> Text -> [()] Source # symmap_of :: DMU -> DefaultMorphism Text -> EndoMap () Source # sym_name :: DMU -> () -> Id Source # sym_label :: DMU -> () -> Maybe String Source # fullSymName :: DMU -> () -> String Source # symKind :: DMU -> () -> String Source # symsOfSen :: DMU -> Text -> () -> [()] Source # pair_symbols :: DMU -> () -> () -> Result () Source #
type Rep Text Source #
Instance details Defined in DMU.Logic_DMU type Rep Text = D1 ('MetaData "Text" "DMU.Logic_DMU" "main" 'True) (C1 ('MetaCons "Text" 'PrefixI 'True) (S1 ('MetaSel ('Just "fromText") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))