Copyright	(c) Pascal Schmidt C. Maeder and Uni Bremen 2002-2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	experimental
Portability	portable
Safe Haskell	None

CASL.Sublogic

Contents

types
class
predicates on CASL_SL
functions for SemiLatticeWithTop instance
functions for the creation of minimal sublogics
functions for Logic instance sublogic to string conversion
- list of all sublogics
computes the sublogic of a given element
projects an element into a given sublogic

Description

Sublogic analysis for CASL

This module provides the sublogic functions (as required by Logic.hs) for CASL. The functions allow to compute the minimal sublogics needed by a given element, to check whether an item is part of a given sublogic, and to project an element into a given sublogic.

Synopsis

type CASL_Sublogics = CASL_SL ()
data CASL_SL a = CASL_SL {
- sub_features :: SubsortingFeatures
- has_part :: Bool
- cons_features :: SortGenerationFeatures
- has_eq :: Bool
- has_pred :: Bool
- which_logic :: CASL_Formulas
- has_empty_sorts :: Bool
- ext_features :: a
}
data CASL_Formulas
- = Atomic
- | Horn
- | GHorn
- | Prenex
- | FOL
- | SOL
data SubsortingFeatures
- = NoSub
- | LocFilSub
- | Sub
data SortGenerationFeatures
- = NoSortGen
- | SortGen {
  - emptyMapping :: Bool
  - onlyInjConstrs :: Bool
  }
class (Ord l, Show l) => Lattice l where
- cjoin :: l -> l -> l
- ctop :: l
- bot :: l
has_sub :: CASL_SL a -> Bool
has_cons :: CASL_SL a -> Bool
mkTop :: a -> CASL_SL a
top :: Lattice a => CASL_SL a
caslTop :: Lattice a => CASL_SL a
cFol :: Lattice a => CASL_SL a
fol :: Lattice a => CASL_SL a
cPrenex :: Lattice a => CASL_SL a
sublogics_max :: Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
comp_list :: Lattice a => [CASL_SL a] -> CASL_SL a
bottom :: Lattice a => CASL_SL a
mkBot :: a -> CASL_SL a
emptyMapConsFeature :: SortGenerationFeatures
need_sub :: Lattice a => CASL_SL a
need_pred :: Lattice a => CASL_SL a
need_horn :: Lattice a => CASL_SL a
need_fol :: Lattice a => CASL_SL a
updExtFeature :: (a -> a) -> CASL_SL a -> CASL_SL a
sublogics_name :: (a -> String) -> CASL_SL a -> String
parseSL :: (String -> Maybe (a, String)) -> String -> Maybe (CASL_SL a)
parseBool :: String -> String -> (Bool, String)
sublogics_all :: Lattice a => [a] -> [CASL_SL a]
sDims :: Lattice a => [[a]] -> [[CASL_SL a]]
sl_sig_items :: Lattice a => (s -> CASL_SL a) -> (f -> CASL_SL a) -> SIG_ITEMS s f -> CASL_SL a
sl_basic_spec :: Lattice a => (b -> CASL_SL a) -> (s -> CASL_SL a) -> (f -> CASL_SL a) -> BASIC_SPEC b s f -> CASL_SL a
sl_opkind :: Lattice a => OpKind -> CASL_SL a
sl_op_type :: Lattice a => OP_TYPE -> CASL_SL a
sl_op_item :: Lattice a => (f -> CASL_SL a) -> OP_ITEM f -> CASL_SL a
sl_pred_item :: Lattice a => (f -> CASL_SL a) -> PRED_ITEM f -> CASL_SL a
sl_sentence :: Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
sl_term :: Lattice a => (f -> CASL_SL a) -> TERM f -> CASL_SL a
sl_symb_items :: Lattice a => SYMB_ITEMS -> CASL_SL a
sl_symb_map_items :: Lattice a => SYMB_MAP_ITEMS -> CASL_SL a
sl_sign :: Lattice a => (e -> CASL_SL a) -> Sign f e -> CASL_SL a
sl_morphism :: Lattice a => (e -> CASL_SL a) -> Morphism f e m -> CASL_SL a
sl_symbol :: Lattice a => Symbol -> CASL_SL a
pr_basic_spec :: Lattice a => (CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT])) -> (CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])) -> (CASL_SL a -> f -> Maybe (FORMULA f)) -> CASL_SL a -> BASIC_SPEC b s f -> BASIC_SPEC b s f
pr_symb_items :: Lattice a => CASL_SL a -> SYMB_ITEMS -> Maybe SYMB_ITEMS
pr_symb_map_items :: Lattice a => CASL_SL a -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
pr_sign :: CASL_SL a -> Sign f e -> Sign f e
pr_morphism :: Lattice a => CASL_SL a -> Morphism f e m -> Morphism f e m
pr_epsilon :: m -> CASL_SL a -> Sign f e -> Morphism f e m
pr_symbol :: Lattice a => CASL_SL a -> Symbol -> Maybe Symbol

types

type CASL_Sublogics = CASL_SL () Source #

data CASL_SL a Source #

Constructors

CASL_SL
Fields sub_features :: SubsortingFeatures subsorting has_part :: Bool partiality cons_features :: SortGenerationFeatures sort generation constraints has_eq :: Bool equality has_pred :: Bool predicates which_logic :: CASL_Formulas first order sublogics has_empty_sorts :: Bool may sorts be empty ext_features :: a features of extension

Instances

Instances details

Logic CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in CASL.Logic_CASL Methods parse_basic_sen :: CASL -> Maybe (CASLBasicSpec -> AParser st CASLFORMULA) Source # stability :: CASL -> Stability Source # data_logic :: CASL -> Maybe AnyLogic Source # top_sublogic :: CASL -> CASL_Sublogics Source # all_sublogics :: CASL -> [CASL_Sublogics] Source # bottomSublogic :: CASL -> Maybe CASL_Sublogics Source # sublogicDimensions :: CASL -> [[CASL_Sublogics]] Source # parseSublogic :: CASL -> String -> Maybe CASL_Sublogics Source # proj_sublogic_epsilon :: CASL -> CASL_Sublogics -> CASLSign -> CASLMor Source # provers :: CASL -> [Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree] Source # default_prover :: CASL -> String Source # cons_checkers :: CASL -> [ConsChecker CASLSign CASLFORMULA CASL_Sublogics CASLMor ProofTree] Source # conservativityCheck :: CASL -> [ConservativityChecker CASLSign CASLFORMULA CASLMor] Source # empty_proof_tree :: CASL -> ProofTree Source # syntaxTable :: CASL -> CASLSign -> Maybe SyntaxTable Source # omdoc_metatheory :: CASL -> Maybe OMCD Source # export_symToOmdoc :: CASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: CASL -> NameMap Symbol -> CASLFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: CASL -> SigMap Symbol -> CASLSign -> [Named CASLFORMULA] -> Result [TCElement] Source # omdocToSym :: CASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: CASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CASLFORMULA)) Source # addOMadtToTheory :: CASL -> SigMapI Symbol -> (CASLSign, [Named CASLFORMULA]) -> [[OmdADT]] -> Result (CASLSign, [Named CASLFORMULA]) Source # addOmdocToTheory :: CASL -> SigMapI Symbol -> (CASLSign, [Named CASLFORMULA]) -> [TCElement] -> Result (CASLSign, [Named CASLFORMULA]) Source # sublogicOfTheo :: CASL -> (CASLSign, [CASLFORMULA]) -> CASL_Sublogics Source #
Logic ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Instance details Defined in ExtModal.Logic_ExtModal Methods parse_basic_sen :: ExtModal -> Maybe (EM_BASIC_SPEC -> AParser st ExtModalFORMULA) Source # stability :: ExtModal -> Stability Source # data_logic :: ExtModal -> Maybe AnyLogic Source # top_sublogic :: ExtModal -> ExtModalSL Source # all_sublogics :: ExtModal -> [ExtModalSL] Source # bottomSublogic :: ExtModal -> Maybe ExtModalSL Source # sublogicDimensions :: ExtModal -> [[ExtModalSL]] Source # parseSublogic :: ExtModal -> String -> Maybe ExtModalSL Source # proj_sublogic_epsilon :: ExtModal -> ExtModalSL -> ExtModalSign -> ExtModalMorph Source # provers :: ExtModal -> [Prover ExtModalSign ExtModalFORMULA ExtModalMorph ExtModalSL ()] Source # default_prover :: ExtModal -> String Source # cons_checkers :: ExtModal -> [ConsChecker ExtModalSign ExtModalFORMULA ExtModalSL ExtModalMorph ()] Source # conservativityCheck :: ExtModal -> [ConservativityChecker ExtModalSign ExtModalFORMULA ExtModalMorph] Source # empty_proof_tree :: ExtModal -> () Source # syntaxTable :: ExtModal -> ExtModalSign -> Maybe SyntaxTable Source # omdoc_metatheory :: ExtModal -> Maybe OMCD Source # export_symToOmdoc :: ExtModal -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: ExtModal -> NameMap Symbol -> ExtModalFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: ExtModal -> SigMap Symbol -> ExtModalSign -> [Named ExtModalFORMULA] -> Result [TCElement] Source # omdocToSym :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ExtModalFORMULA)) Source # addOMadtToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [[OmdADT]] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # addOmdocToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [TCElement] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # sublogicOfTheo :: ExtModal -> (ExtModalSign, [ExtModalFORMULA]) -> ExtModalSL Source #
Logic ConstraintCASL CASL_Sublogics ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol () Source #
Instance details Defined in ConstraintCASL.Logic_ConstraintCASL Methods parse_basic_sen :: ConstraintCASL -> Maybe (ConstraintCASLBasicSpec -> AParser st ConstraintCASLFORMULA) Source # stability :: ConstraintCASL -> Stability Source # data_logic :: ConstraintCASL -> Maybe AnyLogic Source # top_sublogic :: ConstraintCASL -> CASL_Sublogics Source # all_sublogics :: ConstraintCASL -> [CASL_Sublogics] Source # bottomSublogic :: ConstraintCASL -> Maybe CASL_Sublogics Source # sublogicDimensions :: ConstraintCASL -> [[CASL_Sublogics]] Source # parseSublogic :: ConstraintCASL -> String -> Maybe CASL_Sublogics Source # proj_sublogic_epsilon :: ConstraintCASL -> CASL_Sublogics -> ConstraintCASLSign -> ConstraintCASLMor Source # provers :: ConstraintCASL -> [Prover ConstraintCASLSign ConstraintCASLFORMULA ConstraintCASLMor CASL_Sublogics ()] Source # default_prover :: ConstraintCASL -> String Source # cons_checkers :: ConstraintCASL -> [ConsChecker ConstraintCASLSign ConstraintCASLFORMULA CASL_Sublogics ConstraintCASLMor ()] Source # conservativityCheck :: ConstraintCASL -> [ConservativityChecker ConstraintCASLSign ConstraintCASLFORMULA ConstraintCASLMor] Source # empty_proof_tree :: ConstraintCASL -> () Source # syntaxTable :: ConstraintCASL -> ConstraintCASLSign -> Maybe SyntaxTable Source # omdoc_metatheory :: ConstraintCASL -> Maybe OMCD Source # export_symToOmdoc :: ConstraintCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: ConstraintCASL -> NameMap Symbol -> ConstraintCASLFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: ConstraintCASL -> SigMap Symbol -> ConstraintCASLSign -> [Named ConstraintCASLFORMULA] -> Result [TCElement] Source # omdocToSym :: ConstraintCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: ConstraintCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ConstraintCASLFORMULA)) Source # addOMadtToTheory :: ConstraintCASL -> SigMapI Symbol -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> [[OmdADT]] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source # addOmdocToTheory :: ConstraintCASL -> SigMapI Symbol -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> [TCElement] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source # sublogicOfTheo :: ConstraintCASL -> (ConstraintCASLSign, [ConstraintCASLFORMULA]) -> CASL_Sublogics Source #
Logic CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods parse_basic_sen :: CoCASL -> Maybe (C_BASIC_SPEC -> AParser st CoCASLFORMULA) Source # stability :: CoCASL -> Stability Source # data_logic :: CoCASL -> Maybe AnyLogic Source # top_sublogic :: CoCASL -> CoCASL_Sublogics Source # all_sublogics :: CoCASL -> [CoCASL_Sublogics] Source # bottomSublogic :: CoCASL -> Maybe CoCASL_Sublogics Source # sublogicDimensions :: CoCASL -> [[CoCASL_Sublogics]] Source # parseSublogic :: CoCASL -> String -> Maybe CoCASL_Sublogics Source # proj_sublogic_epsilon :: CoCASL -> CoCASL_Sublogics -> CSign -> CoCASLMor Source # provers :: CoCASL -> [Prover CSign CoCASLFORMULA CoCASLMor CoCASL_Sublogics ()] Source # default_prover :: CoCASL -> String Source # cons_checkers :: CoCASL -> [ConsChecker CSign CoCASLFORMULA CoCASL_Sublogics CoCASLMor ()] Source # conservativityCheck :: CoCASL -> [ConservativityChecker CSign CoCASLFORMULA CoCASLMor] Source # empty_proof_tree :: CoCASL -> () Source # syntaxTable :: CoCASL -> CSign -> Maybe SyntaxTable Source # omdoc_metatheory :: CoCASL -> Maybe OMCD Source # export_symToOmdoc :: CoCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: CoCASL -> NameMap Symbol -> CoCASLFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: CoCASL -> SigMap Symbol -> CSign -> [Named CoCASLFORMULA] -> Result [TCElement] Source # omdocToSym :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CoCASLFORMULA)) Source # addOMadtToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [[OmdADT]] -> Result (CSign, [Named CoCASLFORMULA]) Source # addOmdocToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [TCElement] -> Result (CSign, [Named CoCASLFORMULA]) Source # sublogicOfTheo :: CoCASL -> (CSign, [CoCASLFORMULA]) -> CoCASL_Sublogics Source #
Comorphism OWL22CASL OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in OWL2.OWL22CASL Methods sourceLogic :: OWL22CASL -> OWL2 Source # sourceSublogic :: OWL22CASL -> ProfSub Source # sourceSublogicLossy :: OWL22CASL -> ProfSub Source # minSourceTheory :: OWL22CASL -> Maybe (LibName, String) Source # targetLogic :: OWL22CASL -> CASL Source # mapSublogic :: OWL22CASL -> ProfSub -> Maybe CASL_Sublogics Source # map_theory :: OWL22CASL -> (Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: OWL22CASL -> (Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: OWL22CASL -> OWLMorphism -> Result CASLMor Source # map_sentence :: OWL22CASL -> Sign -> Axiom -> Result CASLFORMULA Source # map_symbol :: OWL22CASL -> Sign -> Entity -> Set Symbol Source # extractModel :: OWL22CASL -> Sign -> ProofTree -> Result (Sign, [Named Axiom]) Source # is_model_transportable :: OWL22CASL -> Bool Source # has_model_expansion :: OWL22CASL -> Bool Source # is_weakly_amalgamable :: OWL22CASL -> Bool Source # constituents :: OWL22CASL -> [String] Source # isInclusionComorphism :: OWL22CASL -> Bool Source # rps :: OWL22CASL -> Bool Source # eps :: OWL22CASL -> Bool Source # isGTC :: OWL22CASL -> Bool Source #
Comorphism CASL2OWL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source #
Instance details Defined in OWL2.CASL2OWL Methods sourceLogic :: CASL2OWL -> CASL Source # sourceSublogic :: CASL2OWL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2OWL -> CASL_Sublogics Source # minSourceTheory :: CASL2OWL -> Maybe (LibName, String) Source # targetLogic :: CASL2OWL -> OWL2 Source # mapSublogic :: CASL2OWL -> CASL_Sublogics -> Maybe ProfSub Source # map_theory :: CASL2OWL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Axiom]) Source # mapMarkedTheory :: CASL2OWL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Axiom]) Source # map_morphism :: CASL2OWL -> CASLMor -> Result OWLMorphism Source # map_sentence :: CASL2OWL -> CASLSign -> CASLFORMULA -> Result Axiom Source # map_symbol :: CASL2OWL -> CASLSign -> Symbol -> Set Entity Source # extractModel :: CASL2OWL -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2OWL -> Bool Source # has_model_expansion :: CASL2OWL -> Bool Source # is_weakly_amalgamable :: CASL2OWL -> Bool Source # constituents :: CASL2OWL -> [String] Source # isInclusionComorphism :: CASL2OWL -> Bool Source # rps :: CASL2OWL -> Bool Source # eps :: CASL2OWL -> Bool Source # isGTC :: CASL2OWL -> Bool Source #
Comorphism ExtModal2OWL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source #
Instance details Defined in Comorphisms.ExtModal2OWL Methods sourceLogic :: ExtModal2OWL -> ExtModal Source # sourceSublogic :: ExtModal2OWL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2OWL -> ExtModalSL Source # minSourceTheory :: ExtModal2OWL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2OWL -> OWL2 Source # mapSublogic :: ExtModal2OWL -> ExtModalSL -> Maybe ProfSub Source # map_theory :: ExtModal2OWL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Sign, [Named Axiom]) Source # mapMarkedTheory :: ExtModal2OWL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Sign, [Named Axiom]) Source # map_morphism :: ExtModal2OWL -> ExtModalMorph -> Result OWLMorphism Source # map_sentence :: ExtModal2OWL -> ExtModalSign -> ExtModalFORMULA -> Result Axiom Source # map_symbol :: ExtModal2OWL -> ExtModalSign -> Symbol -> Set Entity Source # extractModel :: ExtModal2OWL -> ExtModalSign -> ProofTree -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2OWL -> Bool Source # has_model_expansion :: ExtModal2OWL -> Bool Source # is_weakly_amalgamable :: ExtModal2OWL -> Bool Source # constituents :: ExtModal2OWL -> [String] Source # isInclusionComorphism :: ExtModal2OWL -> Bool Source # rps :: ExtModal2OWL -> Bool Source # eps :: ExtModal2OWL -> Bool Source # isGTC :: ExtModal2OWL -> Bool Source #
Comorphism RelScheme2CASL RelScheme () RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.RelScheme2CASL Methods sourceLogic :: RelScheme2CASL -> RelScheme Source # sourceSublogic :: RelScheme2CASL -> () Source # sourceSublogicLossy :: RelScheme2CASL -> () Source # minSourceTheory :: RelScheme2CASL -> Maybe (LibName, String) Source # targetLogic :: RelScheme2CASL -> CASL Source # mapSublogic :: RelScheme2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: RelScheme2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: RelScheme2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: RelScheme2CASL -> RSMorphism -> Result CASLMor Source # map_sentence :: RelScheme2CASL -> Sign -> Sentence -> Result CASLFORMULA Source # map_symbol :: RelScheme2CASL -> Sign -> RSSymbol -> Set Symbol Source # extractModel :: RelScheme2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source # is_model_transportable :: RelScheme2CASL -> Bool Source # has_model_expansion :: RelScheme2CASL -> Bool Source # is_weakly_amalgamable :: RelScheme2CASL -> Bool Source # constituents :: RelScheme2CASL -> [String] Source # isInclusionComorphism :: RelScheme2CASL -> Bool Source # rps :: RelScheme2CASL -> Bool Source # eps :: RelScheme2CASL -> Bool Source # isGTC :: RelScheme2CASL -> Bool Source #
Comorphism Prop2CASL Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.Prop2CASL Methods sourceLogic :: Prop2CASL -> Propositional Source # sourceSublogic :: Prop2CASL -> PropSL Source # sourceSublogicLossy :: Prop2CASL -> PropSL Source # minSourceTheory :: Prop2CASL -> Maybe (LibName, String) Source # targetLogic :: Prop2CASL -> CASL Source # mapSublogic :: Prop2CASL -> PropSL -> Maybe CASL_Sublogics Source # map_theory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: Prop2CASL -> Morphism -> Result CASLMor Source # map_sentence :: Prop2CASL -> Sign -> FORMULA -> Result CASLFORMULA Source # map_symbol :: Prop2CASL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: Prop2CASL -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source # is_model_transportable :: Prop2CASL -> Bool Source # has_model_expansion :: Prop2CASL -> Bool Source # is_weakly_amalgamable :: Prop2CASL -> Bool Source # constituents :: Prop2CASL -> [String] Source # isInclusionComorphism :: Prop2CASL -> Bool Source # rps :: Prop2CASL -> Bool Source # eps :: Prop2CASL -> Bool Source # isGTC :: Prop2CASL -> Bool Source #
Comorphism Modal2CASL Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.Modal2CASL Methods sourceLogic :: Modal2CASL -> Modal Source # sourceSublogic :: Modal2CASL -> () Source # sourceSublogicLossy :: Modal2CASL -> () Source # minSourceTheory :: Modal2CASL -> Maybe (LibName, String) Source # targetLogic :: Modal2CASL -> CASL Source # mapSublogic :: Modal2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: Modal2CASL -> (MSign, [Named ModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: Modal2CASL -> (MSign, [Named ModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: Modal2CASL -> ModalMor -> Result CASLMor Source # map_sentence :: Modal2CASL -> MSign -> ModalFORMULA -> Result CASLFORMULA Source # map_symbol :: Modal2CASL -> MSign -> Symbol -> Set Symbol Source # extractModel :: Modal2CASL -> MSign -> ProofTree -> Result (MSign, [Named ModalFORMULA]) Source # is_model_transportable :: Modal2CASL -> Bool Source # has_model_expansion :: Modal2CASL -> Bool Source # is_weakly_amalgamable :: Modal2CASL -> Bool Source # constituents :: Modal2CASL -> [String] Source # isInclusionComorphism :: Modal2CASL -> Bool Source # rps :: Modal2CASL -> Bool Source # eps :: Modal2CASL -> Bool Source # isGTC :: Modal2CASL -> Bool Source #
Comorphism Maude2CASL Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.Maude2CASL Methods sourceLogic :: Maude2CASL -> Maude Source # sourceSublogic :: Maude2CASL -> () Source # sourceSublogicLossy :: Maude2CASL -> () Source # minSourceTheory :: Maude2CASL -> Maybe (LibName, String) Source # targetLogic :: Maude2CASL -> CASL Source # mapSublogic :: Maude2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: Maude2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: Maude2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: Maude2CASL -> Morphism -> Result CASLMor Source # map_sentence :: Maude2CASL -> Sign -> Sentence -> Result CASLFORMULA Source # map_symbol :: Maude2CASL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: Maude2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source # is_model_transportable :: Maude2CASL -> Bool Source # has_model_expansion :: Maude2CASL -> Bool Source # is_weakly_amalgamable :: Maude2CASL -> Bool Source # constituents :: Maude2CASL -> [String] Source # isInclusionComorphism :: Maude2CASL -> Bool Source # rps :: Maude2CASL -> Bool Source # eps :: Maude2CASL -> Bool Source # isGTC :: Maude2CASL -> Bool Source #
Comorphism ExtModal2CASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.ExtModal2CASL Methods sourceLogic :: ExtModal2CASL -> ExtModal Source # sourceSublogic :: ExtModal2CASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2CASL -> ExtModalSL Source # minSourceTheory :: ExtModal2CASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2CASL -> CASL Source # mapSublogic :: ExtModal2CASL -> ExtModalSL -> Maybe CASL_Sublogics Source # map_theory :: ExtModal2CASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: ExtModal2CASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: ExtModal2CASL -> ExtModalMorph -> Result CASLMor Source # map_sentence :: ExtModal2CASL -> ExtModalSign -> ExtModalFORMULA -> Result CASLFORMULA Source # map_symbol :: ExtModal2CASL -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2CASL -> ExtModalSign -> ProofTree -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2CASL -> Bool Source # has_model_expansion :: ExtModal2CASL -> Bool Source # is_weakly_amalgamable :: ExtModal2CASL -> Bool Source # constituents :: ExtModal2CASL -> [String] Source # isInclusionComorphism :: ExtModal2CASL -> Bool Source # rps :: ExtModal2CASL -> Bool Source # eps :: ExtModal2CASL -> Bool Source # isGTC :: ExtModal2CASL -> Bool Source #
Comorphism DFOL2CASL DFOL () BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.DFOL2CASL Methods sourceLogic :: DFOL2CASL -> DFOL Source # sourceSublogic :: DFOL2CASL -> () Source # sourceSublogicLossy :: DFOL2CASL -> () Source # minSourceTheory :: DFOL2CASL -> Maybe (LibName, String) Source # targetLogic :: DFOL2CASL -> CASL Source # mapSublogic :: DFOL2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: DFOL2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: DFOL2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: DFOL2CASL -> Morphism -> Result CASLMor Source # map_sentence :: DFOL2CASL -> Sign -> FORMULA -> Result CASLFORMULA Source # map_symbol :: DFOL2CASL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: DFOL2CASL -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source # is_model_transportable :: DFOL2CASL -> Bool Source # has_model_expansion :: DFOL2CASL -> Bool Source # is_weakly_amalgamable :: DFOL2CASL -> Bool Source # constituents :: DFOL2CASL -> [String] Source # isInclusionComorphism :: DFOL2CASL -> Bool Source # rps :: DFOL2CASL -> Bool Source # eps :: DFOL2CASL -> Bool Source # isGTC :: DFOL2CASL -> Bool Source #
Comorphism CL2CFOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CommonLogic2CASL Methods sourceLogic :: CL2CFOL -> CommonLogic Source # sourceSublogic :: CL2CFOL -> CommonLogicSL Source # sourceSublogicLossy :: CL2CFOL -> CommonLogicSL Source # minSourceTheory :: CL2CFOL -> Maybe (LibName, String) Source # targetLogic :: CL2CFOL -> CASL Source # mapSublogic :: CL2CFOL -> CommonLogicSL -> Maybe CASL_Sublogics Source # map_theory :: CL2CFOL -> (Sign, [Named TEXT_META]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CL2CFOL -> (Sign, [Named TEXT_META]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CL2CFOL -> Morphism -> Result CASLMor Source # map_sentence :: CL2CFOL -> Sign -> TEXT_META -> Result CASLFORMULA Source # map_symbol :: CL2CFOL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: CL2CFOL -> Sign -> ProofTree -> Result (Sign, [Named TEXT_META]) Source # is_model_transportable :: CL2CFOL -> Bool Source # has_model_expansion :: CL2CFOL -> Bool Source # is_weakly_amalgamable :: CL2CFOL -> Bool Source # constituents :: CL2CFOL -> [String] Source # isInclusionComorphism :: CL2CFOL -> Bool Source # rps :: CL2CFOL -> Bool Source # eps :: CL2CFOL -> Bool Source # isGTC :: CL2CFOL -> Bool Source #
Comorphism CSMOF2CASL CSMOF () Metamodel Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CSMOF2CASL Methods sourceLogic :: CSMOF2CASL -> CSMOF Source # sourceSublogic :: CSMOF2CASL -> () Source # sourceSublogicLossy :: CSMOF2CASL -> () Source # minSourceTheory :: CSMOF2CASL -> Maybe (LibName, String) Source # targetLogic :: CSMOF2CASL -> CASL Source # mapSublogic :: CSMOF2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: CSMOF2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CSMOF2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CSMOF2CASL -> Morphism -> Result CASLMor Source # map_sentence :: CSMOF2CASL -> Sign -> Sen -> Result CASLFORMULA Source # map_symbol :: CSMOF2CASL -> Sign -> () -> Set Symbol Source # extractModel :: CSMOF2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source # is_model_transportable :: CSMOF2CASL -> Bool Source # has_model_expansion :: CSMOF2CASL -> Bool Source # is_weakly_amalgamable :: CSMOF2CASL -> Bool Source # constituents :: CSMOF2CASL -> [String] Source # isInclusionComorphism :: CSMOF2CASL -> Bool Source # rps :: CSMOF2CASL -> Bool Source # eps :: CSMOF2CASL -> Bool Source # isGTC :: CSMOF2CASL -> Bool Source #
Comorphism QVTR2CASL QVTR () Transformation Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.QVTR2CASL Methods sourceLogic :: QVTR2CASL -> QVTR Source # sourceSublogic :: QVTR2CASL -> () Source # sourceSublogicLossy :: QVTR2CASL -> () Source # minSourceTheory :: QVTR2CASL -> Maybe (LibName, String) Source # targetLogic :: QVTR2CASL -> CASL Source # mapSublogic :: QVTR2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: QVTR2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: QVTR2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: QVTR2CASL -> Morphism -> Result CASLMor Source # map_sentence :: QVTR2CASL -> Sign -> Sen -> Result CASLFORMULA Source # map_symbol :: QVTR2CASL -> Sign -> () -> Set Symbol Source # extractModel :: QVTR2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source # is_model_transportable :: QVTR2CASL -> Bool Source # has_model_expansion :: QVTR2CASL -> Bool Source # is_weakly_amalgamable :: QVTR2CASL -> Bool Source # constituents :: QVTR2CASL -> [String] Source # isInclusionComorphism :: QVTR2CASL -> Bool Source # rps :: QVTR2CASL -> Bool Source # eps :: QVTR2CASL -> Bool Source # isGTC :: QVTR2CASL -> Bool Source #
Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CFOL2IsabelleHOL Methods sourceLogic :: CFOL2IsabelleHOL -> CASL Source # sourceSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics Source # sourceSublogicLossy :: CFOL2IsabelleHOL -> CASL_Sublogics Source # minSourceTheory :: CFOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CFOL2IsabelleHOL -> Isabelle Source # mapSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics -> Maybe () Source # map_theory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CFOL2IsabelleHOL -> CASLMor -> Result IsabelleMorphism Source # map_sentence :: CFOL2IsabelleHOL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CFOL2IsabelleHOL -> CASLSign -> Symbol -> Set () Source # extractModel :: CFOL2IsabelleHOL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CFOL2IsabelleHOL -> Bool Source # has_model_expansion :: CFOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CFOL2IsabelleHOL -> Bool Source # constituents :: CFOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: CFOL2IsabelleHOL -> Bool Source # rps :: CFOL2IsabelleHOL -> Bool Source # eps :: CFOL2IsabelleHOL -> Bool Source # isGTC :: CFOL2IsabelleHOL -> Bool Source #
Comorphism CASL2TopSort CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2TopSort Methods sourceLogic :: CASL2TopSort -> CASL Source # sourceSublogic :: CASL2TopSort -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2TopSort -> CASL_Sublogics Source # minSourceTheory :: CASL2TopSort -> Maybe (LibName, String) Source # targetLogic :: CASL2TopSort -> CASL Source # mapSublogic :: CASL2TopSort -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2TopSort -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2TopSort -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2TopSort -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2TopSort -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2TopSort -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2TopSort -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2TopSort -> Bool Source # has_model_expansion :: CASL2TopSort -> Bool Source # is_weakly_amalgamable :: CASL2TopSort -> Bool Source # constituents :: CASL2TopSort -> [String] Source # isInclusionComorphism :: CASL2TopSort -> Bool Source # rps :: CASL2TopSort -> Bool Source # eps :: CASL2TopSort -> Bool Source # isGTC :: CASL2TopSort -> Bool Source #
Comorphism CASL2SubCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2SubCFOL Methods sourceLogic :: CASL2SubCFOL -> CASL Source # sourceSublogic :: CASL2SubCFOL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2SubCFOL -> CASL_Sublogics Source # minSourceTheory :: CASL2SubCFOL -> Maybe (LibName, String) Source # targetLogic :: CASL2SubCFOL -> CASL Source # mapSublogic :: CASL2SubCFOL -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2SubCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2SubCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2SubCFOL -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2SubCFOL -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2SubCFOL -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2SubCFOL -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2SubCFOL -> Bool Source # has_model_expansion :: CASL2SubCFOL -> Bool Source # is_weakly_amalgamable :: CASL2SubCFOL -> Bool Source # constituents :: CASL2SubCFOL -> [String] Source # isInclusionComorphism :: CASL2SubCFOL -> Bool Source # rps :: CASL2SubCFOL -> Bool Source # eps :: CASL2SubCFOL -> Bool Source # isGTC :: CASL2SubCFOL -> Bool Source #
Comorphism ExtModal2ExtModalTotal ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.ExtModal2ExtModalTotal Methods sourceLogic :: ExtModal2ExtModalTotal -> ExtModal Source # sourceSublogic :: ExtModal2ExtModalTotal -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2ExtModalTotal -> ExtModalSL Source # minSourceTheory :: ExtModal2ExtModalTotal -> Maybe (LibName, String) Source # targetLogic :: ExtModal2ExtModalTotal -> ExtModal Source # mapSublogic :: ExtModal2ExtModalTotal -> ExtModalSL -> Maybe ExtModalSL Source # map_theory :: ExtModal2ExtModalTotal -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # mapMarkedTheory :: ExtModal2ExtModalTotal -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # map_morphism :: ExtModal2ExtModalTotal -> ExtModalMorph -> Result ExtModalMorph Source # map_sentence :: ExtModal2ExtModalTotal -> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA Source # map_symbol :: ExtModal2ExtModalTotal -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2ExtModalTotal -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2ExtModalTotal -> Bool Source # has_model_expansion :: ExtModal2ExtModalTotal -> Bool Source # is_weakly_amalgamable :: ExtModal2ExtModalTotal -> Bool Source # constituents :: ExtModal2ExtModalTotal -> [String] Source # isInclusionComorphism :: ExtModal2ExtModalTotal -> Bool Source # rps :: ExtModal2ExtModalTotal -> Bool Source # eps :: ExtModal2ExtModalTotal -> Bool Source # isGTC :: ExtModal2ExtModalTotal -> Bool Source #
Comorphism CASL2Skolem CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2Skolem Methods sourceLogic :: CASL2Skolem -> CASL Source # sourceSublogic :: CASL2Skolem -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Skolem -> CASL_Sublogics Source # minSourceTheory :: CASL2Skolem -> Maybe (LibName, String) Source # targetLogic :: CASL2Skolem -> CASL Source # mapSublogic :: CASL2Skolem -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2Skolem -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2Skolem -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2Skolem -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2Skolem -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2Skolem -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2Skolem -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Skolem -> Bool Source # has_model_expansion :: CASL2Skolem -> Bool Source # is_weakly_amalgamable :: CASL2Skolem -> Bool Source # constituents :: CASL2Skolem -> [String] Source # isInclusionComorphism :: CASL2Skolem -> Bool Source # rps :: CASL2Skolem -> Bool Source # eps :: CASL2Skolem -> Bool Source # isGTC :: CASL2Skolem -> Bool Source #
Comorphism CASL2Prop CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2Prop Methods sourceLogic :: CASL2Prop -> CASL Source # sourceSublogic :: CASL2Prop -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Prop -> CASL_Sublogics Source # minSourceTheory :: CASL2Prop -> Maybe (LibName, String) Source # targetLogic :: CASL2Prop -> Propositional Source # mapSublogic :: CASL2Prop -> CASL_Sublogics -> Maybe PropSL Source # map_theory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source # mapMarkedTheory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source # map_morphism :: CASL2Prop -> CASLMor -> Result Morphism Source # map_sentence :: CASL2Prop -> CASLSign -> CASLFORMULA -> Result FORMULA Source # map_symbol :: CASL2Prop -> CASLSign -> Symbol0 -> Set Symbol Source # extractModel :: CASL2Prop -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Prop -> Bool Source # has_model_expansion :: CASL2Prop -> Bool Source # is_weakly_amalgamable :: CASL2Prop -> Bool Source # constituents :: CASL2Prop -> [String] Source # isInclusionComorphism :: CASL2Prop -> Bool Source # rps :: CASL2Prop -> Bool Source # eps :: CASL2Prop -> Bool Source # isGTC :: CASL2Prop -> Bool Source #
Comorphism CASL2Prenex CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2Prenex Methods sourceLogic :: CASL2Prenex -> CASL Source # sourceSublogic :: CASL2Prenex -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Prenex -> CASL_Sublogics Source # minSourceTheory :: CASL2Prenex -> Maybe (LibName, String) Source # targetLogic :: CASL2Prenex -> CASL Source # mapSublogic :: CASL2Prenex -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2Prenex -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2Prenex -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2Prenex -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2Prenex -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2Prenex -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2Prenex -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Prenex -> Bool Source # has_model_expansion :: CASL2Prenex -> Bool Source # is_weakly_amalgamable :: CASL2Prenex -> Bool Source # constituents :: CASL2Prenex -> [String] Source # isInclusionComorphism :: CASL2Prenex -> Bool Source # rps :: CASL2Prenex -> Bool Source # eps :: CASL2Prenex -> Bool Source # isGTC :: CASL2Prenex -> Bool Source #
Comorphism CASL2PCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2PCFOL Methods sourceLogic :: CASL2PCFOL -> CASL Source # sourceSublogic :: CASL2PCFOL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2PCFOL -> CASL_Sublogics Source # minSourceTheory :: CASL2PCFOL -> Maybe (LibName, String) Source # targetLogic :: CASL2PCFOL -> CASL Source # mapSublogic :: CASL2PCFOL -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2PCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2PCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2PCFOL -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2PCFOL -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2PCFOL -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2PCFOL -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2PCFOL -> Bool Source # has_model_expansion :: CASL2PCFOL -> Bool Source # is_weakly_amalgamable :: CASL2PCFOL -> Bool Source # constituents :: CASL2PCFOL -> [String] Source # isInclusionComorphism :: CASL2PCFOL -> Bool Source # rps :: CASL2PCFOL -> Bool Source # eps :: CASL2PCFOL -> Bool Source # isGTC :: CASL2PCFOL -> Bool Source #
Comorphism ExtModal2ExtModalNoSubsorts ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.ExtModal2ExtModalNoSubsorts Methods sourceLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source # sourceSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source # minSourceTheory :: ExtModal2ExtModalNoSubsorts -> Maybe (LibName, String) Source # targetLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source # mapSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL -> Maybe ExtModalSL Source # map_theory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # mapMarkedTheory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # map_morphism :: ExtModal2ExtModalNoSubsorts -> ExtModalMorph -> Result ExtModalMorph Source # map_sentence :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA Source # map_symbol :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2ExtModalNoSubsorts -> Bool Source # has_model_expansion :: ExtModal2ExtModalNoSubsorts -> Bool Source # is_weakly_amalgamable :: ExtModal2ExtModalNoSubsorts -> Bool Source # constituents :: ExtModal2ExtModalNoSubsorts -> [String] Source # isInclusionComorphism :: ExtModal2ExtModalNoSubsorts -> Bool Source # rps :: ExtModal2ExtModalNoSubsorts -> Bool Source # eps :: ExtModal2ExtModalNoSubsorts -> Bool Source # isGTC :: ExtModal2ExtModalNoSubsorts -> Bool Source #
Comorphism CASL2NNF CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2NNF Methods sourceLogic :: CASL2NNF -> CASL Source # sourceSublogic :: CASL2NNF -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2NNF -> CASL_Sublogics Source # minSourceTheory :: CASL2NNF -> Maybe (LibName, String) Source # targetLogic :: CASL2NNF -> CASL Source # mapSublogic :: CASL2NNF -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2NNF -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2NNF -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2NNF -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2NNF -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2NNF -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2NNF -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2NNF -> Bool Source # has_model_expansion :: CASL2NNF -> Bool Source # is_weakly_amalgamable :: CASL2NNF -> Bool Source # constituents :: CASL2NNF -> [String] Source # isInclusionComorphism :: CASL2NNF -> Bool Source # rps :: CASL2NNF -> Bool Source # eps :: CASL2NNF -> Bool Source # isGTC :: CASL2NNF -> Bool Source #
Comorphism CASL2Modal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2Modal Methods sourceLogic :: CASL2Modal -> CASL Source # sourceSublogic :: CASL2Modal -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Modal -> CASL_Sublogics Source # minSourceTheory :: CASL2Modal -> Maybe (LibName, String) Source # targetLogic :: CASL2Modal -> Modal Source # mapSublogic :: CASL2Modal -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2Modal -> (CASLSign, [Named CASLFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source # mapMarkedTheory :: CASL2Modal -> (CASLSign, [Named CASLFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source # map_morphism :: CASL2Modal -> CASLMor -> Result ModalMor Source # map_sentence :: CASL2Modal -> CASLSign -> CASLFORMULA -> Result ModalFORMULA Source # map_symbol :: CASL2Modal -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2Modal -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Modal -> Bool Source # has_model_expansion :: CASL2Modal -> Bool Source # is_weakly_amalgamable :: CASL2Modal -> Bool Source # constituents :: CASL2Modal -> [String] Source # isInclusionComorphism :: CASL2Modal -> Bool Source # rps :: CASL2Modal -> Bool Source # eps :: CASL2Modal -> Bool Source # isGTC :: CASL2Modal -> Bool Source #
Comorphism CASL2Hybrid CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Hybrid () H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2Hybrid Methods sourceLogic :: CASL2Hybrid -> CASL Source # sourceSublogic :: CASL2Hybrid -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Hybrid -> CASL_Sublogics Source # minSourceTheory :: CASL2Hybrid -> Maybe (LibName, String) Source # targetLogic :: CASL2Hybrid -> Hybrid Source # mapSublogic :: CASL2Hybrid -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2Hybrid -> (CASLSign, [Named CASLFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source # mapMarkedTheory :: CASL2Hybrid -> (CASLSign, [Named CASLFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source # map_morphism :: CASL2Hybrid -> CASLMor -> Result HybridMor Source # map_sentence :: CASL2Hybrid -> CASLSign -> CASLFORMULA -> Result HybridFORMULA Source # map_symbol :: CASL2Hybrid -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2Hybrid -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Hybrid -> Bool Source # has_model_expansion :: CASL2Hybrid -> Bool Source # is_weakly_amalgamable :: CASL2Hybrid -> Bool Source # constituents :: CASL2Hybrid -> [String] Source # isInclusionComorphism :: CASL2Hybrid -> Bool Source # rps :: CASL2Hybrid -> Bool Source # eps :: CASL2Hybrid -> Bool Source # isGTC :: CASL2Hybrid -> Bool Source #
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2HasCASL Methods sourceLogic :: CASL2HasCASL -> CASL Source # sourceSublogic :: CASL2HasCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2HasCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2HasCASL -> HasCASL Source # mapSublogic :: CASL2HasCASL -> CASL_Sublogics -> Maybe Sublogic Source # map_theory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: CASL2HasCASL -> CASLMor -> Result Morphism Source # map_sentence :: CASL2HasCASL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2HasCASL -> CASLSign -> Symbol0 -> Set Symbol Source # extractModel :: CASL2HasCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2HasCASL -> Bool Source # has_model_expansion :: CASL2HasCASL -> Bool Source # is_weakly_amalgamable :: CASL2HasCASL -> Bool Source # constituents :: CASL2HasCASL -> [String] Source # isInclusionComorphism :: CASL2HasCASL -> Bool Source # rps :: CASL2HasCASL -> Bool Source # eps :: CASL2HasCASL -> Bool Source # isGTC :: CASL2HasCASL -> Bool Source #
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.ExtModal2HasCASL Methods sourceLogic :: ExtModal2HasCASL -> ExtModal Source # sourceSublogic :: ExtModal2HasCASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2HasCASL -> ExtModalSL Source # minSourceTheory :: ExtModal2HasCASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2HasCASL -> HasCASL Source # mapSublogic :: ExtModal2HasCASL -> ExtModalSL -> Maybe Sublogic Source # map_theory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: ExtModal2HasCASL -> ExtModalMorph -> Result Morphism Source # map_sentence :: ExtModal2HasCASL -> ExtModalSign -> ExtModalFORMULA -> Result Sentence Source # map_symbol :: ExtModal2HasCASL -> ExtModalSign -> Symbol0 -> Set Symbol Source # extractModel :: ExtModal2HasCASL -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2HasCASL -> Bool Source # has_model_expansion :: ExtModal2HasCASL -> Bool Source # is_weakly_amalgamable :: ExtModal2HasCASL -> Bool Source # constituents :: ExtModal2HasCASL -> [String] Source # isInclusionComorphism :: ExtModal2HasCASL -> Bool Source # rps :: ExtModal2HasCASL -> Bool Source # eps :: ExtModal2HasCASL -> Bool Source # isGTC :: ExtModal2HasCASL -> Bool Source #
Comorphism CASL2ExtModal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2ExtModal Methods sourceLogic :: CASL2ExtModal -> CASL Source # sourceSublogic :: CASL2ExtModal -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2ExtModal -> CASL_Sublogics Source # minSourceTheory :: CASL2ExtModal -> Maybe (LibName, String) Source # targetLogic :: CASL2ExtModal -> ExtModal Source # mapSublogic :: CASL2ExtModal -> CASL_Sublogics -> Maybe ExtModalSL Source # map_theory :: CASL2ExtModal -> (CASLSign, [Named CASLFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # mapMarkedTheory :: CASL2ExtModal -> (CASLSign, [Named CASLFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # map_morphism :: CASL2ExtModal -> CASLMor -> Result ExtModalMorph Source # map_sentence :: CASL2ExtModal -> CASLSign -> CASLFORMULA -> Result ExtModalFORMULA Source # map_symbol :: CASL2ExtModal -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2ExtModal -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2ExtModal -> Bool Source # has_model_expansion :: CASL2ExtModal -> Bool Source # is_weakly_amalgamable :: CASL2ExtModal -> Bool Source # constituents :: CASL2ExtModal -> [String] Source # isInclusionComorphism :: CASL2ExtModal -> Bool Source # rps :: CASL2ExtModal -> Bool Source # eps :: CASL2ExtModal -> Bool Source # isGTC :: CASL2ExtModal -> Bool Source #
Comorphism CASL2CspCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source #
Instance details Defined in Comorphisms.CASL2CspCASL Methods sourceLogic :: CASL2CspCASL -> CASL Source # sourceSublogic :: CASL2CspCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2CspCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2CspCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2CspCASL -> CspCASL Source # mapSublogic :: CASL2CspCASL -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2CspCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # mapMarkedTheory :: CASL2CspCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # map_morphism :: CASL2CspCASL -> CASLMor -> Result CspCASLMorphism Source # map_sentence :: CASL2CspCASL -> CASLSign -> CASLFORMULA -> Result CspCASLSen Source # map_symbol :: CASL2CspCASL -> CASLSign -> Symbol -> Set CspSymbol Source # extractModel :: CASL2CspCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2CspCASL -> Bool Source # has_model_expansion :: CASL2CspCASL -> Bool Source # is_weakly_amalgamable :: CASL2CspCASL -> Bool Source # constituents :: CASL2CspCASL -> [String] Source # isInclusionComorphism :: CASL2CspCASL -> Bool Source # rps :: CASL2CspCASL -> Bool Source # eps :: CASL2CspCASL -> Bool Source # isGTC :: CASL2CspCASL -> Bool Source #
Comorphism Adl2CASL Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.Adl2CASL Methods sourceLogic :: Adl2CASL -> Adl Source # sourceSublogic :: Adl2CASL -> () Source # sourceSublogicLossy :: Adl2CASL -> () Source # minSourceTheory :: Adl2CASL -> Maybe (LibName, String) Source # targetLogic :: Adl2CASL -> CASL Source # mapSublogic :: Adl2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: Adl2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: Adl2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: Adl2CASL -> Morphism -> Result CASLMor Source # map_sentence :: Adl2CASL -> Sign -> Sen -> Result CASLFORMULA Source # map_symbol :: Adl2CASL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: Adl2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source # is_model_transportable :: Adl2CASL -> Bool Source # has_model_expansion :: Adl2CASL -> Bool Source # is_weakly_amalgamable :: Adl2CASL -> Bool Source # constituents :: Adl2CASL -> [String] Source # isInclusionComorphism :: Adl2CASL -> Bool Source # rps :: Adl2CASL -> Bool Source # eps :: Adl2CASL -> Bool Source # isGTC :: Adl2CASL -> Bool Source #
Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CoCFOL2IsabelleHOL Methods sourceLogic :: CoCFOL2IsabelleHOL -> CoCASL Source # sourceSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCFOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CoCFOL2IsabelleHOL -> Isabelle Source # mapSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics -> Maybe () Source # map_theory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CoCFOL2IsabelleHOL -> CoCASLMor -> Result IsabelleMorphism Source # map_sentence :: CoCFOL2IsabelleHOL -> CSign -> CoCASLFORMULA -> Result Sentence Source # map_symbol :: CoCFOL2IsabelleHOL -> CSign -> Symbol -> Set () Source # extractModel :: CoCFOL2IsabelleHOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCFOL2IsabelleHOL -> Bool Source # has_model_expansion :: CoCFOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CoCFOL2IsabelleHOL -> Bool Source # constituents :: CoCFOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: CoCFOL2IsabelleHOL -> Bool Source # rps :: CoCFOL2IsabelleHOL -> Bool Source # eps :: CoCFOL2IsabelleHOL -> Bool Source # isGTC :: CoCFOL2IsabelleHOL -> Bool Source #
Comorphism CoCASL2CoSubCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CoCASL2CoSubCFOL Methods sourceLogic :: CoCASL2CoSubCFOL -> CoCASL Source # sourceSublogic :: CoCASL2CoSubCFOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCASL2CoSubCFOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCASL2CoSubCFOL -> Maybe (LibName, String) Source # targetLogic :: CoCASL2CoSubCFOL -> CoCASL Source # mapSublogic :: CoCASL2CoSubCFOL -> CoCASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CoCASL2CoSubCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CoCASL2CoSubCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CoCASL2CoSubCFOL -> CoCASLMor -> Result CoCASLMor Source # map_sentence :: CoCASL2CoSubCFOL -> CSign -> CoCASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CoCASL2CoSubCFOL -> CSign -> Symbol -> Set Symbol Source # extractModel :: CoCASL2CoSubCFOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCASL2CoSubCFOL -> Bool Source # has_model_expansion :: CoCASL2CoSubCFOL -> Bool Source # is_weakly_amalgamable :: CoCASL2CoSubCFOL -> Bool Source # constituents :: CoCASL2CoSubCFOL -> [String] Source # isInclusionComorphism :: CoCASL2CoSubCFOL -> Bool Source # rps :: CoCASL2CoSubCFOL -> Bool Source # eps :: CoCASL2CoSubCFOL -> Bool Source # isGTC :: CoCASL2CoSubCFOL -> Bool Source #
Comorphism CoCASL2CoPCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CoCASL2CoPCFOL Methods sourceLogic :: CoCASL2CoPCFOL -> CoCASL Source # sourceSublogic :: CoCASL2CoPCFOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCASL2CoPCFOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCASL2CoPCFOL -> Maybe (LibName, String) Source # targetLogic :: CoCASL2CoPCFOL -> CoCASL Source # mapSublogic :: CoCASL2CoPCFOL -> CoCASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CoCASL2CoPCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CoCASL2CoPCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CoCASL2CoPCFOL -> CoCASLMor -> Result CoCASLMor Source # map_sentence :: CoCASL2CoPCFOL -> CSign -> CoCASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CoCASL2CoPCFOL -> CSign -> Symbol -> Set Symbol Source # extractModel :: CoCASL2CoPCFOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCASL2CoPCFOL -> Bool Source # has_model_expansion :: CoCASL2CoPCFOL -> Bool Source # is_weakly_amalgamable :: CoCASL2CoPCFOL -> Bool Source # constituents :: CoCASL2CoPCFOL -> [String] Source # isInclusionComorphism :: CoCASL2CoPCFOL -> Bool Source # rps :: CoCASL2CoPCFOL -> Bool Source # eps :: CoCASL2CoPCFOL -> Bool Source # isGTC :: CoCASL2CoPCFOL -> Bool Source #
Comorphism CASL2CoCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2CoCASL Methods sourceLogic :: CASL2CoCASL -> CASL Source # sourceSublogic :: CASL2CoCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2CoCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2CoCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2CoCASL -> CoCASL Source # mapSublogic :: CASL2CoCASL -> CASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CASL2CoCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CASL2CoCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CASL2CoCASL -> CASLMor -> Result CoCASLMor Source # map_sentence :: CASL2CoCASL -> CASLSign -> CASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CASL2CoCASL -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2CoCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2CoCASL -> Bool Source # has_model_expansion :: CASL2CoCASL -> Bool Source # is_weakly_amalgamable :: CASL2CoCASL -> Bool Source # constituents :: CASL2CoCASL -> [String] Source # isInclusionComorphism :: CASL2CoCASL -> Bool Source # rps :: CASL2CoCASL -> Bool Source # eps :: CASL2CoCASL -> Bool Source # isGTC :: CASL2CoCASL -> Bool Source #
Comorphism CASL_DL2CASL CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL_DL2CASL Methods sourceLogic :: CASL_DL2CASL -> CASL_DL Source # sourceSublogic :: CASL_DL2CASL -> CASL_DL_SL Source # sourceSublogicLossy :: CASL_DL2CASL -> CASL_DL_SL Source # minSourceTheory :: CASL_DL2CASL -> Maybe (LibName, String) Source # targetLogic :: CASL_DL2CASL -> CASL Source # mapSublogic :: CASL_DL2CASL -> CASL_DL_SL -> Maybe CASL_Sublogics Source # map_theory :: CASL_DL2CASL -> (DLSign, [Named DLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL_DL2CASL -> (DLSign, [Named DLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL_DL2CASL -> DLMor -> Result CASLMor Source # map_sentence :: CASL_DL2CASL -> DLSign -> DLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL_DL2CASL -> DLSign -> Symbol -> Set Symbol Source # extractModel :: CASL_DL2CASL -> DLSign -> ProofTree -> Result (DLSign, [Named DLFORMULA]) Source # is_model_transportable :: CASL_DL2CASL -> Bool Source # has_model_expansion :: CASL_DL2CASL -> Bool Source # is_weakly_amalgamable :: CASL_DL2CASL -> Bool Source # constituents :: CASL_DL2CASL -> [String] Source # isInclusionComorphism :: CASL_DL2CASL -> Bool Source # rps :: CASL_DL2CASL -> Bool Source # eps :: CASL_DL2CASL -> Bool Source # isGTC :: CASL_DL2CASL -> Bool Source #
Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2VSERefine Methods sourceLogic :: CASL2VSERefine -> CASL Source # sourceSublogic :: CASL2VSERefine -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSERefine -> CASL_Sublogics Source # minSourceTheory :: CASL2VSERefine -> Maybe (LibName, String) Source # targetLogic :: CASL2VSERefine -> VSE Source # mapSublogic :: CASL2VSERefine -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSERefine -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSERefine -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSERefine -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSERefine -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSERefine -> Bool Source # has_model_expansion :: CASL2VSERefine -> Bool Source # is_weakly_amalgamable :: CASL2VSERefine -> Bool Source # constituents :: CASL2VSERefine -> [String] Source # isInclusionComorphism :: CASL2VSERefine -> Bool Source # rps :: CASL2VSERefine -> Bool Source # eps :: CASL2VSERefine -> Bool Source # isGTC :: CASL2VSERefine -> Bool Source #
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2VSEImport Methods sourceLogic :: CASL2VSEImport -> CASL Source # sourceSublogic :: CASL2VSEImport -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSEImport -> CASL_Sublogics Source # minSourceTheory :: CASL2VSEImport -> Maybe (LibName, String) Source # targetLogic :: CASL2VSEImport -> VSE Source # mapSublogic :: CASL2VSEImport -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSEImport -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSEImport -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSEImport -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSEImport -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSEImport -> Bool Source # has_model_expansion :: CASL2VSEImport -> Bool Source # is_weakly_amalgamable :: CASL2VSEImport -> Bool Source # constituents :: CASL2VSEImport -> [String] Source # isInclusionComorphism :: CASL2VSEImport -> Bool Source # rps :: CASL2VSEImport -> Bool Source # eps :: CASL2VSEImport -> Bool Source # isGTC :: CASL2VSEImport -> Bool Source #
Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2VSE Methods sourceLogic :: CASL2VSE -> CASL Source # sourceSublogic :: CASL2VSE -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSE -> CASL_Sublogics Source # minSourceTheory :: CASL2VSE -> Maybe (LibName, String) Source # targetLogic :: CASL2VSE -> VSE Source # mapSublogic :: CASL2VSE -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSE -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSE -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSE -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSE -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSE -> Bool Source # has_model_expansion :: CASL2VSE -> Bool Source # is_weakly_amalgamable :: CASL2VSE -> Bool Source # constituents :: CASL2VSE -> [String] Source # isInclusionComorphism :: CASL2VSE -> Bool Source # rps :: CASL2VSE -> Bool Source # eps :: CASL2VSE -> Bool Source # isGTC :: CASL2VSE -> Bool Source #
Modification MODAL_EMBEDDING (InclComorphism CASL CASL_Sublogics) (CompComorphism CASL2Modal Modal2CASL) CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Modifications.ModalEmbedding Methods tauSigma :: MODAL_EMBEDDING -> CASLSign -> Result CASLMor Source # sourceComorphism :: MODAL_EMBEDDING -> InclComorphism CASL CASL_Sublogics Source # targetComorphism :: MODAL_EMBEDDING -> CompComorphism CASL2Modal Modal2CASL Source #
Eq a => Eq (CASL_SL a) Source #
Instance details Defined in CASL.Sublogic Methods (==) :: CASL_SL a -> CASL_SL a -> Bool (/=) :: CASL_SL a -> CASL_SL a -> Bool
Data a => Data (CASL_SL a) Source #
Instance details Defined in CASL.Sublogic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CASL_SL a -> c (CASL_SL a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (CASL_SL a) toConstr :: CASL_SL a -> Constr dataTypeOf :: CASL_SL a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (CASL_SL a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (CASL_SL a)) gmapT :: (forall b. Data b => b -> b) -> CASL_SL a -> CASL_SL a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CASL_SL a -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CASL_SL a -> r gmapQ :: (forall d. Data d => d -> u) -> CASL_SL a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> CASL_SL a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> CASL_SL a -> m (CASL_SL a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CASL_SL a -> m (CASL_SL a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CASL_SL a -> m (CASL_SL a)
Ord a => Ord (CASL_SL a) Source #
Instance details Defined in CASL.Sublogic Methods compare :: CASL_SL a -> CASL_SL a -> Ordering (<) :: CASL_SL a -> CASL_SL a -> Bool (<=) :: CASL_SL a -> CASL_SL a -> Bool (>) :: CASL_SL a -> CASL_SL a -> Bool (>=) :: CASL_SL a -> CASL_SL a -> Bool max :: CASL_SL a -> CASL_SL a -> CASL_SL a min :: CASL_SL a -> CASL_SL a -> CASL_SL a
Show a => Show (CASL_SL a) Source #
Instance details Defined in CASL.Sublogic Methods showsPrec :: Int -> CASL_SL a -> ShowS show :: CASL_SL a -> String showList :: [CASL_SL a] -> ShowS
Generic (CASL_SL a)
Instance details Defined in CASL.ATC_CASL Associated Types type Rep (CASL_SL a) :: Type -> Type Methods from :: CASL_SL a -> Rep (CASL_SL a) x to :: Rep (CASL_SL a) x -> CASL_SL a
FromJSON a => FromJSON (CASL_SL a)
Instance details Defined in CASL.ATC_CASL Methods parseJSON :: Value -> Parser (CASL_SL a) parseJSONList :: Value -> Parser [CASL_SL a]
ToJSON a => ToJSON (CASL_SL a)
Instance details Defined in CASL.ATC_CASL Methods toJSON :: CASL_SL a -> Value toEncoding :: CASL_SL a -> Encoding toJSONList :: [CASL_SL a] -> Value toEncodingList :: [CASL_SL a] -> Encoding
ShATermConvertible a => ShATermConvertible (CASL_SL a)
Instance details Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> CASL_SL a -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [CASL_SL a] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, CASL_SL a) fromShATermList' :: Int -> ATermTable -> (ATermTable, [CASL_SL a])
NameSL a => SublogicName (CASL_SL a) Source #
Instance details Defined in CASL.Logic_CASL Methods sublogicName :: CASL_SL a -> String Source #
Lattice a => SemiLatticeWithTop (CASL_SL a) Source #
Instance details Defined in CASL.Logic_CASL Methods lub :: CASL_SL a -> CASL_SL a -> CASL_SL a Source # top :: CASL_SL a Source #
Lattice a => ProjectSublogicM (CASL_SL a) Symbol Source #
Instance details Defined in CASL.Logic_CASL Methods projectSublogicM :: CASL_SL a -> Symbol -> Maybe Symbol Source #
Lattice a => ProjectSublogicM (CASL_SL a) SYMB_MAP_ITEMS Source #
Instance details Defined in CASL.Logic_CASL Methods projectSublogicM :: CASL_SL a -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS Source #
Lattice a => ProjectSublogicM (CASL_SL a) SYMB_ITEMS Source #
Instance details Defined in CASL.Logic_CASL Methods projectSublogicM :: CASL_SL a -> SYMB_ITEMS -> Maybe SYMB_ITEMS Source #
Lattice a => MinSublogic (CASL_SL a) Symbol Source #
Instance details Defined in CASL.Logic_CASL Methods minSublogic :: Symbol -> CASL_SL a Source #
Lattice a => MinSublogic (CASL_SL a) SYMB_MAP_ITEMS Source #
Instance details Defined in CASL.Logic_CASL Methods minSublogic :: SYMB_MAP_ITEMS -> CASL_SL a Source #
Lattice a => MinSublogic (CASL_SL a) SYMB_ITEMS Source #
Instance details Defined in CASL.Logic_CASL Methods minSublogic :: SYMB_ITEMS -> CASL_SL a Source #
MinSL a f => MinSublogic (CASL_SL a) (FORMULA f) Source #
Instance details Defined in CASL.Logic_CASL Methods minSublogic :: FORMULA f -> CASL_SL a Source #
MinSL a e => ProjectSublogic (CASL_SL a) (Sign f e) Source #
Instance details Defined in CASL.Logic_CASL Methods projectSublogic :: CASL_SL a -> Sign f e -> Sign f e Source #
MinSL a e => MinSublogic (CASL_SL a) (Sign f e) Source #
Instance details Defined in CASL.Logic_CASL Methods minSublogic :: Sign f e -> CASL_SL a Source #
MinSL a e => ProjectSublogic (CASL_SL a) (Morphism f e m) Source #
Instance details Defined in CASL.Logic_CASL Methods projectSublogic :: CASL_SL a -> Morphism f e m -> Morphism f e m Source #
(MinSL a f, MinSL a s, MinSL a b, ProjForm a f, ProjSigItem a s f, ProjBasic a b s f) => ProjectSublogic (CASL_SL a) (BASIC_SPEC b s f) Source #
Instance details Defined in CASL.Logic_CASL Methods projectSublogic :: CASL_SL a -> BASIC_SPEC b s f -> BASIC_SPEC b s f Source #
MinSL a e => MinSublogic (CASL_SL a) (Morphism f e m) Source #
Instance details Defined in CASL.Logic_CASL Methods minSublogic :: Morphism f e m -> CASL_SL a Source #
(MinSL a f, MinSL a s, MinSL a b) => MinSublogic (CASL_SL a) (BASIC_SPEC b s f) Source #
Instance details Defined in CASL.Logic_CASL Methods minSublogic :: BASIC_SPEC b s f -> CASL_SL a Source #
type Rep (CASL_SL a)
Instance details Defined in CASL.ATC_CASL type Rep (CASL_SL a) = D1 ('MetaData "CASL_SL" "CASL.Sublogic" "main" 'False) (C1 ('MetaCons "CASL_SL" 'PrefixI 'True) (((S1 ('MetaSel ('Just "sub_features") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SubsortingFeatures) :: S1 ('MetaSel ('Just "has_part") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "cons_features") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SortGenerationFeatures) :: S1 ('MetaSel ('Just "has_eq") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :: ((S1 ('MetaSel ('Just "has_pred") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "which_logic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CASL_Formulas)) :: (S1 ('MetaSel ('Just "has_empty_sorts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "ext_features") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))))

data CASL_Formulas Source #

Constructors

Atomic	atomic logic
Horn	positive conditional logic
GHorn	generalized positive conditional logic
Prenex	formulas in prenex normal form
FOL	first-order logic
SOL	second-order logic

Instances

Instances details

Eq CASL_Formulas Source #
Instance details Defined in CASL.Sublogic Methods (==) :: CASL_Formulas -> CASL_Formulas -> Bool (/=) :: CASL_Formulas -> CASL_Formulas -> Bool
Data CASL_Formulas Source #
Instance details Defined in CASL.Sublogic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CASL_Formulas -> c CASL_Formulas gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CASL_Formulas toConstr :: CASL_Formulas -> Constr dataTypeOf :: CASL_Formulas -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CASL_Formulas) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CASL_Formulas) gmapT :: (forall b. Data b => b -> b) -> CASL_Formulas -> CASL_Formulas gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CASL_Formulas -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CASL_Formulas -> r gmapQ :: (forall d. Data d => d -> u) -> CASL_Formulas -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> CASL_Formulas -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> CASL_Formulas -> m CASL_Formulas gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CASL_Formulas -> m CASL_Formulas gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CASL_Formulas -> m CASL_Formulas
Ord CASL_Formulas Source #
Instance details Defined in CASL.Sublogic Methods compare :: CASL_Formulas -> CASL_Formulas -> Ordering (<) :: CASL_Formulas -> CASL_Formulas -> Bool (<=) :: CASL_Formulas -> CASL_Formulas -> Bool (>) :: CASL_Formulas -> CASL_Formulas -> Bool (>=) :: CASL_Formulas -> CASL_Formulas -> Bool max :: CASL_Formulas -> CASL_Formulas -> CASL_Formulas min :: CASL_Formulas -> CASL_Formulas -> CASL_Formulas
Show CASL_Formulas Source #
Instance details Defined in CASL.Sublogic Methods showsPrec :: Int -> CASL_Formulas -> ShowS show :: CASL_Formulas -> String showList :: [CASL_Formulas] -> ShowS
Generic CASL_Formulas
Instance details Defined in CASL.ATC_CASL Associated Types type Rep CASL_Formulas :: Type -> Type Methods from :: CASL_Formulas -> Rep CASL_Formulas x to :: Rep CASL_Formulas x -> CASL_Formulas
FromJSON CASL_Formulas
Instance details Defined in CASL.ATC_CASL Methods parseJSON :: Value -> Parser CASL_Formulas parseJSONList :: Value -> Parser [CASL_Formulas]
ToJSON CASL_Formulas
Instance details Defined in CASL.ATC_CASL Methods toJSON :: CASL_Formulas -> Value toEncoding :: CASL_Formulas -> Encoding toJSONList :: [CASL_Formulas] -> Value toEncodingList :: [CASL_Formulas] -> Encoding
ShATermConvertible CASL_Formulas
Instance details Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> CASL_Formulas -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [CASL_Formulas] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, CASL_Formulas) fromShATermList' :: Int -> ATermTable -> (ATermTable, [CASL_Formulas])
type Rep CASL_Formulas
Instance details Defined in CASL.ATC_CASL type Rep CASL_Formulas = D1 ('MetaData "CASL_Formulas" "CASL.Sublogic" "main" 'False) ((C1 ('MetaCons "Atomic" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Horn" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GHorn" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "Prenex" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FOL" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SOL" 'PrefixI 'False) (U1 :: Type -> Type))))

data SubsortingFeatures Source #

Constructors

NoSub
LocFilSub
Sub

Instances

Instances details

Eq SubsortingFeatures Source #
Instance details Defined in CASL.Sublogic Methods (==) :: SubsortingFeatures -> SubsortingFeatures -> Bool (/=) :: SubsortingFeatures -> SubsortingFeatures -> Bool
Data SubsortingFeatures Source #
Instance details Defined in CASL.Sublogic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SubsortingFeatures -> c SubsortingFeatures gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SubsortingFeatures toConstr :: SubsortingFeatures -> Constr dataTypeOf :: SubsortingFeatures -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SubsortingFeatures) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SubsortingFeatures) gmapT :: (forall b. Data b => b -> b) -> SubsortingFeatures -> SubsortingFeatures gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SubsortingFeatures -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SubsortingFeatures -> r gmapQ :: (forall d. Data d => d -> u) -> SubsortingFeatures -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SubsortingFeatures -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SubsortingFeatures -> m SubsortingFeatures gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SubsortingFeatures -> m SubsortingFeatures gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SubsortingFeatures -> m SubsortingFeatures
Ord SubsortingFeatures Source #
Instance details Defined in CASL.Sublogic Methods compare :: SubsortingFeatures -> SubsortingFeatures -> Ordering (<) :: SubsortingFeatures -> SubsortingFeatures -> Bool (<=) :: SubsortingFeatures -> SubsortingFeatures -> Bool (>) :: SubsortingFeatures -> SubsortingFeatures -> Bool (>=) :: SubsortingFeatures -> SubsortingFeatures -> Bool max :: SubsortingFeatures -> SubsortingFeatures -> SubsortingFeatures min :: SubsortingFeatures -> SubsortingFeatures -> SubsortingFeatures
Show SubsortingFeatures Source #
Instance details Defined in CASL.Sublogic Methods showsPrec :: Int -> SubsortingFeatures -> ShowS show :: SubsortingFeatures -> String showList :: [SubsortingFeatures] -> ShowS
Generic SubsortingFeatures
Instance details Defined in CASL.ATC_CASL Associated Types type Rep SubsortingFeatures :: Type -> Type Methods from :: SubsortingFeatures -> Rep SubsortingFeatures x to :: Rep SubsortingFeatures x -> SubsortingFeatures
FromJSON SubsortingFeatures
Instance details Defined in CASL.ATC_CASL Methods parseJSON :: Value -> Parser SubsortingFeatures parseJSONList :: Value -> Parser [SubsortingFeatures]
ToJSON SubsortingFeatures
Instance details Defined in CASL.ATC_CASL Methods toJSON :: SubsortingFeatures -> Value toEncoding :: SubsortingFeatures -> Encoding toJSONList :: [SubsortingFeatures] -> Value toEncodingList :: [SubsortingFeatures] -> Encoding
ShATermConvertible SubsortingFeatures
Instance details Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> SubsortingFeatures -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SubsortingFeatures] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SubsortingFeatures) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SubsortingFeatures])
type Rep SubsortingFeatures
Instance details Defined in CASL.ATC_CASL type Rep SubsortingFeatures = D1 ('MetaData "SubsortingFeatures" "CASL.Sublogic" "main" 'False) (C1 ('MetaCons "NoSub" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "LocFilSub" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Sub" 'PrefixI 'False) (U1 :: Type -> Type)))

data SortGenerationFeatures Source #

Constructors

NoSortGen
SortGen
Fields emptyMapping :: Bool Mapping of indexed sorts is empty onlyInjConstrs :: Bool only constructors that are subsort injections

Instances

Instances details

Eq SortGenerationFeatures Source #
Instance details Defined in CASL.Sublogic Methods (==) :: SortGenerationFeatures -> SortGenerationFeatures -> Bool (/=) :: SortGenerationFeatures -> SortGenerationFeatures -> Bool
Data SortGenerationFeatures Source #
Instance details Defined in CASL.Sublogic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SortGenerationFeatures -> c SortGenerationFeatures gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SortGenerationFeatures toConstr :: SortGenerationFeatures -> Constr dataTypeOf :: SortGenerationFeatures -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SortGenerationFeatures) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SortGenerationFeatures) gmapT :: (forall b. Data b => b -> b) -> SortGenerationFeatures -> SortGenerationFeatures gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SortGenerationFeatures -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SortGenerationFeatures -> r gmapQ :: (forall d. Data d => d -> u) -> SortGenerationFeatures -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SortGenerationFeatures -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SortGenerationFeatures -> m SortGenerationFeatures gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SortGenerationFeatures -> m SortGenerationFeatures gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SortGenerationFeatures -> m SortGenerationFeatures
Ord SortGenerationFeatures Source #
Instance details Defined in CASL.Sublogic Methods compare :: SortGenerationFeatures -> SortGenerationFeatures -> Ordering (<) :: SortGenerationFeatures -> SortGenerationFeatures -> Bool (<=) :: SortGenerationFeatures -> SortGenerationFeatures -> Bool (>) :: SortGenerationFeatures -> SortGenerationFeatures -> Bool (>=) :: SortGenerationFeatures -> SortGenerationFeatures -> Bool max :: SortGenerationFeatures -> SortGenerationFeatures -> SortGenerationFeatures min :: SortGenerationFeatures -> SortGenerationFeatures -> SortGenerationFeatures
Show SortGenerationFeatures Source #
Instance details Defined in CASL.Sublogic Methods showsPrec :: Int -> SortGenerationFeatures -> ShowS show :: SortGenerationFeatures -> String showList :: [SortGenerationFeatures] -> ShowS
Generic SortGenerationFeatures
Instance details Defined in CASL.ATC_CASL Associated Types type Rep SortGenerationFeatures :: Type -> Type Methods from :: SortGenerationFeatures -> Rep SortGenerationFeatures x to :: Rep SortGenerationFeatures x -> SortGenerationFeatures
FromJSON SortGenerationFeatures
Instance details Defined in CASL.ATC_CASL Methods parseJSON :: Value -> Parser SortGenerationFeatures parseJSONList :: Value -> Parser [SortGenerationFeatures]
ToJSON SortGenerationFeatures
Instance details Defined in CASL.ATC_CASL Methods toJSON :: SortGenerationFeatures -> Value toEncoding :: SortGenerationFeatures -> Encoding toJSONList :: [SortGenerationFeatures] -> Value toEncodingList :: [SortGenerationFeatures] -> Encoding
ShATermConvertible SortGenerationFeatures
Instance details Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> SortGenerationFeatures -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SortGenerationFeatures] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SortGenerationFeatures) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SortGenerationFeatures])
type Rep SortGenerationFeatures
Instance details Defined in CASL.ATC_CASL type Rep SortGenerationFeatures = D1 ('MetaData "SortGenerationFeatures" "CASL.Sublogic" "main" 'False) (C1 ('MetaCons "NoSortGen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SortGen" 'PrefixI 'True) (S1 ('MetaSel ('Just "emptyMapping") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "onlyInjConstrs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))

class

class (Ord l, Show l) => Lattice l where Source #

Methods

cjoin :: l -> l -> l Source #

ctop :: l Source #

bot :: l Source #

Instances

Instances details

Lattice Bool Source #
Instance details Defined in Common.Lattice Methods cjoin :: Bool -> Bool -> Bool Source # ctop :: Bool Source # bot :: Bool Source #
Lattice () Source #
Instance details Defined in Common.Lattice Methods cjoin :: () -> () -> () Source # ctop :: () Source # bot :: () Source #
Lattice Sublogic Source #
Instance details Defined in ExtModal.Sublogic Methods cjoin :: Sublogic -> Sublogic -> Sublogic Source # ctop :: Sublogic Source # bot :: Sublogic Source #
(Lattice a, Lattice b) => Lattice (a, b) Source #
Instance details Defined in Common.Lattice Methods cjoin :: (a, b) -> (a, b) -> (a, b) Source # ctop :: (a, b) Source # bot :: (a, b) Source #