Copyright	(c) Sonja Groening 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

HasCASL.Sublogic

Contents

datatypes
functions for SemiLatticeWithTop instance
combining sublogics restrictions
further sublogic constants
functions for Logic instance
computes the sublogic of a given element

Description

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

Synopsis

data Sublogic = Sublogic {
- has_sub :: Bool
- has_part :: Bool
- has_eq :: Bool
- has_pred :: Bool
- type_classes :: Classes
- has_polymorphism :: Bool
- has_type_constructors :: Bool
- has_products :: Bool
- which_logic :: Formulas
}
data Formulas
- = Atomic
- | Horn
- | GHorn
- | FOL
- | HOL
data Classes
- = NoClasses
- | SimpleTypeClasses
- | ConstructorClasses
topLogic :: Sublogic
sublogic_max :: Sublogic -> Sublogic -> Sublogic
sublogic_min :: Sublogic -> Sublogic -> Sublogic
sublogicUp :: Sublogic -> Sublogic
need_hol :: Sublogic
bottom :: Sublogic
noSubtypes :: Sublogic
noClasses :: Sublogic
totalFuns :: Sublogic
caslLogic :: Sublogic
sublogic_name :: Sublogic -> String
sublogics_all :: [Sublogic]
in_basicSpec :: Sublogic -> BasicSpec -> Bool
in_sentence :: Sublogic -> Sentence -> Bool
in_symbItems :: Sublogic -> SymbItems -> Bool
in_symbMapItems :: Sublogic -> SymbMapItems -> Bool
in_env :: Sublogic -> Env -> Bool
in_morphism :: Sublogic -> Morphism -> Bool
in_symbol :: Sublogic -> Symbol -> Bool
sl_basicSpec :: BasicSpec -> Sublogic
sl_sentence :: Sentence -> Sublogic
sl_symbItems :: SymbItems -> Sublogic
sl_symbMapItems :: SymbMapItems -> Sublogic
sl_env :: Env -> Sublogic
sl_morphism :: Morphism -> Sublogic
sl_symbol :: Symbol -> Sublogic

datatypes

data Sublogic Source #

HasCASL sublogics

Constructors

Sublogic
Fields has_sub :: Bool subsorting has_part :: Bool partiality has_eq :: Bool equality has_pred :: Bool predicates type_classes :: Classes has_polymorphism :: Bool has_type_constructors :: Bool has_products :: Bool which_logic :: Formulas

Instances

Instances details

Eq Sublogic Source #
Instance details Defined in HasCASL.Sublogic Methods (==) :: Sublogic -> Sublogic -> Bool (/=) :: Sublogic -> Sublogic -> Bool
Data Sublogic Source #
Instance details Defined in HasCASL.Sublogic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sublogic -> c Sublogic gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sublogic toConstr :: Sublogic -> Constr dataTypeOf :: Sublogic -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sublogic) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sublogic) gmapT :: (forall b. Data b => b -> b) -> Sublogic -> Sublogic gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sublogic -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sublogic -> r gmapQ :: (forall d. Data d => d -> u) -> Sublogic -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Sublogic -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sublogic -> m Sublogic gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sublogic -> m Sublogic gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sublogic -> m Sublogic
Ord Sublogic Source #
Instance details Defined in HasCASL.Sublogic Methods compare :: Sublogic -> Sublogic -> Ordering (<) :: Sublogic -> Sublogic -> Bool (<=) :: Sublogic -> Sublogic -> Bool (>) :: Sublogic -> Sublogic -> Bool (>=) :: Sublogic -> Sublogic -> Bool max :: Sublogic -> Sublogic -> Sublogic min :: Sublogic -> Sublogic -> Sublogic
Show Sublogic Source #
Instance details Defined in HasCASL.Sublogic Methods showsPrec :: Int -> Sublogic -> ShowS show :: Sublogic -> String showList :: [Sublogic] -> ShowS
Generic Sublogic
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep Sublogic :: Type -> Type Methods from :: Sublogic -> Rep Sublogic x to :: Rep Sublogic x -> Sublogic
FromJSON Sublogic
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser Sublogic parseJSONList :: Value -> Parser [Sublogic]
ToJSON Sublogic
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: Sublogic -> Value toEncoding :: Sublogic -> Encoding toJSONList :: [Sublogic] -> Value toEncodingList :: [Sublogic] -> Encoding
ShATermConvertible Sublogic
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> Sublogic -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Sublogic] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Sublogic) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sublogic])
SublogicName Sublogic Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods sublogicName :: Sublogic -> String Source #
SemiLatticeWithTop Sublogic Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods lub :: Sublogic -> Sublogic -> Sublogic Source # top :: Sublogic Source #
ProjectSublogicM Sublogic SymbMapItems Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods projectSublogicM :: Sublogic -> SymbMapItems -> Maybe SymbMapItems Source #
ProjectSublogicM Sublogic SymbItems Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods projectSublogicM :: Sublogic -> SymbItems -> Maybe SymbItems Source #
ProjectSublogicM Sublogic Symbol Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods projectSublogicM :: Sublogic -> Symbol -> Maybe Symbol Source #
ProjectSublogic Sublogic BasicSpec Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods projectSublogic :: Sublogic -> BasicSpec -> BasicSpec Source #
ProjectSublogic Sublogic Morphism Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods projectSublogic :: Sublogic -> Morphism -> Morphism Source #
ProjectSublogic Sublogic Env Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods projectSublogic :: Sublogic -> Env -> Env Source #
MinSublogic Sublogic SymbMapItems Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods minSublogic :: SymbMapItems -> Sublogic Source #
MinSublogic Sublogic SymbItems Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods minSublogic :: SymbItems -> Sublogic Source #
MinSublogic Sublogic BasicSpec Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods minSublogic :: BasicSpec -> Sublogic Source #
MinSublogic Sublogic Symbol Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods minSublogic :: Symbol -> Sublogic Source #
MinSublogic Sublogic Morphism Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods minSublogic :: Morphism -> Sublogic Source #
MinSublogic Sublogic Env Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods minSublogic :: Env -> Sublogic Source #
MinSublogic Sublogic Sentence Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods minSublogic :: Sentence -> Sublogic Source #
Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source # stability :: HasCASL -> Stability Source # data_logic :: HasCASL -> Maybe AnyLogic Source # top_sublogic :: HasCASL -> Sublogic Source # all_sublogics :: HasCASL -> [Sublogic] Source # bottomSublogic :: HasCASL -> Maybe Sublogic Source # sublogicDimensions :: HasCASL -> [[Sublogic]] Source # parseSublogic :: HasCASL -> String -> Maybe Sublogic Source # proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source # provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source # default_prover :: HasCASL -> String Source # cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source # conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source # empty_proof_tree :: HasCASL -> () Source # syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source # omdoc_metatheory :: HasCASL -> Maybe OMCD Source # export_symToOmdoc :: HasCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source # addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source # sublogicOfTheo :: HasCASL -> (Env, [Sentence]) -> Sublogic Source #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.THFP_P2HasCASL Methods sourceLogic :: THFP_P2HasCASL -> THF Source # sourceSublogic :: THFP_P2HasCASL -> THFSl Source # sourceSublogicLossy :: THFP_P2HasCASL -> THFSl Source # minSourceTheory :: THFP_P2HasCASL -> Maybe (LibName, String) Source # targetLogic :: THFP_P2HasCASL -> HasCASL Source # mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic Source # map_theory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # map_morphism :: THFP_P2HasCASL -> MorphismTHF -> Result Morphism Source # map_sentence :: THFP_P2HasCASL -> SignTHF -> THFFormula -> Result Sentence Source # map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol Source # extractModel :: THFP_P2HasCASL -> SignTHF -> () -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2HasCASL -> Bool Source # has_model_expansion :: THFP_P2HasCASL -> Bool Source # is_weakly_amalgamable :: THFP_P2HasCASL -> Bool Source # constituents :: THFP_P2HasCASL -> [String] Source # isInclusionComorphism :: THFP_P2HasCASL -> Bool Source # rps :: THFP_P2HasCASL -> Bool Source # eps :: THFP_P2HasCASL -> Bool Source # isGTC :: THFP_P2HasCASL -> Bool Source #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2PairsInIsaHOL Methods sourceLogic :: PCoClTyConsHOL2PairsInIsaHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2PairsInIsaHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2PairsInIsaHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # constituents :: PCoClTyConsHOL2PairsInIsaHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # rps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # eps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # isGTC :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2IsabelleHOL Methods sourceLogic :: PCoClTyConsHOL2IsabelleHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2IsabelleHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # constituents :: PCoClTyConsHOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # rps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # eps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # isGTC :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.MonadicHasCASLTranslation Methods sourceLogic :: MonadicHasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: MonadicHasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: MonadicHasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: MonadicHasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: MonadicHasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: MonadicHasCASL2IsabelleHOL -> Bool Source # constituents :: MonadicHasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: MonadicHasCASL2IsabelleHOL -> Bool Source # rps :: MonadicHasCASL2IsabelleHOL -> Bool Source # eps :: MonadicHasCASL2IsabelleHOL -> Bool Source # isGTC :: MonadicHasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.HasCASL2THFP_P Methods sourceLogic :: HasCASL2THFP_P -> HasCASL Source # sourceSublogic :: HasCASL2THFP_P -> Sublogic Source # sourceSublogicLossy :: HasCASL2THFP_P -> Sublogic Source # minSourceTheory :: HasCASL2THFP_P -> Maybe (LibName, String) Source # targetLogic :: HasCASL2THFP_P -> THF Source # mapSublogic :: HasCASL2THFP_P -> Sublogic -> Maybe THFSl Source # map_theory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: HasCASL2THFP_P -> Morphism -> Result MorphismTHF Source # map_sentence :: HasCASL2THFP_P -> Env -> Sentence -> Result THFFormula Source # map_symbol :: HasCASL2THFP_P -> Env -> Symbol -> Set SymbolTHF Source # extractModel :: HasCASL2THFP_P -> Env -> ProofTree -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2THFP_P -> Bool Source # has_model_expansion :: HasCASL2THFP_P -> Bool Source # is_weakly_amalgamable :: HasCASL2THFP_P -> Bool Source # constituents :: HasCASL2THFP_P -> [String] Source # isInclusionComorphism :: HasCASL2THFP_P -> Bool Source # rps :: HasCASL2THFP_P -> Bool Source # eps :: HasCASL2THFP_P -> Bool Source # isGTC :: HasCASL2THFP_P -> Bool Source #
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2PCoClTyConsHOL Methods sourceLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # sourceSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2PCoClTyConsHOL -> Sublogic Source # minSourceTheory :: HasCASL2PCoClTyConsHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # mapSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2PCoClTyConsHOL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2PCoClTyConsHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2PCoClTyConsHOL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2PCoClTyConsHOL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2PCoClTyConsHOL -> Bool Source # has_model_expansion :: HasCASL2PCoClTyConsHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2PCoClTyConsHOL -> Bool Source # constituents :: HasCASL2PCoClTyConsHOL -> [String] Source # isInclusionComorphism :: HasCASL2PCoClTyConsHOL -> Bool Source # rps :: HasCASL2PCoClTyConsHOL -> Bool Source # eps :: HasCASL2PCoClTyConsHOL -> Bool Source # isGTC :: HasCASL2PCoClTyConsHOL -> Bool Source #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods sourceLogic :: HasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: HasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: HasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: HasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: HasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: HasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2IsabelleHOL -> Bool Source # constituents :: HasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: HasCASL2IsabelleHOL -> Bool Source # rps :: HasCASL2IsabelleHOL -> Bool Source # eps :: HasCASL2IsabelleHOL -> Bool Source # isGTC :: HasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2HasCASL Methods sourceLogic :: HasCASL2HasCASL -> HasCASL Source # sourceSublogic :: HasCASL2HasCASL -> Sublogic Source # sourceSublogicLossy :: HasCASL2HasCASL -> Sublogic Source # minSourceTheory :: HasCASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2HasCASL -> HasCASL Source # mapSublogic :: HasCASL2HasCASL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2HasCASL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2HasCASL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2HasCASL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2HasCASL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2HasCASL -> Bool Source # has_model_expansion :: HasCASL2HasCASL -> Bool Source # is_weakly_amalgamable :: HasCASL2HasCASL -> Bool Source # constituents :: HasCASL2HasCASL -> [String] Source # isInclusionComorphism :: HasCASL2HasCASL -> Bool Source # rps :: HasCASL2HasCASL -> Bool Source # eps :: HasCASL2HasCASL -> Bool Source # isGTC :: HasCASL2HasCASL -> 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 #
type Rep Sublogic
Instance details Defined in HasCASL.ATC_HasCASL type Rep Sublogic = D1 ('MetaData "Sublogic" "HasCASL.Sublogic" "main" 'False) (C1 ('MetaCons "Sublogic" 'PrefixI 'True) (((S1 ('MetaSel ('Just "has_sub") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "has_part") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "has_eq") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "has_pred") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :: ((S1 ('MetaSel ('Just "type_classes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Classes) :: S1 ('MetaSel ('Just "has_polymorphism") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "has_type_constructors") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "has_products") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "which_logic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Formulas))))))

data Formulas Source #

formula kinds of HasCASL sublogics

Constructors

Atomic	atomic logic
Horn	positive conditional logic
GHorn	generalized positive conditional logic
FOL	first-order logic
HOL	higher-order logic

Instances

Instances details

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

data Classes Source #

Constructors

NoClasses
SimpleTypeClasses
ConstructorClasses

Instances

Instances details

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