| Copyright | (c) Till Mossakowski, and Uni Bremen 2002-2006 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | till@informatik.uni-bremen.de |
| Stability | provisional |
| Portability | non-portable (various -fglasgow-exts extensions) |
| Safe Haskell | None |
Logic.Logic
Description
Central interface (type class) for logics in Hets
Provides data structures for logics (with symbols). Logics are a type class with an identity type (usually interpreted by a singleton set) which serves to treat logics as data. All the functions in the type class take the identity as first argument in order to determine the logic.
For logic (co)morphisms see Logic.Comorphism
This module uses multiparameter type classes with functional dependencies (http://www.haskell.org/haskellwiki/Functional_dependencies) for defining an interface for the notion of logic. Multiparameter type classes are needed because a logic consists of a collection of types, together with operations on these. Functional dependencies are needed because no operation will involve all types of the multiparameter type class; hence we need a method to derive the missing types. We chose an easy way: for each logic, we introduce a new singleton type that is the name, or constitutes the identity of the logic. All other types of the multiparameter type class depend on this identity constituting type, and all operations take the 'identity constituting' type as first arguments. The value of the argument of the identity constituting type is irrelevant (note that there is only one value of such a type anyway).
Note that we tend to use lid both for the identity type
of a logic, as well as for its unique inhabitant, i.e. lid :: lid.
The other types involved in the definition of logic are as follows:
- sign: signatures, that is, contexts, or non-logical vocabularies, typically consisting of a set of declared sorts, predicates, function symbols, propositional letters etc., together with their typing.
- sentence: logical formulas.
- basic_spec: abstract syntax of basic specifications. The latter are human-readable presentations of a signature together with some sentences.
- symbol: symbols that may occur in a signature, fully qualified with their types
- raw_symbol: symbols that may occur in a signature, possibly not or partially qualified
- morphism: maps between signatures (typically preserving the structure).
- symb_items: abstract syntax of symbol lists, used for declaring some symbols of a signature as hidden.
- symb_map_items: abstract syntax of symbol maps, i.e. human-readable presentations of signature morphisms.
- sublogics: sublogics of the given logic. This type might be a record of Boolean flags, indicating whether some feature is present in the sublogi of not.
- proof_tree: proof trees.
References:
J. A. Goguen and R. M. Burstall Institutions: Abstract Model Theory for Specification and Programming JACM 39, p. 95-146, 1992 (general notion of logic - model theory only)
J. Meseguer General Logics Logic Colloquium 87, p. 275-329, North Holland, 1989 (general notion of logic - also proof theory; notion of logic representation, called map there)
T. Mossakowski: Specification in an arbitrary institution with symbols 14th WADT 1999, LNCS 1827, p. 252-270 (treatment of symbols and raw symbols, see also CASL semantics in the CASL reference manual)
T. Mossakowski, B. Klin: Institution Independent Static Analysis for CASL 15h WADT 2001, LNCS 2267, p. 221-237, 2002. (what is needed for static anaylsis)
S. Autexier and T. Mossakowski Integrating HOLCASL into the Development Graph Manager MAYA FroCoS 2002, LNCS 2309, p. 2-17, 2002. (interface to provers)
CoFI (ed.): CASL Reference Manual, LNCS 2960, Springer Verlag, 2004. (static semantics of CASL structured and architectural specifications)
T. Mossakowski Heterogeneous specification and the heterogeneous tool set Habilitation thesis, University of Bremen, 2005 (the general picture of heterogeneous specification)
- data Stability
- class ShATermConvertible a => Convertible a
- class (Pretty a, Convertible a) => PrintTypeConv a
- class (Eq a, PrintTypeConv a) => EqPrintTypeConv a
- type EndoMap a = Map a a
- class Show lid => Language lid where
- language_name :: lid -> String
- description :: lid -> String
- class (Ord object, Ord morphism) => Category object morphism | morphism -> object where
- isIdentity :: Category object morphism => morphism -> Bool
- comp :: Category object morphism => morphism -> morphism -> Result morphism
- class (Language lid, PrintTypeConv basic_spec, GetRange basic_spec, Monoid basic_spec, Pretty symbol, EqPrintTypeConv symb_items, EqPrintTypeConv symb_map_items) => Syntax lid basic_spec symbol symb_items symb_map_items | lid -> basic_spec symbol symb_items symb_map_items where
- parsersAndPrinters :: lid -> Map String (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
- parse_basic_spec :: lid -> Maybe (PrefixMap -> AParser st basic_spec)
- parseSingleSymbItem :: lid -> Maybe (AParser st symb_items)
- parse_symb_items :: lid -> Maybe (AParser st symb_items)
- parse_symb_map_items :: lid -> Maybe (AParser st symb_map_items)
- toItem :: lid -> basic_spec -> Item
- basicSpecParser :: Syntax lid basic_spec symbol symb_items symb_map_items => Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec)
- basicSpecPrinter :: Syntax lid basic_spec symbol symb_items symb_map_items => Maybe IRI -> lid -> Maybe (basic_spec -> Doc)
- basicSpecSyntaxes :: Syntax lid basic_spec symbol symb_items symb_map_items => lid -> [String]
- parserAndPrinter :: Syntax lid basic_spec symbol symb_items symb_map_items => Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
- lookupDefault :: Syntax lid basic_spec symbol symb_items symb_map_items => lid -> Maybe IRI -> Map String b -> Maybe b
- showSyntax :: Language lid => lid -> Maybe IRI -> String
- makeDefault :: b -> Map String b
- addSyntax :: String -> b -> Map String b -> Map String b
- class (Language lid, Category sign morphism, Ord sentence, Ord symbol, PrintTypeConv sign, PrintTypeConv morphism, GetRange sentence, GetRange symbol, PrintTypeConv sentence, ToJson sentence, ToXml sentence, PrintTypeConv symbol) => Sentences lid sentence sign morphism symbol | lid -> sentence sign morphism symbol where
- map_sen :: lid -> morphism -> sentence -> Result sentence
- simplify_sen :: lid -> sign -> sentence -> sentence
- negation :: lid -> sentence -> Maybe sentence
- print_sign :: lid -> sign -> Doc
- print_named :: lid -> Named sentence -> Doc
- sym_of :: lid -> sign -> [Set symbol]
- mostSymsOf :: lid -> sign -> [symbol]
- symmap_of :: lid -> morphism -> EndoMap symbol
- sym_name :: lid -> symbol -> Id
- sym_label :: lid -> symbol -> Maybe String
- fullSymName :: lid -> symbol -> String
- symKind :: lid -> symbol -> String
- symsOfSen :: lid -> sentence -> [symbol]
- pair_symbols :: lid -> symbol -> symbol -> Result symbol
- singletonList :: a -> [a]
- symset_of :: forall lid sentence sign morphism symbol. Sentences lid sentence sign morphism symbol => lid -> sign -> Set symbol
- symlist_of :: forall lid sentence sign morphism symbol. Sentences lid sentence sign morphism symbol => lid -> sign -> [symbol]
- inlineAxioms :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol => lid -> String -> [Named sentence]
- statFail :: (Language lid, Monad m) => lid -> String -> m a
- statError :: Language lid => lid -> String -> a
- statErrMsg :: Language lid => lid -> String -> String
- data REL_REF
- class (Syntax lid basic_spec symbol symb_items symb_map_items, Sentences lid sentence sign morphism symbol, GetRange raw_symbol, Ord raw_symbol, Pretty raw_symbol, Typeable raw_symbol) => StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol | lid -> basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol where
- basic_analysis :: lid -> Maybe ((basic_spec, sign, GlobalAnnos) -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
- sen_analysis :: lid -> Maybe ((basic_spec, sign, sentence) -> Result sentence)
- extBasicAnalysis :: lid -> IRI -> LibName -> basic_spec -> sign -> GlobalAnnos -> Result (basic_spec, ExtSign sign symbol, [Named sentence])
- stat_symb_map_items :: lid -> sign -> Maybe sign -> [symb_map_items] -> Result (EndoMap raw_symbol)
- stat_symb_items :: lid -> sign -> [symb_items] -> Result [raw_symbol]
- convertTheory :: lid -> Maybe ((sign, [Named sentence]) -> basic_spec)
- ensures_amalgamability :: lid -> ([CASLAmalgOpt], Gr sign (Int, morphism), [(Int, morphism)], Gr String String) -> Result Amalgamates
- quotient_term_algebra :: lid -> morphism -> [Named sentence] -> Result (sign, [Named sentence])
- signature_colimit :: lid -> Gr sign (Int, morphism) -> Result (sign, Map Int morphism)
- qualify :: lid -> SIMPLE_ID -> LibName -> morphism -> sign -> Result (morphism, [Named sentence])
- symbol_to_raw :: lid -> symbol -> raw_symbol
- id_to_raw :: lid -> Id -> raw_symbol
- matches :: lid -> symbol -> raw_symbol -> Bool
- empty_signature :: lid -> sign
- add_symb_to_sign :: lid -> sign -> symbol -> Result sign
- signature_union :: lid -> sign -> sign -> Result sign
- signatureDiff :: lid -> sign -> sign -> Result sign
- intersection :: lid -> sign -> sign -> Result sign
- final_union :: lid -> sign -> sign -> Result sign
- morphism_union :: lid -> morphism -> morphism -> Result morphism
- is_subsig :: lid -> sign -> sign -> Bool
- subsig_inclusion :: lid -> sign -> sign -> Result morphism
- generated_sign, cogenerated_sign :: lid -> Set symbol -> sign -> Result morphism
- induced_from_morphism :: lid -> EndoMap raw_symbol -> sign -> Result morphism
- induced_from_to_morphism :: lid -> EndoMap raw_symbol -> ExtSign sign symbol -> ExtSign sign symbol -> Result morphism
- is_transportable :: lid -> morphism -> Bool
- is_injective :: lid -> morphism -> Bool
- theory_to_taxonomy :: lid -> TaxoGraphKind -> MMiSSOntology -> sign -> [Named sentence] -> Result MMiSSOntology
- corresp2th :: lid -> sign -> sign -> [symb_items] -> [symb_items] -> EndoMap symbol -> EndoMap symbol -> REL_REF -> Result (sign, [Named sentence], sign, sign, EndoMap symbol, EndoMap symbol)
- equiv2cospan :: lid -> sign -> sign -> [symb_items] -> [symb_items] -> Result (sign, sign, sign, EndoMap symbol, EndoMap symbol)
- printTheory :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol => Maybe IRI -> lid -> (sign, [Named sentence]) -> Doc
- inclusion :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol => lid -> sign -> sign -> Result morphism
- class (Ord l, Show l) => SemiLatticeWithTop l where
- isSubElem :: SemiLatticeWithTop l => l -> l -> Bool
- class MinSublogic sublogic item where
- minSublogic :: item -> sublogic
- class MinSublogic sublogic item => ProjectSublogic sublogic item where
- projectSublogic :: sublogic -> item -> item
- class MinSublogic sublogic item => ProjectSublogicM sublogic item where
- projectSublogicM :: sublogic -> item -> Maybe item
- class SublogicName l where
- sublogicName :: l -> String
- type SyntaxTable = (PrecMap, AssocMap)
- class (StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol, SemiLatticeWithTop sublogics, MinSublogic sublogics sentence, ProjectSublogic sublogics basic_spec, ProjectSublogicM sublogics symb_items, ProjectSublogicM sublogics symb_map_items, ProjectSublogic sublogics sign, ProjectSublogic sublogics morphism, ProjectSublogicM sublogics symbol, Convertible sublogics, SublogicName sublogics, Ord proof_tree, Show proof_tree, Convertible proof_tree) => Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree | lid -> sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree where
- parse_basic_sen :: lid -> Maybe (basic_spec -> AParser st sentence)
- stability :: lid -> Stability
- data_logic :: lid -> Maybe AnyLogic
- top_sublogic :: lid -> sublogics
- all_sublogics :: lid -> [sublogics]
- bottomSublogic :: lid -> Maybe sublogics
- sublogicDimensions :: lid -> [[sublogics]]
- parseSublogic :: lid -> String -> Maybe sublogics
- proj_sublogic_epsilon :: lid -> sublogics -> sign -> morphism
- provers :: lid -> [Prover sign sentence morphism sublogics proof_tree]
- cons_checkers :: lid -> [ConsChecker sign sentence sublogics morphism proof_tree]
- conservativityCheck :: lid -> [ConservativityChecker sign sentence morphism]
- empty_proof_tree :: lid -> proof_tree
- syntaxTable :: lid -> sign -> Maybe SyntaxTable
- omdoc_metatheory :: lid -> Maybe OMCD
- export_symToOmdoc :: lid -> NameMap symbol -> symbol -> String -> Result TCElement
- export_senToOmdoc :: lid -> NameMap symbol -> sentence -> Result TCorOMElement
- export_theoryToOmdoc :: lid -> SigMap symbol -> sign -> [Named sentence] -> Result [TCElement]
- omdocToSym :: lid -> SigMapI symbol -> TCElement -> String -> Result symbol
- omdocToSen :: lid -> SigMapI symbol -> TCElement -> String -> Result (Maybe (Named sentence))
- addOMadtToTheory :: lid -> SigMapI symbol -> (sign, [Named sentence]) -> [[OmdADT]] -> Result (sign, [Named sentence])
- addOmdocToTheory :: lid -> SigMapI symbol -> (sign, [Named sentence]) -> [TCElement] -> Result (sign, [Named sentence])
- class Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => LogicalFramework lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree | lid -> sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree where
- base_sig :: lid -> sign
- write_logic :: lid -> String -> String
- write_syntax :: lid -> String -> morphism -> String
- write_proof :: lid -> String -> morphism -> String
- write_model :: lid -> String -> morphism -> String
- read_morphism :: lid -> FilePath -> morphism
- write_comorphism :: lid -> String -> String -> String -> morphism -> morphism -> morphism -> String
- emptyTheory :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol => lid -> Theory sign sentence proof_tree
- data AnyLogic = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree . Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => Logic lid
Documentation
class ShATermConvertible a => Convertible a
shortcut for class constraints
Instances
| ShATermConvertible a => Convertible a |
class (Pretty a, Convertible a) => PrintTypeConv a
shortcut for class constraints
Instances
| (Pretty a, Convertible a) => PrintTypeConv a |
class (Eq a, PrintTypeConv a) => EqPrintTypeConv a
shortcut for class constraints with equality
Instances
| (Eq a, PrintTypeConv a) => EqPrintTypeConv a |
class Show lid => Language lid where
the name of a logic. Define instances like "data CASL = CASL deriving (Show, Typeable, Data)"
Minimal complete definition
Nothing
Instances
class (Ord object, Ord morphism) => Category object morphism | morphism -> object where
Categories are given as usual: objects, morphisms, identities, domain, codomain and composition. The type id is the name, or the identity of the category. It is an argument to all functions of the type class, serving disambiguation among instances (via the functional dependency lid -> object morphism). The types for objects and morphisms may be restricted to subtypes, using legal_obj and legal_mor. For example, for the category of sets and injective maps, legal_mor would check injectivity. Since Eq is a subclass of Category, it is also possible to impose a quotient on the types for objects and morphisms. Require Ord instances only for efficiency, i.e. in sets or maps.
Minimal complete definition
Methods
ide :: object -> morphism
identity morphisms
composeMorphisms :: morphism -> morphism -> Result morphism
composition, in diagrammatic order, if intermediate objects are equal (not checked!)
dom, cod :: morphism -> object
domain and codomain of morphisms
inverse :: morphism -> Result morphism
the inverse of a morphism
isInclusion :: morphism -> Bool
test if the signature morphism an inclusion
legal_mor :: morphism -> Result ()
is a value of type morphism denoting a legal morphism?
Instances
| Category Sign RDFMorphism | |
| Category Sign OWLMorphism | |
| Category Sign Morphism | |
| Category Sign Morphism | Instance of Category for Maude |
| Category Sign Morphism | |
| Category Sign Morphism | |
| Category Sign Morphism | Instance of Category for temporal logic |
| Category Sign RSMorphism | Instance of Category for Rel |
| Category Sign Morphism | Instance of Category for propositional logic |
| Category Sign Morphism | Instance of Category for propositional logic |
| Category Sign Morphism | Instance of Category for CSL logic |
| Category Env Morphism | |
| Category OMDoc_Sign OMDoc_Morphism | |
| Category Sgn_Wrap Mor | |
| Category G_sign GMorphism | |
| Ord sign => Category sign (DefaultMorphism sign) | |
| (Ord f, Ord e, Ord m, MorphismExtension e m) => Category (Sign f e) (Morphism f e m) |
isIdentity :: Category object morphism => morphism -> Bool
test if the signature morphism is the identity
class (Language lid, PrintTypeConv basic_spec, GetRange basic_spec, Monoid basic_spec, Pretty symbol, EqPrintTypeConv symb_items, EqPrintTypeConv symb_map_items) => Syntax lid basic_spec symbol symb_items symb_map_items | lid -> basic_spec symbol symb_items symb_map_items where
Abstract syntax, parsing and printing. There are three types for abstract syntax: basic_spec is for basic specifications (see CASL RefMan p. 5ff.), symb_items is for symbol lists (see CASL RefMan p. 35ff.), symb_map_items is for symbol maps (see CASL RefMan p. 35ff.).
Minimal complete definition
Nothing
Methods
parsersAndPrinters :: lid -> Map String (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
parsers and printers
parse_basic_spec :: lid -> Maybe (PrefixMap -> AParser st basic_spec)
parser for basic specifications
parseSingleSymbItem :: lid -> Maybe (AParser st symb_items)
parser for a single symbol returned as list
parse_symb_items :: lid -> Maybe (AParser st symb_items)
parser for symbol lists
parse_symb_map_items :: lid -> Maybe (AParser st symb_map_items)
parser for symbol maps
Instances
basicSpecParser :: Syntax lid basic_spec symbol symb_items symb_map_items => Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec)
basicSpecPrinter :: Syntax lid basic_spec symbol symb_items symb_map_items => Maybe IRI -> lid -> Maybe (basic_spec -> Doc)
basicSpecSyntaxes :: Syntax lid basic_spec symbol symb_items symb_map_items => lid -> [String]
parserAndPrinter :: Syntax lid basic_spec symbol symb_items symb_map_items => Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
lookupDefault :: Syntax lid basic_spec symbol symb_items symb_map_items => lid -> Maybe IRI -> Map String b -> Maybe b
function to lookup parser or printer
showSyntax :: Language lid => lid -> Maybe IRI -> String
makeDefault :: b -> Map String b
class (Language lid, Category sign morphism, Ord sentence, Ord symbol, PrintTypeConv sign, PrintTypeConv morphism, GetRange sentence, GetRange symbol, PrintTypeConv sentence, ToJson sentence, ToXml sentence, PrintTypeConv symbol) => Sentences lid sentence sign morphism symbol | lid -> sentence sign morphism symbol where
Sentences, provers and symbols. Provers capture the entailment relation between sets of sentences and sentences. They may return proof trees witnessing proofs. Signatures are equipped with underlying sets of symbols (such that the category of signatures becomes a concrete category), see CASL RefMan p. 191ff.
Minimal complete definition
Nothing
Methods
map_sen :: lid -> morphism -> sentence -> Result sentence
sentence translation along a signature morphism
simplify_sen :: lid -> sign -> sentence -> sentence
simplification of sentences (leave out qualifications)
negation :: lid -> sentence -> Maybe sentence
negation of a sentence for disproving
print_sign :: lid -> sign -> Doc
modified signature printing when followed by sentences
print_named :: lid -> Named sentence -> Doc
print a sentence with comments
sym_of :: lid -> sign -> [Set symbol]
dependency ordered list of symbol sets for a signature
mostSymsOf :: lid -> sign -> [symbol]
Dependency ordered list of a bigger symbol set for a
signature. This function contains more symbols than those being subject
to hiding and renaming (given by sym_of) to better represent a
signature as a set of symbols given within xml files. At least for CASL
additional symbols for (direct) subsorts will be created, but note, that
no symbol for a partial function will be created, if the signature
contains this function as total, although a signature with just that
partial function would be a subsignature. This function is supposed to
work over partial signatures created by signatureDiff.
symmap_of :: lid -> morphism -> EndoMap symbol
symbol map for a signature morphism
sym_name :: lid -> symbol -> Id
symbols have a name, see CASL RefMan p. 192
sym_label :: lid -> symbol -> Maybe String
some symbols have a label for better readability
fullSymName :: lid -> symbol -> String
the fully qualified name for XML output (i.e. of OWL2)
symKind :: lid -> symbol -> String
a logic dependent kind of a symbol
symsOfSen :: lid -> sentence -> [symbol]
the symbols occuring in a sentence (any order)
pair_symbols :: lid -> symbol -> symbol -> Result symbol
combine two symbols into another one
Instances
singletonList :: a -> [a]
makes a singleton list from the given value
symset_of :: forall lid sentence sign morphism symbol. Sentences lid sentence sign morphism symbol => lid -> sign -> Set symbol
set of symbols for a signature
symlist_of :: forall lid sentence sign morphism symbol. Sentences lid sentence sign morphism symbol => lid -> sign -> [symbol]
dependency ordered list of symbols for a signature
inlineAxioms :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol => lid -> String -> [Named sentence]
a dummy static analysis function to allow type checking *.inline.hs files
statErrMsg :: Language lid => lid -> String -> String
error message for static analysis
data REL_REF
class (Syntax lid basic_spec symbol symb_items symb_map_items, Sentences lid sentence sign morphism symbol, GetRange raw_symbol, Ord raw_symbol, Pretty raw_symbol, Typeable raw_symbol) => StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol | lid -> basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol where
Minimal complete definition
Methods
basic_analysis :: lid -> Maybe ((basic_spec, sign, GlobalAnnos) -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
static analysis of basic specifications and symbol maps. The resulting bspec has analyzed axioms in it. The resulting sign is an extension of the input sign plus newly declared or redeclared symbols. See CASL RefMan p. 138 ff.
sen_analysis :: lid -> Maybe ((basic_spec, sign, sentence) -> Result sentence)
Analysis of just sentences
extBasicAnalysis :: lid -> IRI -> LibName -> basic_spec -> sign -> GlobalAnnos -> Result (basic_spec, ExtSign sign symbol, [Named sentence])
a basic analysis with additional arguments
stat_symb_map_items :: lid -> sign -> Maybe sign -> [symb_map_items] -> Result (EndoMap raw_symbol)
static analysis of symbol maps, see CASL RefMan p. 222f.
stat_symb_items :: lid -> sign -> [symb_items] -> Result [raw_symbol]
static analysis of symbol lists, see CASL RefMan p. 221f.
convertTheory :: lid -> Maybe ((sign, [Named sentence]) -> basic_spec)
convert a theory to basic specs for different serializations
ensures_amalgamability :: lid -> ([CASLAmalgOpt], Gr sign (Int, morphism), [(Int, morphism)], Gr String String) -> Result Amalgamates
architectural sharing analysis, see CASL RefMan p. 247ff.
quotient_term_algebra :: lid -> morphism -> [Named sentence] -> Result (sign, [Named sentence])
quotient term algebra for normalization of freeness
signature_colimit :: lid -> Gr sign (Int, morphism) -> Result (sign, Map Int morphism)
signature colimits
qualify :: lid -> SIMPLE_ID -> LibName -> morphism -> sign -> Result (morphism, [Named sentence])
rename and qualify the symbols considering a united incoming morphisms, code out overloading and create sentences for the overloading relation
symbol_to_raw :: lid -> symbol -> raw_symbol
Construe a symbol, like f:->t, as a raw symbol. This is a one-sided inverse to the function SymSySigSym in the CASL RefMan p. 192.
id_to_raw :: lid -> Id -> raw_symbol
Construe an identifier, like f, as a raw symbol. See CASL RefMan p. 192, function IDAsSym
matches :: lid -> symbol -> raw_symbol -> Bool
Check whether a symbol matches a raw symbol, for example, f:s->t matches f. See CASL RefMan p. 192
empty_signature :: lid -> sign
the empty (initial) signature, see CASL RefMan p. 193
add_symb_to_sign :: lid -> sign -> symbol -> Result sign
adds a symbol to a given signature
signature_union :: lid -> sign -> sign -> Result sign
union of signatures, see CASL RefMan p. 193
signatureDiff :: lid -> sign -> sign -> Result sign
difference of signatures resulting in unclosed pre-signatures
intersection :: lid -> sign -> sign -> Result sign
intersection of signatures
final_union :: lid -> sign -> sign -> Result sign
final union of signatures, see CASL RefMan p. 194
morphism_union :: lid -> morphism -> morphism -> Result morphism
union of signature morphims, see CASL RefMan p. 196
is_subsig :: lid -> sign -> sign -> Bool
subsignatures, see CASL RefMan p. 194
subsig_inclusion :: lid -> sign -> sign -> Result morphism
construct the inclusion morphisms between subsignatures, see CASL RefMan p. 194
generated_sign, cogenerated_sign :: lid -> Set symbol -> sign -> Result morphism
the signature (co)generated by a set of symbols in another signature is the smallest (largest) signature containing (excluding) the set of symbols. Needed for revealing and hiding, see CASL RefMan p. 197ff.
induced_from_morphism :: lid -> EndoMap raw_symbol -> sign -> Result morphism
Induce a signature morphism from a source signature and a raw symbol map. Needed for translation (SP with SM). See CASL RefMan p. 198
induced_from_to_morphism :: lid -> EndoMap raw_symbol -> ExtSign sign symbol -> ExtSign sign symbol -> Result morphism
Induce a signature morphism between two signatures by a raw symbol map. Needed for instantiation and views. See CASL RefMan p. 198f.
is_transportable :: lid -> morphism -> Bool
Check whether a signature morphism is transportable. See CASL RefMan p. 304f.
is_injective :: lid -> morphism -> Bool
Check whether the underlying symbol map of a signature morphism is injective
theory_to_taxonomy :: lid -> TaxoGraphKind -> MMiSSOntology -> sign -> [Named sentence] -> Result MMiSSOntology
generate an ontological taxonomy, if this makes sense
corresp2th :: lid -> sign -> sign -> [symb_items] -> [symb_items] -> EndoMap symbol -> EndoMap symbol -> REL_REF -> Result (sign, [Named sentence], sign, sign, EndoMap symbol, EndoMap symbol)
create a theory from a correspondence
equiv2cospan :: lid -> sign -> sign -> [symb_items] -> [symb_items] -> Result (sign, sign, sign, EndoMap symbol, EndoMap symbol)
create a co-span fragment from an equivalence
Instances
printTheory :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol => Maybe IRI -> lid -> (sign, [Named sentence]) -> Doc
print a whole theory
inclusion :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol => lid -> sign -> sign -> Result morphism
guarded inclusion
class (Ord l, Show l) => SemiLatticeWithTop l where
semi lattices with top (needed for sublogics). Note that Ord is
only used for efficiency and is not related to the partial order given
by the lattice. Only Eq is used to define isSubElem
Instances
| SemiLatticeWithTop () | |
| SemiLatticeWithTop HolLightSL | Sublogics |
| SemiLatticeWithTop CASL_DL_SL | |
| SemiLatticeWithTop ProfSub | |
| SemiLatticeWithTop CommonLogicSL | Sublogics |
| SemiLatticeWithTop PropSL | Sublogics |
| SemiLatticeWithTop QBFSL | Sublogics |
| SemiLatticeWithTop Sublogic | |
| SemiLatticeWithTop THFSl | |
| Lattice a => SemiLatticeWithTop (CASL_SL a) | |
| (SemiLatticeWithTop sublogics1, SemiLatticeWithTop sublogics2) => SemiLatticeWithTop (SublogicsPair sublogics1 sublogics2) |
isSubElem :: SemiLatticeWithTop l => l -> l -> Bool
less or equal for semi lattices
class MinSublogic sublogic item where
class providing the minimal sublogic of an item
Methods
minSublogic :: item -> sublogic
Instances
class MinSublogic sublogic item => ProjectSublogic sublogic item where
class providing also the projection of an item to a sublogic
Methods
projectSublogic :: sublogic -> item -> item
Instances
class MinSublogic sublogic item => ProjectSublogicM sublogic item where
like ProjectSublogic, but providing a partial projection
Methods
projectSublogicM :: sublogic -> item -> Maybe item
Instances
class SublogicName l where
a class for providing a sublogi name
Methods
sublogicName :: l -> String
Instances
| SublogicName () | |
| SublogicName HolLightSL | |
| SublogicName CASL_DL_SL | |
| SublogicName ProfSub | |
| SublogicName CommonLogicSL | |
| SublogicName PropSL | |
| SublogicName QBFSL | |
| SublogicName Sublogic | |
| SublogicName THFSl | |
| NameSL a => SublogicName (CASL_SL a) | |
| (SublogicName sublogics1, SublogicName sublogics2) => SublogicName (SublogicsPair sublogics1 sublogics2) |
type SyntaxTable = (PrecMap, AssocMap)
a type for syntax information eventually stored in the signature
class (StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol, SemiLatticeWithTop sublogics, MinSublogic sublogics sentence, ProjectSublogic sublogics basic_spec, ProjectSublogicM sublogics symb_items, ProjectSublogicM sublogics symb_map_items, ProjectSublogic sublogics sign, ProjectSublogic sublogics morphism, ProjectSublogicM sublogics symbol, Convertible sublogics, SublogicName sublogics, Ord proof_tree, Show proof_tree, Convertible proof_tree) => Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree | lid -> sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree where
Minimal complete definition
Nothing
Methods
parse_basic_sen :: lid -> Maybe (basic_spec -> AParser st sentence)
stability of the implementation
data_logic :: lid -> Maybe AnyLogic
for a process logic, return its data logic
top_sublogic :: lid -> sublogics
the top sublogic, corresponding to the whole logic
all_sublogics :: lid -> [sublogics]
list all the sublogics of the current logic
bottomSublogic :: lid -> Maybe sublogics
sublogicDimensions :: lid -> [[sublogics]]
parseSublogic :: lid -> String -> Maybe sublogics
parse sublogic (override more efficiently)
proj_sublogic_epsilon :: lid -> sublogics -> sign -> morphism
provide the embedding of a projected signature into the original signature
provers :: lid -> [Prover sign sentence morphism sublogics proof_tree]
several provers can be provided. See module Logic.Prover
cons_checkers :: lid -> [ConsChecker sign sentence sublogics morphism proof_tree]
consistency checkers
conservativityCheck :: lid -> [ConservativityChecker sign sentence morphism]
conservativity checkers
empty_proof_tree :: lid -> proof_tree
the empty proof tree
syntaxTable :: lid -> sign -> Maybe SyntaxTable
omdoc_metatheory :: lid -> Maybe OMCD
export_symToOmdoc :: lid -> NameMap symbol -> symbol -> String -> Result TCElement
export_senToOmdoc :: lid -> NameMap symbol -> sentence -> Result TCorOMElement
export_theoryToOmdoc :: lid -> SigMap symbol -> sign -> [Named sentence] -> Result [TCElement]
additional information which has to be exported can be exported by this function
omdocToSym :: lid -> SigMapI symbol -> TCElement -> String -> Result symbol
omdocToSen :: lid -> SigMapI symbol -> TCElement -> String -> Result (Maybe (Named sentence))
addOMadtToTheory :: lid -> SigMapI symbol -> (sign, [Named sentence]) -> [[OmdADT]] -> Result (sign, [Named sentence])
Algebraic Data Types are imported with this function. By default the input is returned without changes.
addOmdocToTheory :: lid -> SigMapI symbol -> (sign, [Named sentence]) -> [TCElement] -> Result (sign, [Named sentence])
additional information which has to be imported can be imported by this function. By default the input is returned without changes.
Instances
class Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => LogicalFramework lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree | lid -> sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree where
Minimal complete definition
Nothing
Methods
base_sig :: lid -> sign
the base signature
write_logic :: lid -> String -> String
generation of the object logic instances second argument is object logic name
write_syntax :: lid -> String -> morphism -> String
generation of the Ltruth morphism declaration second argument is the object logic name third argument is the Ltruth morphism
write_proof :: lid -> String -> morphism -> String
write_model :: lid -> String -> morphism -> String
read_morphism :: lid -> FilePath -> morphism
write_comorphism :: lid -> String -> String -> String -> morphism -> morphism -> morphism -> String
Instances
| LogicalFramework Isabelle () () Sentence () () Sign IsabelleMorphism () () () | |
| LogicalFramework LF () BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RAW_SYM () | |
| LogicalFramework Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () |
emptyTheory :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol => lid -> Theory sign sentence proof_tree
the empty theory