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

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 #

Minimal complete definition

morSourceLogic, morSourceSublogic, morTargetLogic, morTargetSublogic, morMapSublogicSign, morMapSublogicSen, morMap_sign, morMap_morphism, morMap_sentence, morMap_sign_symbol

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

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 #

data IdMorphism lid sublogics Source #

identity morphisms

Constructors

IdMorphism lid sublogics

Instances

(Show sublogics, Show lid) => Show (IdMorphism lid sublogics) Source #
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 #
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 #
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

Minimal complete definition

indMorMap_sign, indMorMap_morphism, epsilon

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

Eq cid => Eq (SpanDomain cid) Source #
Methods (==) :: SpanDomain cid -> SpanDomain cid -> Bool (/=) :: SpanDomain cid -> SpanDomain cid -> Bool
Show cid => Show (SpanDomain cid) Source #
Methods showsPrec :: Int -> SpanDomain cid -> ShowS show :: SpanDomain cid -> String showList :: [SpanDomain cid] -> ShowS
Language cid => Language (SpanDomain cid) Source #
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 #
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 (AParser st ()) Source # parse_symb_items :: SpanDomain cid -> Maybe (AParser st ()) Source # parse_symb_map_items :: SpanDomain cid -> Maybe (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) => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 Source #
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) => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1 sign_symbol1 Source #
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) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2 Source #
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

(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) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2 Source #
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 b, Eq a) => Eq (SublogicsPair a b) Source #
Methods (==) :: SublogicsPair a b -> SublogicsPair a b -> Bool (/=) :: SublogicsPair a b -> SublogicsPair a b -> Bool
(Ord b, Ord a) => Ord (SublogicsPair a b) Source #
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 b, Show a) => Show (SublogicsPair a b) Source #
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 #
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 #
Methods sublogicName :: SublogicsPair sublogics1 sublogics2 -> String Source #
(SemiLatticeWithTop sublogics1, SemiLatticeWithTop sublogics2) => SemiLatticeWithTop (SublogicsPair sublogics1 sublogics2) Source #
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 #
Methods projectSublogicM :: SublogicsPair sublogics1 sublogics2 -> sign1 -> Maybe sign1 Source #
(MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2) => ProjectSublogic (SublogicsPair sublogics1 sublogics2) alpha Source #
Methods projectSublogic :: SublogicsPair sublogics1 sublogics2 -> alpha -> alpha Source #
(MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2) => MinSublogic (SublogicsPair sublogics1 sublogics2) alpha Source #
Methods minSublogic :: alpha -> SublogicsPair sublogics1 sublogics2 Source #
(SemiLatticeWithTop sublogics1, MinSublogic sublogics2 sentence2) => MinSublogic (SublogicsPair sublogics1 sublogics2) (S2 sentence2) Source #
Methods minSublogic :: S2 sentence2 -> SublogicsPair sublogics1 sublogics2 Source #

newtype S2 s Source #

Constructors

S2
Fields sentence2 :: s

Instances

Eq s => Eq (S2 s) Source #
Methods (==) :: S2 s -> S2 s -> Bool (/=) :: S2 s -> S2 s -> Bool
Data s => Data (S2 s) Source #
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 :: (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 #
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 #
Methods showsPrec :: Int -> S2 s -> ShowS show :: S2 s -> String showList :: [S2 s] -> ShowS
ShATermConvertible s => ShATermConvertible (S2 s) Source #
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])
GetRange s => GetRange (S2 s) Source #
Methods getRange :: S2 s -> Range Source # rangeSpan :: S2 s -> [Pos] Source #
Pretty s => Pretty (S2 s) Source #
Methods pretty :: S2 s -> Doc Source # pretties :: [S2 s] -> Doc Source #
ToJson s => ToJson (S2 s) Source #
Methods asJson :: S2 s -> Json Source #
ToXml s => ToXml (S2 s) Source #
Methods asXml :: S2 s -> Element 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) => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 Source #
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) => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1 sign_symbol1 Source #
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) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2 Source #
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 #
Methods minSublogic :: S2 sentence2 -> SublogicsPair sublogics1 sublogics2 Source #

Morphisms

data AnyMorphism Source #

Existential type for morphisms

Constructors

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

Show AnyMorphism Source #
Methods showsPrec :: Int -> AnyMorphism -> ShowS show :: AnyMorphism -> String showList :: [AnyMorphism] -> ShowS