Hets - the Heterogeneous Tool Set

Copyright(c) Sonja Groening C. Maeder and Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityexperimental
Portabilityportable
Safe HaskellNone

HasCASL.Sublogic

Contents

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

datatypes

data Sublogic Source #

HasCASL sublogics

Constructors

Sublogic 

Fields

Instances

Eq Sublogic Source # 

Methods

(==) :: Sublogic -> Sublogic -> Bool

(/=) :: Sublogic -> Sublogic -> Bool

Data Sublogic Source # 

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

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 # 

Methods

showsPrec :: Int -> Sublogic -> ShowS

show :: Sublogic -> String

showList :: [Sublogic] -> ShowS

Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 

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 #

Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () 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 # 
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 # 
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 

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

Eq Formulas Source # 

Methods

(==) :: Formulas -> Formulas -> Bool

(/=) :: Formulas -> Formulas -> Bool

Data Formulas Source # 

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

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 # 

Methods

showsPrec :: Int -> Formulas -> ShowS

show :: Formulas -> String

showList :: [Formulas] -> ShowS

data Classes Source #

Instances

Eq Classes Source # 

Methods

(==) :: Classes -> Classes -> Bool

(/=) :: Classes -> Classes -> Bool

Data Classes Source # 

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

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 # 

Methods

showsPrec :: Int -> Classes -> ShowS

show :: Classes -> String

showList :: [Classes] -> ShowS

functions for SemiLatticeWithTop instance

topLogic :: Sublogic Source #

top element

combining sublogics restrictions

sublogicUp :: Sublogic -> Sublogic Source #

make sublogic consistent w.r.t. illegal combinations

further sublogic constants

bottom :: Sublogic Source #

bottom sublogic

noSubtypes :: Sublogic Source #

top sublogic without subtypes

noClasses :: Sublogic Source #

top sublogic without type classes

totalFuns :: Sublogic Source #

top sublogic without partiality

functions for Logic instance

sublogic to string converstion

sublogic_name :: Sublogic -> String Source #

the sublogic name as a singleton string list

list of all sublogics

sublogics_all :: [Sublogic] Source #

generate a list of all sublogics for HasCASL

checks if element is in given sublogic

in_env :: Sublogic -> Env -> Bool Source #

computes the sublogic of a given element