Hets - the Heterogeneous Tool Set

Copyright(c) Till Mossakowski Uni Bremen 2002-2004
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable (via Logic)
Safe HaskellNone

Logic.Morphism

Contents

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 #

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 # 

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

(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 #

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 #

(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

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 #

(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