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

Logic.Morphism

Contents

Morphisms

Description

Interface (type class) for logic projections (morphisms) in Hets

Provides data structures for institution morphisms. These are just collections of functions between (some of) the types of logics.

Synopsis

class (Language cid, Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2) => Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2 | cid -> lid1, cid -> lid2, lid1 -> sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1, lid2 -> sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2 where
- morSourceLogic :: cid -> lid1
- morSourceSublogic :: cid -> sublogics1
- morTargetLogic :: cid -> lid2
- morTargetSublogic :: cid -> sublogics2
- morMapSublogicSign :: cid -> sublogics1 -> sublogics2
- morMapSublogicSen :: cid -> sublogics2 -> sublogics1
- morMap_sign :: cid -> sign1 -> Maybe sign2
- morMap_morphism :: cid -> morphism1 -> Maybe morphism2
- morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
- morMap_sign_symbol :: cid -> sign_symbol1 -> Set sign_symbol2
data IdMorphism lid sublogics = IdMorphism lid sublogics
class Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2 => InducingComorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2 where
- indMorMap_sign :: cid -> sign2 -> Maybe sign1
- indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1
- epsilon :: cid -> sign2 -> Maybe morphism2
data SpanDomain cid = SpanDomain cid
data SublogicsPair a b = SublogicsPair a b
newtype S2 s = S2 {
- sentence2 :: s
}
data AnyMorphism = forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2.Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => Morphism cid

Documentation

class (Language cid, Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2) => Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2 | cid -> lid1, cid -> lid2, lid1 -> sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1, lid2 -> sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2 where Source #

Methods

morSourceLogic :: cid -> lid1 Source #

morSourceSublogic :: cid -> sublogics1 Source #

morTargetLogic :: cid -> lid2 Source #

morTargetSublogic :: cid -> sublogics2 Source #

morMapSublogicSign :: cid -> sublogics1 -> sublogics2 Source #

morMapSublogicSen :: cid -> sublogics2 -> sublogics1 Source #

morMap_sign :: cid -> sign1 -> Maybe sign2 Source #

morMap_morphism :: cid -> morphism1 -> Maybe morphism2 Source #

morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1 Source #

morMap_sign_symbol :: cid -> sign_symbol1 -> Set sign_symbol2 Source #

Instances

Instances details

Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism sign_symbol symbol proof_tree => Morphism (IdMorphism lid sublogics) lid sublogics basic_spec sentence symb_items symb_map_items sign morphism sign_symbol symbol proof_tree lid sublogics basic_spec sentence symb_items symb_map_items sign morphism sign_symbol symbol proof_tree Source #

Instance details

Defined in Logic.Morphism

Methods

morSourceLogic :: IdMorphism lid sublogics -> lid Source #

morSourceSublogic :: IdMorphism lid sublogics -> sublogics Source #

morTargetLogic :: IdMorphism lid sublogics -> lid Source #

morTargetSublogic :: IdMorphism lid sublogics -> sublogics Source #

morMapSublogicSign :: IdMorphism lid sublogics -> sublogics -> sublogics Source #

morMapSublogicSen :: IdMorphism lid sublogics -> sublogics -> sublogics Source #

morMap_sign :: IdMorphism lid sublogics -> sign -> Maybe sign Source #

morMap_morphism :: IdMorphism lid sublogics -> morphism -> Maybe morphism Source #

morMap_sentence :: IdMorphism lid sublogics -> sign -> sentence -> Maybe sentence Source #

morMap_sign_symbol :: IdMorphism lid sublogics -> sign_symbol -> Set sign_symbol Source #

data IdMorphism lid sublogics Source #

identity morphisms

Constructors

IdMorphism lid sublogics

Instances

Instances details

(Show lid, Show sublogics) => Show (IdMorphism lid sublogics) Source #
Instance details Defined in Logic.Morphism Methods showsPrec :: Int -> IdMorphism lid sublogics -> ShowS show :: IdMorphism lid sublogics -> String showList :: [IdMorphism lid sublogics] -> ShowS
Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism sign_symbol symbol proof_tree => Language (IdMorphism lid sublogics) Source #
Instance details Defined in Logic.Morphism Methods language_name :: IdMorphism lid sublogics -> String Source # description :: IdMorphism lid sublogics -> String Source #
Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism sign_symbol symbol proof_tree => Morphism (IdMorphism lid sublogics) lid sublogics basic_spec sentence symb_items symb_map_items sign morphism sign_symbol symbol proof_tree lid sublogics basic_spec sentence symb_items symb_map_items sign morphism sign_symbol symbol proof_tree Source #
Instance details Defined in Logic.Morphism Methods morSourceLogic :: IdMorphism lid sublogics -> lid Source # morSourceSublogic :: IdMorphism lid sublogics -> sublogics Source # morTargetLogic :: IdMorphism lid sublogics -> lid Source # morTargetSublogic :: IdMorphism lid sublogics -> sublogics Source # morMapSublogicSign :: IdMorphism lid sublogics -> sublogics -> sublogics Source # morMapSublogicSen :: IdMorphism lid sublogics -> sublogics -> sublogics Source # morMap_sign :: IdMorphism lid sublogics -> sign -> Maybe sign Source # morMap_morphism :: IdMorphism lid sublogics -> morphism -> Maybe morphism Source # morMap_sentence :: IdMorphism lid sublogics -> sign -> sentence -> Maybe sentence Source # morMap_sign_symbol :: IdMorphism lid sublogics -> sign_symbol -> Set sign_symbol Source #

class Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2 => InducingComorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2 where Source #

comorphisms inducing morphisms

Methods

indMorMap_sign :: cid -> sign2 -> Maybe sign1 Source #

indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1 Source #

epsilon :: cid -> sign2 -> Maybe morphism2 Source #

data SpanDomain cid Source #

Constructors

SpanDomain cid

Instances

Instances details

Eq cid => Eq (SpanDomain cid) Source #
Instance details Defined in Logic.Morphism Methods (==) :: SpanDomain cid -> SpanDomain cid -> Bool (/=) :: SpanDomain cid -> SpanDomain cid -> Bool
Show cid => Show (SpanDomain cid) Source #
Instance details Defined in Logic.Morphism Methods showsPrec :: Int -> SpanDomain cid -> ShowS show :: SpanDomain cid -> String showList :: [SpanDomain cid] -> ShowS
Language cid => Language (SpanDomain cid) Source #
Instance details Defined in Logic.Morphism Methods language_name :: SpanDomain cid -> String Source # description :: SpanDomain cid -> String Source #
(Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2, Pretty sign_symbol1) => Syntax (SpanDomain cid) () sign_symbol1 () () Source #
Instance details Defined in Logic.Morphism Methods parsersAndPrinters :: SpanDomain cid -> Map String (PrefixMap -> AParser st (), () -> Doc) Source # parse_basic_spec :: SpanDomain cid -> Maybe (PrefixMap -> AParser st ()) Source # parseSingleSymbItem :: SpanDomain cid -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_items :: SpanDomain cid -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: SpanDomain cid -> Maybe (PrefixMap -> AParser st ()) Source # toItem :: SpanDomain cid -> () -> Item Source # symb_items_name :: SpanDomain cid -> () -> [String] Source #
(Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2, Ord symbol1, GetRange symbol1, Pretty symbol1, Typeable symbol1, Data sentence2) => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 Source #
Instance details Defined in Logic.Morphism Methods basic_analysis :: SpanDomain cid -> Maybe (((), sign1, GlobalAnnos) -> Result ((), ExtSign sign1 sign_symbol1, [Named (S2 sentence2)])) Source # sen_analysis :: SpanDomain cid -> Maybe (((), sign1, S2 sentence2) -> Result (S2 sentence2)) Source # extBasicAnalysis :: SpanDomain cid -> IRI -> LibName -> () -> sign1 -> GlobalAnnos -> Result ((), ExtSign sign1 sign_symbol1, [Named (S2 sentence2)]) Source # stat_symb_map_items :: SpanDomain cid -> sign1 -> Maybe sign1 -> [()] -> Result (EndoMap symbol1) Source # stat_symb_items :: SpanDomain cid -> sign1 -> [()] -> Result [symbol1] Source # convertTheory :: SpanDomain cid -> Maybe ((sign1, [Named (S2 sentence2)]) -> ()) Source # ensures_amalgamability :: SpanDomain cid -> ([CASLAmalgOpt], Gr sign1 (Int, morphism1), [(Int, morphism1)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: SpanDomain cid -> morphism1 -> [Named (S2 sentence2)] -> Result (sign1, [Named (S2 sentence2)]) Source # signature_colimit :: SpanDomain cid -> Gr sign1 (Int, morphism1) -> Result (sign1, Map Int morphism1) Source # qualify :: SpanDomain cid -> SIMPLE_ID -> LibName -> morphism1 -> sign1 -> Result (morphism1, [Named (S2 sentence2)]) Source # symbol_to_raw :: SpanDomain cid -> sign_symbol1 -> symbol1 Source # id_to_raw :: SpanDomain cid -> Id -> symbol1 Source # matches :: SpanDomain cid -> sign_symbol1 -> symbol1 -> Bool Source # empty_signature :: SpanDomain cid -> sign1 Source # add_symb_to_sign :: SpanDomain cid -> sign1 -> sign_symbol1 -> Result sign1 Source # signature_union :: SpanDomain cid -> sign1 -> sign1 -> Result sign1 Source # signatureDiff :: SpanDomain cid -> sign1 -> sign1 -> Result sign1 Source # intersection :: SpanDomain cid -> sign1 -> sign1 -> Result sign1 Source # final_union :: SpanDomain cid -> sign1 -> sign1 -> Result sign1 Source # morphism_union :: SpanDomain cid -> morphism1 -> morphism1 -> Result morphism1 Source # is_subsig :: SpanDomain cid -> sign1 -> sign1 -> Bool Source # subsig_inclusion :: SpanDomain cid -> sign1 -> sign1 -> Result morphism1 Source # generated_sign :: SpanDomain cid -> Set sign_symbol1 -> sign1 -> Result morphism1 Source # cogenerated_sign :: SpanDomain cid -> Set sign_symbol1 -> sign1 -> Result morphism1 Source # induced_from_morphism :: SpanDomain cid -> EndoMap symbol1 -> sign1 -> Result morphism1 Source # induced_from_to_morphism :: SpanDomain cid -> EndoMap symbol1 -> ExtSign sign1 sign_symbol1 -> ExtSign sign1 sign_symbol1 -> Result morphism1 Source # is_transportable :: SpanDomain cid -> morphism1 -> Bool Source # is_injective :: SpanDomain cid -> morphism1 -> Bool Source # theory_to_taxonomy :: SpanDomain cid -> TaxoGraphKind -> MMiSSOntology -> sign1 -> [Named (S2 sentence2)] -> Result MMiSSOntology Source # corresp2th :: SpanDomain cid -> String -> Bool -> sign1 -> sign1 -> [()] -> [()] -> EndoMap sign_symbol1 -> EndoMap sign_symbol1 -> REL_REF -> Result (sign1, [Named (S2 sentence2)], sign1, sign1, EndoMap sign_symbol1, EndoMap sign_symbol1) Source # equiv2cospan :: SpanDomain cid -> sign1 -> sign1 -> [()] -> [()] -> Result (sign1, sign1, sign1, EndoMap sign_symbol1, EndoMap sign_symbol1) Source # extract_module :: SpanDomain cid -> [IRI] -> (sign1, [Named (S2 sentence2)]) -> Result (sign1, [Named (S2 sentence2)]) Source #
(Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2, Category sign1 morphism1, Ord sign_symbol1, GetRange sign_symbol1, Data sentence2) => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1 sign_symbol1 Source #
Instance details Defined in Logic.Morphism Methods map_sen :: SpanDomain cid -> morphism1 -> S2 sentence2 -> Result (S2 sentence2) Source # simplify_sen :: SpanDomain cid -> sign1 -> S2 sentence2 -> S2 sentence2 Source # negation :: SpanDomain cid -> S2 sentence2 -> Maybe (S2 sentence2) Source # print_sign :: SpanDomain cid -> sign1 -> Doc Source # print_named :: SpanDomain cid -> Named (S2 sentence2) -> Doc Source # sym_of :: SpanDomain cid -> sign1 -> [Set sign_symbol1] Source # mostSymsOf :: SpanDomain cid -> sign1 -> [sign_symbol1] Source # symmap_of :: SpanDomain cid -> morphism1 -> EndoMap sign_symbol1 Source # sym_name :: SpanDomain cid -> sign_symbol1 -> Id Source # sym_label :: SpanDomain cid -> sign_symbol1 -> Maybe String Source # fullSymName :: SpanDomain cid -> sign_symbol1 -> String Source # symKind :: SpanDomain cid -> sign_symbol1 -> String Source # symsOfSen :: SpanDomain cid -> sign1 -> S2 sentence2 -> [sign_symbol1] Source # pair_symbols :: SpanDomain cid -> sign_symbol1 -> sign_symbol1 -> Result sign_symbol1 Source #
(MinSublogic sublogics1 (), Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2, Ord proof_tree2, Show proof_tree2, Data sentence2) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2 Source #
Instance details Defined in Logic.Morphism Methods parse_basic_sen :: SpanDomain cid -> Maybe (() -> AParser st (S2 sentence2)) Source # stability :: SpanDomain cid -> Stability Source # data_logic :: SpanDomain cid -> Maybe AnyLogic Source # top_sublogic :: SpanDomain cid -> SublogicsPair sublogics1 sublogics2 Source # all_sublogics :: SpanDomain cid -> [SublogicsPair sublogics1 sublogics2] Source # bottomSublogic :: SpanDomain cid -> Maybe (SublogicsPair sublogics1 sublogics2) Source # sublogicDimensions :: SpanDomain cid -> [[SublogicsPair sublogics1 sublogics2]] Source # parseSublogic :: SpanDomain cid -> String -> Maybe (SublogicsPair sublogics1 sublogics2) Source # proj_sublogic_epsilon :: SpanDomain cid -> SublogicsPair sublogics1 sublogics2 -> sign1 -> morphism1 Source # provers :: SpanDomain cid -> [Prover sign1 (S2 sentence2) morphism1 (SublogicsPair sublogics1 sublogics2) proof_tree2] Source # default_prover :: SpanDomain cid -> String Source # cons_checkers :: SpanDomain cid -> [ConsChecker sign1 (S2 sentence2) (SublogicsPair sublogics1 sublogics2) morphism1 proof_tree2] Source # conservativityCheck :: SpanDomain cid -> [ConservativityChecker sign1 (S2 sentence2) morphism1] Source # empty_proof_tree :: SpanDomain cid -> proof_tree2 Source # syntaxTable :: SpanDomain cid -> sign1 -> Maybe SyntaxTable Source # omdoc_metatheory :: SpanDomain cid -> Maybe OMCD Source # export_symToOmdoc :: SpanDomain cid -> NameMap sign_symbol1 -> sign_symbol1 -> String -> Result TCElement Source # export_senToOmdoc :: SpanDomain cid -> NameMap sign_symbol1 -> S2 sentence2 -> Result TCorOMElement Source # export_theoryToOmdoc :: SpanDomain cid -> SigMap sign_symbol1 -> sign1 -> [Named (S2 sentence2)] -> Result [TCElement] Source # omdocToSym :: SpanDomain cid -> SigMapI sign_symbol1 -> TCElement -> String -> Result sign_symbol1 Source # omdocToSen :: SpanDomain cid -> SigMapI sign_symbol1 -> TCElement -> String -> Result (Maybe (Named (S2 sentence2))) Source # addOMadtToTheory :: SpanDomain cid -> SigMapI sign_symbol1 -> (sign1, [Named (S2 sentence2)]) -> [[OmdADT]] -> Result (sign1, [Named (S2 sentence2)]) Source # addOmdocToTheory :: SpanDomain cid -> SigMapI sign_symbol1 -> (sign1, [Named (S2 sentence2)]) -> [TCElement] -> Result (sign1, [Named (S2 sentence2)]) Source # sublogicOfTheo :: SpanDomain cid -> (sign1, [S2 sentence2]) -> SublogicsPair sublogics1 sublogics2 Source #

data SublogicsPair a b Source #

Constructors

SublogicsPair a b

Instances

Instances details

(MinSublogic sublogics1 (), Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2, Ord proof_tree2, Show proof_tree2, Data sentence2) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2 Source #
Instance details Defined in Logic.Morphism Methods parse_basic_sen :: SpanDomain cid -> Maybe (() -> AParser st (S2 sentence2)) Source # stability :: SpanDomain cid -> Stability Source # data_logic :: SpanDomain cid -> Maybe AnyLogic Source # top_sublogic :: SpanDomain cid -> SublogicsPair sublogics1 sublogics2 Source # all_sublogics :: SpanDomain cid -> [SublogicsPair sublogics1 sublogics2] Source # bottomSublogic :: SpanDomain cid -> Maybe (SublogicsPair sublogics1 sublogics2) Source # sublogicDimensions :: SpanDomain cid -> [[SublogicsPair sublogics1 sublogics2]] Source # parseSublogic :: SpanDomain cid -> String -> Maybe (SublogicsPair sublogics1 sublogics2) Source # proj_sublogic_epsilon :: SpanDomain cid -> SublogicsPair sublogics1 sublogics2 -> sign1 -> morphism1 Source # provers :: SpanDomain cid -> [Prover sign1 (S2 sentence2) morphism1 (SublogicsPair sublogics1 sublogics2) proof_tree2] Source # default_prover :: SpanDomain cid -> String Source # cons_checkers :: SpanDomain cid -> [ConsChecker sign1 (S2 sentence2) (SublogicsPair sublogics1 sublogics2) morphism1 proof_tree2] Source # conservativityCheck :: SpanDomain cid -> [ConservativityChecker sign1 (S2 sentence2) morphism1] Source # empty_proof_tree :: SpanDomain cid -> proof_tree2 Source # syntaxTable :: SpanDomain cid -> sign1 -> Maybe SyntaxTable Source # omdoc_metatheory :: SpanDomain cid -> Maybe OMCD Source # export_symToOmdoc :: SpanDomain cid -> NameMap sign_symbol1 -> sign_symbol1 -> String -> Result TCElement Source # export_senToOmdoc :: SpanDomain cid -> NameMap sign_symbol1 -> S2 sentence2 -> Result TCorOMElement Source # export_theoryToOmdoc :: SpanDomain cid -> SigMap sign_symbol1 -> sign1 -> [Named (S2 sentence2)] -> Result [TCElement] Source # omdocToSym :: SpanDomain cid -> SigMapI sign_symbol1 -> TCElement -> String -> Result sign_symbol1 Source # omdocToSen :: SpanDomain cid -> SigMapI sign_symbol1 -> TCElement -> String -> Result (Maybe (Named (S2 sentence2))) Source # addOMadtToTheory :: SpanDomain cid -> SigMapI sign_symbol1 -> (sign1, [Named (S2 sentence2)]) -> [[OmdADT]] -> Result (sign1, [Named (S2 sentence2)]) Source # addOmdocToTheory :: SpanDomain cid -> SigMapI sign_symbol1 -> (sign1, [Named (S2 sentence2)]) -> [TCElement] -> Result (sign1, [Named (S2 sentence2)]) Source # sublogicOfTheo :: SpanDomain cid -> (sign1, [S2 sentence2]) -> SublogicsPair sublogics1 sublogics2 Source #
(Eq a, Eq b) => Eq (SublogicsPair a b) Source #
Instance details Defined in Logic.Morphism Methods (==) :: SublogicsPair a b -> SublogicsPair a b -> Bool (/=) :: SublogicsPair a b -> SublogicsPair a b -> Bool
(Ord a, Ord b) => Ord (SublogicsPair a b) Source #
Instance details Defined in Logic.Morphism Methods compare :: SublogicsPair a b -> SublogicsPair a b -> Ordering (<) :: SublogicsPair a b -> SublogicsPair a b -> Bool (<=) :: SublogicsPair a b -> SublogicsPair a b -> Bool (>) :: SublogicsPair a b -> SublogicsPair a b -> Bool (>=) :: SublogicsPair a b -> SublogicsPair a b -> Bool max :: SublogicsPair a b -> SublogicsPair a b -> SublogicsPair a b min :: SublogicsPair a b -> SublogicsPair a b -> SublogicsPair a b
(Show a, Show b) => Show (SublogicsPair a b) Source #
Instance details Defined in Logic.Morphism Methods showsPrec :: Int -> SublogicsPair a b -> ShowS show :: SublogicsPair a b -> String showList :: [SublogicsPair a b] -> ShowS
(ShATermConvertible a, ShATermConvertible b) => ShATermConvertible (SublogicsPair a b) Source #
Instance details Defined in Logic.Morphism Methods toShATermAux :: ATermTable -> SublogicsPair a b -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SublogicsPair a b] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SublogicsPair a b) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SublogicsPair a b])
(SublogicName sublogics1, SublogicName sublogics2) => SublogicName (SublogicsPair sublogics1 sublogics2) Source #
Instance details Defined in Logic.Morphism Methods sublogicName :: SublogicsPair sublogics1 sublogics2 -> String Source #
(SemiLatticeWithTop sublogics1, SemiLatticeWithTop sublogics2) => SemiLatticeWithTop (SublogicsPair sublogics1 sublogics2) Source #
Instance details Defined in Logic.Morphism Methods lub :: SublogicsPair sublogics1 sublogics2 -> SublogicsPair sublogics1 sublogics2 -> SublogicsPair sublogics1 sublogics2 Source # top :: SublogicsPair sublogics1 sublogics2 Source #
(MinSublogic sublogics1 sign1, SemiLatticeWithTop sublogics2) => ProjectSublogicM (SublogicsPair sublogics1 sublogics2) sign1 Source #
Instance details Defined in Logic.Morphism Methods projectSublogicM :: SublogicsPair sublogics1 sublogics2 -> sign1 -> Maybe sign1 Source #
(MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2) => ProjectSublogic (SublogicsPair sublogics1 sublogics2) alpha Source #
Instance details Defined in Logic.Morphism Methods projectSublogic :: SublogicsPair sublogics1 sublogics2 -> alpha -> alpha Source #
(MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2) => MinSublogic (SublogicsPair sublogics1 sublogics2) alpha Source #
Instance details Defined in Logic.Morphism Methods minSublogic :: alpha -> SublogicsPair sublogics1 sublogics2 Source #
(SemiLatticeWithTop sublogics1, MinSublogic sublogics2 sentence2) => MinSublogic (SublogicsPair sublogics1 sublogics2) (S2 sentence2) Source #
Instance details Defined in Logic.Morphism Methods minSublogic :: S2 sentence2 -> SublogicsPair sublogics1 sublogics2 Source #

newtype S2 s Source #

Constructors

S2
Fields sentence2 :: s

Instances

Instances details

Eq s => Eq (S2 s) Source #
Instance details Defined in Logic.Morphism Methods (==) :: S2 s -> S2 s -> Bool (/=) :: S2 s -> S2 s -> Bool
Data s => Data (S2 s) Source #
Instance details Defined in Logic.Morphism Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> S2 s -> c (S2 s) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (S2 s) toConstr :: S2 s -> Constr dataTypeOf :: S2 s -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (S2 s)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (S2 s)) gmapT :: (forall b. Data b => b -> b) -> S2 s -> S2 s gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> S2 s -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> S2 s -> r gmapQ :: (forall d. Data d => d -> u) -> S2 s -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> S2 s -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> S2 s -> m (S2 s) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> S2 s -> m (S2 s) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> S2 s -> m (S2 s)
Ord s => Ord (S2 s) Source #
Instance details Defined in Logic.Morphism Methods compare :: S2 s -> S2 s -> Ordering (<) :: S2 s -> S2 s -> Bool (<=) :: S2 s -> S2 s -> Bool (>) :: S2 s -> S2 s -> Bool (>=) :: S2 s -> S2 s -> Bool max :: S2 s -> S2 s -> S2 s min :: S2 s -> S2 s -> S2 s
Show s => Show (S2 s) Source #
Instance details Defined in Logic.Morphism Methods showsPrec :: Int -> S2 s -> ShowS show :: S2 s -> String showList :: [S2 s] -> ShowS
Generic (S2 s) Source #
Instance details Defined in Logic.Morphism Associated Types type Rep (S2 s) :: Type -> Type Methods from :: S2 s -> Rep (S2 s) x to :: Rep (S2 s) x -> S2 s
GetRange s => GetRange (S2 s) Source #
Instance details Defined in Logic.Morphism Methods getRange :: S2 s -> Range Source # rangeSpan :: S2 s -> [Pos] Source #
ShATermConvertible s => ShATermConvertible (S2 s) Source #
Instance details Defined in Logic.Morphism Methods toShATermAux :: ATermTable -> S2 s -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [S2 s] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, S2 s) fromShATermList' :: Int -> ATermTable -> (ATermTable, [S2 s])
Pretty s => Pretty (S2 s) Source #
Instance details Defined in Logic.Morphism Methods pretty :: S2 s -> Doc Source # pretties :: [S2 s] -> Doc Source #
Data a => ToXml (S2 a) Source #
Instance details Defined in Logic.Morphism Methods asXml :: S2 a -> Element Source #
Data a => ToJson (S2 a) Source #
Instance details Defined in Logic.Morphism Methods asJson :: S2 a -> Json Source #
(Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2, Ord symbol1, GetRange symbol1, Pretty symbol1, Typeable symbol1, Data sentence2) => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 Source #
Instance details Defined in Logic.Morphism Methods basic_analysis :: SpanDomain cid -> Maybe (((), sign1, GlobalAnnos) -> Result ((), ExtSign sign1 sign_symbol1, [Named (S2 sentence2)])) Source # sen_analysis :: SpanDomain cid -> Maybe (((), sign1, S2 sentence2) -> Result (S2 sentence2)) Source # extBasicAnalysis :: SpanDomain cid -> IRI -> LibName -> () -> sign1 -> GlobalAnnos -> Result ((), ExtSign sign1 sign_symbol1, [Named (S2 sentence2)]) Source # stat_symb_map_items :: SpanDomain cid -> sign1 -> Maybe sign1 -> [()] -> Result (EndoMap symbol1) Source # stat_symb_items :: SpanDomain cid -> sign1 -> [()] -> Result [symbol1] Source # convertTheory :: SpanDomain cid -> Maybe ((sign1, [Named (S2 sentence2)]) -> ()) Source # ensures_amalgamability :: SpanDomain cid -> ([CASLAmalgOpt], Gr sign1 (Int, morphism1), [(Int, morphism1)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: SpanDomain cid -> morphism1 -> [Named (S2 sentence2)] -> Result (sign1, [Named (S2 sentence2)]) Source # signature_colimit :: SpanDomain cid -> Gr sign1 (Int, morphism1) -> Result (sign1, Map Int morphism1) Source # qualify :: SpanDomain cid -> SIMPLE_ID -> LibName -> morphism1 -> sign1 -> Result (morphism1, [Named (S2 sentence2)]) Source # symbol_to_raw :: SpanDomain cid -> sign_symbol1 -> symbol1 Source # id_to_raw :: SpanDomain cid -> Id -> symbol1 Source # matches :: SpanDomain cid -> sign_symbol1 -> symbol1 -> Bool Source # empty_signature :: SpanDomain cid -> sign1 Source # add_symb_to_sign :: SpanDomain cid -> sign1 -> sign_symbol1 -> Result sign1 Source # signature_union :: SpanDomain cid -> sign1 -> sign1 -> Result sign1 Source # signatureDiff :: SpanDomain cid -> sign1 -> sign1 -> Result sign1 Source # intersection :: SpanDomain cid -> sign1 -> sign1 -> Result sign1 Source # final_union :: SpanDomain cid -> sign1 -> sign1 -> Result sign1 Source # morphism_union :: SpanDomain cid -> morphism1 -> morphism1 -> Result morphism1 Source # is_subsig :: SpanDomain cid -> sign1 -> sign1 -> Bool Source # subsig_inclusion :: SpanDomain cid -> sign1 -> sign1 -> Result morphism1 Source # generated_sign :: SpanDomain cid -> Set sign_symbol1 -> sign1 -> Result morphism1 Source # cogenerated_sign :: SpanDomain cid -> Set sign_symbol1 -> sign1 -> Result morphism1 Source # induced_from_morphism :: SpanDomain cid -> EndoMap symbol1 -> sign1 -> Result morphism1 Source # induced_from_to_morphism :: SpanDomain cid -> EndoMap symbol1 -> ExtSign sign1 sign_symbol1 -> ExtSign sign1 sign_symbol1 -> Result morphism1 Source # is_transportable :: SpanDomain cid -> morphism1 -> Bool Source # is_injective :: SpanDomain cid -> morphism1 -> Bool Source # theory_to_taxonomy :: SpanDomain cid -> TaxoGraphKind -> MMiSSOntology -> sign1 -> [Named (S2 sentence2)] -> Result MMiSSOntology Source # corresp2th :: SpanDomain cid -> String -> Bool -> sign1 -> sign1 -> [()] -> [()] -> EndoMap sign_symbol1 -> EndoMap sign_symbol1 -> REL_REF -> Result (sign1, [Named (S2 sentence2)], sign1, sign1, EndoMap sign_symbol1, EndoMap sign_symbol1) Source # equiv2cospan :: SpanDomain cid -> sign1 -> sign1 -> [()] -> [()] -> Result (sign1, sign1, sign1, EndoMap sign_symbol1, EndoMap sign_symbol1) Source # extract_module :: SpanDomain cid -> [IRI] -> (sign1, [Named (S2 sentence2)]) -> Result (sign1, [Named (S2 sentence2)]) Source #
(Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2, Category sign1 morphism1, Ord sign_symbol1, GetRange sign_symbol1, Data sentence2) => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1 sign_symbol1 Source #
Instance details Defined in Logic.Morphism Methods map_sen :: SpanDomain cid -> morphism1 -> S2 sentence2 -> Result (S2 sentence2) Source # simplify_sen :: SpanDomain cid -> sign1 -> S2 sentence2 -> S2 sentence2 Source # negation :: SpanDomain cid -> S2 sentence2 -> Maybe (S2 sentence2) Source # print_sign :: SpanDomain cid -> sign1 -> Doc Source # print_named :: SpanDomain cid -> Named (S2 sentence2) -> Doc Source # sym_of :: SpanDomain cid -> sign1 -> [Set sign_symbol1] Source # mostSymsOf :: SpanDomain cid -> sign1 -> [sign_symbol1] Source # symmap_of :: SpanDomain cid -> morphism1 -> EndoMap sign_symbol1 Source # sym_name :: SpanDomain cid -> sign_symbol1 -> Id Source # sym_label :: SpanDomain cid -> sign_symbol1 -> Maybe String Source # fullSymName :: SpanDomain cid -> sign_symbol1 -> String Source # symKind :: SpanDomain cid -> sign_symbol1 -> String Source # symsOfSen :: SpanDomain cid -> sign1 -> S2 sentence2 -> [sign_symbol1] Source # pair_symbols :: SpanDomain cid -> sign_symbol1 -> sign_symbol1 -> Result sign_symbol1 Source #
(MinSublogic sublogics1 (), Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2, Ord proof_tree2, Show proof_tree2, Data sentence2) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2 Source #
Instance details Defined in Logic.Morphism Methods parse_basic_sen :: SpanDomain cid -> Maybe (() -> AParser st (S2 sentence2)) Source # stability :: SpanDomain cid -> Stability Source # data_logic :: SpanDomain cid -> Maybe AnyLogic Source # top_sublogic :: SpanDomain cid -> SublogicsPair sublogics1 sublogics2 Source # all_sublogics :: SpanDomain cid -> [SublogicsPair sublogics1 sublogics2] Source # bottomSublogic :: SpanDomain cid -> Maybe (SublogicsPair sublogics1 sublogics2) Source # sublogicDimensions :: SpanDomain cid -> [[SublogicsPair sublogics1 sublogics2]] Source # parseSublogic :: SpanDomain cid -> String -> Maybe (SublogicsPair sublogics1 sublogics2) Source # proj_sublogic_epsilon :: SpanDomain cid -> SublogicsPair sublogics1 sublogics2 -> sign1 -> morphism1 Source # provers :: SpanDomain cid -> [Prover sign1 (S2 sentence2) morphism1 (SublogicsPair sublogics1 sublogics2) proof_tree2] Source # default_prover :: SpanDomain cid -> String Source # cons_checkers :: SpanDomain cid -> [ConsChecker sign1 (S2 sentence2) (SublogicsPair sublogics1 sublogics2) morphism1 proof_tree2] Source # conservativityCheck :: SpanDomain cid -> [ConservativityChecker sign1 (S2 sentence2) morphism1] Source # empty_proof_tree :: SpanDomain cid -> proof_tree2 Source # syntaxTable :: SpanDomain cid -> sign1 -> Maybe SyntaxTable Source # omdoc_metatheory :: SpanDomain cid -> Maybe OMCD Source # export_symToOmdoc :: SpanDomain cid -> NameMap sign_symbol1 -> sign_symbol1 -> String -> Result TCElement Source # export_senToOmdoc :: SpanDomain cid -> NameMap sign_symbol1 -> S2 sentence2 -> Result TCorOMElement Source # export_theoryToOmdoc :: SpanDomain cid -> SigMap sign_symbol1 -> sign1 -> [Named (S2 sentence2)] -> Result [TCElement] Source # omdocToSym :: SpanDomain cid -> SigMapI sign_symbol1 -> TCElement -> String -> Result sign_symbol1 Source # omdocToSen :: SpanDomain cid -> SigMapI sign_symbol1 -> TCElement -> String -> Result (Maybe (Named (S2 sentence2))) Source # addOMadtToTheory :: SpanDomain cid -> SigMapI sign_symbol1 -> (sign1, [Named (S2 sentence2)]) -> [[OmdADT]] -> Result (sign1, [Named (S2 sentence2)]) Source # addOmdocToTheory :: SpanDomain cid -> SigMapI sign_symbol1 -> (sign1, [Named (S2 sentence2)]) -> [TCElement] -> Result (sign1, [Named (S2 sentence2)]) Source # sublogicOfTheo :: SpanDomain cid -> (sign1, [S2 sentence2]) -> SublogicsPair sublogics1 sublogics2 Source #
(SemiLatticeWithTop sublogics1, MinSublogic sublogics2 sentence2) => MinSublogic (SublogicsPair sublogics1 sublogics2) (S2 sentence2) Source #
Instance details Defined in Logic.Morphism Methods minSublogic :: S2 sentence2 -> SublogicsPair sublogics1 sublogics2 Source #
type Rep (S2 s) Source #
Instance details Defined in Logic.Morphism type Rep (S2 s) = D1 ('MetaData "S2" "Logic.Morphism" "main" 'True) (C1 ('MetaCons "S2" 'PrefixI 'True) (S1 ('MetaSel ('Just "sentence2") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 s)))

Morphisms

data AnyMorphism Source #

Existential type for morphisms

Constructors

forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2.Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => Morphism cid

Instances

Instances details

Show AnyMorphism Source #
Instance details Defined in Logic.Morphism Methods showsPrec :: Int -> AnyMorphism -> ShowS show :: AnyMorphism -> String showList :: [AnyMorphism] -> ShowS