Copyright	(c) Christian Maeder and Uni Bremen 2003-2005
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	experimental
Portability	portable
Safe Haskell	Safe

HasCASL.Le

Contents

class info
type info
sentences
variables
assumptions
the local environment and final signature
accessing the environment
morphisms
symbol stuff

Description

abstract syntax during static analysis

Synopsis

class info

data ClassInfo Source #

store the raw kind and all superclasses of a class identifier

Constructors

ClassInfo
Fields rawKind :: RawKind classKinds :: Set Kind

Instances

Eq ClassInfo Source #
Methods (==) :: ClassInfo -> ClassInfo -> Bool (/=) :: ClassInfo -> ClassInfo -> Bool
Data ClassInfo Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ClassInfo -> c ClassInfo gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ClassInfo toConstr :: ClassInfo -> Constr dataTypeOf :: ClassInfo -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c ClassInfo) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ClassInfo) gmapT :: (forall b. Data b => b -> b) -> ClassInfo -> ClassInfo gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ClassInfo -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ClassInfo -> r gmapQ :: (forall d. Data d => d -> u) -> ClassInfo -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ClassInfo -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ClassInfo -> m ClassInfo gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ClassInfo -> m ClassInfo gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ClassInfo -> m ClassInfo
Ord ClassInfo Source #
Methods compare :: ClassInfo -> ClassInfo -> Ordering (<) :: ClassInfo -> ClassInfo -> Bool (<=) :: ClassInfo -> ClassInfo -> Bool (>) :: ClassInfo -> ClassInfo -> Bool (>=) :: ClassInfo -> ClassInfo -> Bool max :: ClassInfo -> ClassInfo -> ClassInfo min :: ClassInfo -> ClassInfo -> ClassInfo
Show ClassInfo Source #
Methods showsPrec :: Int -> ClassInfo -> ShowS show :: ClassInfo -> String showList :: [ClassInfo] -> ShowS

type ClassMap = Map Id ClassInfo Source #

mapping class identifiers to their definition

type info

data GenKind Source #

data type generatedness indicator

Constructors

Free
Generated
Loose

Instances

Eq GenKind Source #
Methods (==) :: GenKind -> GenKind -> Bool (/=) :: GenKind -> GenKind -> Bool
Data GenKind Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GenKind -> c GenKind gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GenKind toConstr :: GenKind -> Constr dataTypeOf :: GenKind -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c GenKind) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GenKind) gmapT :: (forall b. Data b => b -> b) -> GenKind -> GenKind gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GenKind -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GenKind -> r gmapQ :: (forall d. Data d => d -> u) -> GenKind -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> GenKind -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> GenKind -> m GenKind gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GenKind -> m GenKind gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GenKind -> m GenKind
Ord GenKind Source #
Methods compare :: GenKind -> GenKind -> Ordering (<) :: GenKind -> GenKind -> Bool (<=) :: GenKind -> GenKind -> Bool (>) :: GenKind -> GenKind -> Bool (>=) :: GenKind -> GenKind -> Bool max :: GenKind -> GenKind -> GenKind min :: GenKind -> GenKind -> GenKind
Show GenKind Source #
Methods showsPrec :: Int -> GenKind -> ShowS show :: GenKind -> String showList :: [GenKind] -> ShowS

data AltDefn Source #

an analysed alternative with a list of (product) types

Constructors

Construct (Maybe Id) [Type] Partiality [[Selector]]

Instances

Eq AltDefn Source #
Methods (==) :: AltDefn -> AltDefn -> Bool (/=) :: AltDefn -> AltDefn -> Bool
Data AltDefn Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AltDefn -> c AltDefn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AltDefn toConstr :: AltDefn -> Constr dataTypeOf :: AltDefn -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c AltDefn) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AltDefn) gmapT :: (forall b. Data b => b -> b) -> AltDefn -> AltDefn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AltDefn -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AltDefn -> r gmapQ :: (forall d. Data d => d -> u) -> AltDefn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> AltDefn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> AltDefn -> m AltDefn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AltDefn -> m AltDefn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AltDefn -> m AltDefn
Ord AltDefn Source #
Methods compare :: AltDefn -> AltDefn -> Ordering (<) :: AltDefn -> AltDefn -> Bool (<=) :: AltDefn -> AltDefn -> Bool (>) :: AltDefn -> AltDefn -> Bool (>=) :: AltDefn -> AltDefn -> Bool max :: AltDefn -> AltDefn -> AltDefn min :: AltDefn -> AltDefn -> AltDefn
Show AltDefn Source #
Methods showsPrec :: Int -> AltDefn -> ShowS show :: AltDefn -> String showList :: [AltDefn] -> ShowS

data Selector Source #

an analysed component

Constructors

Select (Maybe Id) Type Partiality

Instances

Eq Selector Source #
Methods (==) :: Selector -> Selector -> Bool (/=) :: Selector -> Selector -> Bool
Data Selector Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Selector -> c Selector gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Selector toConstr :: Selector -> Constr dataTypeOf :: Selector -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Selector) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Selector) gmapT :: (forall b. Data b => b -> b) -> Selector -> Selector gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Selector -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Selector -> r gmapQ :: (forall d. Data d => d -> u) -> Selector -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Selector -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Selector -> m Selector gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Selector -> m Selector gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Selector -> m Selector
Ord Selector Source #
Methods compare :: Selector -> Selector -> Ordering (<) :: Selector -> Selector -> Bool (<=) :: Selector -> Selector -> Bool (>) :: Selector -> Selector -> Bool (>=) :: Selector -> Selector -> Bool max :: Selector -> Selector -> Selector min :: Selector -> Selector -> Selector
Show Selector Source #
Methods showsPrec :: Int -> Selector -> ShowS show :: Selector -> String showList :: [Selector] -> ShowS

type IdMap = Map Id Id Source #

a mapping of type (and disjoint class) identifiers

data DataEntry Source #

data entries are produced from possibly mutual recursive data types. The top-level identifiers of these types are never renamed but there renaming is stored in the identifier map. This identifier map must never be empty (even without renamings) because (the domain of) this map is used to store the other (recursively dependent) top-level identifiers.

Constructors

DataEntry IdMap Id GenKind [TypeArg] RawKind (Set AltDefn)

Instances

Eq DataEntry Source #
Methods (==) :: DataEntry -> DataEntry -> Bool (/=) :: DataEntry -> DataEntry -> Bool
Data DataEntry Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataEntry -> c DataEntry gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataEntry toConstr :: DataEntry -> Constr dataTypeOf :: DataEntry -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c DataEntry) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataEntry) gmapT :: (forall b. Data b => b -> b) -> DataEntry -> DataEntry gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataEntry -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataEntry -> r gmapQ :: (forall d. Data d => d -> u) -> DataEntry -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DataEntry -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataEntry -> m DataEntry gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataEntry -> m DataEntry gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataEntry -> m DataEntry
Ord DataEntry Source #
Methods compare :: DataEntry -> DataEntry -> Ordering (<) :: DataEntry -> DataEntry -> Bool (<=) :: DataEntry -> DataEntry -> Bool (>) :: DataEntry -> DataEntry -> Bool (>=) :: DataEntry -> DataEntry -> Bool max :: DataEntry -> DataEntry -> DataEntry min :: DataEntry -> DataEntry -> DataEntry
Show DataEntry Source #
Methods showsPrec :: Int -> DataEntry -> ShowS show :: DataEntry -> String showList :: [DataEntry] -> ShowS

data TypeDefn Source #

possible definitions for type identifiers

Constructors

NoTypeDefn
PreDatatype
DatatypeDefn DataEntry
AliasTypeDefn Type

Instances

Eq TypeDefn Source #
Methods (==) :: TypeDefn -> TypeDefn -> Bool (/=) :: TypeDefn -> TypeDefn -> Bool
Data TypeDefn Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeDefn -> c TypeDefn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeDefn toConstr :: TypeDefn -> Constr dataTypeOf :: TypeDefn -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TypeDefn) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeDefn) gmapT :: (forall b. Data b => b -> b) -> TypeDefn -> TypeDefn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeDefn -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeDefn -> r gmapQ :: (forall d. Data d => d -> u) -> TypeDefn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeDefn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn
Ord TypeDefn Source #
Methods compare :: TypeDefn -> TypeDefn -> Ordering (<) :: TypeDefn -> TypeDefn -> Bool (<=) :: TypeDefn -> TypeDefn -> Bool (>) :: TypeDefn -> TypeDefn -> Bool (>=) :: TypeDefn -> TypeDefn -> Bool max :: TypeDefn -> TypeDefn -> TypeDefn min :: TypeDefn -> TypeDefn -> TypeDefn
Show TypeDefn Source #
Methods showsPrec :: Int -> TypeDefn -> ShowS show :: TypeDefn -> String showList :: [TypeDefn] -> ShowS

data TypeInfo Source #

for type identifiers also store the raw kind, instances and supertypes

Constructors

TypeInfo
Fields typeKind :: RawKind otherTypeKinds :: Set Kind superTypes :: Set Id typeDefn :: TypeDefn

Instances

Eq TypeInfo Source #
Methods (==) :: TypeInfo -> TypeInfo -> Bool (/=) :: TypeInfo -> TypeInfo -> Bool
Data TypeInfo Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeInfo -> c TypeInfo gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeInfo toConstr :: TypeInfo -> Constr dataTypeOf :: TypeInfo -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TypeInfo) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeInfo) gmapT :: (forall b. Data b => b -> b) -> TypeInfo -> TypeInfo gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeInfo -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeInfo -> r gmapQ :: (forall d. Data d => d -> u) -> TypeInfo -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeInfo -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo
Ord TypeInfo Source #
Methods compare :: TypeInfo -> TypeInfo -> Ordering (<) :: TypeInfo -> TypeInfo -> Bool (<=) :: TypeInfo -> TypeInfo -> Bool (>) :: TypeInfo -> TypeInfo -> Bool (>=) :: TypeInfo -> TypeInfo -> Bool max :: TypeInfo -> TypeInfo -> TypeInfo min :: TypeInfo -> TypeInfo -> TypeInfo
Show TypeInfo Source #
Methods showsPrec :: Int -> TypeInfo -> ShowS show :: TypeInfo -> String showList :: [TypeInfo] -> ShowS

type TypeMap = Map Id TypeInfo Source #

mapping type identifiers to their definition

starTypeInfo :: TypeInfo Source #

the minimal information for a sort

mapType :: IdMap -> Type -> Type Source #

rename the type according to identifier map (for comorphisms)

sentences

data Sentence Source #

data types are also special sentences because of their properties

Constructors

Formula Term
DatatypeSen [DataEntry]
ProgEqSen Id TypeScheme ProgEq

Instances

Eq Sentence Source #
Methods (==) :: Sentence -> Sentence -> Bool (/=) :: Sentence -> Sentence -> Bool
Data Sentence Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sentence -> c Sentence gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sentence toConstr :: Sentence -> Constr dataTypeOf :: Sentence -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Sentence) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sentence) gmapT :: (forall b. Data b => b -> b) -> Sentence -> Sentence gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sentence -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sentence -> r gmapQ :: (forall d. Data d => d -> u) -> Sentence -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Sentence -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sentence -> m Sentence gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sentence -> m Sentence gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sentence -> m Sentence
Ord Sentence Source #
Methods compare :: Sentence -> Sentence -> Ordering (<) :: Sentence -> Sentence -> Bool (<=) :: Sentence -> Sentence -> Bool (>) :: Sentence -> Sentence -> Bool (>=) :: Sentence -> Sentence -> Bool max :: Sentence -> Sentence -> Sentence min :: Sentence -> Sentence -> Sentence
Show Sentence Source #
Methods showsPrec :: Int -> Sentence -> ShowS show :: Sentence -> String showList :: [Sentence] -> ShowS
GetRange Sentence Source #
Methods getRange :: Sentence -> Range Source # rangeSpan :: Sentence -> [Pos] Source #
Sentences HasCASL Sentence Env Morphism Symbol Source #
Methods map_sen :: HasCASL -> Morphism -> Sentence -> Result Sentence Source # simplify_sen :: HasCASL -> Env -> Sentence -> Sentence Source # negation :: HasCASL -> Sentence -> Maybe Sentence Source # print_sign :: HasCASL -> Env -> Doc Source # print_named :: HasCASL -> Named Sentence -> Doc Source # sym_of :: HasCASL -> Env -> [Set Symbol] Source # mostSymsOf :: HasCASL -> Env -> [Symbol] Source # symmap_of :: HasCASL -> Morphism -> EndoMap Symbol Source # sym_name :: HasCASL -> Symbol -> Id Source # sym_label :: HasCASL -> Symbol -> Maybe String Source # fullSymName :: HasCASL -> Symbol -> String Source # symKind :: HasCASL -> Symbol -> String Source # symsOfSen :: HasCASL -> Env -> Sentence -> [Symbol] Source # pair_symbols :: HasCASL -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source #
Methods basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source # sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source # extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source # stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source # convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source # ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source # signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source # qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source # id_to_raw :: HasCASL -> Id -> RawSymbol Source # matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: HasCASL -> Env Source # add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source # signature_union :: HasCASL -> Env -> Env -> Result Env Source # signatureDiff :: HasCASL -> Env -> Env -> Result Env Source # intersection :: HasCASL -> Env -> Env -> Result Env Source # final_union :: HasCASL -> Env -> Env -> Result Env Source # morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: HasCASL -> Env -> Env -> Bool Source # subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source # generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source # induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source # is_transportable :: HasCASL -> Morphism -> Bool Source # is_injective :: HasCASL -> Morphism -> Bool Source # theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #
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 # sublogicOfTheo :: HasCASL -> (Env, [Sentence]) -> Sublogic Source #
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
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 #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
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 #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
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 #
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 -> Symbol -> 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 #
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 #
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 -> Symbol -> 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 #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
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 #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
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 #

variables

data TypeVarDefn Source #

type variable are kept separately

Constructors

TypeVarDefn Variance VarKind RawKind Int

Instances

Data TypeVarDefn Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeVarDefn -> c TypeVarDefn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeVarDefn toConstr :: TypeVarDefn -> Constr dataTypeOf :: TypeVarDefn -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TypeVarDefn) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeVarDefn) gmapT :: (forall b. Data b => b -> b) -> TypeVarDefn -> TypeVarDefn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeVarDefn -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeVarDefn -> r gmapQ :: (forall d. Data d => d -> u) -> TypeVarDefn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeVarDefn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn
Show TypeVarDefn Source #
Methods showsPrec :: Int -> TypeVarDefn -> ShowS show :: TypeVarDefn -> String showList :: [TypeVarDefn] -> ShowS

type LocalTypeVars = Map Id TypeVarDefn Source #

mapping type variables to their definition

data VarDefn Source #

the type of a local variable

Constructors

VarDefn Type

Instances

Data VarDefn Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VarDefn -> c VarDefn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VarDefn toConstr :: VarDefn -> Constr dataTypeOf :: VarDefn -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c VarDefn) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarDefn) gmapT :: (forall b. Data b => b -> b) -> VarDefn -> VarDefn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VarDefn -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VarDefn -> r gmapQ :: (forall d. Data d => d -> u) -> VarDefn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> VarDefn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> VarDefn -> m VarDefn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VarDefn -> m VarDefn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VarDefn -> m VarDefn
Show VarDefn Source #
Methods showsPrec :: Int -> VarDefn -> ShowS show :: VarDefn -> String showList :: [VarDefn] -> ShowS

assumptions

data ConstrInfo Source #

name and scheme of a constructor

Constructors

ConstrInfo
Fields constrId :: Id constrType :: TypeScheme

Instances

Eq ConstrInfo Source #
Methods (==) :: ConstrInfo -> ConstrInfo -> Bool (/=) :: ConstrInfo -> ConstrInfo -> Bool
Data ConstrInfo Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConstrInfo -> c ConstrInfo gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConstrInfo toConstr :: ConstrInfo -> Constr dataTypeOf :: ConstrInfo -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c ConstrInfo) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConstrInfo) gmapT :: (forall b. Data b => b -> b) -> ConstrInfo -> ConstrInfo gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConstrInfo -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConstrInfo -> r gmapQ :: (forall d. Data d => d -> u) -> ConstrInfo -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ConstrInfo -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConstrInfo -> m ConstrInfo gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConstrInfo -> m ConstrInfo gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConstrInfo -> m ConstrInfo
Ord ConstrInfo Source #
Methods compare :: ConstrInfo -> ConstrInfo -> Ordering (<) :: ConstrInfo -> ConstrInfo -> Bool (<=) :: ConstrInfo -> ConstrInfo -> Bool (>) :: ConstrInfo -> ConstrInfo -> Bool (>=) :: ConstrInfo -> ConstrInfo -> Bool max :: ConstrInfo -> ConstrInfo -> ConstrInfo min :: ConstrInfo -> ConstrInfo -> ConstrInfo
Show ConstrInfo Source #
Methods showsPrec :: Int -> ConstrInfo -> ShowS show :: ConstrInfo -> String showList :: [ConstrInfo] -> ShowS

data OpDefn Source #

possible definitions of functions

Constructors

NoOpDefn OpBrand
ConstructData Id	target type
SelectData (Set ConstrInfo) Id	constructors of source type
Definition OpBrand Term

Instances

Eq OpDefn Source #
Methods (==) :: OpDefn -> OpDefn -> Bool (/=) :: OpDefn -> OpDefn -> Bool
Data OpDefn Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpDefn -> c OpDefn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpDefn toConstr :: OpDefn -> Constr dataTypeOf :: OpDefn -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c OpDefn) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpDefn) gmapT :: (forall b. Data b => b -> b) -> OpDefn -> OpDefn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpDefn -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpDefn -> r gmapQ :: (forall d. Data d => d -> u) -> OpDefn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> OpDefn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpDefn -> m OpDefn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpDefn -> m OpDefn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpDefn -> m OpDefn
Ord OpDefn Source #
Methods compare :: OpDefn -> OpDefn -> Ordering (<) :: OpDefn -> OpDefn -> Bool (<=) :: OpDefn -> OpDefn -> Bool (>) :: OpDefn -> OpDefn -> Bool (>=) :: OpDefn -> OpDefn -> Bool max :: OpDefn -> OpDefn -> OpDefn min :: OpDefn -> OpDefn -> OpDefn
Show OpDefn Source #
Methods showsPrec :: Int -> OpDefn -> ShowS show :: OpDefn -> String showList :: [OpDefn] -> ShowS

data OpInfo Source #

scheme, attributes and definition for function identifiers

Constructors

OpInfo
Fields opType :: TypeScheme opAttrs :: Set OpAttr opDefn :: OpDefn

Instances

Eq OpInfo Source #
Methods (==) :: OpInfo -> OpInfo -> Bool (/=) :: OpInfo -> OpInfo -> Bool
Data OpInfo Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpInfo -> c OpInfo gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpInfo toConstr :: OpInfo -> Constr dataTypeOf :: OpInfo -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c OpInfo) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpInfo) gmapT :: (forall b. Data b => b -> b) -> OpInfo -> OpInfo gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpInfo -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpInfo -> r gmapQ :: (forall d. Data d => d -> u) -> OpInfo -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> OpInfo -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo
Ord OpInfo Source #
Methods compare :: OpInfo -> OpInfo -> Ordering (<) :: OpInfo -> OpInfo -> Bool (<=) :: OpInfo -> OpInfo -> Bool (>) :: OpInfo -> OpInfo -> Bool (>=) :: OpInfo -> OpInfo -> Bool max :: OpInfo -> OpInfo -> OpInfo min :: OpInfo -> OpInfo -> OpInfo
Show OpInfo Source #
Methods showsPrec :: Int -> OpInfo -> ShowS show :: OpInfo -> String showList :: [OpInfo] -> ShowS

isConstructor :: OpInfo -> Bool Source #

test for constructor

type Assumps = Map Id (Set OpInfo) Source #

mapping operation identifiers to their definition

the local environment and final signature

data Env Source #

the signature is established by the classes, types and assumptions

Constructors

Env
Fields classMap :: ClassMap typeMap :: TypeMap localTypeVars :: LocalTypeVars assumps :: Assumps binders :: Map Id Id localVars :: Map Id VarDefn sentences :: [Named Sentence] declSymbs :: Set Symbol envDiags :: [Diagnosis] preIds :: (PrecMap, Set Id) globAnnos :: GlobalAnnos counter :: Int

Instances

Eq Env Source #
Methods (==) :: Env -> Env -> Bool (/=) :: Env -> Env -> Bool
Data Env Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Env -> c Env gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Env toConstr :: Env -> Constr dataTypeOf :: Env -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Env) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Env) gmapT :: (forall b. Data b => b -> b) -> Env -> Env gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Env -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Env -> r gmapQ :: (forall d. Data d => d -> u) -> Env -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Env -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Env -> m Env gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Env -> m Env gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Env -> m Env
Ord Env Source #
Methods compare :: Env -> Env -> Ordering (<) :: Env -> Env -> Bool (<=) :: Env -> Env -> Bool (>) :: Env -> Env -> Bool (>=) :: Env -> Env -> Bool max :: Env -> Env -> Env min :: Env -> Env -> Env
Show Env Source #
Methods showsPrec :: Int -> Env -> ShowS show :: Env -> String showList :: [Env] -> ShowS
Sentences HasCASL Sentence Env Morphism Symbol Source #
Methods map_sen :: HasCASL -> Morphism -> Sentence -> Result Sentence Source # simplify_sen :: HasCASL -> Env -> Sentence -> Sentence Source # negation :: HasCASL -> Sentence -> Maybe Sentence Source # print_sign :: HasCASL -> Env -> Doc Source # print_named :: HasCASL -> Named Sentence -> Doc Source # sym_of :: HasCASL -> Env -> [Set Symbol] Source # mostSymsOf :: HasCASL -> Env -> [Symbol] Source # symmap_of :: HasCASL -> Morphism -> EndoMap Symbol Source # sym_name :: HasCASL -> Symbol -> Id Source # sym_label :: HasCASL -> Symbol -> Maybe String Source # fullSymName :: HasCASL -> Symbol -> String Source # symKind :: HasCASL -> Symbol -> String Source # symsOfSen :: HasCASL -> Env -> Sentence -> [Symbol] Source # pair_symbols :: HasCASL -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source #
Methods basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source # sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source # extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source # stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source # convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source # ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source # signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source # qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source # id_to_raw :: HasCASL -> Id -> RawSymbol Source # matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: HasCASL -> Env Source # add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source # signature_union :: HasCASL -> Env -> Env -> Result Env Source # signatureDiff :: HasCASL -> Env -> Env -> Result Env Source # intersection :: HasCASL -> Env -> Env -> Result Env Source # final_union :: HasCASL -> Env -> Env -> Result Env Source # morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: HasCASL -> Env -> Env -> Bool Source # subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source # generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source # induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source # is_transportable :: HasCASL -> Morphism -> Bool Source # is_injective :: HasCASL -> Morphism -> Bool Source # theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #
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 # sublogicOfTheo :: HasCASL -> (Env, [Sentence]) -> Sublogic Source #
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
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 #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
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 #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
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 #
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 -> Symbol -> 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 #
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 #
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 -> Symbol -> 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 #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
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 #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
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 #

initialEnv :: Env Source #

the empty environment (fresh variables start with 1)

data Constrain Source #

Constructors

Kinding Type Kind
Subtyping Type Type

Instances

Eq Constrain Source #
Methods (==) :: Constrain -> Constrain -> Bool (/=) :: Constrain -> Constrain -> Bool
Data Constrain Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Constrain -> c Constrain gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Constrain toConstr :: Constrain -> Constr dataTypeOf :: Constrain -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Constrain) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constrain) gmapT :: (forall b. Data b => b -> b) -> Constrain -> Constrain gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Constrain -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Constrain -> r gmapQ :: (forall d. Data d => d -> u) -> Constrain -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Constrain -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Constrain -> m Constrain gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Constrain -> m Constrain gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Constrain -> m Constrain
Ord Constrain Source #
Methods compare :: Constrain -> Constrain -> Ordering (<) :: Constrain -> Constrain -> Bool (<=) :: Constrain -> Constrain -> Bool (>) :: Constrain -> Constrain -> Bool (>=) :: Constrain -> Constrain -> Bool max :: Constrain -> Constrain -> Constrain min :: Constrain -> Constrain -> Constrain
Show Constrain Source #
Methods showsPrec :: Int -> Constrain -> ShowS show :: Constrain -> String showList :: [Constrain] -> ShowS

accessing the environment

addDiags :: [Diagnosis] -> State Env () Source #

add diagnostic messages

appendSentences :: [Named Sentence] -> State Env () Source #

add sentences

putClassMap :: ClassMap -> State Env () Source #

store a class map

putLocalVars :: Map Id VarDefn -> State Env () Source #

store local assumptions

fromResult :: (Env -> Result a) -> State Env (Maybe a) Source #

converting a result to a state computation

addSymbol :: Symbol -> State Env () Source #

add the symbol to the state

putLocalTypeVars :: LocalTypeVars -> State Env () Source #

store local type variables

putTypeMap :: TypeMap -> State Env () Source #

store a complete type map

putAssumps :: Assumps -> State Env () Source #

store assumptions

putBinders :: Map Id Id -> State Env () Source #

store assumptions

getVar :: VarDecl -> Id Source #

get the variable

checkUniqueVars :: [VarDecl] -> State Env () Source #

check uniqueness of variables

morphisms

type FunMap = Map (Id, TypeScheme) (Id, TypeScheme) Source #

data Morphism Source #

keep types and class disjoint and use a single identifier map for both

Constructors

Morphism
Fields msource :: Env mtarget :: Env typeIdMap :: IdMap classIdMap :: IdMap funMap :: FunMap

Instances

Eq Morphism Source #
Methods (==) :: Morphism -> Morphism -> Bool (/=) :: Morphism -> Morphism -> Bool
Data Morphism Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Morphism -> c Morphism gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Morphism toConstr :: Morphism -> Constr dataTypeOf :: Morphism -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Morphism) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Morphism) gmapT :: (forall b. Data b => b -> b) -> Morphism -> Morphism gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Morphism -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Morphism -> r gmapQ :: (forall d. Data d => d -> u) -> Morphism -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Morphism -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Morphism -> m Morphism gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Morphism -> m Morphism gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Morphism -> m Morphism
Ord Morphism Source #
Methods compare :: Morphism -> Morphism -> Ordering (<) :: Morphism -> Morphism -> Bool (<=) :: Morphism -> Morphism -> Bool (>) :: Morphism -> Morphism -> Bool (>=) :: Morphism -> Morphism -> Bool max :: Morphism -> Morphism -> Morphism min :: Morphism -> Morphism -> Morphism
Show Morphism Source #
Methods showsPrec :: Int -> Morphism -> ShowS show :: Morphism -> String showList :: [Morphism] -> ShowS
Sentences HasCASL Sentence Env Morphism Symbol Source #
Methods map_sen :: HasCASL -> Morphism -> Sentence -> Result Sentence Source # simplify_sen :: HasCASL -> Env -> Sentence -> Sentence Source # negation :: HasCASL -> Sentence -> Maybe Sentence Source # print_sign :: HasCASL -> Env -> Doc Source # print_named :: HasCASL -> Named Sentence -> Doc Source # sym_of :: HasCASL -> Env -> [Set Symbol] Source # mostSymsOf :: HasCASL -> Env -> [Symbol] Source # symmap_of :: HasCASL -> Morphism -> EndoMap Symbol Source # sym_name :: HasCASL -> Symbol -> Id Source # sym_label :: HasCASL -> Symbol -> Maybe String Source # fullSymName :: HasCASL -> Symbol -> String Source # symKind :: HasCASL -> Symbol -> String Source # symsOfSen :: HasCASL -> Env -> Sentence -> [Symbol] Source # pair_symbols :: HasCASL -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source #
Methods basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source # sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source # extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source # stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source # convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source # ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source # signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source # qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source # id_to_raw :: HasCASL -> Id -> RawSymbol Source # matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: HasCASL -> Env Source # add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source # signature_union :: HasCASL -> Env -> Env -> Result Env Source # signatureDiff :: HasCASL -> Env -> Env -> Result Env Source # intersection :: HasCASL -> Env -> Env -> Result Env Source # final_union :: HasCASL -> Env -> Env -> Result Env Source # morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: HasCASL -> Env -> Env -> Bool Source # subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source # generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source # induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source # is_transportable :: HasCASL -> Morphism -> Bool Source # is_injective :: HasCASL -> Morphism -> Bool Source # theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #
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 # sublogicOfTheo :: HasCASL -> (Env, [Sentence]) -> Sublogic Source #
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
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 #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
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 #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
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 #
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 -> Symbol -> 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 #
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 #
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 -> Symbol -> 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 #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
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 #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
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 #

mkMorphism :: Env -> Env -> Morphism Source #

construct morphism for subsignatures

isInclMor :: Morphism -> Bool Source #

symbol stuff

data SymbolType Source #

the type or kind of an identifier

Constructors

OpAsItemType TypeScheme
TypeAsItemType RawKind
ClassAsItemType RawKind
SuperClassSymbol Kind
TypeKindInstance Kind
SuperTypeSymbol Id
TypeAliasSymbol Type
PredAsItemType TypeScheme

Instances

Eq SymbolType Source #
Methods (==) :: SymbolType -> SymbolType -> Bool (/=) :: SymbolType -> SymbolType -> Bool
Data SymbolType Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbolType -> c SymbolType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbolType toConstr :: SymbolType -> Constr dataTypeOf :: SymbolType -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c SymbolType) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbolType) gmapT :: (forall b. Data b => b -> b) -> SymbolType -> SymbolType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbolType -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbolType -> r gmapQ :: (forall d. Data d => d -> u) -> SymbolType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbolType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType
Ord SymbolType Source #
Methods compare :: SymbolType -> SymbolType -> Ordering (<) :: SymbolType -> SymbolType -> Bool (<=) :: SymbolType -> SymbolType -> Bool (>) :: SymbolType -> SymbolType -> Bool (>=) :: SymbolType -> SymbolType -> Bool max :: SymbolType -> SymbolType -> SymbolType min :: SymbolType -> SymbolType -> SymbolType
Show SymbolType Source #
Methods showsPrec :: Int -> SymbolType -> ShowS show :: SymbolType -> String showList :: [SymbolType] -> ShowS

data Symbol Source #

symbols with their type

Constructors

Symbol
Fields symName :: Id symType :: SymbolType

Instances

Eq Symbol Source #
Methods (==) :: Symbol -> Symbol -> Bool (/=) :: Symbol -> Symbol -> Bool
Data Symbol Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Symbol -> c Symbol gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Symbol toConstr :: Symbol -> Constr dataTypeOf :: Symbol -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Symbol) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol) gmapT :: (forall b. Data b => b -> b) -> Symbol -> Symbol gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r gmapQ :: (forall d. Data d => d -> u) -> Symbol -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Symbol -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol
Ord Symbol Source #
Methods compare :: Symbol -> Symbol -> Ordering (<) :: Symbol -> Symbol -> Bool (<=) :: Symbol -> Symbol -> Bool (>) :: Symbol -> Symbol -> Bool (>=) :: Symbol -> Symbol -> Bool max :: Symbol -> Symbol -> Symbol min :: Symbol -> Symbol -> Symbol
Show Symbol Source #
Methods showsPrec :: Int -> Symbol -> ShowS show :: Symbol -> String showList :: [Symbol] -> ShowS
Sentences HasCASL Sentence Env Morphism Symbol Source #
Methods map_sen :: HasCASL -> Morphism -> Sentence -> Result Sentence Source # simplify_sen :: HasCASL -> Env -> Sentence -> Sentence Source # negation :: HasCASL -> Sentence -> Maybe Sentence Source # print_sign :: HasCASL -> Env -> Doc Source # print_named :: HasCASL -> Named Sentence -> Doc Source # sym_of :: HasCASL -> Env -> [Set Symbol] Source # mostSymsOf :: HasCASL -> Env -> [Symbol] Source # symmap_of :: HasCASL -> Morphism -> EndoMap Symbol Source # sym_name :: HasCASL -> Symbol -> Id Source # sym_label :: HasCASL -> Symbol -> Maybe String Source # fullSymName :: HasCASL -> Symbol -> String Source # symKind :: HasCASL -> Symbol -> String Source # symsOfSen :: HasCASL -> Env -> Sentence -> [Symbol] Source # pair_symbols :: HasCASL -> Symbol -> Symbol -> Result Symbol Source #
Syntax HasCASL BasicSpec Symbol SymbItems SymbMapItems Source #
Methods parsersAndPrinters :: HasCASL -> Map String (PrefixMap -> AParser st BasicSpec, BasicSpec -> Doc) Source # parse_basic_spec :: HasCASL -> Maybe (PrefixMap -> AParser st BasicSpec) Source # parseSingleSymbItem :: HasCASL -> Maybe (AParser st SymbItems) Source # parse_symb_items :: HasCASL -> Maybe (AParser st SymbItems) Source # parse_symb_map_items :: HasCASL -> Maybe (AParser st SymbMapItems) Source # toItem :: HasCASL -> BasicSpec -> Item Source # symb_items_name :: HasCASL -> SymbItems -> [String] Source #
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source #
Methods basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source # sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source # extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source # stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source # convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source # ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source # signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source # qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source # id_to_raw :: HasCASL -> Id -> RawSymbol Source # matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: HasCASL -> Env Source # add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source # signature_union :: HasCASL -> Env -> Env -> Result Env Source # signatureDiff :: HasCASL -> Env -> Env -> Result Env Source # intersection :: HasCASL -> Env -> Env -> Result Env Source # final_union :: HasCASL -> Env -> Env -> Result Env Source # morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: HasCASL -> Env -> Env -> Bool Source # subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source # generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source # induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source # is_transportable :: HasCASL -> Morphism -> Bool Source # is_injective :: HasCASL -> Morphism -> Bool Source # theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #
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 # sublogicOfTheo :: HasCASL -> (Env, [Sentence]) -> Sublogic Source #
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
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 #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
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 #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
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 #
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 -> Symbol -> 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 #
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 #
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 -> Symbol -> 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 #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
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 #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
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 #

type SymbolMap = Map Symbol Symbol Source #

mapping symbols to symbols

type SymbolSet = Set Symbol Source #

a set of symbols

idToTypeSymbol :: Id -> RawKind -> Symbol Source #

create a type symbol

idToClassSymbol :: Id -> RawKind -> Symbol Source #

create a class symbol

idToOpSymbol :: Id -> TypeScheme -> Symbol Source #

create an operation symbol

data RawSymbol Source #

raw symbols where the type of a qualified raw symbol can be a type scheme and also be a kind if the symbol kind is unknown.

Constructors

AnID Id
AKindedId SymbKind Id
ASymbol Symbol

Instances

Eq RawSymbol Source #
Methods (==) :: RawSymbol -> RawSymbol -> Bool (/=) :: RawSymbol -> RawSymbol -> Bool
Data RawSymbol Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RawSymbol -> c RawSymbol gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RawSymbol toConstr :: RawSymbol -> Constr dataTypeOf :: RawSymbol -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c RawSymbol) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RawSymbol) gmapT :: (forall b. Data b => b -> b) -> RawSymbol -> RawSymbol gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RawSymbol -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RawSymbol -> r gmapQ :: (forall d. Data d => d -> u) -> RawSymbol -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RawSymbol -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
Ord RawSymbol Source #
Methods compare :: RawSymbol -> RawSymbol -> Ordering (<) :: RawSymbol -> RawSymbol -> Bool (<=) :: RawSymbol -> RawSymbol -> Bool (>) :: RawSymbol -> RawSymbol -> Bool (>=) :: RawSymbol -> RawSymbol -> Bool max :: RawSymbol -> RawSymbol -> RawSymbol min :: RawSymbol -> RawSymbol -> RawSymbol
Show RawSymbol Source #
Methods showsPrec :: Int -> RawSymbol -> ShowS show :: RawSymbol -> String showList :: [RawSymbol] -> ShowS
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source #
Methods basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source # sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source # extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source # stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source # convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source # ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source # signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source # qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source # id_to_raw :: HasCASL -> Id -> RawSymbol Source # matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: HasCASL -> Env Source # add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source # signature_union :: HasCASL -> Env -> Env -> Result Env Source # signatureDiff :: HasCASL -> Env -> Env -> Result Env Source # intersection :: HasCASL -> Env -> Env -> Result Env Source # final_union :: HasCASL -> Env -> Env -> Result Env Source # morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: HasCASL -> Env -> Env -> Bool Source # subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source # generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source # induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source # is_transportable :: HasCASL -> Morphism -> Bool Source # is_injective :: HasCASL -> Morphism -> Bool Source # theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #
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 # sublogicOfTheo :: HasCASL -> (Env, [Sentence]) -> Sublogic Source #
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
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 #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
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 #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
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 Sentence]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence]) 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 #
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 #
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 -> Symbol -> 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 #
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 #
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 -> Symbol -> 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 #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
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 #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
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 #

type RawSymbolMap = Map RawSymbol RawSymbol Source #

mapping raw symbols to raw symbols

idToRaw :: Id -> RawSymbol Source #

create a raw symbol from an identifier

rawSymName :: RawSymbol -> Id Source #

extract the top identifer from a raw symbol

symbTypeToKind :: SymbolType -> SymbKind Source #

convert a symbol type to a symbol kind

symbolToRaw :: Symbol -> RawSymbol Source #

wrap a symbol as raw symbol (is ASymbol)

symbKindToRaw :: SymbKind -> Id -> RawSymbol Source #

create a raw symbol from a symbol kind and an identifier

getCompoundLists :: Env -> Set [Id] Source #