Hets - the Heterogeneous Tool Set
Copyright(c) Pascal Schmidt C. Maeder and Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityexperimental
Portabilityportable
Safe HaskellNone

CASL.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

types

data CASL_SL a Source #

Constructors

CASL_SL 

Fields

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lattice a => ProjectSublogicM (CASL_SL a) SYMB_ITEMS Source # 
Instance details

Defined in CASL.Logic_CASL

Lattice a => MinSublogic (CASL_SL a) Symbol Source # 
Instance details

Defined in CASL.Logic_CASL

Lattice a => MinSublogic (CASL_SL a) SYMB_MAP_ITEMS Source # 
Instance details

Defined in CASL.Logic_CASL

Lattice a => MinSublogic (CASL_SL a) SYMB_ITEMS Source # 
Instance details

Defined in CASL.Logic_CASL

MinSL a f => MinSublogic (CASL_SL a) (FORMULA f) Source # 
Instance details

Defined in CASL.Logic_CASL

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

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

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

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

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

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

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

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

Instances

Instances details
Eq SortGenerationFeatures Source # 
Instance details

Defined in CASL.Sublogic

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

Show SortGenerationFeatures Source # 
Instance details

Defined in CASL.Sublogic

Generic SortGenerationFeatures 
Instance details

Defined in CASL.ATC_CASL

Associated Types

type Rep SortGenerationFeatures :: Type -> Type

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

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) :*: S1 ('MetaSel ('Just "totality") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SortGenTotality))))

data SortGenTotality Source #

Constructors

SomePartial

partial constructors in gen constraints

OnlyTotal

no partial constructors

OnlyFree

only free types; no partial cons possible

Instances

Instances details
Eq SortGenTotality Source # 
Instance details

Defined in CASL.Sublogic

Data SortGenTotality 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) -> SortGenTotality -> c SortGenTotality

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SortGenTotality

toConstr :: SortGenTotality -> Constr

dataTypeOf :: SortGenTotality -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SortGenTotality)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SortGenTotality)

gmapT :: (forall b. Data b => b -> b) -> SortGenTotality -> SortGenTotality

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SortGenTotality -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SortGenTotality -> r

gmapQ :: (forall d. Data d => d -> u) -> SortGenTotality -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SortGenTotality -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SortGenTotality -> m SortGenTotality

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SortGenTotality -> m SortGenTotality

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SortGenTotality -> m SortGenTotality

Ord SortGenTotality Source # 
Instance details

Defined in CASL.Sublogic

Show SortGenTotality Source # 
Instance details

Defined in CASL.Sublogic

Methods

showsPrec :: Int -> SortGenTotality -> ShowS

show :: SortGenTotality -> String

showList :: [SortGenTotality] -> ShowS

Generic SortGenTotality 
Instance details

Defined in CASL.ATC_CASL

Associated Types

type Rep SortGenTotality :: Type -> Type

FromJSON SortGenTotality 
Instance details

Defined in CASL.ATC_CASL

Methods

parseJSON :: Value -> Parser SortGenTotality

parseJSONList :: Value -> Parser [SortGenTotality]

ToJSON SortGenTotality 
Instance details

Defined in CASL.ATC_CASL

Methods

toJSON :: SortGenTotality -> Value

toEncoding :: SortGenTotality -> Encoding

toJSONList :: [SortGenTotality] -> Value

toEncodingList :: [SortGenTotality] -> Encoding

ShATermConvertible SortGenTotality 
Instance details

Defined in CASL.ATC_CASL

Methods

toShATermAux :: ATermTable -> SortGenTotality -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [SortGenTotality] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, SortGenTotality)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [SortGenTotality])

type Rep SortGenTotality 
Instance details

Defined in CASL.ATC_CASL

type Rep SortGenTotality = D1 ('MetaData "SortGenTotality" "CASL.Sublogic" "main" 'False) (C1 ('MetaCons "SomePartial" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OnlyTotal" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OnlyFree" 'PrefixI 'False) (U1 :: Type -> Type)))

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

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

predicates on CASL_SL

has_sub :: CASL_SL a -> Bool Source #

has_cons :: CASL_SL a -> Bool Source #

functions for SemiLatticeWithTop instance

mkTop :: a -> CASL_SL a Source #

functions for the creation of minimal sublogics

mkBot :: a -> CASL_SL a Source #

updExtFeature :: (a -> a) -> CASL_SL a -> CASL_SL a Source #

functions for Logic instance sublogic to string conversion

sublogics_name :: (a -> String) -> CASL_SL a -> String Source #

parseSL :: (String -> Maybe (a, String)) -> String -> Maybe (CASL_SL a) Source #

parseBool :: String -> String -> (Bool, String) Source #

list of all sublogics

sublogics_all :: Lattice a => [a] -> [CASL_SL a] Source #

sDims :: Lattice a => [[a]] -> [[CASL_SL a]] Source #

computes the sublogic of a given element

sl_sig_items :: Lattice a => (s -> CASL_SL a) -> (f -> CASL_SL a) -> SIG_ITEMS s f -> CASL_SL a Source #

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

sl_op_item :: Lattice a => (f -> CASL_SL a) -> OP_ITEM f -> CASL_SL a Source #

sl_pred_item :: Lattice a => (f -> CASL_SL a) -> PRED_ITEM f -> CASL_SL a Source #

sl_sentence :: Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a Source #

sl_term :: Lattice a => (f -> CASL_SL a) -> TERM f -> CASL_SL a Source #

sl_sign :: Lattice a => (e -> CASL_SL a) -> Sign f e -> CASL_SL a Source #

sl_morphism :: Lattice a => (e -> CASL_SL a) -> Morphism f e m -> CASL_SL a Source #

projects an element into a given sublogic

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

pr_sign :: CASL_SL a -> Sign f e -> Sign f e Source #

pr_morphism :: Lattice a => CASL_SL a -> Morphism f e m -> Morphism f e m Source #

pr_epsilon :: m -> CASL_SL a -> Sign f e -> Morphism f e m Source #

pr_symbol :: Lattice a => CASL_SL a -> Symbol -> Maybe Symbol Source #