Copyright	(c) Kristina Sojakova DFKI Bremen 2009
License	GPLv2 or higher, see LICENSE.txt
Maintainer	k.sojakova@jacobs-university.de
Stability	experimental
Portability	portable Signatures of this logic are composed of a logical framework name (currently one of LF, Isabelle, or Maude) to be used as a meta-logic, and a tuple of signature and morphism names which determine the object logic. As such the logic Framework does not have any sentences and only identity signature morphisms. For reference see Integrating Logical Frameworks in Hets by M. Codescu et al (WADT10).
Safe Haskell	None

Framework.Logic_Framework

Contents

Orphan instances

Description

Documentation

type Morphism = DefaultMorphism LogicDef Source #

data Framework Source #

Constructors

Framework

Instances

Instances details

Show Framework Source #
Instance details Defined in Framework.Logic_Framework Methods showsPrec :: Int -> Framework -> ShowS show :: Framework -> String showList :: [Framework] -> ShowS
Language Framework Source #
Instance details Defined in Framework.Logic_Framework Methods language_name :: Framework -> String Source # description :: Framework -> String Source #
Sentences Framework () LogicDef Morphism () Source #
Instance details Defined in Framework.Logic_Framework Methods map_sen :: Framework -> Morphism -> () -> Result () Source # simplify_sen :: Framework -> LogicDef -> () -> () Source # negation :: Framework -> () -> Maybe () Source # print_sign :: Framework -> LogicDef -> Doc Source # print_named :: Framework -> Named () -> Doc Source # sym_of :: Framework -> LogicDef -> [Set ()] Source # mostSymsOf :: Framework -> LogicDef -> [()] Source # symmap_of :: Framework -> Morphism -> EndoMap () Source # sym_name :: Framework -> () -> Id Source # sym_label :: Framework -> () -> Maybe String Source # fullSymName :: Framework -> () -> String Source # symKind :: Framework -> () -> String Source # symsOfSen :: Framework -> LogicDef -> () -> [()] Source # pair_symbols :: Framework -> () -> () -> Result () Source #
Syntax Framework LogicDef () () () Source #
Instance details Defined in Framework.Logic_Framework Methods parsersAndPrinters :: Framework -> Map String (PrefixMap -> AParser st LogicDef, LogicDef -> Doc) Source # parse_basic_spec :: Framework -> Maybe (PrefixMap -> AParser st LogicDef) Source # parseSingleSymbItem :: Framework -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_items :: Framework -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: Framework -> Maybe (PrefixMap -> AParser st ()) Source # toItem :: Framework -> LogicDef -> Item Source # symb_items_name :: Framework -> () -> [String] Source #
StaticAnalysis Framework LogicDef () () () LogicDef Morphism () () Source #
Instance details Defined in Framework.Logic_Framework Methods basic_analysis :: Framework -> Maybe ((LogicDef, LogicDef, GlobalAnnos) -> Result (LogicDef, ExtSign LogicDef (), [Named ()])) Source # sen_analysis :: Framework -> Maybe ((LogicDef, LogicDef, ()) -> Result ()) Source # extBasicAnalysis :: Framework -> IRI -> LibName -> LogicDef -> LogicDef -> GlobalAnnos -> Result (LogicDef, ExtSign LogicDef (), [Named ()]) Source # stat_symb_map_items :: Framework -> LogicDef -> Maybe LogicDef -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: Framework -> LogicDef -> [()] -> Result [()] Source # convertTheory :: Framework -> Maybe ((LogicDef, [Named ()]) -> LogicDef) Source # ensures_amalgamability :: Framework -> ([CASLAmalgOpt], Gr LogicDef (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Framework -> Morphism -> [Named ()] -> Result (LogicDef, [Named ()]) Source # signature_colimit :: Framework -> Gr LogicDef (Int, Morphism) -> Result (LogicDef, Map Int Morphism) Source # qualify :: Framework -> SIMPLE_ID -> LibName -> Morphism -> LogicDef -> Result (Morphism, [Named ()]) Source # symbol_to_raw :: Framework -> () -> () Source # id_to_raw :: Framework -> Id -> () Source # matches :: Framework -> () -> () -> Bool Source # empty_signature :: Framework -> LogicDef Source # add_symb_to_sign :: Framework -> LogicDef -> () -> Result LogicDef Source # signature_union :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source # signatureDiff :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source # intersection :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source # final_union :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source # morphism_union :: Framework -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: Framework -> LogicDef -> LogicDef -> Bool Source # subsig_inclusion :: Framework -> LogicDef -> LogicDef -> Result Morphism Source # generated_sign :: Framework -> Set () -> LogicDef -> Result Morphism Source # cogenerated_sign :: Framework -> Set () -> LogicDef -> Result Morphism Source # induced_from_morphism :: Framework -> EndoMap () -> LogicDef -> Result Morphism Source # induced_from_to_morphism :: Framework -> EndoMap () -> ExtSign LogicDef () -> ExtSign LogicDef () -> Result Morphism Source # is_transportable :: Framework -> Morphism -> Bool Source # is_injective :: Framework -> Morphism -> Bool Source # theory_to_taxonomy :: Framework -> TaxoGraphKind -> MMiSSOntology -> LogicDef -> [Named ()] -> Result MMiSSOntology Source # corresp2th :: Framework -> String -> Bool -> LogicDef -> LogicDef -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (LogicDef, [Named ()], LogicDef, LogicDef, EndoMap (), EndoMap ()) Source # equiv2cospan :: Framework -> LogicDef -> LogicDef -> [()] -> [()] -> Result (LogicDef, LogicDef, LogicDef, EndoMap (), EndoMap ()) Source # extract_module :: Framework -> [IRI] -> (LogicDef, [Named ()]) -> Result (LogicDef, [Named ()]) Source #
Logic Framework () LogicDef () () () LogicDef Morphism () () () Source #
Instance details Defined in Framework.Logic_Framework Methods parse_basic_sen :: Framework -> Maybe (LogicDef -> AParser st ()) Source # stability :: Framework -> Stability Source # data_logic :: Framework -> Maybe AnyLogic Source # top_sublogic :: Framework -> () Source # all_sublogics :: Framework -> [()] Source # bottomSublogic :: Framework -> Maybe () Source # sublogicDimensions :: Framework -> [[()]] Source # parseSublogic :: Framework -> String -> Maybe () Source # proj_sublogic_epsilon :: Framework -> () -> LogicDef -> Morphism Source # provers :: Framework -> [Prover LogicDef () Morphism () ()] Source # default_prover :: Framework -> String Source # cons_checkers :: Framework -> [ConsChecker LogicDef () () Morphism ()] Source # conservativityCheck :: Framework -> [ConservativityChecker LogicDef () Morphism] Source # empty_proof_tree :: Framework -> () Source # syntaxTable :: Framework -> LogicDef -> Maybe SyntaxTable Source # omdoc_metatheory :: Framework -> Maybe OMCD Source # export_symToOmdoc :: Framework -> NameMap () -> () -> String -> Result TCElement Source # export_senToOmdoc :: Framework -> NameMap () -> () -> Result TCorOMElement Source # export_theoryToOmdoc :: Framework -> SigMap () -> LogicDef -> [Named ()] -> Result [TCElement] Source # omdocToSym :: Framework -> SigMapI () -> TCElement -> String -> Result () Source # omdocToSen :: Framework -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source # addOMadtToTheory :: Framework -> SigMapI () -> (LogicDef, [Named ()]) -> [[OmdADT]] -> Result (LogicDef, [Named ()]) Source # addOmdocToTheory :: Framework -> SigMapI () -> (LogicDef, [Named ()]) -> [TCElement] -> Result (LogicDef, [Named ()]) Source # sublogicOfTheo :: Framework -> (LogicDef, [()]) -> () Source #

type MorphismCom = DefaultMorphism ComorphismDef Source #

data FrameworkCom Source #

Constructors

FrameworkCom

Instances

Instances details

Show FrameworkCom Source #
Instance details Defined in Framework.Logic_Framework Methods showsPrec :: Int -> FrameworkCom -> ShowS show :: FrameworkCom -> String showList :: [FrameworkCom] -> ShowS
Language FrameworkCom Source #
Instance details Defined in Framework.Logic_Framework Methods language_name :: FrameworkCom -> String Source # description :: FrameworkCom -> String Source #
Sentences FrameworkCom () ComorphismDef MorphismCom () Source #
Instance details Defined in Framework.Logic_Framework Methods map_sen :: FrameworkCom -> MorphismCom -> () -> Result () Source # simplify_sen :: FrameworkCom -> ComorphismDef -> () -> () Source # negation :: FrameworkCom -> () -> Maybe () Source # print_sign :: FrameworkCom -> ComorphismDef -> Doc Source # print_named :: FrameworkCom -> Named () -> Doc Source # sym_of :: FrameworkCom -> ComorphismDef -> [Set ()] Source # mostSymsOf :: FrameworkCom -> ComorphismDef -> [()] Source # symmap_of :: FrameworkCom -> MorphismCom -> EndoMap () Source # sym_name :: FrameworkCom -> () -> Id Source # sym_label :: FrameworkCom -> () -> Maybe String Source # fullSymName :: FrameworkCom -> () -> String Source # symKind :: FrameworkCom -> () -> String Source # symsOfSen :: FrameworkCom -> ComorphismDef -> () -> [()] Source # pair_symbols :: FrameworkCom -> () -> () -> Result () Source #
Syntax FrameworkCom ComorphismDef () () () Source #
Instance details Defined in Framework.Logic_Framework Methods parsersAndPrinters :: FrameworkCom -> Map String (PrefixMap -> AParser st ComorphismDef, ComorphismDef -> Doc) Source # parse_basic_spec :: FrameworkCom -> Maybe (PrefixMap -> AParser st ComorphismDef) Source # parseSingleSymbItem :: FrameworkCom -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_items :: FrameworkCom -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: FrameworkCom -> Maybe (PrefixMap -> AParser st ()) Source # toItem :: FrameworkCom -> ComorphismDef -> Item Source # symb_items_name :: FrameworkCom -> () -> [String] Source #
StaticAnalysis FrameworkCom ComorphismDef () () () ComorphismDef MorphismCom () () Source #
Instance details Defined in Framework.Logic_Framework Methods basic_analysis :: FrameworkCom -> Maybe ((ComorphismDef, ComorphismDef, GlobalAnnos) -> Result (ComorphismDef, ExtSign ComorphismDef (), [Named ()])) Source # sen_analysis :: FrameworkCom -> Maybe ((ComorphismDef, ComorphismDef, ()) -> Result ()) Source # extBasicAnalysis :: FrameworkCom -> IRI -> LibName -> ComorphismDef -> ComorphismDef -> GlobalAnnos -> Result (ComorphismDef, ExtSign ComorphismDef (), [Named ()]) Source # stat_symb_map_items :: FrameworkCom -> ComorphismDef -> Maybe ComorphismDef -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: FrameworkCom -> ComorphismDef -> [()] -> Result [()] Source # convertTheory :: FrameworkCom -> Maybe ((ComorphismDef, [Named ()]) -> ComorphismDef) Source # ensures_amalgamability :: FrameworkCom -> ([CASLAmalgOpt], Gr ComorphismDef (Int, MorphismCom), [(Int, MorphismCom)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: FrameworkCom -> MorphismCom -> [Named ()] -> Result (ComorphismDef, [Named ()]) Source # signature_colimit :: FrameworkCom -> Gr ComorphismDef (Int, MorphismCom) -> Result (ComorphismDef, Map Int MorphismCom) Source # qualify :: FrameworkCom -> SIMPLE_ID -> LibName -> MorphismCom -> ComorphismDef -> Result (MorphismCom, [Named ()]) Source # symbol_to_raw :: FrameworkCom -> () -> () Source # id_to_raw :: FrameworkCom -> Id -> () Source # matches :: FrameworkCom -> () -> () -> Bool Source # empty_signature :: FrameworkCom -> ComorphismDef Source # add_symb_to_sign :: FrameworkCom -> ComorphismDef -> () -> Result ComorphismDef Source # signature_union :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source # signatureDiff :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source # intersection :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source # final_union :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source # morphism_union :: FrameworkCom -> MorphismCom -> MorphismCom -> Result MorphismCom Source # is_subsig :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Bool Source # subsig_inclusion :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result MorphismCom Source # generated_sign :: FrameworkCom -> Set () -> ComorphismDef -> Result MorphismCom Source # cogenerated_sign :: FrameworkCom -> Set () -> ComorphismDef -> Result MorphismCom Source # induced_from_morphism :: FrameworkCom -> EndoMap () -> ComorphismDef -> Result MorphismCom Source # induced_from_to_morphism :: FrameworkCom -> EndoMap () -> ExtSign ComorphismDef () -> ExtSign ComorphismDef () -> Result MorphismCom Source # is_transportable :: FrameworkCom -> MorphismCom -> Bool Source # is_injective :: FrameworkCom -> MorphismCom -> Bool Source # theory_to_taxonomy :: FrameworkCom -> TaxoGraphKind -> MMiSSOntology -> ComorphismDef -> [Named ()] -> Result MMiSSOntology Source # corresp2th :: FrameworkCom -> String -> Bool -> ComorphismDef -> ComorphismDef -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (ComorphismDef, [Named ()], ComorphismDef, ComorphismDef, EndoMap (), EndoMap ()) Source # equiv2cospan :: FrameworkCom -> ComorphismDef -> ComorphismDef -> [()] -> [()] -> Result (ComorphismDef, ComorphismDef, ComorphismDef, EndoMap (), EndoMap ()) Source # extract_module :: FrameworkCom -> [IRI] -> (ComorphismDef, [Named ()]) -> Result (ComorphismDef, [Named ()]) Source #
Logic FrameworkCom () ComorphismDef () () () ComorphismDef MorphismCom () () () Source #
Instance details Defined in Framework.Logic_Framework Methods parse_basic_sen :: FrameworkCom -> Maybe (ComorphismDef -> AParser st ()) Source # stability :: FrameworkCom -> Stability Source # data_logic :: FrameworkCom -> Maybe AnyLogic Source # top_sublogic :: FrameworkCom -> () Source # all_sublogics :: FrameworkCom -> [()] Source # bottomSublogic :: FrameworkCom -> Maybe () Source # sublogicDimensions :: FrameworkCom -> [[()]] Source # parseSublogic :: FrameworkCom -> String -> Maybe () Source # proj_sublogic_epsilon :: FrameworkCom -> () -> ComorphismDef -> MorphismCom Source # provers :: FrameworkCom -> [Prover ComorphismDef () MorphismCom () ()] Source # default_prover :: FrameworkCom -> String Source # cons_checkers :: FrameworkCom -> [ConsChecker ComorphismDef () () MorphismCom ()] Source # conservativityCheck :: FrameworkCom -> [ConservativityChecker ComorphismDef () MorphismCom] Source # empty_proof_tree :: FrameworkCom -> () Source # syntaxTable :: FrameworkCom -> ComorphismDef -> Maybe SyntaxTable Source # omdoc_metatheory :: FrameworkCom -> Maybe OMCD Source # export_symToOmdoc :: FrameworkCom -> NameMap () -> () -> String -> Result TCElement Source # export_senToOmdoc :: FrameworkCom -> NameMap () -> () -> Result TCorOMElement Source # export_theoryToOmdoc :: FrameworkCom -> SigMap () -> ComorphismDef -> [Named ()] -> Result [TCElement] Source # omdocToSym :: FrameworkCom -> SigMapI () -> TCElement -> String -> Result () Source # omdocToSen :: FrameworkCom -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source # addOMadtToTheory :: FrameworkCom -> SigMapI () -> (ComorphismDef, [Named ()]) -> [[OmdADT]] -> Result (ComorphismDef, [Named ()]) Source # addOmdocToTheory :: FrameworkCom -> SigMapI () -> (ComorphismDef, [Named ()]) -> [TCElement] -> Result (ComorphismDef, [Named ()]) Source # sublogicOfTheo :: FrameworkCom -> (ComorphismDef, [()]) -> () Source #

Orphan instances

Semigroup ComorphismDef Source #
Instance details Methods (<>) :: ComorphismDef -> ComorphismDef -> ComorphismDef # sconcat :: NonEmpty ComorphismDef -> ComorphismDef stimes :: Integral b => b -> ComorphismDef -> ComorphismDef
Semigroup LogicDef Source #
Instance details Methods (<>) :: LogicDef -> LogicDef -> LogicDef # sconcat :: NonEmpty LogicDef -> LogicDef stimes :: Integral b => b -> LogicDef -> LogicDef
Monoid ComorphismDef Source #
Instance details Methods mempty :: ComorphismDef mappend :: ComorphismDef -> ComorphismDef -> ComorphismDef mconcat :: [ComorphismDef] -> ComorphismDef
Monoid LogicDef Source #
Instance details Methods mempty :: LogicDef mappend :: LogicDef -> LogicDef -> LogicDef mconcat :: [LogicDef] -> LogicDef