Hets - the Heterogeneous Tool Set

Copyright(c) Till Mossakowski and Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable (various -fglasgow-exts extensions)
Safe HaskellNone

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

Documentation

data Stability Source #

Stability of logic implementations

Instances

Eq Stability Source # 

Methods

(==) :: Stability -> Stability -> Bool

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

Show Stability Source # 

Methods

showsPrec :: Int -> Stability -> ShowS

show :: Stability -> String

showList :: [Stability] -> ShowS

class ShATermConvertible a => Convertible a Source #

shortcut for class constraints

Instances

ShATermConvertible a => Convertible a Source # 

class (Pretty a, Convertible a) => PrintTypeConv a Source #

shortcut for class constraints

Instances

class (Eq a, PrintTypeConv a) => EqPrintTypeConv a Source #

shortcut for class constraints with equality

Instances

type EndoMap a = Map a a Source #

maps from a to a

class Show lid => Language lid where Source #

the name of a logic. Define instances like "data CASL = CASL deriving (Show, Typeable, Data)"

Methods

language_name :: lid -> String Source #

description :: lid -> String Source #

Instances

Language CSMOF Source # 

Methods

language_name :: CSMOF -> String Source #

description :: CSMOF -> String Source #

Language DMU Source # 

Methods

language_name :: DMU -> String Source #

description :: DMU -> String Source #

Language Isabelle Source # 

Methods

language_name :: Isabelle -> String Source #

description :: Isabelle -> String Source #

Language OMDoc_PUN Source # 

Methods

language_name :: OMDoc_PUN -> String Source #

description :: OMDoc_PUN -> String Source #

Language QVTR Source # 

Methods

language_name :: QVTR -> String Source #

description :: QVTR -> String Source #

Language RDF Source # 

Methods

language_name :: RDF -> String Source #

description :: RDF -> String Source #

Language Temporal Source #

Instance of Language for temporal logic

Methods

language_name :: Temporal -> String Source #

description :: Temporal -> String Source #

Language HasCASL Source # 

Methods

language_name :: HasCASL -> String Source #

description :: HasCASL -> String Source #

Language RelScheme Source # 

Methods

language_name :: RelScheme -> String Source #

description :: RelScheme -> String Source #

Language HasCASL2HasCASL Source # 
Language HasCASL2IsabelleHOL Source # 
Language HasCASL2PCoClTyConsHOL Source # 
Language MonadicHasCASL2IsabelleHOL Source # 
Language PCoClTyConsHOL2IsabelleHOL Source # 
Language PCoClTyConsHOL2PairsInIsaHOL Source # 
Language Grothendieck Source # 
Language CASL Source # 

Methods

language_name :: CASL -> String Source #

description :: CASL -> String Source #

Language CASL_DL Source # 

Methods

language_name :: CASL_DL -> String Source #

description :: CASL_DL -> String Source #

Language COL Source # 

Methods

language_name :: COL -> String Source #

description :: COL -> String Source #

Language CoCASL Source # 

Methods

language_name :: CoCASL -> String Source #

description :: CoCASL -> String Source #

Language CASL2CoCASL Source # 
Language CASL2HasCASL Source # 
Language CASL2NNF Source # 

Methods

language_name :: CASL2NNF -> String Source #

description :: CASL2NNF -> String Source #

Language CASL2PCFOL Source # 

Methods

language_name :: CASL2PCFOL -> String Source #

description :: CASL2PCFOL -> String Source #

Language CoCASL2CoPCFOL Source # 
Language CASL2Prenex Source # 
Language CASL2Skolem Source # 
Language CASL2SubCFOL Source # 
Language CoCASL2CoSubCFOL Source # 
Language CASL2TopSort Source # 
Language CASL_DL2CASL Source # 
Language CFOL2IsabelleHOL Source # 
Language CoCFOL2IsabelleHOL Source # 
Language CSMOF2CASL Source # 

Methods

language_name :: CSMOF2CASL -> String Source #

description :: CSMOF2CASL -> String Source #

Language QVTR2CASL Source # 

Methods

language_name :: QVTR2CASL -> String Source #

description :: QVTR2CASL -> String Source #

Language RelScheme2CASL Source # 
Language ConstraintCASL Source # 
Language CASL2CspCASL Source # 
Language ExtModal Source # 

Methods

language_name :: ExtModal -> String Source #

description :: ExtModal -> String Source #

Language CASL2ExtModal Source # 
Language ExtModal2CASL Source # 
Language ExtModal2ExtModalNoSubsorts Source # 
Language ExtModal2ExtModalTotal Source # 
Language ExtModal2HasCASL Source # 
Language Fpl Source # 

Methods

language_name :: Fpl -> String Source #

description :: Fpl -> String Source #

Language Hybrid Source # 

Methods

language_name :: Hybrid -> String Source #

description :: Hybrid -> String Source #

Language CASL2Hybrid Source # 
Language Hybrid2CASL Source # 
Language Modal Source # 

Methods

language_name :: Modal -> String Source #

description :: Modal -> String Source #

Language CASL2Modal Source # 

Methods

language_name :: CASL2Modal -> String Source #

description :: CASL2Modal -> String Source #

Language CspCASL2Modal Source # 
Language Modal2CASL Source # 

Methods

language_name :: Modal2CASL -> String Source #

description :: Modal2CASL -> String Source #

Language MODAL_EMBEDDING Source # 
Language VSE Source # 

Methods

language_name :: VSE -> String Source #

description :: VSE -> String Source #

Language CASL2VSE Source # 

Methods

language_name :: CASL2VSE -> String Source #

description :: CASL2VSE -> String Source #

Language CASL2VSEImport Source # 
Language CASL2VSERefine Source # 
Language THF Source # 

Methods

language_name :: THF -> String Source #

description :: THF -> String Source #

Language HasCASL2THFP_P Source # 
Language THFP2THF0 Source # 

Methods

language_name :: THFP2THF0 -> String Source #

description :: THFP2THF0 -> String Source #

Language THFP_P2HasCASL Source # 
Language THFP_P2THFP Source # 
Language OWL2 Source # 

Methods

language_name :: OWL2 -> String Source #

description :: OWL2 -> String Source #

Language CASL2OWL Source # 

Methods

language_name :: CASL2OWL -> String Source #

description :: CASL2OWL -> String Source #

Language ExtModal2OWL Source # 
Language DMU2OWL2 Source # 

Methods

language_name :: DMU2OWL2 -> String Source #

description :: DMU2OWL2 -> String Source #

Language OWL22CASL Source # 

Methods

language_name :: OWL22CASL -> String Source #

description :: OWL22CASL -> String Source #

Language Adl Source # 

Methods

language_name :: Adl -> String Source #

description :: Adl -> String Source #

Language Adl2CASL Source # 

Methods

language_name :: Adl2CASL -> String Source #

description :: Adl2CASL -> String Source #

Language CSL Source # 

Methods

language_name :: CSL -> String Source #

description :: CSL -> String Source #

Language CommonLogic Source # 
Language CL2CFOL Source # 

Methods

language_name :: CL2CFOL -> String Source #

description :: CL2CFOL -> String Source #

Language CommonLogic2IsabelleHOL Source # 
Language CommonLogicModuleElimination Source # 
Language OWL22CommonLogic Source # 
Language DFOL Source # 

Methods

language_name :: DFOL -> String Source #

description :: DFOL -> String Source #

Language DFOL2CASL Source # 

Methods

language_name :: DFOL2CASL -> String Source #

description :: DFOL2CASL -> String Source #

Language FrameworkCom Source # 
Language Framework Source # 

Methods

language_name :: Framework -> String Source #

description :: Framework -> String Source #

Language FreeCAD Source # 

Methods

language_name :: FreeCAD -> String Source #

description :: FreeCAD -> String Source #

Language HolLight Source # 

Methods

language_name :: HolLight -> String Source #

description :: HolLight -> String Source #

Language HolLight2Isabelle Source # 
Language LF Source # 

Methods

language_name :: LF -> String Source #

description :: LF -> String Source #

Language Maude Source #

Instance of Language for Maude

Methods

language_name :: Maude -> String Source #

description :: Maude -> String Source #

Language Maude2CASL Source # 

Methods

language_name :: Maude2CASL -> String Source #

description :: Maude2CASL -> String Source #

Language Propositional Source # 
Language CASL2Prop Source # 

Methods

language_name :: CASL2Prop -> String Source #

description :: CASL2Prop -> String Source #

Language Prop2CASL Source # 

Methods

language_name :: Prop2CASL -> String Source #

description :: Prop2CASL -> String Source #

Language Prop2CommonLogic Source # 
Language Propositional2OWL2 Source # 
Language QBF Source # 

Methods

language_name :: QBF -> String Source #

description :: QBF -> String Source #

Language Prop2QBF Source # 

Methods

language_name :: Prop2QBF -> String Source #

description :: Prop2QBF -> String Source #

Language QBF2Prop Source # 

Methods

language_name :: QBF2Prop -> String Source #

description :: QBF2Prop -> String Source #

Language SoftFOL Source # 

Methods

language_name :: SoftFOL -> String Source #

description :: SoftFOL -> String Source #

Language SoftFOL2CommonLogic Source # 
Language TPTP Source # 

Methods

language_name :: TPTP -> String Source #

description :: TPTP -> String Source #

Language Hybridize Source # 

Methods

language_name :: Hybridize -> String Source #

description :: Hybridize -> String Source #

Language lid => Language (IdModif lid) Source # 

Methods

language_name :: IdModif lid -> String Source #

description :: IdModif lid -> String Source #

Language cid => Language (SpanDomain cid) Source # 

Methods

language_name :: SpanDomain cid -> String Source #

description :: SpanDomain cid -> String Source #

Show a => Language (GenCspCASL a) Source # 

Methods

language_name :: GenCspCASL a -> String Source #

description :: GenCspCASL a -> String Source #

(Language cid1, Language cid2) => Language (CompComorphism cid1 cid2) Source # 

Methods

language_name :: CompComorphism cid1 cid2 -> String Source #

description :: CompComorphism cid1 cid2 -> String Source #

(Language lid, Eq sublogics, Show sublogics, SublogicName sublogics) => Language (InclComorphism lid sublogics) Source # 

Methods

language_name :: InclComorphism lid sublogics -> String Source #

description :: InclComorphism lid sublogics -> String Source #

(Language lid1, Language lid2) => Language (HorCompModif lid1 lid2) Source # 

Methods

language_name :: HorCompModif lid1 lid2 -> String Source #

description :: HorCompModif lid1 lid2 -> String Source #

(Language lid1, Language lid2) => Language (VerCompModif lid1 lid2) Source # 

Methods

language_name :: VerCompModif lid1 lid2 -> String Source #

description :: VerCompModif lid1 lid2 -> String Source #

Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism sign_symbol symbol proof_tree => Language (IdMorphism lid sublogics) Source # 

Methods

language_name :: IdMorphism lid sublogics -> String Source #

description :: IdMorphism lid sublogics -> String Source #

(Show a, Show b) => Language (CspCASL2CspCASL a b) Source # 

Methods

language_name :: CspCASL2CspCASL a b -> String Source #

description :: CspCASL2CspCASL a b -> String Source #

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

ide, composeMorphisms, dom, cod

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, 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?

isIdentity :: Category object morphism => morphism -> Bool Source #

test if the signature morphism is the identity

comp :: Category object morphism => morphism -> morphism -> Result morphism Source #

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

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 (AParser st symb_items) Source #

parser for a single symbol returned as list

parse_symb_items :: lid -> Maybe (AParser st symb_items) Source #

parser for symbol lists

parse_symb_map_items :: lid -> Maybe (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

Syntax CSMOF Metamodel () () () Source # 
Syntax DMU Text () () () Source # 

Methods

parsersAndPrinters :: DMU -> Map String (PrefixMap -> AParser st Text, Text -> Doc) Source #

parse_basic_spec :: DMU -> Maybe (PrefixMap -> AParser st Text) Source #

parseSingleSymbItem :: DMU -> Maybe (AParser st ()) Source #

parse_symb_items :: DMU -> Maybe (AParser st ()) Source #

parse_symb_map_items :: DMU -> Maybe (AParser st ()) Source #

toItem :: DMU -> Text -> Item Source #

symb_items_name :: DMU -> () -> [String] Source #

Syntax Isabelle () () () () Source # 

Methods

parsersAndPrinters :: Isabelle -> Map String (PrefixMap -> AParser st (), () -> Doc) Source #

parse_basic_spec :: Isabelle -> Maybe (PrefixMap -> AParser st ()) Source #

parseSingleSymbItem :: Isabelle -> Maybe (AParser st ()) Source #

parse_symb_items :: Isabelle -> Maybe (AParser st ()) Source #

parse_symb_map_items :: Isabelle -> Maybe (AParser st ()) Source #

toItem :: Isabelle -> () -> Item Source #

symb_items_name :: Isabelle -> () -> [String] Source #

Syntax OMDoc_PUN () Symbol () () Source # 

Methods

parsersAndPrinters :: OMDoc_PUN -> Map String (PrefixMap -> AParser st (), () -> Doc) Source #

parse_basic_spec :: OMDoc_PUN -> Maybe (PrefixMap -> AParser st ()) Source #

parseSingleSymbItem :: OMDoc_PUN -> Maybe (AParser st ()) Source #

parse_symb_items :: OMDoc_PUN -> Maybe (AParser st ()) Source #

parse_symb_map_items :: OMDoc_PUN -> Maybe (AParser st ()) Source #

toItem :: OMDoc_PUN -> () -> Item Source #

symb_items_name :: OMDoc_PUN -> () -> [String] Source #

Syntax QVTR Transformation () () () Source # 
Syntax RDF TurtleDocument RDFEntity SymbItems SymbMapItems Source # 
Syntax Temporal BASIC_SPEC Symbol () () Source #

Syntax of Temporal logic

Syntax HasCASL BasicSpec Symbol SymbItems SymbMapItems Source # 
Syntax RelScheme RSScheme RSSymbol () () Source #

Syntax of Rel

Syntax CASL CASLBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax CASL_DL DL_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax COL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax CoCASL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax ConstraintCASL ConstraintCASLBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax ExtModal EM_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax Fpl FplBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax Hybrid H_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax Modal M_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax THF BasicSpecTHF SymbolTHF () () Source # 
Syntax OWL2 OntologyDocument Entity SymbItems SymbMapItems Source # 
Syntax Adl Context Symbol () () Source # 

Methods

parsersAndPrinters :: Adl -> Map String (PrefixMap -> AParser st Context, Context -> Doc) Source #

parse_basic_spec :: Adl -> Maybe (PrefixMap -> AParser st Context) Source #

parseSingleSymbItem :: Adl -> Maybe (AParser st ()) Source #

parse_symb_items :: Adl -> Maybe (AParser st ()) Source #

parse_symb_map_items :: Adl -> Maybe (AParser st ()) Source #

toItem :: Adl -> Context -> Item Source #

symb_items_name :: Adl -> () -> [String] Source #

Syntax CSL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #

Syntax of CSL logic

Syntax CommonLogic BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax DFOL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax FrameworkCom ComorphismDef () () () Source # 
Syntax Framework LogicDef () () () Source # 
Syntax FreeCAD Document () () () Source # 
Syntax HolLight () () () () Source # 

Methods

parsersAndPrinters :: HolLight -> Map String (PrefixMap -> AParser st (), () -> Doc) Source #

parse_basic_spec :: HolLight -> Maybe (PrefixMap -> AParser st ()) Source #

parseSingleSymbItem :: HolLight -> Maybe (AParser st ()) Source #

parse_symb_items :: HolLight -> Maybe (AParser st ()) Source #

parse_symb_map_items :: HolLight -> Maybe (AParser st ()) Source #

toItem :: HolLight -> () -> Item Source #

symb_items_name :: HolLight -> () -> [String] Source #

Syntax LF BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax Maude MaudeText Symbol () () Source #

Instance of Syntax for Maude

Syntax Propositional BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax QBF BASICSPEC Symbol SYMBITEMS SYMBMAPITEMS Source #

Syntax of Propositional logic

Syntax TPTP BASIC_SPEC Symbol () () Source # 
Syntax Hybridize Spc_Wrap Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax SoftFOL [TPTP] SFSymbol () () Source # 
(Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2, Pretty sign_symbol1) => Syntax (SpanDomain cid) () sign_symbol1 () () Source # 

Methods

parsersAndPrinters :: SpanDomain cid -> Map String (PrefixMap -> AParser st (), () -> Doc) Source #

parse_basic_spec :: SpanDomain cid -> Maybe (PrefixMap -> AParser st ()) Source #

parseSingleSymbItem :: SpanDomain cid -> Maybe (AParser st ()) Source #

parse_symb_items :: SpanDomain cid -> Maybe (AParser st ()) Source #

parse_symb_map_items :: SpanDomain cid -> Maybe (AParser st ()) Source #

toItem :: SpanDomain cid -> () -> Item Source #

symb_items_name :: SpanDomain cid -> () -> [String] Source #

Show a => Syntax (GenCspCASL a) CspBasicSpec CspSymbol CspSymbItems CspSymbMapItems Source #

Syntax of CspCASL

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 #

addSyntax :: String -> b -> Map String 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.

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

Sentences CSMOF Sen Sign Morphism () Source # 

Methods

map_sen :: CSMOF -> Morphism -> Sen -> Result Sen Source #

simplify_sen :: CSMOF -> Sign -> Sen -> Sen Source #

negation :: CSMOF -> Sen -> Maybe Sen Source #

print_sign :: CSMOF -> Sign -> Doc Source #

print_named :: CSMOF -> Named Sen -> Doc Source #

sym_of :: CSMOF -> Sign -> [Set ()] Source #

mostSymsOf :: CSMOF -> Sign -> [()] Source #

symmap_of :: CSMOF -> Morphism -> EndoMap () Source #

sym_name :: CSMOF -> () -> Id Source #

sym_label :: CSMOF -> () -> Maybe String Source #

fullSymName :: CSMOF -> () -> String Source #

symKind :: CSMOF -> () -> String Source #

symsOfSen :: CSMOF -> Sign -> Sen -> [()] Source #

pair_symbols :: CSMOF -> () -> () -> Result () Source #

Sentences Isabelle Sentence Sign IsabelleMorphism () Source # 
Sentences OMDoc_PUN () OMDoc_Sign OMDoc_Morphism Symbol Source # 
Sentences QVTR Sen Sign Morphism () Source # 

Methods

map_sen :: QVTR -> Morphism -> Sen -> Result Sen Source #

simplify_sen :: QVTR -> Sign -> Sen -> Sen Source #

negation :: QVTR -> Sen -> Maybe Sen Source #

print_sign :: QVTR -> Sign -> Doc Source #

print_named :: QVTR -> Named Sen -> Doc Source #

sym_of :: QVTR -> Sign -> [Set ()] Source #

mostSymsOf :: QVTR -> Sign -> [()] Source #

symmap_of :: QVTR -> Morphism -> EndoMap () Source #

sym_name :: QVTR -> () -> Id Source #

sym_label :: QVTR -> () -> Maybe String Source #

fullSymName :: QVTR -> () -> String Source #

symKind :: QVTR -> () -> String Source #

symsOfSen :: QVTR -> Sign -> Sen -> [()] Source #

pair_symbols :: QVTR -> () -> () -> Result () Source #

Sentences RDF Axiom Sign RDFMorphism RDFEntity Source # 
Sentences Temporal FORMULA Sign Morphism Symbol Source #

Instance of Sentences for temporal logic

Sentences HasCASL Sentence Env Morphism Symbol Source # 
Sentences RelScheme Sentence Sign RSMorphism RSSymbol Source #

Instance of Sentences for Rel

Sentences CASL CASLFORMULA CASLSign CASLMor Symbol Source # 
Sentences CASL_DL DLFORMULA DLSign DLMor Symbol Source # 
Sentences COL COLFORMULA CSign COLMor Symbol Source # 
Sentences CoCASL CoCASLFORMULA CSign CoCASLMor Symbol Source # 
Sentences ConstraintCASL ConstraintCASLFORMULA ConstraintCASLSign ConstraintCASLMor Symbol Source # 
Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol Source # 
Sentences Fpl FplForm FplSign FplMor Symbol Source # 
Sentences Hybrid HybridFORMULA HSign HybridMor Symbol Source # 
Sentences Modal ModalFORMULA MSign ModalMor Symbol Source # 
Sentences VSE Sentence VSESign VSEMor Symbol Source # 
Sentences THF THFFormula SignTHF MorphismTHF SymbolTHF Source # 
Sentences OWL2 Axiom Sign OWLMorphism Entity Source # 
Sentences Adl Sen Sign Morphism Symbol Source # 
Sentences CSL CMD Sign Morphism Symbol Source #

Instance of Sentences for reduce logic

Sentences CommonLogic TEXT_META Sign Morphism Symbol Source # 
Sentences DFOL FORMULA Sign Morphism Symbol Source # 
Sentences FrameworkCom () ComorphismDef MorphismCom () Source # 
Sentences Framework () LogicDef Morphism () Source # 

Methods

map_sen :: Framework -> Morphism -> () -> Result () Source #

simplify_sen :: Framework -> LogicDef -> () -> () Source #

negation :: Framework -> () -> Maybe () Source #

print_sign :: Framework -> LogicDef -> Doc Source #

print_named :: Framework -> Named () -> Doc Source #

sym_of :: Framework -> LogicDef -> [Set ()] Source #

mostSymsOf :: Framework -> LogicDef -> [()] Source #

symmap_of :: Framework -> Morphism -> EndoMap () Source #

sym_name :: Framework -> () -> Id Source #

sym_label :: Framework -> () -> Maybe String Source #

fullSymName :: Framework -> () -> String Source #

symKind :: Framework -> () -> String Source #

symsOfSen :: Framework -> LogicDef -> () -> [()] Source #

pair_symbols :: Framework -> () -> () -> Result () Source #

Sentences FreeCAD () Sign FCMorphism () Source # 

Methods

map_sen :: FreeCAD -> FCMorphism -> () -> Result () Source #

simplify_sen :: FreeCAD -> Sign -> () -> () Source #

negation :: FreeCAD -> () -> Maybe () Source #

print_sign :: FreeCAD -> Sign -> Doc Source #

print_named :: FreeCAD -> Named () -> Doc Source #

sym_of :: FreeCAD -> Sign -> [Set ()] Source #

mostSymsOf :: FreeCAD -> Sign -> [()] Source #

symmap_of :: FreeCAD -> FCMorphism -> EndoMap () Source #

sym_name :: FreeCAD -> () -> Id Source #

sym_label :: FreeCAD -> () -> Maybe String Source #

fullSymName :: FreeCAD -> () -> String Source #

symKind :: FreeCAD -> () -> String Source #

symsOfSen :: FreeCAD -> Sign -> () -> [()] Source #

pair_symbols :: FreeCAD -> () -> () -> Result () Source #

Sentences HolLight Sentence Sign HolLightMorphism () Source # 
Sentences LF Sentence Sign Morphism Symbol Source # 
Sentences Maude Sentence Sign Morphism Symbol Source #

Instance of Sentences for Maude

Sentences Propositional FORMULA Sign Morphism Symbol Source #

Instance of Sentences for propositional logic

Sentences QBF FORMULA Sign Morphism Symbol Source #

Instance of Sentences for propositional logic

Sentences SoftFOL Sentence Sign SoftFOLMorphism SFSymbol Source # 
Sentences TPTP Sentence Sign Morphism Symbol Source # 
Sentences Hybridize Frm_Wrap Sgn_Wrap Mor Symbol Source # 
Sentences DMU () Text (DefaultMorphism Text) () Source # 

Methods

map_sen :: DMU -> DefaultMorphism Text -> () -> Result () Source #

simplify_sen :: DMU -> Text -> () -> () Source #

negation :: DMU -> () -> Maybe () Source #

print_sign :: DMU -> Text -> Doc Source #

print_named :: DMU -> Named () -> Doc Source #

sym_of :: DMU -> Text -> [Set ()] Source #

mostSymsOf :: DMU -> Text -> [()] Source #

symmap_of :: DMU -> DefaultMorphism Text -> EndoMap () Source #

sym_name :: DMU -> () -> Id Source #

sym_label :: DMU -> () -> Maybe String Source #

fullSymName :: DMU -> () -> String Source #

symKind :: DMU -> () -> String Source #

symsOfSen :: DMU -> Text -> () -> [()] Source #

pair_symbols :: DMU -> () -> () -> Result () Source #

Show a => Sentences (GenCspCASL a) CspCASLSen CspCASLSign CspCASLMorphism CspSymbol Source #

Instance of Sentences for CspCASL

(Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2, Category sign1 morphism1, Ord sign_symbol1, GetRange sign_symbol1) => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1 sign_symbol1 Source # 

Methods

map_sen :: SpanDomain cid -> morphism1 -> S2 sentence2 -> Result (S2 sentence2) Source #

simplify_sen :: SpanDomain cid -> sign1 -> S2 sentence2 -> S2 sentence2 Source #

negation :: SpanDomain cid -> S2 sentence2 -> Maybe (S2 sentence2) Source #

print_sign :: SpanDomain cid -> sign1 -> Doc Source #

print_named :: SpanDomain cid -> Named (S2 sentence2) -> Doc Source #

sym_of :: SpanDomain cid -> sign1 -> [Set sign_symbol1] Source #

mostSymsOf :: SpanDomain cid -> sign1 -> [sign_symbol1] Source #

symmap_of :: SpanDomain cid -> morphism1 -> EndoMap sign_symbol1 Source #

sym_name :: SpanDomain cid -> sign_symbol1 -> Id Source #

sym_label :: SpanDomain cid -> sign_symbol1 -> Maybe String Source #

fullSymName :: SpanDomain cid -> sign_symbol1 -> String Source #

symKind :: SpanDomain cid -> sign_symbol1 -> String Source #

symsOfSen :: SpanDomain cid -> sign1 -> S2 sentence2 -> [sign_symbol1] Source #

pair_symbols :: SpanDomain cid -> sign_symbol1 -> sign_symbol1 -> Result sign_symbol1 Source #

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, Monad m) => lid -> String -> m a Source #

fail function for static analysis

statError :: Language lid => lid -> String -> a Source #

statErrMsg :: Language lid => lid -> String -> String Source #

error message for static analysis

data REL_REF Source #

Instances

Eq REL_REF Source # 

Methods

(==) :: REL_REF -> REL_REF -> Bool

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

Show REL_REF Source # 

Methods

showsPrec :: Int -> REL_REF -> ShowS

show :: REL_REF -> String

showList :: [REL_REF] -> ShowS

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

empty_signature

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, 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

Instances

StaticAnalysis CSMOF Metamodel Sen () () Sign Morphism () () Source # 

Methods

basic_analysis :: CSMOF -> Maybe ((Metamodel, Sign, GlobalAnnos) -> Result (Metamodel, ExtSign Sign (), [Named Sen])) Source #

sen_analysis :: CSMOF -> Maybe ((Metamodel, Sign, Sen) -> Result Sen) Source #

extBasicAnalysis :: CSMOF -> IRI -> LibName -> Metamodel -> Sign -> GlobalAnnos -> Result (Metamodel, ExtSign Sign (), [Named Sen]) Source #

stat_symb_map_items :: CSMOF -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: CSMOF -> Sign -> [()] -> Result [()] Source #

convertTheory :: CSMOF -> Maybe ((Sign, [Named Sen]) -> Metamodel) Source #

ensures_amalgamability :: CSMOF -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CSMOF -> Morphism -> [Named Sen] -> Result (Sign, [Named Sen]) Source #

signature_colimit :: CSMOF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: CSMOF -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sen]) Source #

symbol_to_raw :: CSMOF -> () -> () Source #

id_to_raw :: CSMOF -> Id -> () Source #

matches :: CSMOF -> () -> () -> Bool Source #

empty_signature :: CSMOF -> Sign Source #

add_symb_to_sign :: CSMOF -> Sign -> () -> Result Sign Source #

signature_union :: CSMOF -> Sign -> Sign -> Result Sign Source #

signatureDiff :: CSMOF -> Sign -> Sign -> Result Sign Source #

intersection :: CSMOF -> Sign -> Sign -> Result Sign Source #

final_union :: CSMOF -> Sign -> Sign -> Result Sign Source #

morphism_union :: CSMOF -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: CSMOF -> Sign -> Sign -> Bool Source #

subsig_inclusion :: CSMOF -> Sign -> Sign -> Result Morphism Source #

generated_sign :: CSMOF -> Set () -> Sign -> Result Morphism Source #

cogenerated_sign :: CSMOF -> Set () -> Sign -> Result Morphism Source #

induced_from_morphism :: CSMOF -> EndoMap () -> Sign -> Result Morphism Source #

induced_from_to_morphism :: CSMOF -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result Morphism Source #

is_transportable :: CSMOF -> Morphism -> Bool Source #

is_injective :: CSMOF -> Morphism -> Bool Source #

theory_to_taxonomy :: CSMOF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sen] -> Result MMiSSOntology Source #

corresp2th :: CSMOF -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named Sen], Sign, Sign, EndoMap (), EndoMap ()) Source #

equiv2cospan :: CSMOF -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source #

extract_module :: CSMOF -> [IRI] -> (Sign, [Named Sen]) -> Result (Sign, [Named Sen]) Source #

StaticAnalysis Isabelle () Sentence () () Sign IsabelleMorphism () () Source # 

Methods

basic_analysis :: Isabelle -> Maybe (((), Sign, GlobalAnnos) -> Result ((), ExtSign Sign (), [Named Sentence])) Source #

sen_analysis :: Isabelle -> Maybe (((), Sign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: Isabelle -> IRI -> LibName -> () -> Sign -> GlobalAnnos -> Result ((), ExtSign Sign (), [Named Sentence]) Source #

stat_symb_map_items :: Isabelle -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: Isabelle -> Sign -> [()] -> Result [()] Source #

convertTheory :: Isabelle -> Maybe ((Sign, [Named Sentence]) -> ()) Source #

ensures_amalgamability :: Isabelle -> ([CASLAmalgOpt], Gr Sign (Int, IsabelleMorphism), [(Int, IsabelleMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Isabelle -> IsabelleMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: Isabelle -> Gr Sign (Int, IsabelleMorphism) -> Result (Sign, Map Int IsabelleMorphism) Source #

qualify :: Isabelle -> SIMPLE_ID -> LibName -> IsabelleMorphism -> Sign -> Result (IsabelleMorphism, [Named Sentence]) Source #

symbol_to_raw :: Isabelle -> () -> () Source #

id_to_raw :: Isabelle -> Id -> () Source #

matches :: Isabelle -> () -> () -> Bool Source #

empty_signature :: Isabelle -> Sign Source #

add_symb_to_sign :: Isabelle -> Sign -> () -> Result Sign Source #

signature_union :: Isabelle -> Sign -> Sign -> Result Sign Source #

signatureDiff :: Isabelle -> Sign -> Sign -> Result Sign Source #

intersection :: Isabelle -> Sign -> Sign -> Result Sign Source #

final_union :: Isabelle -> Sign -> Sign -> Result Sign Source #

morphism_union :: Isabelle -> IsabelleMorphism -> IsabelleMorphism -> Result IsabelleMorphism Source #

is_subsig :: Isabelle -> Sign -> Sign -> Bool Source #

subsig_inclusion :: Isabelle -> Sign -> Sign -> Result IsabelleMorphism Source #

generated_sign :: Isabelle -> Set () -> Sign -> Result IsabelleMorphism Source #

cogenerated_sign :: Isabelle -> Set () -> Sign -> Result IsabelleMorphism Source #

induced_from_morphism :: Isabelle -> EndoMap () -> Sign -> Result IsabelleMorphism Source #

induced_from_to_morphism :: Isabelle -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result IsabelleMorphism Source #

is_transportable :: Isabelle -> IsabelleMorphism -> Bool Source #

is_injective :: Isabelle -> IsabelleMorphism -> Bool Source #

theory_to_taxonomy :: Isabelle -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: Isabelle -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap (), EndoMap ()) Source #

equiv2cospan :: Isabelle -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source #

extract_module :: Isabelle -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

StaticAnalysis OMDoc_PUN () () () () OMDoc_Sign OMDoc_Morphism Symbol () Source # 

Methods

basic_analysis :: OMDoc_PUN -> Maybe (((), OMDoc_Sign, GlobalAnnos) -> Result ((), ExtSign OMDoc_Sign Symbol, [Named ()])) Source #

sen_analysis :: OMDoc_PUN -> Maybe (((), OMDoc_Sign, ()) -> Result ()) Source #

extBasicAnalysis :: OMDoc_PUN -> IRI -> LibName -> () -> OMDoc_Sign -> GlobalAnnos -> Result ((), ExtSign OMDoc_Sign Symbol, [Named ()]) Source #

stat_symb_map_items :: OMDoc_PUN -> OMDoc_Sign -> Maybe OMDoc_Sign -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: OMDoc_PUN -> OMDoc_Sign -> [()] -> Result [()] Source #

convertTheory :: OMDoc_PUN -> Maybe ((OMDoc_Sign, [Named ()]) -> ()) Source #

ensures_amalgamability :: OMDoc_PUN -> ([CASLAmalgOpt], Gr OMDoc_Sign (Int, OMDoc_Morphism), [(Int, OMDoc_Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: OMDoc_PUN -> OMDoc_Morphism -> [Named ()] -> Result (OMDoc_Sign, [Named ()]) Source #

signature_colimit :: OMDoc_PUN -> Gr OMDoc_Sign (Int, OMDoc_Morphism) -> Result (OMDoc_Sign, Map Int OMDoc_Morphism) Source #

qualify :: OMDoc_PUN -> SIMPLE_ID -> LibName -> OMDoc_Morphism -> OMDoc_Sign -> Result (OMDoc_Morphism, [Named ()]) Source #

symbol_to_raw :: OMDoc_PUN -> Symbol -> () Source #

id_to_raw :: OMDoc_PUN -> Id -> () Source #

matches :: OMDoc_PUN -> Symbol -> () -> Bool Source #

empty_signature :: OMDoc_PUN -> OMDoc_Sign Source #

add_symb_to_sign :: OMDoc_PUN -> OMDoc_Sign -> Symbol -> Result OMDoc_Sign Source #

signature_union :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Sign Source #

signatureDiff :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Sign Source #

intersection :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Sign Source #

final_union :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Sign Source #

morphism_union :: OMDoc_PUN -> OMDoc_Morphism -> OMDoc_Morphism -> Result OMDoc_Morphism Source #

is_subsig :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Bool Source #

subsig_inclusion :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Morphism Source #

generated_sign :: OMDoc_PUN -> Set Symbol -> OMDoc_Sign -> Result OMDoc_Morphism Source #

cogenerated_sign :: OMDoc_PUN -> Set Symbol -> OMDoc_Sign -> Result OMDoc_Morphism Source #

induced_from_morphism :: OMDoc_PUN -> EndoMap () -> OMDoc_Sign -> Result OMDoc_Morphism Source #

induced_from_to_morphism :: OMDoc_PUN -> EndoMap () -> ExtSign OMDoc_Sign Symbol -> ExtSign OMDoc_Sign Symbol -> Result OMDoc_Morphism Source #

is_transportable :: OMDoc_PUN -> OMDoc_Morphism -> Bool Source #

is_injective :: OMDoc_PUN -> OMDoc_Morphism -> Bool Source #

theory_to_taxonomy :: OMDoc_PUN -> TaxoGraphKind -> MMiSSOntology -> OMDoc_Sign -> [Named ()] -> Result MMiSSOntology Source #

corresp2th :: OMDoc_PUN -> String -> Bool -> OMDoc_Sign -> OMDoc_Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (OMDoc_Sign, [Named ()], OMDoc_Sign, OMDoc_Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> [()] -> [()] -> Result (OMDoc_Sign, OMDoc_Sign, OMDoc_Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: OMDoc_PUN -> [IRI] -> (OMDoc_Sign, [Named ()]) -> Result (OMDoc_Sign, [Named ()]) Source #

StaticAnalysis QVTR Transformation Sen () () Sign Morphism () () Source # 

Methods

basic_analysis :: QVTR -> Maybe ((Transformation, Sign, GlobalAnnos) -> Result (Transformation, ExtSign Sign (), [Named Sen])) Source #

sen_analysis :: QVTR -> Maybe ((Transformation, Sign, Sen) -> Result Sen) Source #

extBasicAnalysis :: QVTR -> IRI -> LibName -> Transformation -> Sign -> GlobalAnnos -> Result (Transformation, ExtSign Sign (), [Named Sen]) Source #

stat_symb_map_items :: QVTR -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: QVTR -> Sign -> [()] -> Result [()] Source #

convertTheory :: QVTR -> Maybe ((Sign, [Named Sen]) -> Transformation) Source #

ensures_amalgamability :: QVTR -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: QVTR -> Morphism -> [Named Sen] -> Result (Sign, [Named Sen]) Source #

signature_colimit :: QVTR -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: QVTR -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sen]) Source #

symbol_to_raw :: QVTR -> () -> () Source #

id_to_raw :: QVTR -> Id -> () Source #

matches :: QVTR -> () -> () -> Bool Source #

empty_signature :: QVTR -> Sign Source #

add_symb_to_sign :: QVTR -> Sign -> () -> Result Sign Source #

signature_union :: QVTR -> Sign -> Sign -> Result Sign Source #

signatureDiff :: QVTR -> Sign -> Sign -> Result Sign Source #

intersection :: QVTR -> Sign -> Sign -> Result Sign Source #

final_union :: QVTR -> Sign -> Sign -> Result Sign Source #

morphism_union :: QVTR -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: QVTR -> Sign -> Sign -> Bool Source #

subsig_inclusion :: QVTR -> Sign -> Sign -> Result Morphism Source #

generated_sign :: QVTR -> Set () -> Sign -> Result Morphism Source #

cogenerated_sign :: QVTR -> Set () -> Sign -> Result Morphism Source #

induced_from_morphism :: QVTR -> EndoMap () -> Sign -> Result Morphism Source #

induced_from_to_morphism :: QVTR -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result Morphism Source #

is_transportable :: QVTR -> Morphism -> Bool Source #

is_injective :: QVTR -> Morphism -> Bool Source #

theory_to_taxonomy :: QVTR -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sen] -> Result MMiSSOntology Source #

corresp2th :: QVTR -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named Sen], Sign, Sign, EndoMap (), EndoMap ()) Source #

equiv2cospan :: QVTR -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source #

extract_module :: QVTR -> [IRI] -> (Sign, [Named Sen]) -> Result (Sign, [Named Sen]) Source #

StaticAnalysis RDF TurtleDocument Axiom SymbItems SymbMapItems Sign RDFMorphism RDFEntity RawSymb Source # 

Methods

basic_analysis :: RDF -> Maybe ((TurtleDocument, Sign, GlobalAnnos) -> Result (TurtleDocument, ExtSign Sign RDFEntity, [Named Axiom])) Source #

sen_analysis :: RDF -> Maybe ((TurtleDocument, Sign, Axiom) -> Result Axiom) Source #

extBasicAnalysis :: RDF -> IRI -> LibName -> TurtleDocument -> Sign -> GlobalAnnos -> Result (TurtleDocument, ExtSign Sign RDFEntity, [Named Axiom]) Source #

stat_symb_map_items :: RDF -> Sign -> Maybe Sign -> [SymbMapItems] -> Result (EndoMap RawSymb) Source #

stat_symb_items :: RDF -> Sign -> [SymbItems] -> Result [RawSymb] Source #

convertTheory :: RDF -> Maybe ((Sign, [Named Axiom]) -> TurtleDocument) Source #

ensures_amalgamability :: RDF -> ([CASLAmalgOpt], Gr Sign (Int, RDFMorphism), [(Int, RDFMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: RDF -> RDFMorphism -> [Named Axiom] -> Result (Sign, [Named Axiom]) Source #

signature_colimit :: RDF -> Gr Sign (Int, RDFMorphism) -> Result (Sign, Map Int RDFMorphism) Source #

qualify :: RDF -> SIMPLE_ID -> LibName -> RDFMorphism -> Sign -> Result (RDFMorphism, [Named Axiom]) Source #

symbol_to_raw :: RDF -> RDFEntity -> RawSymb Source #

id_to_raw :: RDF -> Id -> RawSymb Source #

matches :: RDF -> RDFEntity -> RawSymb -> Bool Source #

empty_signature :: RDF -> Sign Source #

add_symb_to_sign :: RDF -> Sign -> RDFEntity -> Result Sign Source #

signature_union :: RDF -> Sign -> Sign -> Result Sign Source #

signatureDiff :: RDF -> Sign -> Sign -> Result Sign Source #

intersection :: RDF -> Sign -> Sign -> Result Sign Source #

final_union :: RDF -> Sign -> Sign -> Result Sign Source #

morphism_union :: RDF -> RDFMorphism -> RDFMorphism -> Result RDFMorphism Source #

is_subsig :: RDF -> Sign -> Sign -> Bool Source #

subsig_inclusion :: RDF -> Sign -> Sign -> Result RDFMorphism Source #

generated_sign :: RDF -> Set RDFEntity -> Sign -> Result RDFMorphism Source #

cogenerated_sign :: RDF -> Set RDFEntity -> Sign -> Result RDFMorphism Source #

induced_from_morphism :: RDF -> EndoMap RawSymb -> Sign -> Result RDFMorphism Source #

induced_from_to_morphism :: RDF -> EndoMap RawSymb -> ExtSign Sign RDFEntity -> ExtSign Sign RDFEntity -> Result RDFMorphism Source #

is_transportable :: RDF -> RDFMorphism -> Bool Source #

is_injective :: RDF -> RDFMorphism -> Bool Source #

theory_to_taxonomy :: RDF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Axiom] -> Result MMiSSOntology Source #

corresp2th :: RDF -> String -> Bool -> Sign -> Sign -> [SymbItems] -> [SymbItems] -> EndoMap RDFEntity -> EndoMap RDFEntity -> REL_REF -> Result (Sign, [Named Axiom], Sign, Sign, EndoMap RDFEntity, EndoMap RDFEntity) Source #

equiv2cospan :: RDF -> Sign -> Sign -> [SymbItems] -> [SymbItems] -> Result (Sign, Sign, Sign, EndoMap RDFEntity, EndoMap RDFEntity) Source #

extract_module :: RDF -> [IRI] -> (Sign, [Named Axiom]) -> Result (Sign, [Named Axiom]) Source #

StaticAnalysis Temporal BASIC_SPEC FORMULA () () Sign Morphism Symbol Symbol Source #

Static Analysis for propositional logic

Methods

basic_analysis :: Temporal -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])) Source #

sen_analysis :: Temporal -> Maybe ((BASIC_SPEC, Sign, FORMULA) -> Result FORMULA) Source #

extBasicAnalysis :: Temporal -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA]) Source #

stat_symb_map_items :: Temporal -> Sign -> Maybe Sign -> [()] -> Result (EndoMap Symbol) Source #

stat_symb_items :: Temporal -> Sign -> [()] -> Result [Symbol] Source #

convertTheory :: Temporal -> Maybe ((Sign, [Named FORMULA]) -> BASIC_SPEC) Source #

ensures_amalgamability :: Temporal -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Temporal -> Morphism -> [Named FORMULA] -> Result (Sign, [Named FORMULA]) Source #

signature_colimit :: Temporal -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: Temporal -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named FORMULA]) Source #

symbol_to_raw :: Temporal -> Symbol -> Symbol Source #

id_to_raw :: Temporal -> Id -> Symbol Source #

matches :: Temporal -> Symbol -> Symbol -> Bool Source #

empty_signature :: Temporal -> Sign Source #

add_symb_to_sign :: Temporal -> Sign -> Symbol -> Result Sign Source #

signature_union :: Temporal -> Sign -> Sign -> Result Sign Source #

signatureDiff :: Temporal -> Sign -> Sign -> Result Sign Source #

intersection :: Temporal -> Sign -> Sign -> Result Sign Source #

final_union :: Temporal -> Sign -> Sign -> Result Sign Source #

morphism_union :: Temporal -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: Temporal -> Sign -> Sign -> Bool Source #

subsig_inclusion :: Temporal -> Sign -> Sign -> Result Morphism Source #

generated_sign :: Temporal -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: Temporal -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: Temporal -> EndoMap Symbol -> Sign -> Result Morphism Source #

induced_from_to_morphism :: Temporal -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: Temporal -> Morphism -> Bool Source #

is_injective :: Temporal -> Morphism -> Bool Source #

theory_to_taxonomy :: Temporal -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named FORMULA] -> Result MMiSSOntology Source #

corresp2th :: Temporal -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Temporal -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Temporal -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) 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 #

StaticAnalysis RelScheme RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol Source #

Static Analysis for Rel

Methods

basic_analysis :: RelScheme -> Maybe ((RSScheme, Sign, GlobalAnnos) -> Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence])) Source #

sen_analysis :: RelScheme -> Maybe ((RSScheme, Sign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: RelScheme -> IRI -> LibName -> RSScheme -> Sign -> GlobalAnnos -> Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence]) Source #

stat_symb_map_items :: RelScheme -> Sign -> Maybe Sign -> [()] -> Result (EndoMap RSRawSymbol) Source #

stat_symb_items :: RelScheme -> Sign -> [()] -> Result [RSRawSymbol] Source #

convertTheory :: RelScheme -> Maybe ((Sign, [Named Sentence]) -> RSScheme) Source #

ensures_amalgamability :: RelScheme -> ([CASLAmalgOpt], Gr Sign (Int, RSMorphism), [(Int, RSMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: RelScheme -> RSMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: RelScheme -> Gr Sign (Int, RSMorphism) -> Result (Sign, Map Int RSMorphism) Source #

qualify :: RelScheme -> SIMPLE_ID -> LibName -> RSMorphism -> Sign -> Result (RSMorphism, [Named Sentence]) Source #

symbol_to_raw :: RelScheme -> RSSymbol -> RSRawSymbol Source #

id_to_raw :: RelScheme -> Id -> RSRawSymbol Source #

matches :: RelScheme -> RSSymbol -> RSRawSymbol -> Bool Source #

empty_signature :: RelScheme -> Sign Source #

add_symb_to_sign :: RelScheme -> Sign -> RSSymbol -> Result Sign Source #

signature_union :: RelScheme -> Sign -> Sign -> Result Sign Source #

signatureDiff :: RelScheme -> Sign -> Sign -> Result Sign Source #

intersection :: RelScheme -> Sign -> Sign -> Result Sign Source #

final_union :: RelScheme -> Sign -> Sign -> Result Sign Source #

morphism_union :: RelScheme -> RSMorphism -> RSMorphism -> Result RSMorphism Source #

is_subsig :: RelScheme -> Sign -> Sign -> Bool Source #

subsig_inclusion :: RelScheme -> Sign -> Sign -> Result RSMorphism Source #

generated_sign :: RelScheme -> Set RSSymbol -> Sign -> Result RSMorphism Source #

cogenerated_sign :: RelScheme -> Set RSSymbol -> Sign -> Result RSMorphism Source #

induced_from_morphism :: RelScheme -> EndoMap RSRawSymbol -> Sign -> Result RSMorphism Source #

induced_from_to_morphism :: RelScheme -> EndoMap RSRawSymbol -> ExtSign Sign RSSymbol -> ExtSign Sign RSSymbol -> Result RSMorphism Source #

is_transportable :: RelScheme -> RSMorphism -> Bool Source #

is_injective :: RelScheme -> RSMorphism -> Bool Source #

theory_to_taxonomy :: RelScheme -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: RelScheme -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap RSSymbol -> EndoMap RSSymbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap RSSymbol, EndoMap RSSymbol) Source #

equiv2cospan :: RelScheme -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap RSSymbol, EndoMap RSSymbol) Source #

extract_module :: RelScheme -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

StaticAnalysis CASL CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol Source # 

Methods

basic_analysis :: CASL -> Maybe ((CASLBasicSpec, CASLSign, GlobalAnnos) -> Result (CASLBasicSpec, ExtSign CASLSign Symbol, [Named CASLFORMULA])) Source #

sen_analysis :: CASL -> Maybe ((CASLBasicSpec, CASLSign, CASLFORMULA) -> Result CASLFORMULA) Source #

extBasicAnalysis :: CASL -> IRI -> LibName -> CASLBasicSpec -> CASLSign -> GlobalAnnos -> Result (CASLBasicSpec, ExtSign CASLSign Symbol, [Named CASLFORMULA]) Source #

stat_symb_map_items :: CASL -> CASLSign -> Maybe CASLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: CASL -> CASLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: CASL -> Maybe ((CASLSign, [Named CASLFORMULA]) -> CASLBasicSpec) Source #

ensures_amalgamability :: CASL -> ([CASLAmalgOpt], Gr CASLSign (Int, CASLMor), [(Int, CASLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CASL -> CASLMor -> [Named CASLFORMULA] -> Result (CASLSign, [Named CASLFORMULA]) Source #

signature_colimit :: CASL -> Gr CASLSign (Int, CASLMor) -> Result (CASLSign, Map Int CASLMor) Source #

qualify :: CASL -> SIMPLE_ID -> LibName -> CASLMor -> CASLSign -> Result (CASLMor, [Named CASLFORMULA]) Source #

symbol_to_raw :: CASL -> Symbol -> RawSymbol Source #

id_to_raw :: CASL -> Id -> RawSymbol Source #

matches :: CASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: CASL -> CASLSign Source #

add_symb_to_sign :: CASL -> CASLSign -> Symbol -> Result CASLSign Source #

signature_union :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source #

signatureDiff :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source #

intersection :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source #

final_union :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source #

morphism_union :: CASL -> CASLMor -> CASLMor -> Result CASLMor Source #

is_subsig :: CASL -> CASLSign -> CASLSign -> Bool Source #

subsig_inclusion :: CASL -> CASLSign -> CASLSign -> Result CASLMor Source #

generated_sign :: CASL -> Set Symbol -> CASLSign -> Result CASLMor Source #

cogenerated_sign :: CASL -> Set Symbol -> CASLSign -> Result CASLMor Source #

induced_from_morphism :: CASL -> EndoMap RawSymbol -> CASLSign -> Result CASLMor Source #

induced_from_to_morphism :: CASL -> EndoMap RawSymbol -> ExtSign CASLSign Symbol -> ExtSign CASLSign Symbol -> Result CASLMor Source #

is_transportable :: CASL -> CASLMor -> Bool Source #

is_injective :: CASL -> CASLMor -> Bool Source #

theory_to_taxonomy :: CASL -> TaxoGraphKind -> MMiSSOntology -> CASLSign -> [Named CASLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: CASL -> String -> Bool -> CASLSign -> CASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CASLSign, [Named CASLFORMULA], CASLSign, CASLSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CASL -> CASLSign -> CASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CASLSign, CASLSign, CASLSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CASL -> [IRI] -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

StaticAnalysis CASL_DL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol Source # 

Methods

basic_analysis :: CASL_DL -> Maybe ((DL_BASIC_SPEC, DLSign, GlobalAnnos) -> Result (DL_BASIC_SPEC, ExtSign DLSign Symbol, [Named DLFORMULA])) Source #

sen_analysis :: CASL_DL -> Maybe ((DL_BASIC_SPEC, DLSign, DLFORMULA) -> Result DLFORMULA) Source #

extBasicAnalysis :: CASL_DL -> IRI -> LibName -> DL_BASIC_SPEC -> DLSign -> GlobalAnnos -> Result (DL_BASIC_SPEC, ExtSign DLSign Symbol, [Named DLFORMULA]) Source #

stat_symb_map_items :: CASL_DL -> DLSign -> Maybe DLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: CASL_DL -> DLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: CASL_DL -> Maybe ((DLSign, [Named DLFORMULA]) -> DL_BASIC_SPEC) Source #

ensures_amalgamability :: CASL_DL -> ([CASLAmalgOpt], Gr DLSign (Int, DLMor), [(Int, DLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CASL_DL -> DLMor -> [Named DLFORMULA] -> Result (DLSign, [Named DLFORMULA]) Source #

signature_colimit :: CASL_DL -> Gr DLSign (Int, DLMor) -> Result (DLSign, Map Int DLMor) Source #

qualify :: CASL_DL -> SIMPLE_ID -> LibName -> DLMor -> DLSign -> Result (DLMor, [Named DLFORMULA]) Source #

symbol_to_raw :: CASL_DL -> Symbol -> RawSymbol Source #

id_to_raw :: CASL_DL -> Id -> RawSymbol Source #

matches :: CASL_DL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: CASL_DL -> DLSign Source #

add_symb_to_sign :: CASL_DL -> DLSign -> Symbol -> Result DLSign Source #

signature_union :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source #

signatureDiff :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source #

intersection :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source #

final_union :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source #

morphism_union :: CASL_DL -> DLMor -> DLMor -> Result DLMor Source #

is_subsig :: CASL_DL -> DLSign -> DLSign -> Bool Source #

subsig_inclusion :: CASL_DL -> DLSign -> DLSign -> Result DLMor Source #

generated_sign :: CASL_DL -> Set Symbol -> DLSign -> Result DLMor Source #

cogenerated_sign :: CASL_DL -> Set Symbol -> DLSign -> Result DLMor Source #

induced_from_morphism :: CASL_DL -> EndoMap RawSymbol -> DLSign -> Result DLMor Source #

induced_from_to_morphism :: CASL_DL -> EndoMap RawSymbol -> ExtSign DLSign Symbol -> ExtSign DLSign Symbol -> Result DLMor Source #

is_transportable :: CASL_DL -> DLMor -> Bool Source #

is_injective :: CASL_DL -> DLMor -> Bool Source #

theory_to_taxonomy :: CASL_DL -> TaxoGraphKind -> MMiSSOntology -> DLSign -> [Named DLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: CASL_DL -> String -> Bool -> DLSign -> DLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (DLSign, [Named DLFORMULA], DLSign, DLSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CASL_DL -> DLSign -> DLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (DLSign, DLSign, DLSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CASL_DL -> [IRI] -> (DLSign, [Named DLFORMULA]) -> Result (DLSign, [Named DLFORMULA]) Source #

StaticAnalysis COL C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol Source # 

Methods

basic_analysis :: COL -> Maybe ((C_BASIC_SPEC, CSign, GlobalAnnos) -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA])) Source #

sen_analysis :: COL -> Maybe ((C_BASIC_SPEC, CSign, COLFORMULA) -> Result COLFORMULA) Source #

extBasicAnalysis :: COL -> IRI -> LibName -> C_BASIC_SPEC -> CSign -> GlobalAnnos -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA]) Source #

stat_symb_map_items :: COL -> CSign -> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: COL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: COL -> Maybe ((CSign, [Named COLFORMULA]) -> C_BASIC_SPEC) Source #

ensures_amalgamability :: COL -> ([CASLAmalgOpt], Gr CSign (Int, COLMor), [(Int, COLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: COL -> COLMor -> [Named COLFORMULA] -> Result (CSign, [Named COLFORMULA]) Source #

signature_colimit :: COL -> Gr CSign (Int, COLMor) -> Result (CSign, Map Int COLMor) Source #

qualify :: COL -> SIMPLE_ID -> LibName -> COLMor -> CSign -> Result (COLMor, [Named COLFORMULA]) Source #

symbol_to_raw :: COL -> Symbol -> RawSymbol Source #

id_to_raw :: COL -> Id -> RawSymbol Source #

matches :: COL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: COL -> CSign Source #

add_symb_to_sign :: COL -> CSign -> Symbol -> Result CSign Source #

signature_union :: COL -> CSign -> CSign -> Result CSign Source #

signatureDiff :: COL -> CSign -> CSign -> Result CSign Source #

intersection :: COL -> CSign -> CSign -> Result CSign Source #

final_union :: COL -> CSign -> CSign -> Result CSign Source #

morphism_union :: COL -> COLMor -> COLMor -> Result COLMor Source #

is_subsig :: COL -> CSign -> CSign -> Bool Source #

subsig_inclusion :: COL -> CSign -> CSign -> Result COLMor Source #

generated_sign :: COL -> Set Symbol -> CSign -> Result COLMor Source #

cogenerated_sign :: COL -> Set Symbol -> CSign -> Result COLMor Source #

induced_from_morphism :: COL -> EndoMap RawSymbol -> CSign -> Result COLMor Source #

induced_from_to_morphism :: COL -> EndoMap RawSymbol -> ExtSign CSign Symbol -> ExtSign CSign Symbol -> Result COLMor Source #

is_transportable :: COL -> COLMor -> Bool Source #

is_injective :: COL -> COLMor -> Bool Source #

theory_to_taxonomy :: COL -> TaxoGraphKind -> MMiSSOntology -> CSign -> [Named COLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: COL -> String -> Bool -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CSign, [Named COLFORMULA], CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: COL -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CSign, CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: COL -> [IRI] -> (CSign, [Named COLFORMULA]) -> Result (CSign, [Named COLFORMULA]) Source #

StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol Source # 

Methods

basic_analysis :: CoCASL -> Maybe ((C_BASIC_SPEC, CSign, GlobalAnnos) -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named CoCASLFORMULA])) Source #

sen_analysis :: CoCASL -> Maybe ((C_BASIC_SPEC, CSign, CoCASLFORMULA) -> Result CoCASLFORMULA) Source #

extBasicAnalysis :: CoCASL -> IRI -> LibName -> C_BASIC_SPEC -> CSign -> GlobalAnnos -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named CoCASLFORMULA]) Source #

stat_symb_map_items :: CoCASL -> CSign -> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: CoCASL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: CoCASL -> Maybe ((CSign, [Named CoCASLFORMULA]) -> C_BASIC_SPEC) Source #

ensures_amalgamability :: CoCASL -> ([CASLAmalgOpt], Gr CSign (Int, CoCASLMor), [(Int, CoCASLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CoCASL -> CoCASLMor -> [Named CoCASLFORMULA] -> Result (CSign, [Named CoCASLFORMULA]) Source #

signature_colimit :: CoCASL -> Gr CSign (Int, CoCASLMor) -> Result (CSign, Map Int CoCASLMor) Source #

qualify :: CoCASL -> SIMPLE_ID -> LibName -> CoCASLMor -> CSign -> Result (CoCASLMor, [Named CoCASLFORMULA]) Source #

symbol_to_raw :: CoCASL -> Symbol -> RawSymbol Source #

id_to_raw :: CoCASL -> Id -> RawSymbol Source #

matches :: CoCASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: CoCASL -> CSign Source #

add_symb_to_sign :: CoCASL -> CSign -> Symbol -> Result CSign Source #

signature_union :: CoCASL -> CSign -> CSign -> Result CSign Source #

signatureDiff :: CoCASL -> CSign -> CSign -> Result CSign Source #

intersection :: CoCASL -> CSign -> CSign -> Result CSign Source #

final_union :: CoCASL -> CSign -> CSign -> Result CSign Source #

morphism_union :: CoCASL -> CoCASLMor -> CoCASLMor -> Result CoCASLMor Source #

is_subsig :: CoCASL -> CSign -> CSign -> Bool Source #

subsig_inclusion :: CoCASL -> CSign -> CSign -> Result CoCASLMor Source #

generated_sign :: CoCASL -> Set Symbol -> CSign -> Result CoCASLMor Source #

cogenerated_sign :: CoCASL -> Set Symbol -> CSign -> Result CoCASLMor Source #

induced_from_morphism :: CoCASL -> EndoMap RawSymbol -> CSign -> Result CoCASLMor Source #

induced_from_to_morphism :: CoCASL -> EndoMap RawSymbol -> ExtSign CSign Symbol -> ExtSign CSign Symbol -> Result CoCASLMor Source #

is_transportable :: CoCASL -> CoCASLMor -> Bool Source #

is_injective :: CoCASL -> CoCASLMor -> Bool Source #

theory_to_taxonomy :: CoCASL -> TaxoGraphKind -> MMiSSOntology -> CSign -> [Named CoCASLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: CoCASL -> String -> Bool -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CSign, [Named CoCASLFORMULA], CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CoCASL -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CSign, CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CoCASL -> [IRI] -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source #

StaticAnalysis ConstraintCASL ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol Source # 

Methods

basic_analysis :: ConstraintCASL -> Maybe ((ConstraintCASLBasicSpec, ConstraintCASLSign, GlobalAnnos) -> Result (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol, [Named ConstraintCASLFORMULA])) Source #

sen_analysis :: ConstraintCASL -> Maybe ((ConstraintCASLBasicSpec, ConstraintCASLSign, ConstraintCASLFORMULA) -> Result ConstraintCASLFORMULA) Source #

extBasicAnalysis :: ConstraintCASL -> IRI -> LibName -> ConstraintCASLBasicSpec -> ConstraintCASLSign -> GlobalAnnos -> Result (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol, [Named ConstraintCASLFORMULA]) Source #

stat_symb_map_items :: ConstraintCASL -> ConstraintCASLSign -> Maybe ConstraintCASLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: ConstraintCASL -> ConstraintCASLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: ConstraintCASL -> Maybe ((ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> ConstraintCASLBasicSpec) Source #

ensures_amalgamability :: ConstraintCASL -> ([CASLAmalgOpt], Gr ConstraintCASLSign (Int, ConstraintCASLMor), [(Int, ConstraintCASLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: ConstraintCASL -> ConstraintCASLMor -> [Named ConstraintCASLFORMULA] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #

signature_colimit :: ConstraintCASL -> Gr ConstraintCASLSign (Int, ConstraintCASLMor) -> Result (ConstraintCASLSign, Map Int ConstraintCASLMor) Source #

qualify :: ConstraintCASL -> SIMPLE_ID -> LibName -> ConstraintCASLMor -> ConstraintCASLSign -> Result (ConstraintCASLMor, [Named ConstraintCASLFORMULA]) Source #

symbol_to_raw :: ConstraintCASL -> Symbol -> RawSymbol Source #

id_to_raw :: ConstraintCASL -> Id -> RawSymbol Source #

matches :: ConstraintCASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: ConstraintCASL -> ConstraintCASLSign Source #

add_symb_to_sign :: ConstraintCASL -> ConstraintCASLSign -> Symbol -> Result ConstraintCASLSign Source #

signature_union :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source #

signatureDiff :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source #

intersection :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source #

final_union :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source #

morphism_union :: ConstraintCASL -> ConstraintCASLMor -> ConstraintCASLMor -> Result ConstraintCASLMor Source #

is_subsig :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Bool Source #

subsig_inclusion :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLMor Source #

generated_sign :: ConstraintCASL -> Set Symbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source #

cogenerated_sign :: ConstraintCASL -> Set Symbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source #

induced_from_morphism :: ConstraintCASL -> EndoMap RawSymbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source #

induced_from_to_morphism :: ConstraintCASL -> EndoMap RawSymbol -> ExtSign ConstraintCASLSign Symbol -> ExtSign ConstraintCASLSign Symbol -> Result ConstraintCASLMor Source #

is_transportable :: ConstraintCASL -> ConstraintCASLMor -> Bool Source #

is_injective :: ConstraintCASL -> ConstraintCASLMor -> Bool Source #

theory_to_taxonomy :: ConstraintCASL -> TaxoGraphKind -> MMiSSOntology -> ConstraintCASLSign -> [Named ConstraintCASLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: ConstraintCASL -> String -> Bool -> ConstraintCASLSign -> ConstraintCASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA], ConstraintCASLSign, ConstraintCASLSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (ConstraintCASLSign, ConstraintCASLSign, ConstraintCASLSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: ConstraintCASL -> [IRI] -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #

StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol Source # 

Methods

basic_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, GlobalAnnos) -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA])) Source #

sen_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, ExtModalFORMULA) -> Result ExtModalFORMULA) Source #

extBasicAnalysis :: ExtModal -> IRI -> LibName -> EM_BASIC_SPEC -> ExtModalSign -> GlobalAnnos -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA]) Source #

stat_symb_map_items :: ExtModal -> ExtModalSign -> Maybe ExtModalSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: ExtModal -> ExtModalSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: ExtModal -> Maybe ((ExtModalSign, [Named ExtModalFORMULA]) -> EM_BASIC_SPEC) Source #

ensures_amalgamability :: ExtModal -> ([CASLAmalgOpt], Gr ExtModalSign (Int, ExtModalMorph), [(Int, ExtModalMorph)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: ExtModal -> ExtModalMorph -> [Named ExtModalFORMULA] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

signature_colimit :: ExtModal -> Gr ExtModalSign (Int, ExtModalMorph) -> Result (ExtModalSign, Map Int ExtModalMorph) Source #

qualify :: ExtModal -> SIMPLE_ID -> LibName -> ExtModalMorph -> ExtModalSign -> Result (ExtModalMorph, [Named ExtModalFORMULA]) Source #

symbol_to_raw :: ExtModal -> Symbol -> RawSymbol Source #

id_to_raw :: ExtModal -> Id -> RawSymbol Source #

matches :: ExtModal -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: ExtModal -> ExtModalSign Source #

add_symb_to_sign :: ExtModal -> ExtModalSign -> Symbol -> Result ExtModalSign Source #

signature_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

signatureDiff :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

intersection :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

final_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

morphism_union :: ExtModal -> ExtModalMorph -> ExtModalMorph -> Result ExtModalMorph Source #

is_subsig :: ExtModal -> ExtModalSign -> ExtModalSign -> Bool Source #

subsig_inclusion :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalMorph Source #

generated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source #

cogenerated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source #

induced_from_morphism :: ExtModal -> EndoMap RawSymbol -> ExtModalSign -> Result ExtModalMorph Source #

induced_from_to_morphism :: ExtModal -> EndoMap RawSymbol -> ExtSign ExtModalSign Symbol -> ExtSign ExtModalSign Symbol -> Result ExtModalMorph Source #

is_transportable :: ExtModal -> ExtModalMorph -> Bool Source #

is_injective :: ExtModal -> ExtModalMorph -> Bool Source #

theory_to_taxonomy :: ExtModal -> TaxoGraphKind -> MMiSSOntology -> ExtModalSign -> [Named ExtModalFORMULA] -> Result MMiSSOntology Source #

corresp2th :: ExtModal -> String -> Bool -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (ExtModalSign, [Named ExtModalFORMULA], ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: ExtModal -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (ExtModalSign, ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: ExtModal -> [IRI] -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

StaticAnalysis Fpl FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol Source # 

Methods

basic_analysis :: Fpl -> Maybe ((FplBasicSpec, FplSign, GlobalAnnos) -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])) Source #

sen_analysis :: Fpl -> Maybe ((FplBasicSpec, FplSign, FplForm) -> Result FplForm) Source #

extBasicAnalysis :: Fpl -> IRI -> LibName -> FplBasicSpec -> FplSign -> GlobalAnnos -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm]) Source #

stat_symb_map_items :: Fpl -> FplSign -> Maybe FplSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Fpl -> FplSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: Fpl -> Maybe ((FplSign, [Named FplForm]) -> FplBasicSpec) Source #

ensures_amalgamability :: Fpl -> ([CASLAmalgOpt], Gr FplSign (Int, FplMor), [(Int, FplMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Fpl -> FplMor -> [Named FplForm] -> Result (FplSign, [Named FplForm]) Source #

signature_colimit :: Fpl -> Gr FplSign (Int, FplMor) -> Result (FplSign, Map Int FplMor) Source #

qualify :: Fpl -> SIMPLE_ID -> LibName -> FplMor -> FplSign -> Result (FplMor, [Named FplForm]) Source #

symbol_to_raw :: Fpl -> Symbol -> RawSymbol Source #

id_to_raw :: Fpl -> Id -> RawSymbol Source #

matches :: Fpl -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: Fpl -> FplSign Source #

add_symb_to_sign :: Fpl -> FplSign -> Symbol -> Result FplSign Source #

signature_union :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

signatureDiff :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

intersection :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

final_union :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

morphism_union :: Fpl -> FplMor -> FplMor -> Result FplMor Source #

is_subsig :: Fpl -> FplSign -> FplSign -> Bool Source #

subsig_inclusion :: Fpl -> FplSign -> FplSign -> Result FplMor Source #

generated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor Source #

cogenerated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor Source #

induced_from_morphism :: Fpl -> EndoMap RawSymbol -> FplSign -> Result FplMor Source #

induced_from_to_morphism :: Fpl -> EndoMap RawSymbol -> ExtSign FplSign Symbol -> ExtSign FplSign Symbol -> Result FplMor Source #

is_transportable :: Fpl -> FplMor -> Bool Source #

is_injective :: Fpl -> FplMor -> Bool Source #

theory_to_taxonomy :: Fpl -> TaxoGraphKind -> MMiSSOntology -> FplSign -> [Named FplForm] -> Result MMiSSOntology Source #

corresp2th :: Fpl -> String -> Bool -> FplSign -> FplSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (FplSign, [Named FplForm], FplSign, FplSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Fpl -> FplSign -> FplSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (FplSign, FplSign, FplSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Fpl -> [IRI] -> (FplSign, [Named FplForm]) -> Result (FplSign, [Named FplForm]) Source #

StaticAnalysis Hybrid H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol Source # 

Methods

basic_analysis :: Hybrid -> Maybe ((H_BASIC_SPEC, HSign, GlobalAnnos) -> Result (H_BASIC_SPEC, ExtSign HSign Symbol, [Named HybridFORMULA])) Source #

sen_analysis :: Hybrid -> Maybe ((H_BASIC_SPEC, HSign, HybridFORMULA) -> Result HybridFORMULA) Source #

extBasicAnalysis :: Hybrid -> IRI -> LibName -> H_BASIC_SPEC -> HSign -> GlobalAnnos -> Result (H_BASIC_SPEC, ExtSign HSign Symbol, [Named HybridFORMULA]) Source #

stat_symb_map_items :: Hybrid -> HSign -> Maybe HSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Hybrid -> HSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: Hybrid -> Maybe ((HSign, [Named HybridFORMULA]) -> H_BASIC_SPEC) Source #

ensures_amalgamability :: Hybrid -> ([CASLAmalgOpt], Gr HSign (Int, HybridMor), [(Int, HybridMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Hybrid -> HybridMor -> [Named HybridFORMULA] -> Result (HSign, [Named HybridFORMULA]) Source #

signature_colimit :: Hybrid -> Gr HSign (Int, HybridMor) -> Result (HSign, Map Int HybridMor) Source #

qualify :: Hybrid -> SIMPLE_ID -> LibName -> HybridMor -> HSign -> Result (HybridMor, [Named HybridFORMULA]) Source #

symbol_to_raw :: Hybrid -> Symbol -> RawSymbol Source #

id_to_raw :: Hybrid -> Id -> RawSymbol Source #

matches :: Hybrid -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: Hybrid -> HSign Source #

add_symb_to_sign :: Hybrid -> HSign -> Symbol -> Result HSign Source #

signature_union :: Hybrid -> HSign -> HSign -> Result HSign Source #

signatureDiff :: Hybrid -> HSign -> HSign -> Result HSign Source #

intersection :: Hybrid -> HSign -> HSign -> Result HSign Source #

final_union :: Hybrid -> HSign -> HSign -> Result HSign Source #

morphism_union :: Hybrid -> HybridMor -> HybridMor -> Result HybridMor Source #

is_subsig :: Hybrid -> HSign -> HSign -> Bool Source #

subsig_inclusion :: Hybrid -> HSign -> HSign -> Result HybridMor Source #

generated_sign :: Hybrid -> Set Symbol -> HSign -> Result HybridMor Source #

cogenerated_sign :: Hybrid -> Set Symbol -> HSign -> Result HybridMor Source #

induced_from_morphism :: Hybrid -> EndoMap RawSymbol -> HSign -> Result HybridMor Source #

induced_from_to_morphism :: Hybrid -> EndoMap RawSymbol -> ExtSign HSign Symbol -> ExtSign HSign Symbol -> Result HybridMor Source #

is_transportable :: Hybrid -> HybridMor -> Bool Source #

is_injective :: Hybrid -> HybridMor -> Bool Source #

theory_to_taxonomy :: Hybrid -> TaxoGraphKind -> MMiSSOntology -> HSign -> [Named HybridFORMULA] -> Result MMiSSOntology Source #

corresp2th :: Hybrid -> String -> Bool -> HSign -> HSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (HSign, [Named HybridFORMULA], HSign, HSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Hybrid -> HSign -> HSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (HSign, HSign, HSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Hybrid -> [IRI] -> (HSign, [Named HybridFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source #

StaticAnalysis Modal M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol Source # 

Methods

basic_analysis :: Modal -> Maybe ((M_BASIC_SPEC, MSign, GlobalAnnos) -> Result (M_BASIC_SPEC, ExtSign MSign Symbol, [Named ModalFORMULA])) Source #

sen_analysis :: Modal -> Maybe ((M_BASIC_SPEC, MSign, ModalFORMULA) -> Result ModalFORMULA) Source #

extBasicAnalysis :: Modal -> IRI -> LibName -> M_BASIC_SPEC -> MSign -> GlobalAnnos -> Result (M_BASIC_SPEC, ExtSign MSign Symbol, [Named ModalFORMULA]) Source #

stat_symb_map_items :: Modal -> MSign -> Maybe MSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Modal -> MSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: Modal -> Maybe ((MSign, [Named ModalFORMULA]) -> M_BASIC_SPEC) Source #

ensures_amalgamability :: Modal -> ([CASLAmalgOpt], Gr MSign (Int, ModalMor), [(Int, ModalMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Modal -> ModalMor -> [Named ModalFORMULA] -> Result (MSign, [Named ModalFORMULA]) Source #

signature_colimit :: Modal -> Gr MSign (Int, ModalMor) -> Result (MSign, Map Int ModalMor) Source #

qualify :: Modal -> SIMPLE_ID -> LibName -> ModalMor -> MSign -> Result (ModalMor, [Named ModalFORMULA]) Source #

symbol_to_raw :: Modal -> Symbol -> RawSymbol Source #

id_to_raw :: Modal -> Id -> RawSymbol Source #

matches :: Modal -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: Modal -> MSign Source #

add_symb_to_sign :: Modal -> MSign -> Symbol -> Result MSign Source #

signature_union :: Modal -> MSign -> MSign -> Result MSign Source #

signatureDiff :: Modal -> MSign -> MSign -> Result MSign Source #

intersection :: Modal -> MSign -> MSign -> Result MSign Source #

final_union :: Modal -> MSign -> MSign -> Result MSign Source #

morphism_union :: Modal -> ModalMor -> ModalMor -> Result ModalMor Source #

is_subsig :: Modal -> MSign -> MSign -> Bool Source #

subsig_inclusion :: Modal -> MSign -> MSign -> Result ModalMor Source #

generated_sign :: Modal -> Set Symbol -> MSign -> Result ModalMor Source #

cogenerated_sign :: Modal -> Set Symbol -> MSign -> Result ModalMor Source #

induced_from_morphism :: Modal -> EndoMap RawSymbol -> MSign -> Result ModalMor Source #

induced_from_to_morphism :: Modal -> EndoMap RawSymbol -> ExtSign MSign Symbol -> ExtSign MSign Symbol -> Result ModalMor Source #

is_transportable :: Modal -> ModalMor -> Bool Source #

is_injective :: Modal -> ModalMor -> Bool Source #

theory_to_taxonomy :: Modal -> TaxoGraphKind -> MMiSSOntology -> MSign -> [Named ModalFORMULA] -> Result MMiSSOntology Source #

corresp2th :: Modal -> String -> Bool -> MSign -> MSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (MSign, [Named ModalFORMULA], MSign, MSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Modal -> MSign -> MSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (MSign, MSign, MSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Modal -> [IRI] -> (MSign, [Named ModalFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source #

StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source # 

Methods

basic_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, GlobalAnnos) -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])) Source #

sen_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: VSE -> IRI -> LibName -> VSEBasicSpec -> VSESign -> GlobalAnnos -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: VSE -> VSESign -> Maybe VSESign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: VSE -> VSESign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: VSE -> Maybe ((VSESign, [Named Sentence]) -> VSEBasicSpec) Source #

ensures_amalgamability :: VSE -> ([CASLAmalgOpt], Gr VSESign (Int, VSEMor), [(Int, VSEMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: VSE -> VSEMor -> [Named Sentence] -> Result (VSESign, [Named Sentence]) Source #

signature_colimit :: VSE -> Gr VSESign (Int, VSEMor) -> Result (VSESign, Map Int VSEMor) Source #

qualify :: VSE -> SIMPLE_ID -> LibName -> VSEMor -> VSESign -> Result (VSEMor, [Named Sentence]) Source #

symbol_to_raw :: VSE -> Symbol -> RawSymbol Source #

id_to_raw :: VSE -> Id -> RawSymbol Source #

matches :: VSE -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: VSE -> VSESign Source #

add_symb_to_sign :: VSE -> VSESign -> Symbol -> Result VSESign Source #

signature_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

signatureDiff :: VSE -> VSESign -> VSESign -> Result VSESign Source #

intersection :: VSE -> VSESign -> VSESign -> Result VSESign Source #

final_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

morphism_union :: VSE -> VSEMor -> VSEMor -> Result VSEMor Source #

is_subsig :: VSE -> VSESign -> VSESign -> Bool Source #

subsig_inclusion :: VSE -> VSESign -> VSESign -> Result VSEMor Source #

generated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

cogenerated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

induced_from_morphism :: VSE -> EndoMap RawSymbol -> VSESign -> Result VSEMor Source #

induced_from_to_morphism :: VSE -> EndoMap RawSymbol -> ExtSign VSESign Symbol -> ExtSign VSESign Symbol -> Result VSEMor Source #

is_transportable :: VSE -> VSEMor -> Bool Source #

is_injective :: VSE -> VSEMor -> Bool Source #

theory_to_taxonomy :: VSE -> TaxoGraphKind -> MMiSSOntology -> VSESign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: VSE -> String -> Bool -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (VSESign, [Named Sentence], VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: VSE -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (VSESign, VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: VSE -> [IRI] -> (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence]) Source #

StaticAnalysis THF BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () Source # 

Methods

basic_analysis :: THF -> Maybe ((BasicSpecTHF, SignTHF, GlobalAnnos) -> Result (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])) Source #

sen_analysis :: THF -> Maybe ((BasicSpecTHF, SignTHF, THFFormula) -> Result THFFormula) Source #

extBasicAnalysis :: THF -> IRI -> LibName -> BasicSpecTHF -> SignTHF -> GlobalAnnos -> Result (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula]) Source #

stat_symb_map_items :: THF -> SignTHF -> Maybe SignTHF -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: THF -> SignTHF -> [()] -> Result [()] Source #

convertTheory :: THF -> Maybe ((SignTHF, [Named THFFormula]) -> BasicSpecTHF) Source #

ensures_amalgamability :: THF -> ([CASLAmalgOpt], Gr SignTHF (Int, MorphismTHF), [(Int, MorphismTHF)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: THF -> MorphismTHF -> [Named THFFormula] -> Result (SignTHF, [Named THFFormula]) Source #

signature_colimit :: THF -> Gr SignTHF (Int, MorphismTHF) -> Result (SignTHF, Map Int MorphismTHF) Source #

qualify :: THF -> SIMPLE_ID -> LibName -> MorphismTHF -> SignTHF -> Result (MorphismTHF, [Named THFFormula]) Source #

symbol_to_raw :: THF -> SymbolTHF -> () Source #

id_to_raw :: THF -> Id -> () Source #

matches :: THF -> SymbolTHF -> () -> Bool Source #

empty_signature :: THF -> SignTHF Source #

add_symb_to_sign :: THF -> SignTHF -> SymbolTHF -> Result SignTHF Source #

signature_union :: THF -> SignTHF -> SignTHF -> Result SignTHF Source #

signatureDiff :: THF -> SignTHF -> SignTHF -> Result SignTHF Source #

intersection :: THF -> SignTHF -> SignTHF -> Result SignTHF Source #

final_union :: THF -> SignTHF -> SignTHF -> Result SignTHF Source #

morphism_union :: THF -> MorphismTHF -> MorphismTHF -> Result MorphismTHF Source #

is_subsig :: THF -> SignTHF -> SignTHF -> Bool Source #

subsig_inclusion :: THF -> SignTHF -> SignTHF -> Result MorphismTHF Source #

generated_sign :: THF -> Set SymbolTHF -> SignTHF -> Result MorphismTHF Source #

cogenerated_sign :: THF -> Set SymbolTHF -> SignTHF -> Result MorphismTHF Source #

induced_from_morphism :: THF -> EndoMap () -> SignTHF -> Result MorphismTHF Source #

induced_from_to_morphism :: THF -> EndoMap () -> ExtSign SignTHF SymbolTHF -> ExtSign SignTHF SymbolTHF -> Result MorphismTHF Source #

is_transportable :: THF -> MorphismTHF -> Bool Source #

is_injective :: THF -> MorphismTHF -> Bool Source #

theory_to_taxonomy :: THF -> TaxoGraphKind -> MMiSSOntology -> SignTHF -> [Named THFFormula] -> Result MMiSSOntology Source #

corresp2th :: THF -> String -> Bool -> SignTHF -> SignTHF -> [()] -> [()] -> EndoMap SymbolTHF -> EndoMap SymbolTHF -> REL_REF -> Result (SignTHF, [Named THFFormula], SignTHF, SignTHF, EndoMap SymbolTHF, EndoMap SymbolTHF) Source #

equiv2cospan :: THF -> SignTHF -> SignTHF -> [()] -> [()] -> Result (SignTHF, SignTHF, SignTHF, EndoMap SymbolTHF, EndoMap SymbolTHF) Source #

extract_module :: THF -> [IRI] -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #

StaticAnalysis OWL2 OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb Source # 

Methods

basic_analysis :: OWL2 -> Maybe ((OntologyDocument, Sign, GlobalAnnos) -> Result (OntologyDocument, ExtSign Sign Entity, [Named Axiom])) Source #

sen_analysis :: OWL2 -> Maybe ((OntologyDocument, Sign, Axiom) -> Result Axiom) Source #

extBasicAnalysis :: OWL2 -> IRI -> LibName -> OntologyDocument -> Sign -> GlobalAnnos -> Result (OntologyDocument, ExtSign Sign Entity, [Named Axiom]) Source #

stat_symb_map_items :: OWL2 -> Sign -> Maybe Sign -> [SymbMapItems] -> Result (EndoMap RawSymb) Source #

stat_symb_items :: OWL2 -> Sign -> [SymbItems] -> Result [RawSymb] Source #

convertTheory :: OWL2 -> Maybe ((Sign, [Named Axiom]) -> OntologyDocument) Source #

ensures_amalgamability :: OWL2 -> ([CASLAmalgOpt], Gr Sign (Int, OWLMorphism), [(Int, OWLMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: OWL2 -> OWLMorphism -> [Named Axiom] -> Result (Sign, [Named Axiom]) Source #

signature_colimit :: OWL2 -> Gr Sign (Int, OWLMorphism) -> Result (Sign, Map Int OWLMorphism) Source #

qualify :: OWL2 -> SIMPLE_ID -> LibName -> OWLMorphism -> Sign -> Result (OWLMorphism, [Named Axiom]) Source #

symbol_to_raw :: OWL2 -> Entity -> RawSymb Source #

id_to_raw :: OWL2 -> Id -> RawSymb Source #

matches :: OWL2 -> Entity -> RawSymb -> Bool Source #

empty_signature :: OWL2 -> Sign Source #

add_symb_to_sign :: OWL2 -> Sign -> Entity -> Result Sign Source #

signature_union :: OWL2 -> Sign -> Sign -> Result Sign Source #

signatureDiff :: OWL2 -> Sign -> Sign -> Result Sign Source #

intersection :: OWL2 -> Sign -> Sign -> Result Sign Source #

final_union :: OWL2 -> Sign -> Sign -> Result Sign Source #

morphism_union :: OWL2 -> OWLMorphism -> OWLMorphism -> Result OWLMorphism Source #

is_subsig :: OWL2 -> Sign -> Sign -> Bool Source #

subsig_inclusion :: OWL2 -> Sign -> Sign -> Result OWLMorphism Source #

generated_sign :: OWL2 -> Set Entity -> Sign -> Result OWLMorphism Source #

cogenerated_sign :: OWL2 -> Set Entity -> Sign -> Result OWLMorphism Source #

induced_from_morphism :: OWL2 -> EndoMap RawSymb -> Sign -> Result OWLMorphism Source #

induced_from_to_morphism :: OWL2 -> EndoMap RawSymb -> ExtSign Sign Entity -> ExtSign Sign Entity -> Result OWLMorphism Source #

is_transportable :: OWL2 -> OWLMorphism -> Bool Source #

is_injective :: OWL2 -> OWLMorphism -> Bool Source #

theory_to_taxonomy :: OWL2 -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Axiom] -> Result MMiSSOntology Source #

corresp2th :: OWL2 -> String -> Bool -> Sign -> Sign -> [SymbItems] -> [SymbItems] -> EndoMap Entity -> EndoMap Entity -> REL_REF -> Result (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity) Source #

equiv2cospan :: OWL2 -> Sign -> Sign -> [SymbItems] -> [SymbItems] -> Result (Sign, Sign, Sign, EndoMap Entity, EndoMap Entity) Source #

extract_module :: OWL2 -> [IRI] -> (Sign, [Named Axiom]) -> Result (Sign, [Named Axiom]) Source #

StaticAnalysis Adl Context Sen () () Sign Morphism Symbol RawSymbol Source # 

Methods

basic_analysis :: Adl -> Maybe ((Context, Sign, GlobalAnnos) -> Result (Context, ExtSign Sign Symbol, [Named Sen])) Source #

sen_analysis :: Adl -> Maybe ((Context, Sign, Sen) -> Result Sen) Source #

extBasicAnalysis :: Adl -> IRI -> LibName -> Context -> Sign -> GlobalAnnos -> Result (Context, ExtSign Sign Symbol, [Named Sen]) Source #

stat_symb_map_items :: Adl -> Sign -> Maybe Sign -> [()] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Adl -> Sign -> [()] -> Result [RawSymbol] Source #

convertTheory :: Adl -> Maybe ((Sign, [Named Sen]) -> Context) Source #

ensures_amalgamability :: Adl -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Adl -> Morphism -> [Named Sen] -> Result (Sign, [Named Sen]) Source #

signature_colimit :: Adl -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: Adl -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sen]) Source #

symbol_to_raw :: Adl -> Symbol -> RawSymbol Source #

id_to_raw :: Adl -> Id -> RawSymbol Source #

matches :: Adl -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: Adl -> Sign Source #

add_symb_to_sign :: Adl -> Sign -> Symbol -> Result Sign Source #

signature_union :: Adl -> Sign -> Sign -> Result Sign Source #

signatureDiff :: Adl -> Sign -> Sign -> Result Sign Source #

intersection :: Adl -> Sign -> Sign -> Result Sign Source #

final_union :: Adl -> Sign -> Sign -> Result Sign Source #

morphism_union :: Adl -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: Adl -> Sign -> Sign -> Bool Source #

subsig_inclusion :: Adl -> Sign -> Sign -> Result Morphism Source #

generated_sign :: Adl -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: Adl -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: Adl -> EndoMap RawSymbol -> Sign -> Result Morphism Source #

induced_from_to_morphism :: Adl -> EndoMap RawSymbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: Adl -> Morphism -> Bool Source #

is_injective :: Adl -> Morphism -> Bool Source #

theory_to_taxonomy :: Adl -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sen] -> Result MMiSSOntology Source #

corresp2th :: Adl -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sen], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Adl -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Adl -> [IRI] -> (Sign, [Named Sen]) -> Result (Sign, [Named Sen]) Source #

StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source #

Static Analysis for reduce logic

Methods

basic_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])) Source #

sen_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, CMD) -> Result CMD) Source #

extBasicAnalysis :: CSL -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD]) Source #

stat_symb_map_items :: CSL -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source #

stat_symb_items :: CSL -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source #

convertTheory :: CSL -> Maybe ((Sign, [Named CMD]) -> BASIC_SPEC) Source #

ensures_amalgamability :: CSL -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CSL -> Morphism -> [Named CMD] -> Result (Sign, [Named CMD]) Source #

signature_colimit :: CSL -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: CSL -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named CMD]) Source #

symbol_to_raw :: CSL -> Symbol -> Symbol Source #

id_to_raw :: CSL -> Id -> Symbol Source #

matches :: CSL -> Symbol -> Symbol -> Bool Source #

empty_signature :: CSL -> Sign Source #

add_symb_to_sign :: CSL -> Sign -> Symbol -> Result Sign Source #

signature_union :: CSL -> Sign -> Sign -> Result Sign Source #

signatureDiff :: CSL -> Sign -> Sign -> Result Sign Source #

intersection :: CSL -> Sign -> Sign -> Result Sign Source #

final_union :: CSL -> Sign -> Sign -> Result Sign Source #

morphism_union :: CSL -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: CSL -> Sign -> Sign -> Bool Source #

subsig_inclusion :: CSL -> Sign -> Sign -> Result Morphism Source #

generated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: CSL -> EndoMap Symbol -> Sign -> Result Morphism Source #

induced_from_to_morphism :: CSL -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: CSL -> Morphism -> Bool Source #

is_injective :: CSL -> Morphism -> Bool Source #

theory_to_taxonomy :: CSL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named CMD] -> Result MMiSSOntology Source #

corresp2th :: CSL -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named CMD], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CSL -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CSL -> [IRI] -> (Sign, [Named CMD]) -> Result (Sign, [Named CMD]) Source #

StaticAnalysis CommonLogic BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source # 

Methods

basic_analysis :: CommonLogic -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META])) Source #

sen_analysis :: CommonLogic -> Maybe ((BASIC_SPEC, Sign, TEXT_META) -> Result TEXT_META) Source #

extBasicAnalysis :: CommonLogic -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META]) Source #

stat_symb_map_items :: CommonLogic -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source #

stat_symb_items :: CommonLogic -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source #

convertTheory :: CommonLogic -> Maybe ((Sign, [Named TEXT_META]) -> BASIC_SPEC) Source #

ensures_amalgamability :: CommonLogic -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CommonLogic -> Morphism -> [Named TEXT_META] -> Result (Sign, [Named TEXT_META]) Source #

signature_colimit :: CommonLogic -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: CommonLogic -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named TEXT_META]) Source #

symbol_to_raw :: CommonLogic -> Symbol -> Symbol Source #

id_to_raw :: CommonLogic -> Id -> Symbol Source #

matches :: CommonLogic -> Symbol -> Symbol -> Bool Source #

empty_signature :: CommonLogic -> Sign Source #

add_symb_to_sign :: CommonLogic -> Sign -> Symbol -> Result Sign Source #

signature_union :: CommonLogic -> Sign -> Sign -> Result Sign Source #

signatureDiff :: CommonLogic -> Sign -> Sign -> Result Sign Source #

intersection :: CommonLogic -> Sign -> Sign -> Result Sign Source #

final_union :: CommonLogic -> Sign -> Sign -> Result Sign Source #

morphism_union :: CommonLogic -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: CommonLogic -> Sign -> Sign -> Bool Source #

subsig_inclusion :: CommonLogic -> Sign -> Sign -> Result Morphism Source #

generated_sign :: CommonLogic -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: CommonLogic -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: CommonLogic -> EndoMap Symbol -> Sign -> Result Morphism Source #

induced_from_to_morphism :: CommonLogic -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: CommonLogic -> Morphism -> Bool Source #

is_injective :: CommonLogic -> Morphism -> Bool Source #

theory_to_taxonomy :: CommonLogic -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named TEXT_META] -> Result MMiSSOntology Source #

corresp2th :: CommonLogic -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named TEXT_META], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CommonLogic -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CommonLogic -> [IRI] -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source #

StaticAnalysis DFOL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source # 

Methods

basic_analysis :: DFOL -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])) Source #

sen_analysis :: DFOL -> Maybe ((BASIC_SPEC, Sign, FORMULA) -> Result FORMULA) Source #

extBasicAnalysis :: DFOL -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA]) Source #

stat_symb_map_items :: DFOL -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source #

stat_symb_items :: DFOL -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source #

convertTheory :: DFOL -> Maybe ((Sign, [Named FORMULA]) -> BASIC_SPEC) Source #

ensures_amalgamability :: DFOL -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: DFOL -> Morphism -> [Named FORMULA] -> Result (Sign, [Named FORMULA]) Source #

signature_colimit :: DFOL -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: DFOL -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named FORMULA]) Source #

symbol_to_raw :: DFOL -> Symbol -> Symbol Source #

id_to_raw :: DFOL -> Id -> Symbol Source #

matches :: DFOL -> Symbol -> Symbol -> Bool Source #

empty_signature :: DFOL -> Sign Source #

add_symb_to_sign :: DFOL -> Sign -> Symbol -> Result Sign Source #

signature_union :: DFOL -> Sign -> Sign -> Result Sign Source #

signatureDiff :: DFOL -> Sign -> Sign -> Result Sign Source #

intersection :: DFOL -> Sign -> Sign -> Result Sign Source #

final_union :: DFOL -> Sign -> Sign -> Result Sign Source #

morphism_union :: DFOL -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: DFOL -> Sign -> Sign -> Bool Source #

subsig_inclusion :: DFOL -> Sign -> Sign -> Result Morphism Source #

generated_sign :: DFOL -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: DFOL -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: DFOL -> EndoMap Symbol -> Sign -> Result Morphism Source #

induced_from_to_morphism :: DFOL -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: DFOL -> Morphism -> Bool Source #

is_injective :: DFOL -> Morphism -> Bool Source #

theory_to_taxonomy :: DFOL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named FORMULA] -> Result MMiSSOntology Source #

corresp2th :: DFOL -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: DFOL -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: DFOL -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source #

StaticAnalysis FrameworkCom ComorphismDef () () () ComorphismDef MorphismCom () () Source # 

Methods

basic_analysis :: FrameworkCom -> Maybe ((ComorphismDef, ComorphismDef, GlobalAnnos) -> Result (ComorphismDef, ExtSign ComorphismDef (), [Named ()])) Source #

sen_analysis :: FrameworkCom -> Maybe ((ComorphismDef, ComorphismDef, ()) -> Result ()) Source #

extBasicAnalysis :: FrameworkCom -> IRI -> LibName -> ComorphismDef -> ComorphismDef -> GlobalAnnos -> Result (ComorphismDef, ExtSign ComorphismDef (), [Named ()]) Source #

stat_symb_map_items :: FrameworkCom -> ComorphismDef -> Maybe ComorphismDef -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: FrameworkCom -> ComorphismDef -> [()] -> Result [()] Source #

convertTheory :: FrameworkCom -> Maybe ((ComorphismDef, [Named ()]) -> ComorphismDef) Source #

ensures_amalgamability :: FrameworkCom -> ([CASLAmalgOpt], Gr ComorphismDef (Int, MorphismCom), [(Int, MorphismCom)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: FrameworkCom -> MorphismCom -> [Named ()] -> Result (ComorphismDef, [Named ()]) Source #

signature_colimit :: FrameworkCom -> Gr ComorphismDef (Int, MorphismCom) -> Result (ComorphismDef, Map Int MorphismCom) Source #

qualify :: FrameworkCom -> SIMPLE_ID -> LibName -> MorphismCom -> ComorphismDef -> Result (MorphismCom, [Named ()]) Source #

symbol_to_raw :: FrameworkCom -> () -> () Source #

id_to_raw :: FrameworkCom -> Id -> () Source #

matches :: FrameworkCom -> () -> () -> Bool Source #

empty_signature :: FrameworkCom -> ComorphismDef Source #

add_symb_to_sign :: FrameworkCom -> ComorphismDef -> () -> Result ComorphismDef Source #

signature_union :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source #

signatureDiff :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source #

intersection :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source #

final_union :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source #

morphism_union :: FrameworkCom -> MorphismCom -> MorphismCom -> Result MorphismCom Source #

is_subsig :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Bool Source #

subsig_inclusion :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result MorphismCom Source #

generated_sign :: FrameworkCom -> Set () -> ComorphismDef -> Result MorphismCom Source #

cogenerated_sign :: FrameworkCom -> Set () -> ComorphismDef -> Result MorphismCom Source #

induced_from_morphism :: FrameworkCom -> EndoMap () -> ComorphismDef -> Result MorphismCom Source #

induced_from_to_morphism :: FrameworkCom -> EndoMap () -> ExtSign ComorphismDef () -> ExtSign ComorphismDef () -> Result MorphismCom Source #

is_transportable :: FrameworkCom -> MorphismCom -> Bool Source #

is_injective :: FrameworkCom -> MorphismCom -> Bool Source #

theory_to_taxonomy :: FrameworkCom -> TaxoGraphKind -> MMiSSOntology -> ComorphismDef -> [Named ()] -> Result MMiSSOntology Source #

corresp2th :: FrameworkCom -> String -> Bool -> ComorphismDef -> ComorphismDef -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (ComorphismDef, [Named ()], ComorphismDef, ComorphismDef, EndoMap (), EndoMap ()) Source #

equiv2cospan :: FrameworkCom -> ComorphismDef -> ComorphismDef -> [()] -> [()] -> Result (ComorphismDef, ComorphismDef, ComorphismDef, EndoMap (), EndoMap ()) Source #

extract_module :: FrameworkCom -> [IRI] -> (ComorphismDef, [Named ()]) -> Result (ComorphismDef, [Named ()]) Source #

StaticAnalysis Framework LogicDef () () () LogicDef Morphism () () Source # 

Methods

basic_analysis :: Framework -> Maybe ((LogicDef, LogicDef, GlobalAnnos) -> Result (LogicDef, ExtSign LogicDef (), [Named ()])) Source #

sen_analysis :: Framework -> Maybe ((LogicDef, LogicDef, ()) -> Result ()) Source #

extBasicAnalysis :: Framework -> IRI -> LibName -> LogicDef -> LogicDef -> GlobalAnnos -> Result (LogicDef, ExtSign LogicDef (), [Named ()]) Source #

stat_symb_map_items :: Framework -> LogicDef -> Maybe LogicDef -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: Framework -> LogicDef -> [()] -> Result [()] Source #

convertTheory :: Framework -> Maybe ((LogicDef, [Named ()]) -> LogicDef) Source #

ensures_amalgamability :: Framework -> ([CASLAmalgOpt], Gr LogicDef (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Framework -> Morphism -> [Named ()] -> Result (LogicDef, [Named ()]) Source #

signature_colimit :: Framework -> Gr LogicDef (Int, Morphism) -> Result (LogicDef, Map Int Morphism) Source #

qualify :: Framework -> SIMPLE_ID -> LibName -> Morphism -> LogicDef -> Result (Morphism, [Named ()]) Source #

symbol_to_raw :: Framework -> () -> () Source #

id_to_raw :: Framework -> Id -> () Source #

matches :: Framework -> () -> () -> Bool Source #

empty_signature :: Framework -> LogicDef Source #

add_symb_to_sign :: Framework -> LogicDef -> () -> Result LogicDef Source #

signature_union :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source #

signatureDiff :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source #

intersection :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source #

final_union :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source #

morphism_union :: Framework -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: Framework -> LogicDef -> LogicDef -> Bool Source #

subsig_inclusion :: Framework -> LogicDef -> LogicDef -> Result Morphism Source #

generated_sign :: Framework -> Set () -> LogicDef -> Result Morphism Source #

cogenerated_sign :: Framework -> Set () -> LogicDef -> Result Morphism Source #

induced_from_morphism :: Framework -> EndoMap () -> LogicDef -> Result Morphism Source #

induced_from_to_morphism :: Framework -> EndoMap () -> ExtSign LogicDef () -> ExtSign LogicDef () -> Result Morphism Source #

is_transportable :: Framework -> Morphism -> Bool Source #

is_injective :: Framework -> Morphism -> Bool Source #

theory_to_taxonomy :: Framework -> TaxoGraphKind -> MMiSSOntology -> LogicDef -> [Named ()] -> Result MMiSSOntology Source #

corresp2th :: Framework -> String -> Bool -> LogicDef -> LogicDef -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (LogicDef, [Named ()], LogicDef, LogicDef, EndoMap (), EndoMap ()) Source #

equiv2cospan :: Framework -> LogicDef -> LogicDef -> [()] -> [()] -> Result (LogicDef, LogicDef, LogicDef, EndoMap (), EndoMap ()) Source #

extract_module :: Framework -> [IRI] -> (LogicDef, [Named ()]) -> Result (LogicDef, [Named ()]) Source #

StaticAnalysis FreeCAD Document () () () Sign FCMorphism () () Source # 

Methods

basic_analysis :: FreeCAD -> Maybe ((Document, Sign, GlobalAnnos) -> Result (Document, ExtSign Sign (), [Named ()])) Source #

sen_analysis :: FreeCAD -> Maybe ((Document, Sign, ()) -> Result ()) Source #

extBasicAnalysis :: FreeCAD -> IRI -> LibName -> Document -> Sign -> GlobalAnnos -> Result (Document, ExtSign Sign (), [Named ()]) Source #

stat_symb_map_items :: FreeCAD -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: FreeCAD -> Sign -> [()] -> Result [()] Source #

convertTheory :: FreeCAD -> Maybe ((Sign, [Named ()]) -> Document) Source #

ensures_amalgamability :: FreeCAD -> ([CASLAmalgOpt], Gr Sign (Int, FCMorphism), [(Int, FCMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: FreeCAD -> FCMorphism -> [Named ()] -> Result (Sign, [Named ()]) Source #

signature_colimit :: FreeCAD -> Gr Sign (Int, FCMorphism) -> Result (Sign, Map Int FCMorphism) Source #

qualify :: FreeCAD -> SIMPLE_ID -> LibName -> FCMorphism -> Sign -> Result (FCMorphism, [Named ()]) Source #

symbol_to_raw :: FreeCAD -> () -> () Source #

id_to_raw :: FreeCAD -> Id -> () Source #

matches :: FreeCAD -> () -> () -> Bool Source #

empty_signature :: FreeCAD -> Sign Source #

add_symb_to_sign :: FreeCAD -> Sign -> () -> Result Sign Source #

signature_union :: FreeCAD -> Sign -> Sign -> Result Sign Source #

signatureDiff :: FreeCAD -> Sign -> Sign -> Result Sign Source #

intersection :: FreeCAD -> Sign -> Sign -> Result Sign Source #

final_union :: FreeCAD -> Sign -> Sign -> Result Sign Source #

morphism_union :: FreeCAD -> FCMorphism -> FCMorphism -> Result FCMorphism Source #

is_subsig :: FreeCAD -> Sign -> Sign -> Bool Source #

subsig_inclusion :: FreeCAD -> Sign -> Sign -> Result FCMorphism Source #

generated_sign :: FreeCAD -> Set () -> Sign -> Result FCMorphism Source #

cogenerated_sign :: FreeCAD -> Set () -> Sign -> Result FCMorphism Source #

induced_from_morphism :: FreeCAD -> EndoMap () -> Sign -> Result FCMorphism Source #

induced_from_to_morphism :: FreeCAD -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result FCMorphism Source #

is_transportable :: FreeCAD -> FCMorphism -> Bool Source #

is_injective :: FreeCAD -> FCMorphism -> Bool Source #

theory_to_taxonomy :: FreeCAD -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named ()] -> Result MMiSSOntology Source #

corresp2th :: FreeCAD -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named ()], Sign, Sign, EndoMap (), EndoMap ()) Source #

equiv2cospan :: FreeCAD -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source #

extract_module :: FreeCAD -> [IRI] -> (Sign, [Named ()]) -> Result (Sign, [Named ()]) Source #

StaticAnalysis HolLight () Sentence () () Sign HolLightMorphism () () Source #

Static Analysis for propositional logic