| 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)
Synopsis
- data Stability
- class ShATermConvertible a => Convertible a
- class (Pretty a, Convertible a, ToJSON a, FromJSON 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
- short_description :: Language lid => lid -> String
- class (Ord object, Ord morphism) => Category object morphism | morphism -> object where
- ide :: object -> morphism
- composeMorphisms :: morphism -> morphism -> Result morphism
- dom, cod :: morphism -> object
- inverse :: morphism -> Result morphism
- isInclusion :: morphism -> Bool
- legal_mor :: morphism -> Result ()
- 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 (PrefixMap -> AParser st symb_items)
- parse_symb_items :: lid -> Maybe (PrefixMap -> AParser st symb_items)
- parse_symb_map_items :: lid -> Maybe (PrefixMap -> AParser st symb_map_items)
- toItem :: lid -> basic_spec -> Item
- symb_items_name :: lid -> symb_items -> [String]
- 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 -> sign -> 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, MonadFail 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 -> String -> Bool -> 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)
- extract_module :: lid -> [IRI] -> (sign, [Named sentence]) -> Result (sign, [Named sentence])
- 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]
- default_prover :: lid -> String
- 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])
- sublogicOfTheo :: lid -> (sign, [sentence]) -> sublogics
- 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
Stability of logic implementations
Constructors
| Stable | |
| Testing | |
| Unstable | |
| Experimental |
class ShATermConvertible a => Convertible a Source #
shortcut for class constraints
Instances
| ShATermConvertible a => Convertible a Source # | |
Defined in Logic.Logic | |
class (Pretty a, Convertible a, ToJSON a, FromJSON a) => PrintTypeConv a Source #
shortcut for class constraints
Instances
| (Pretty a, Convertible a, ToJSON a, FromJSON a) => PrintTypeConv a Source # | |
Defined in Logic.Logic | |
class (Eq a, PrintTypeConv a) => EqPrintTypeConv a Source #
shortcut for class constraints with equality
Instances
| (Eq a, PrintTypeConv a) => EqPrintTypeConv a Source # | |
Defined in Logic.Logic | |
class Show lid => Language lid where Source #
the name of a logic. Define instances like "data CASL = CASL deriving (Show, Typeable, Data)"
Minimal complete definition
Nothing
Instances
short_description :: Language lid => lid -> String Source #
class (Ord object, Ord morphism) => Category object morphism | morphism -> object where Source #
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 Source #
identity morphisms
composeMorphisms :: morphism -> morphism -> Result morphism Source #
composition, in diagrammatic order, if intermediate objects are equal (not checked!)
dom :: morphism -> object Source #
domain and codomain of morphisms
cod :: morphism -> object Source #
domain and codomain of morphisms
inverse :: morphism -> Result morphism Source #
the inverse of a morphism
isInclusion :: morphism -> Bool Source #
test if the signature morphism an inclusion
legal_mor :: morphism -> Result () Source #
is a value of type morphism denoting a legal morphism?
Instances
isIdentity :: Category object morphism => morphism -> Bool Source #
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 Source #
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) Source #
parsers and printers
parse_basic_spec :: lid -> Maybe (PrefixMap -> AParser st basic_spec) Source #
parser for basic specifications
parseSingleSymbItem :: lid -> Maybe (PrefixMap -> AParser st symb_items) Source #
parser for a single symbol returned as list
parse_symb_items :: lid -> Maybe (PrefixMap -> AParser st symb_items) Source #
parser for symbol lists
parse_symb_map_items :: lid -> Maybe (PrefixMap -> AParser st symb_map_items) Source #
parser for symbol maps
toItem :: lid -> basic_spec -> Item Source #
symb_items_name :: lid -> symb_items -> [String] Source #
Instances
basicSpecParser :: Syntax lid basic_spec symbol symb_items symb_map_items => Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec) Source #
basicSpecPrinter :: Syntax lid basic_spec symbol symb_items symb_map_items => Maybe IRI -> lid -> Maybe (basic_spec -> Doc) Source #
basicSpecSyntaxes :: Syntax lid basic_spec symbol symb_items symb_map_items => lid -> [String] Source #
parserAndPrinter :: Syntax lid basic_spec symbol symb_items symb_map_items => Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec, basic_spec -> Doc) Source #
lookupDefault :: Syntax lid basic_spec symbol symb_items symb_map_items => lid -> Maybe IRI -> Map String b -> Maybe b Source #
function to lookup parser or printer
showSyntax :: Language lid => lid -> Maybe IRI -> String Source #
makeDefault :: b -> Map String b Source #
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 Source #
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 Source #
sentence translation along a signature morphism
simplify_sen :: lid -> sign -> sentence -> sentence Source #
simplification of sentences (leave out qualifications)
negation :: lid -> sentence -> Maybe sentence Source #
negation of a sentence for disproving
print_sign :: lid -> sign -> Doc Source #
modified signature printing when followed by sentences
print_named :: lid -> Named sentence -> Doc Source #
print a sentence with comments
sym_of :: lid -> sign -> [Set symbol] Source #
dependency ordered list of symbol sets for a signature
mostSymsOf :: lid -> sign -> [symbol] Source #
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 Source #
symbol map for a signature morphism
sym_name :: lid -> symbol -> Id Source #
symbols have a name, see CASL RefMan p. 192
sym_label :: lid -> symbol -> Maybe String Source #
some symbols have a label for better readability
fullSymName :: lid -> symbol -> String Source #
the fully qualified name for XML output (i.e. of OWL2)
symKind :: lid -> symbol -> String Source #
a logic dependent kind of a symbol
symsOfSen :: lid -> sign -> sentence -> [symbol] Source #
the symbols occuring in a sentence (any order)
pair_symbols :: lid -> symbol -> symbol -> Result symbol Source #
combine two symbols into another one
Instances
singletonList :: a -> [a] Source #
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 Source #
set of symbols for a signature
symlist_of :: forall lid sentence sign morphism symbol. Sentences lid sentence sign morphism symbol => lid -> sign -> [symbol] Source #
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] Source #
a dummy static analysis function to allow type checking *.inline.hs files
statFail :: (Language lid, MonadFail m) => lid -> String -> m a Source #
fail function for static analysis
statErrMsg :: Language lid => lid -> String -> String Source #
error message for static analysis
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 Source #
Minimal complete definition
Methods
basic_analysis :: lid -> Maybe ((basic_spec, sign, GlobalAnnos) -> Result (basic_spec, ExtSign sign symbol, [Named sentence])) Source #
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) Source #
Analysis of just sentences
extBasicAnalysis :: lid -> IRI -> LibName -> basic_spec -> sign -> GlobalAnnos -> Result (basic_spec, ExtSign sign symbol, [Named sentence]) Source #
a basic analysis with additional arguments
stat_symb_map_items :: lid -> sign -> Maybe sign -> [symb_map_items] -> Result (EndoMap raw_symbol) Source #
static analysis of symbol maps, see CASL RefMan p. 222f.
stat_symb_items :: lid -> sign -> [symb_items] -> Result [raw_symbol] Source #
static analysis of symbol lists, see CASL RefMan p. 221f.
convertTheory :: lid -> Maybe ((sign, [Named sentence]) -> basic_spec) Source #
convert a theory to basic specs for different serializations
ensures_amalgamability :: lid -> ([CASLAmalgOpt], Gr sign (Int, morphism), [(Int, morphism)], Gr String String) -> Result Amalgamates Source #
architectural sharing analysis, see CASL RefMan p. 247ff.
quotient_term_algebra :: lid -> morphism -> [Named sentence] -> Result (sign, [Named sentence]) Source #
quotient term algebra for normalization of freeness
signature_colimit :: lid -> Gr sign (Int, morphism) -> Result (sign, Map Int morphism) Source #
signature colimits
qualify :: lid -> SIMPLE_ID -> LibName -> morphism -> sign -> Result (morphism, [Named sentence]) Source #
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 Source #
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 Source #
Construe an identifier, like f, as a raw symbol. See CASL RefMan p. 192, function IDAsSym
matches :: lid -> symbol -> raw_symbol -> Bool Source #
Check whether a symbol matches a raw symbol, for example, f:s->t matches f. See CASL RefMan p. 192
empty_signature :: lid -> sign Source #
the empty (initial) signature, see CASL RefMan p. 193
add_symb_to_sign :: lid -> sign -> symbol -> Result sign Source #
adds a symbol to a given signature
signature_union :: lid -> sign -> sign -> Result sign Source #
union of signatures, see CASL RefMan p. 193
signatureDiff :: lid -> sign -> sign -> Result sign Source #
difference of signatures resulting in unclosed pre-signatures
intersection :: lid -> sign -> sign -> Result sign Source #
intersection of signatures
final_union :: lid -> sign -> sign -> Result sign Source #
final union of signatures, see CASL RefMan p. 194
morphism_union :: lid -> morphism -> morphism -> Result morphism Source #
union of signature morphims, see CASL RefMan p. 196
is_subsig :: lid -> sign -> sign -> Bool Source #
subsignatures, see CASL RefMan p. 194
subsig_inclusion :: lid -> sign -> sign -> Result morphism Source #
construct the inclusion morphisms between subsignatures, see CASL RefMan p. 194
generated_sign :: lid -> Set symbol -> sign -> Result morphism Source #
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.
cogenerated_sign :: lid -> Set symbol -> sign -> Result morphism Source #
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 Source #
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 Source #
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 Source #
Check whether a signature morphism is transportable. See CASL RefMan p. 304f.
is_injective :: lid -> morphism -> Bool Source #
Check whether the underlying symbol map of a signature morphism is injective
theory_to_taxonomy :: lid -> TaxoGraphKind -> MMiSSOntology -> sign -> [Named sentence] -> Result MMiSSOntology Source #
generate an ontological taxonomy, if this makes sense
corresp2th :: lid -> String -> Bool -> sign -> sign -> [symb_items] -> [symb_items] -> EndoMap symbol -> EndoMap symbol -> REL_REF -> Result (sign, [Named sentence], sign, sign, EndoMap symbol, EndoMap symbol) Source #
create a theory from a correspondence
equiv2cospan :: lid -> sign -> sign -> [symb_items] -> [symb_items] -> Result (sign, sign, sign, EndoMap symbol, EndoMap symbol) Source #
create a co-span fragment from an equivalence
extract_module :: lid -> [IRI] -> (sign, [Named sentence]) -> Result (sign, [Named sentence]) Source #
extract the module