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

Instances details
Eq Stability Source # 
Instance details

Defined in Logic.Logic

Methods

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

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

Show Stability Source # 
Instance details

Defined in Logic.Logic

Methods

showsPrec :: Int -> Stability -> ShowS

show :: Stability -> String

showList :: [Stability] -> ShowS

class ShATermConvertible a => Convertible a Source #

shortcut for class constraints

Instances

Instances details
ShATermConvertible a => Convertible a Source # 
Instance details

Defined in Logic.Logic

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

shortcut for class constraints

Instances

Instances details
(Pretty a, Convertible a, ToJSON a, FromJSON a) => PrintTypeConv a Source # 
Instance details

Defined in Logic.Logic

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

shortcut for class constraints with equality

Instances

Instances details
(Eq a, PrintTypeConv a) => EqPrintTypeConv a Source # 
Instance details

Defined in Logic.Logic

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

Minimal complete definition

Nothing

Methods

language_name :: lid -> String Source #

description :: lid -> String Source #

Instances

Instances details
Language RelScheme Source # 
Instance details

Defined in RelationalScheme.Logic_Rel

Methods

language_name :: RelScheme -> String Source #

description :: RelScheme -> String Source #

Language RDF Source # 
Instance details

Defined in RDF.Logic_RDF

Methods

language_name :: RDF -> String Source #

description :: RDF -> String Source #

Language QVTR Source # 
Instance details

Defined in QVTR.Logic_QVTR

Methods

language_name :: QVTR -> String Source #

description :: QVTR -> String Source #

Language OMDoc_PUN Source # 
Instance details

Defined in OMDoc.Logic_OMDoc

Methods

language_name :: OMDoc_PUN -> String Source #

description :: OMDoc_PUN -> String Source #

Language Maude Source #

Instance of Language for Maude

Instance details

Defined in Maude.Logic_Maude

Methods

language_name :: Maude -> String Source #

description :: Maude -> String Source #

Language Grothendieck Source # 
Instance details

Defined in Logic.Grothendieck

Language THF Source # 
Instance details

Defined in THF.Logic_THF

Methods

language_name :: THF -> String Source #

description :: THF -> String Source #

Language TPTP Source # 
Instance details

Defined in TPTP.Logic_TPTP

Methods

language_name :: TPTP -> String Source #

description :: TPTP -> String Source #

Language SoftFOL Source # 
Instance details

Defined in SoftFOL.Logic_SoftFOL

Methods

language_name :: SoftFOL -> String Source #

description :: SoftFOL -> String Source #

Language QBF Source # 
Instance details

Defined in QBF.Logic_QBF

Methods

language_name :: QBF -> String Source #

description :: QBF -> String Source #

Language Propositional Source # 
Instance details

Defined in Propositional.Logic_Propositional

Language OWL2 Source # 
Instance details

Defined in OWL2.Logic_OWL2

Methods

language_name :: OWL2 -> String Source #

description :: OWL2 -> String Source #

Language Propositional2OWL2 Source # 
Instance details

Defined in OWL2.Propositional2OWL2

Language NeSyPatterns Source # 
Instance details

Defined in NeSyPatterns.Logic_NeSyPatterns

Language OWL22NeSyPatterns Source # 
Instance details

Defined in OWL2.OWL22NeSyPatterns

Language LF Source # 
Instance details

Defined in LF.Logic_LF

Methods

language_name :: LF -> String Source #

description :: LF -> String Source #

Language Isabelle Source # 
Instance details

Defined in Isabelle.Logic_Isabelle

Methods

language_name :: Isabelle -> String Source #

description :: Isabelle -> String Source #

Language HolLight Source # 
Instance details

Defined in HolLight.Logic_HolLight

Methods

language_name :: HolLight -> String Source #

description :: HolLight -> String Source #

Language HasCASL Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

Methods

language_name :: HasCASL -> String Source #

description :: HasCASL -> String Source #

Language FreeCAD Source # 
Instance details

Defined in FreeCAD.Logic_FreeCAD

Methods

language_name :: FreeCAD -> String Source #

description :: FreeCAD -> String Source #

Language FrameworkCom Source # 
Instance details

Defined in Framework.Logic_Framework

Language Framework Source # 
Instance details

Defined in Framework.Logic_Framework

Methods

language_name :: Framework -> String Source #

description :: Framework -> String Source #

Language DMU Source # 
Instance details

Defined in DMU.Logic_DMU

Methods

language_name :: DMU -> String Source #

description :: DMU -> String Source #

Language DMU2OWL2 Source # 
Instance details

Defined in OWL2.DMU2OWL2

Methods

language_name :: DMU2OWL2 -> String Source #

description :: DMU2OWL2 -> String Source #

Language DFOL Source # 
Instance details

Defined in DFOL.Logic_DFOL

Methods

language_name :: DFOL -> String Source #

description :: DFOL -> String Source #

Language THFP_P2THFP Source # 
Instance details

Defined in Comorphisms.THFP_P2THFP

Language THFP_P2HasCASL Source # 
Instance details

Defined in Comorphisms.THFP_P2HasCASL

Language THFP2THF0 Source # 
Instance details

Defined in Comorphisms.THFP2THF0

Methods

language_name :: THFP2THF0 -> String Source #

description :: THFP2THF0 -> String Source #

Language QBF2Prop Source # 
Instance details

Defined in Comorphisms.QBF2Prop

Methods

language_name :: QBF2Prop -> String Source #

description :: QBF2Prop -> String Source #

Language Prop2QBF Source # 
Instance details

Defined in Comorphisms.Prop2QBF

Methods

language_name :: Prop2QBF -> String Source #

description :: Prop2QBF -> String Source #

Language PCoClTyConsHOL2PairsInIsaHOL Source # 
Instance details

Defined in Comorphisms.PCoClTyConsHOL2PairsInIsaHOL

Language PCoClTyConsHOL2IsabelleHOL Source # 
Instance details

Defined in Comorphisms.PCoClTyConsHOL2IsabelleHOL

Language MonadicHasCASL2IsabelleHOL Source # 
Instance details

Defined in Comorphisms.MonadicHasCASLTranslation

Language HolLight2Isabelle Source # 
Instance details

Defined in Comorphisms.HolLight2Isabelle

Language HasCASL2THFP_P Source # 
Instance details

Defined in Comorphisms.HasCASL2THFP_P

Language HasCASL2PCoClTyConsHOL Source # 
Instance details

Defined in Comorphisms.HasCASL2PCoClTyConsHOL

Language HasCASL2IsabelleHOL Source # 
Instance details

Defined in Comorphisms.HasCASL2IsabelleHOL

Language HasCASL2HasCASL Source # 
Instance details

Defined in Comorphisms.HasCASL2HasCASL

Language CommonLogic Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

Language OWL22CommonLogic Source # 
Instance details

Defined in OWL2.OWL22CommonLogic

Language SoftFOL2CommonLogic Source # 
Instance details

Defined in Comorphisms.SoftFOL2CommonLogic

Language Prop2CommonLogic Source # 
Instance details

Defined in Comorphisms.Prop2CommonLogic

Language CommonLogicModuleElimination Source # 
Instance details

Defined in Comorphisms.CommonLogicModuleElimination

Language CommonLogic2IsabelleHOL Source # 
Instance details

Defined in Comorphisms.CommonLogic2IsabelleHOL

Language CSMOF Source # 
Instance details

Defined in CSMOF.Logic_CSMOF

Methods

language_name :: CSMOF -> String Source #

description :: CSMOF -> String Source #

Language CSL Source # 
Instance details

Defined in CSL.Logic_CSL

Methods

language_name :: CSL -> String Source #

description :: CSL -> String Source #

Language Adl Source # 
Instance details

Defined in Adl.Logic_Adl

Methods

language_name :: Adl -> String Source #

description :: Adl -> String Source #

Language CASL Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

language_name :: CASL -> String Source #

description :: CASL -> String Source #

Language OWL22CASL Source # 
Instance details

Defined in OWL2.OWL22CASL

Methods

language_name :: OWL22CASL -> String Source #

description :: OWL22CASL -> String Source #

Language CASL2OWL Source # 
Instance details

Defined in OWL2.CASL2OWL

Methods

language_name :: CASL2OWL -> String Source #

description :: CASL2OWL -> String Source #

Language Modal Source # 
Instance details

Defined in Modal.Logic_Modal

Methods

language_name :: Modal -> String Source #

description :: Modal -> String Source #

Language Hybrid Source # 
Instance details

Defined in Hybrid.Logic_Hybrid

Methods

language_name :: Hybrid -> String Source #

description :: Hybrid -> String Source #

Language Fpl Source # 
Instance details

Defined in Fpl.Logic_Fpl

Methods

language_name :: Fpl -> String Source #

description :: Fpl -> String Source #

Language ExtModal Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Methods

language_name :: ExtModal -> String Source #

description :: ExtModal -> String Source #

Language ExtModal2OWL Source # 
Instance details

Defined in Comorphisms.ExtModal2OWL

Language ConstraintCASL Source # 
Instance details

Defined in ConstraintCASL.Logic_ConstraintCASL

Language RelScheme2CASL Source # 
Instance details

Defined in Comorphisms.RelScheme2CASL

Language Prop2CASL Source # 
Instance details

Defined in Comorphisms.Prop2CASL

Methods

language_name :: Prop2CASL -> String Source #

description :: Prop2CASL -> String Source #

Language Modal2CASL Source # 
Instance details

Defined in Comorphisms.Modal2CASL

Methods

language_name :: Modal2CASL -> String Source #

description :: Modal2CASL -> String Source #

Language Maude2CASL Source # 
Instance details

Defined in Comorphisms.Maude2CASL

Methods

language_name :: Maude2CASL -> String Source #

description :: Maude2CASL -> String Source #

Language Hybrid2CASL Source # 
Instance details

Defined in Comorphisms.Hybrid2CASL

Language ExtModal2CASL Source # 
Instance details

Defined in Comorphisms.ExtModal2CASL

Language DFOL2CASL Source # 
Instance details

Defined in Comorphisms.DFOL2CASL

Methods

language_name :: DFOL2CASL -> String Source #

description :: DFOL2CASL -> String Source #

Language CL2CFOL Source # 
Instance details

Defined in Comorphisms.CommonLogic2CASL

Methods

language_name :: CL2CFOL -> String Source #

description :: CL2CFOL -> String Source #

Language CSMOF2CASL Source # 
Instance details

Defined in Comorphisms.CSMOF2CASL

Methods

language_name :: CSMOF2CASL -> String Source #

description :: CSMOF2CASL -> String Source #

Language QVTR2CASL Source # 
Instance details

Defined in Comorphisms.QVTR2CASL

Methods

language_name :: QVTR2CASL -> String Source #

description :: QVTR2CASL -> String Source #

Language CFOL2IsabelleHOL Source # 
Instance details

Defined in Comorphisms.CFOL2IsabelleHOL

Language CASL2TopSort Source # 
Instance details

Defined in Comorphisms.CASL2TopSort

Language CASL2SubCFOL Source # 
Instance details

Defined in Comorphisms.CASL2SubCFOL

Language ExtModal2ExtModalTotal Source # 
Instance details

Defined in Comorphisms.ExtModal2ExtModalTotal

Language CASL2Skolem Source # 
Instance details

Defined in Comorphisms.CASL2Skolem

Language CASL2Prop Source # 
Instance details

Defined in Comorphisms.CASL2Prop

Methods

language_name :: CASL2Prop -> String Source #

description :: CASL2Prop -> String Source #

Language CASL2Prenex Source # 
Instance details

Defined in Comorphisms.CASL2Prenex

Language CASL2PCFOL Source # 
Instance details

Defined in Comorphisms.CASL2PCFOL

Methods

language_name :: CASL2PCFOL -> String Source #

description :: CASL2PCFOL -> String Source #

Language CspCASL2Modal Source # 
Instance details

Defined in Comorphisms.CspCASL2Modal

Language ExtModal2ExtModalNoSubsorts Source # 
Instance details

Defined in Comorphisms.ExtModal2ExtModalNoSubsorts

Language CASL2NNF Source # 
Instance details

Defined in Comorphisms.CASL2NNF

Methods

language_name :: CASL2NNF -> String Source #

description :: CASL2NNF -> String Source #

Language CASL2Modal Source # 
Instance details

Defined in Comorphisms.CASL2Modal

Methods

language_name :: CASL2Modal -> String Source #

description :: CASL2Modal -> String Source #

Language MODAL_EMBEDDING Source # 
Instance details

Defined in Modifications.ModalEmbedding

Language CASL2Hybrid Source # 
Instance details

Defined in Comorphisms.CASL2Hybrid

Language CASL2HasCASL Source # 
Instance details

Defined in Comorphisms.CASL2HasCASL

Language ExtModal2HasCASL Source # 
Instance details

Defined in Comorphisms.ExtModal2HasCASL

Language CASL2ExtModal Source # 
Instance details

Defined in Comorphisms.CASL2ExtModal

Language CASL2CspCASL Source # 
Instance details

Defined in Comorphisms.CASL2CspCASL

Language Adl2CASL Source # 
Instance details

Defined in Comorphisms.Adl2CASL

Methods

language_name :: Adl2CASL -> String Source #

description :: Adl2CASL -> String Source #

Language CoCASL Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Methods

language_name :: CoCASL -> String Source #

description :: CoCASL -> String Source #

Language CoCFOL2IsabelleHOL Source # 
Instance details

Defined in Comorphisms.CoCFOL2IsabelleHOL

Language CoCASL2CoSubCFOL Source # 
Instance details

Defined in Comorphisms.CoCASL2CoSubCFOL

Language CoCASL2CoPCFOL Source # 
Instance details

Defined in Comorphisms.CoCASL2CoPCFOL

Language CASL2CoCASL Source # 
Instance details

Defined in Comorphisms.CASL2CoCASL

Language COL Source # 
Instance details

Defined in COL.Logic_COL

Methods

language_name :: COL -> String Source #

description :: COL -> String Source #

Language CASL_DL Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Methods

language_name :: CASL_DL -> String Source #

description :: CASL_DL -> String Source #

Language CASL_DL2CASL Source # 
Instance details

Defined in Comorphisms.CASL_DL2CASL

Language Temporal Source #

Instance of Language for temporal logic

Instance details

Defined in Temporal.Logic_Temporal

Methods

language_name :: Temporal -> String Source #

description :: Temporal -> String Source #

Language Hybridize Source # 
Instance details

Defined in TopHybrid.Logic_TopHybrid

Methods

language_name :: Hybridize -> String Source #

description :: Hybridize -> String Source #

Language VSE Source # 
Instance details

Defined in VSE.Logic_VSE

Methods

language_name :: VSE -> String Source #

description :: VSE -> String Source #

Language CASL2VSERefine Source # 
Instance details

Defined in Comorphisms.CASL2VSERefine

Language CASL2VSEImport Source # 
Instance details

Defined in Comorphisms.CASL2VSEImport

Language CASL2VSE Source # 
Instance details

Defined in Comorphisms.CASL2VSE

Methods

language_name :: CASL2VSE -> String Source #

description :: CASL2VSE -> String Source #

Language cid => Language (SpanDomain cid) Source # 
Instance details

Defined in Logic.Morphism

Methods

language_name :: SpanDomain cid -> String Source #

description :: SpanDomain cid -> String Source #

Language lid => Language (IdModif lid) Source # 
Instance details

Defined in Logic.Modification

Methods

language_name :: IdModif lid -> String Source #

description :: IdModif lid -> String Source #

Show a => Language (GenCspCASL a) Source # 
Instance details

Defined in CspCASL.Logic_CspCASL

Methods

language_name :: GenCspCASL a -> String Source #

description :: GenCspCASL a -> String Source #

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

Defined in Logic.Comorphism

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 # 
Instance details

Defined in Logic.Comorphism

Methods

language_name :: InclComorphism lid sublogics -> String Source #

description :: InclComorphism lid sublogics -> 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 # 
Instance details

Defined in Logic.Morphism

Methods

language_name :: IdMorphism lid sublogics -> String Source #

description :: IdMorphism lid sublogics -> String Source #

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

Defined in Logic.Modification

Methods

language_name :: HorCompModif lid1 lid2 -> String Source #

description :: HorCompModif lid1 lid2 -> String Source #

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

Defined in Logic.Modification

Methods

language_name :: VerCompModif lid1 lid2 -> String Source #

description :: VerCompModif lid1 lid2 -> String Source #

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

Defined in CspCASL.Comorphisms

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 :: morphism -> object Source #

domain and codomain of morphisms

cod :: morphism -> object Source #

domain and codomain of morphisms

inverse :: morphism -> Result morphism Source #

the inverse of a morphism

isInclusion :: morphism -> Bool Source #

test if the signature morphism an inclusion

legal_mor :: morphism -> Result () Source #

is a value of type morphism denoting a legal morphism?

Instances

Instances details
Category Sign Morphism Source #

Instance of Category for CSL logic

Instance details

Defined in CSL.Logic_CSL

Category Sign Morphism Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

Category Sign Morphism Source # 
Instance details

Defined in DFOL.Logic_DFOL

Category Env Morphism Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

Category Sign Morphism Source # 
Instance details

Defined in LF.Logic_LF

Category Sign Morphism Source #

Instance of Category for Maude

Instance details

Defined in Maude.Logic_Maude

Category Sign OWLMorphism Source # 
Instance details

Defined in OWL2.Logic_OWL2

Category Sign Morphism Source #

Instance of Category for propositional logic

Instance details

Defined in NeSyPatterns.Logic_NeSyPatterns

Category Sign Morphism Source #

Instance of Category for propositional logic

Instance details

Defined in Propositional.Logic_Propositional

Category Sign Morphism Source #

Instance of Category for propositional logic

Instance details

Defined in QBF.Logic_QBF

Category Sign RDFMorphism Source # 
Instance details

Defined in RDF.Logic_RDF

Category Sign RSMorphism Source #

Instance of Category for Rel

Instance details

Defined in RelationalScheme.Logic_Rel

Category OMDoc_Sign OMDoc_Morphism Source # 
Instance details

Defined in OMDoc.Logic_OMDoc

Category G_sign GMorphism Source # 
Instance details

Defined in Logic.Grothendieck

Category Sign Morphism Source #

Instance of Category for temporal logic

Instance details

Defined in Temporal.Logic_Temporal

Category Sgn_Wrap Mor Source # 
Instance details

Defined in TopHybrid.Logic_TopHybrid

Ord sign => Category sign (DefaultMorphism sign) Source # 
Instance details

Defined in Logic.Logic

(Ord f, Ord e, Ord m, MorphismExtension e m) => Category (Sign f e) (Morphism f e m) Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

ide :: Sign f e -> Morphism f e m Source #

composeMorphisms :: Morphism f e m -> Morphism f e m -> Result (Morphism f e m) Source #

dom :: Morphism f e m -> Sign f e Source #

cod :: Morphism f e m -> Sign f e Source #

inverse :: Morphism f e m -> Result (Morphism f e m) Source #

isInclusion :: Morphism f e m -> Bool Source #

legal_mor :: Morphism f e m -> Result () Source #

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

Minimal complete definition

Nothing

Methods

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

parsers and printers

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

parser for basic specifications

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

parser for a single symbol returned as list

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

parser for symbol lists

parse_symb_map_items :: lid -> Maybe (PrefixMap -> AParser st symb_map_items) Source #

parser for symbol maps

toItem :: lid -> basic_spec -> Item Source #

symb_items_name :: lid -> symb_items -> [String] Source #

Instances

Instances details
Syntax RelScheme RSScheme RSSymbol () () Source #

Syntax of Rel

Instance details

Defined in RelationalScheme.Logic_Rel

Syntax RDF TurtleDocument RDFEntity SymbItems SymbMapItems Source # 
Instance details

Defined in RDF.Logic_RDF

Syntax QVTR Transformation () () () Source # 
Instance details

Defined in QVTR.Logic_QVTR

Syntax OMDoc_PUN () Symbol () () Source # 
Instance details

Defined in OMDoc.Logic_OMDoc

Syntax Maude MaudeText Symbol () () Source #

Instance of Syntax for Maude

Instance details

Defined in Maude.Logic_Maude

Syntax THF BasicSpecTHF SymbolTHF () () Source # 
Instance details

Defined in THF.Logic_THF

Syntax TPTP BASIC_SPEC Symbol () () Source # 
Instance details

Defined in TPTP.Logic_TPTP

Syntax QBF BASICSPEC Symbol SYMBITEMS SYMBMAPITEMS Source #

Syntax of Propositional logic

Instance details

Defined in QBF.Logic_QBF

Syntax Propositional BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in Propositional.Logic_Propositional

Syntax OWL2 OntologyDocument Entity SymbItems SymbMapItems Source # 
Instance details

Defined in OWL2.Logic_OWL2

Syntax NeSyPatterns BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in NeSyPatterns.Logic_NeSyPatterns

Syntax LF BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in LF.Logic_LF

Syntax Isabelle () () () () Source # 
Instance details

Defined in Isabelle.Logic_Isabelle

Syntax HolLight () () () () Source # 
Instance details

Defined in HolLight.Logic_HolLight

Syntax HasCASL BasicSpec Symbol SymbItems SymbMapItems Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

Syntax FreeCAD Document () () () Source # 
Instance details

Defined in FreeCAD.Logic_FreeCAD

Syntax FrameworkCom ComorphismDef () () () Source # 
Instance details

Defined in Framework.Logic_Framework

Syntax Framework LogicDef () () () Source # 
Instance details

Defined in Framework.Logic_Framework

Syntax DMU Text () () () Source # 
Instance details

Defined in DMU.Logic_DMU

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

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

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

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

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

Syntax DFOL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in DFOL.Logic_DFOL

Syntax CommonLogic BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

Syntax CSMOF Metamodel () () () Source # 
Instance details

Defined in CSMOF.Logic_CSMOF

Syntax CSL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #

Syntax of CSL logic

Instance details

Defined in CSL.Logic_CSL

Syntax Adl Context Symbol () () Source # 
Instance details

Defined in Adl.Logic_Adl

Syntax CASL CASLBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in CASL.Logic_CASL

Syntax Modal M_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in Modal.Logic_Modal

Syntax Hybrid H_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in Hybrid.Logic_Hybrid

Syntax Fpl FplBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in Fpl.Logic_Fpl

Syntax ExtModal EM_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Syntax ConstraintCASL ConstraintCASLBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in ConstraintCASL.Logic_ConstraintCASL

Syntax CoCASL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Syntax COL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in COL.Logic_COL

Syntax CASL_DL DL_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Syntax Temporal BASIC_SPEC Symbol () () Source #

Syntax of Temporal logic

Instance details

Defined in Temporal.Logic_Temporal

Syntax Hybridize Spc_Wrap Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in TopHybrid.Logic_TopHybrid

Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in VSE.Logic_VSE

Syntax SoftFOL [TPTP] SFSymbol () () Source # 
Instance details

Defined in SoftFOL.Logic_SoftFOL

(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 # 
Instance details

Defined in Logic.Morphism

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

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

parse_symb_map_items :: SpanDomain cid -> Maybe (PrefixMap -> 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

Instance details

Defined in CspCASL.Logic_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.

Minimal complete definition

Nothing

Methods

map_sen :: lid -> morphism -> sentence -> Result sentence Source #

sentence translation along a signature morphism

simplify_sen :: lid -> sign -> sentence -> sentence Source #

simplification of sentences (leave out qualifications)

negation :: lid -> sentence -> Maybe sentence Source #

negation of a sentence for disproving

print_sign :: lid -> sign -> Doc Source #

modified signature printing when followed by sentences

print_named :: lid -> Named sentence -> Doc Source #

print a sentence with comments

sym_of :: lid -> sign -> [Set symbol] Source #

dependency ordered list of symbol sets for a signature

mostSymsOf :: lid -> sign -> [symbol] Source #

Dependency ordered list of a bigger symbol set for a signature. This function contains more symbols than those being subject to hiding and renaming (given by sym_of) to better represent a signature as a set of symbols given within xml files. At least for CASL additional symbols for (direct) subsorts will be created, but note, that no symbol for a partial function will be created, if the signature contains this function as total, although a signature with just that partial function would be a subsignature. This function is supposed to work over partial signatures created by signatureDiff.

symmap_of :: lid -> morphism -> EndoMap symbol Source #

symbol map for a signature morphism

sym_name :: lid -> symbol -> Id Source #

symbols have a name, see CASL RefMan p. 192

sym_label :: lid -> symbol -> Maybe String Source #

some symbols have a label for better readability

fullSymName :: lid -> symbol -> String Source #

the fully qualified name for XML output (i.e. of OWL2)

symKind :: lid -> symbol -> String Source #

a logic dependent kind of a symbol

symsOfSen :: lid -> sign -> sentence -> [symbol] Source #

the symbols occuring in a sentence (any order)

pair_symbols :: lid -> symbol -> symbol -> Result symbol Source #

combine two symbols into another one

Instances

Instances details
Sentences RelScheme Sentence Sign RSMorphism RSSymbol Source #

Instance of Sentences for Rel

Instance details

Defined in RelationalScheme.Logic_Rel

Sentences RDF Axiom Sign RDFMorphism RDFEntity Source # 
Instance details

Defined in RDF.Logic_RDF

Sentences QVTR Sen Sign Morphism () Source # 
Instance details

Defined in QVTR.Logic_QVTR

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 OMDoc_PUN () OMDoc_Sign OMDoc_Morphism Symbol Source # 
Instance details

Defined in OMDoc.Logic_OMDoc

Sentences Maude Sentence Sign Morphism Symbol Source #

Instance of Sentences for Maude

Instance details

Defined in Maude.Logic_Maude

Sentences THF THFFormula SignTHF MorphismTHF SymbolTHF Source # 
Instance details

Defined in THF.Logic_THF

Sentences TPTP Sentence Sign Morphism Symbol Source # 
Instance details

Defined in TPTP.Logic_TPTP

Sentences SoftFOL Sentence Sign SoftFOLMorphism SFSymbol Source # 
Instance details

Defined in SoftFOL.Logic_SoftFOL

Sentences QBF FORMULA Sign Morphism Symbol Source #

Instance of Sentences for propositional logic

Instance details

Defined in QBF.Logic_QBF

Sentences Propositional FORMULA Sign Morphism Symbol Source #

Instance of Sentences for propositional logic

Instance details

Defined in Propositional.Logic_Propositional

Sentences OWL2 Axiom Sign OWLMorphism Entity Source # 
Instance details

Defined in OWL2.Logic_OWL2

Sentences NeSyPatterns () Sign Morphism Symbol Source #

Instance of Sentences for propositional logic

Instance details

Defined in NeSyPatterns.Logic_NeSyPatterns

Sentences LF Sentence Sign Morphism Symbol Source # 
Instance details

Defined in LF.Logic_LF

Sentences Isabelle Sentence Sign IsabelleMorphism () Source # 
Instance details

Defined in Isabelle.Logic_Isabelle

Sentences HolLight Sentence Sign HolLightMorphism () Source # 
Instance details

Defined in HolLight.Logic_HolLight

Sentences HasCASL Sentence Env Morphism Symbol Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

Sentences FreeCAD () Sign FCMorphism () Source # 
Instance details

Defined in FreeCAD.Logic_FreeCAD

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 FrameworkCom () ComorphismDef MorphismCom () Source # 
Instance details

Defined in Framework.Logic_Framework

Sentences Framework () LogicDef Morphism () Source # 
Instance details

Defined in Framework.Logic_Framework

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 DFOL FORMULA Sign Morphism Symbol Source # 
Instance details

Defined in DFOL.Logic_DFOL

Sentences CommonLogic TEXT_META Sign Morphism Symbol Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

Sentences CSMOF Sen Sign Morphism () Source # 
Instance details

Defined in CSMOF.Logic_CSMOF

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 CSL CMD Sign Morphism Symbol Source #

Instance of Sentences for reduce logic

Instance details

Defined in CSL.Logic_CSL

Sentences Adl Sen Sign Morphism Symbol Source # 
Instance details

Defined in Adl.Logic_Adl

Sentences CASL CASLFORMULA CASLSign CASLMor Symbol Source # 
Instance details

Defined in CASL.Logic_CASL

Sentences Modal ModalFORMULA MSign ModalMor Symbol Source # 
Instance details

Defined in Modal.Logic_Modal

Sentences Hybrid HybridFORMULA HSign HybridMor Symbol Source # 
Instance details

Defined in Hybrid.Logic_Hybrid

Sentences Fpl FplForm FplSign FplMor Symbol Source # 
Instance details

Defined in Fpl.Logic_Fpl

Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Sentences ConstraintCASL ConstraintCASLFORMULA ConstraintCASLSign ConstraintCASLMor Symbol Source # 
Instance details

Defined in ConstraintCASL.Logic_ConstraintCASL

Sentences CoCASL CoCASLFORMULA CSign CoCASLMor Symbol Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Sentences COL COLFORMULA CSign COLMor Symbol Source # 
Instance details

Defined in COL.Logic_COL

Sentences CASL_DL DLFORMULA DLSign DLMor Symbol Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Sentences Temporal FORMULA Sign Morphism Symbol Source #

Instance of Sentences for temporal logic

Instance details

Defined in Temporal.Logic_Temporal

Sentences Hybridize Frm_Wrap Sgn_Wrap Mor Symbol Source # 
Instance details

Defined in TopHybrid.Logic_TopHybrid

Sentences VSE Sentence VSESign VSEMor Symbol Source # 
Instance details

Defined in VSE.Logic_VSE

Sentences DMU () Text (DefaultMorphism Text) () Source # 
Instance details

Defined in DMU.Logic_DMU

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

Instance details

Defined in CspCASL.Logic_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, Data sentence2) => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1 sign_symbol1 Source # 
Instance details

Defined in Logic.Morphism

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

Instances details
Eq REL_REF Source # 
Instance details

Defined in Logic.Logic

Methods

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

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

Show REL_REF Source # 
Instance details

Defined in Logic.Logic

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 :: lid -> Set symbol -> sign -> Result morphism Source #

the signature (co)generated by a set of symbols in another signature is the smallest (largest) signature containing (excluding) the set of symbols. Needed for revealing and hiding, see CASL RefMan p. 197ff.

cogenerated_sign :: lid -> Set symbol -> sign -> Result morphism Source #

the signature (co)generated by a set of symbols in another signature is the smallest (largest) signature containing (excluding) the set of symbols. Needed for revealing and hiding, see CASL RefMan p. 197ff.

induced_from_morphism :: lid -> EndoMap raw_symbol -> sign -> Result morphism Source #

Induce a signature morphism from a source signature and a raw symbol map. Needed for translation (SP with SM). See CASL RefMan p. 198

induced_from_to_morphism :: lid -> EndoMap raw_symbol -> ExtSign sign symbol -> ExtSign sign symbol -> Result morphism Source #

Induce a signature morphism between two signatures by a raw symbol map. Needed for instantiation and views. See CASL RefMan p. 198f.

is_transportable :: lid -> morphism -> Bool Source #

Check whether a signature morphism is transportable. See CASL RefMan p. 304f.

is_injective :: lid -> morphism -> Bool Source #

Check whether the underlying symbol map of a signature morphism is injective

theory_to_taxonomy :: lid -> TaxoGraphKind -> MMiSSOntology -> sign -> [Named sentence] -> Result MMiSSOntology Source #

generate an ontological taxonomy, if this makes sense

corresp2th :: lid -> String -> Bool -> sign -> sign -> [symb_items] -> [symb_items] -> EndoMap symbol -> EndoMap symbol -> REL_REF -> Result (sign, [Named sentence], sign, sign, EndoMap symbol, EndoMap symbol) Source #

create a theory from a correspondence

equiv2cospan :: lid -> sign -> sign -> [symb_items] -> [symb_items] -> Result (sign, sign, sign, EndoMap symbol, EndoMap symbol) Source #

create a co-span fragment from an equivalence

extract_module :: lid -> [IRI] -> (sign, [Named sentence]) -> Result (sign, [Named sentence]) Source #

extract the module

Instances

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

Static Analysis for Rel

Instance details

Defined in RelationalScheme.Logic_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 RDF TurtleDocument Axiom SymbItems SymbMapItems Sign RDFMorphism RDFEntity RawSymb Source # 
Instance details

Defined in RDF.Logic_RDF

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 QVTR Transformation Sen () () Sign Morphism () () Source # 
Instance details

Defined in QVTR.Logic_QVTR

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 OMDoc_PUN () () () () OMDoc_Sign OMDoc_Morphism Symbol () Source # 
Instance details

Defined in OMDoc.Logic_OMDoc

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 Maude MaudeText Sentence () () Sign Morphism Symbol Symbol Source #

Instance of StaticAnalysis for Maude

Instance details

Defined in Maude.Logic_Maude

Methods

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

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

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

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

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

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

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

quotient_term_algebra :: Maude -> Morphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

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

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

symbol_to_raw :: Maude -> Symbol -> Symbol Source #

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

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

empty_signature :: Maude -> Sign Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Defined in THF.Logic_THF

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 TPTP BASIC_SPEC Sentence () () Sign Morphism Symbol () Source # 
Instance details

Defined in TPTP.Logic_TPTP

Methods

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

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

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

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

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

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

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

quotient_term_algebra :: TPTP -> Morphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

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

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

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

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

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

empty_signature :: TPTP -> Sign Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

StaticAnalysis QBF BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol Source #

Static Analysis for propositional logic

Instance details

Defined in QBF.Logic_QBF

Methods

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

sen_analysis :: QBF -> Maybe ((BASICSPEC, Sign, FORMULA) -> Result FORMULA) Source #

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

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

stat_symb_items :: QBF -> Sign -> [SYMBITEMS] -> Result [Symbol] Source #

convertTheory :: QBF -> Maybe ((Sign, [Named FORMULA]) -> BASICSPEC) Source #

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

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

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

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

symbol_to_raw :: QBF -> Symbol -> Symbol Source #

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

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

empty_signature :: QBF -> Sign Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

extract_module :: QBF -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source #

StaticAnalysis Propositional BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source #

Static Analysis for propositional logic

Instance details

Defined in Propositional.Logic_Propositional

Methods

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

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

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

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

stat_symb_items :: Propositional -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source #

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

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

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

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

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

symbol_to_raw :: Propositional -> Symbol -> Symbol Source #

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

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

empty_signature :: Propositional -> Sign Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

corresp2th :: Propositional -> 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 :: Propositional -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Propositional -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source #

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

Defined in OWL2.Logic_OWL2

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 NeSyPatterns BASIC_SPEC () SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source #

Static Analysis for propositional logic

Instance details

Defined in NeSyPatterns.Logic_NeSyPatterns

Methods

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

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

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

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

stat_symb_items :: NeSyPatterns -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source #

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

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

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

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

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

symbol_to_raw :: NeSyPatterns -> Symbol -> Symbol Source #

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

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

empty_signature :: NeSyPatterns -> Sign Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theory_to_taxonomy :: NeSyPatterns -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named ()] -> Result MMiSSOntology Source #

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

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

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

StaticAnalysis LF BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RAW_SYM Source # 
Instance details

Defined in LF.Logic_LF

Methods

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

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

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

stat_symb_map_items :: LF -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RAW_SYM) Source #

stat_symb_items :: LF -> Sign -> [SYMB_ITEMS] -> Result [RAW_SYM] Source #

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

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

quotient_term_algebra :: LF -> Morphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

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

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

symbol_to_raw :: LF -> Symbol -> RAW_SYM Source #

id_to_raw :: LF -> Id -> RAW_SYM Source #

matches :: LF -> Symbol -> RAW_SYM -> Bool Source #

empty_signature :: LF -> Sign Source #

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

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

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

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

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

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

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

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

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

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

induced_from_morphism :: LF -> EndoMap RAW_SYM -> Sign -> Result Morphism Source #

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

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

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

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

corresp2th :: LF -> 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 #

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

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

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

Defined in Isabelle.Logic_Isabelle

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 HolLight () Sentence () () Sign HolLightMorphism () () Source #

Static Analysis for propositional logic

Instance details

Defined in HolLight.Logic_HolLight

Methods

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

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

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

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

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

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

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

quotient_term_algebra :: HolLight -> HolLightMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: HolLight -> Gr Sign (Int, HolLightMorphism) -> Result (Sign, Map Int HolLightMorphism) Source #

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

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

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

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

empty_signature :: HolLight -> Sign Source #

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

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

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

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

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

morphism_union :: HolLight -> HolLightMorphism -> HolLightMorphism -> Result HolLightMorphism Source #

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

subsig_inclusion :: HolLight -> Sign -> Sign -> Result HolLightMorphism Source #

generated_sign :: HolLight -> Set () -> Sign -> Result HolLightMorphism Source #

cogenerated_sign :: HolLight -> Set () -> Sign -> Result HolLightMorphism Source #

induced_from_morphism :: HolLight -> EndoMap () -> Sign -> Result HolLightMorphism Source #

induced_from_to_morphism :: HolLight -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result HolLightMorphism Source #

is_transportable :: HolLight -> HolLightMorphism -> Bool Source #

is_injective :: HolLight -> HolLightMorphism -> Bool Source #

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

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

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

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

StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

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 FreeCAD Document () () () Sign FCMorphism () () Source # 
Instance details

Defined in FreeCAD.Logic_FreeCAD

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 FrameworkCom ComorphismDef () () () ComorphismDef MorphismCom () () Source # 
Instance details

Defined in Framework.Logic_Framework

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 # 
Instance details

Defined in Framework.Logic_Framework

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 DFOL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source # 
Instance details

Defined in DFOL.Logic_DFOL

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 CommonLogic BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

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 CSMOF Metamodel Sen () () Sign Morphism () () Source # 
Instance details

Defined in CSMOF.Logic_CSMOF

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 CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source #

Static Analysis for reduce logic

Instance details

Defined in CSL.Logic_CSL

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 Adl Context Sen () () Sign Morphism Symbol RawSymbol Source # 
Instance details

Defined in Adl.Logic_Adl

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 CASL CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol Source # 
Instance details

Defined in CASL.Logic_CASL

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 Modal M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol Source # 
Instance details

Defined in Modal.Logic_Modal

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 Hybrid H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol Source # 
Instance details

Defined in Hybrid.Logic_Hybrid

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 Fpl FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol Source # 
Instance details

Defined in Fpl.Logic_Fpl

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 ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

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 ConstraintCASL ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol Source # 
Instance details

Defined in ConstraintCASL.Logic_ConstraintCASL

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 CoCASL C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

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 COL C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol Source # 
Instance details

Defined in COL.Logic_COL

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 CASL_DL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

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 Temporal BASIC_SPEC FORMULA () () Sign Morphism Symbol Symbol Source #

Static Analysis for propositional logic

Instance details

Defined in Temporal.Logic_Temporal

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 Hybridize Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS Sgn_Wrap Mor Symbol RawSymbol Source # 
Instance details

Defined in TopHybrid.Logic_TopHybrid

Methods

basic_analysis :: Hybridize -> Maybe ((Spc_Wrap, Sgn_Wrap, GlobalAnnos) -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap])) Source #

sen_analysis :: Hybridize -> Maybe ((Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap) Source #

extBasicAnalysis :: Hybridize -> IRI -> LibName -> Spc_Wrap -> Sgn_Wrap -> GlobalAnnos -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap]) Source #

stat_symb_map_items :: Hybridize -> Sgn_Wrap -> Maybe Sgn_Wrap -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Hybridize -> Sgn_Wrap -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: Hybridize -> Maybe ((Sgn_Wrap, [Named Frm_Wrap]) -> Spc_Wrap) Source #

ensures_amalgamability :: Hybridize -> ([CASLAmalgOpt], Gr Sgn_Wrap (Int, Mor), [(Int, Mor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Hybridize -> Mor -> [Named Frm_Wrap] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source #

signature_colimit :: Hybridize -> Gr Sgn_Wrap (Int, Mor) -> Result (Sgn_Wrap, Map Int Mor) Source #

qualify :: Hybridize -> SIMPLE_ID -> LibName -> Mor -> Sgn_Wrap -> Result (Mor, [Named Frm_Wrap]) Source #

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

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

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

empty_signature :: Hybridize -> Sgn_Wrap Source #

add_symb_to_sign :: Hybridize -> Sgn_Wrap -> Symbol -> Result Sgn_Wrap Source #

signature_union :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source #

signatureDiff :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source #

intersection :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source #

final_union :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source #

morphism_union :: Hybridize -> Mor -> Mor -> Result Mor Source #

is_subsig :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Bool Source #

subsig_inclusion :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Mor Source #

generated_sign :: Hybridize -> Set Symbol -> Sgn_Wrap -> Result Mor Source #

cogenerated_sign :: Hybridize -> Set Symbol -> Sgn_Wrap -> Result Mor Source #

induced_from_morphism :: Hybridize -> EndoMap RawSymbol -> Sgn_Wrap -> Result Mor Source #

induced_from_to_morphism :: Hybridize -> EndoMap RawSymbol -> ExtSign Sgn_Wrap Symbol -> ExtSign Sgn_Wrap Symbol -> Result Mor Source #

is_transportable :: Hybridize -> Mor -> Bool Source #

is_injective :: Hybridize -> Mor -> Bool Source #

theory_to_taxonomy :: Hybridize -> TaxoGraphKind -> MMiSSOntology -> Sgn_Wrap -> [Named Frm_Wrap] -> Result MMiSSOntology Source #

corresp2th :: Hybridize -> String -> Bool -> Sgn_Wrap -> Sgn_Wrap -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sgn_Wrap, [Named Frm_Wrap], Sgn_Wrap, Sgn_Wrap, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sgn_Wrap, Sgn_Wrap, Sgn_Wrap, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Hybridize -> [IRI] -> (Sgn_Wrap, [Named Frm_Wrap]) -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source #

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

Defined in VSE.Logic_VSE

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 DMU Text () () () Text (DefaultMorphism Text) () () Source # 
Instance details

Defined in DMU.Logic_DMU

Methods

basic_analysis :: DMU -> Maybe ((Text, Text, GlobalAnnos) -> Result (Text, ExtSign Text (), [Named ()])) Source #

sen_analysis :: DMU -> Maybe ((Text, Text, ()) -> Result ()) Source #

extBasicAnalysis :: DMU -> IRI -> LibName -> Text -> Text -> GlobalAnnos -> Result (Text, ExtSign Text (), [Named ()]) Source #

stat_symb_map_items :: DMU -> Text -> Maybe Text -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: DMU -> Text -> [()] -> Result [()] Source #

convertTheory :: DMU -> Maybe ((Text, [Named ()]) -> Text) Source #

ensures_amalgamability :: DMU -> ([CASLAmalgOpt], Gr Text (Int, DefaultMorphism Text), [(Int, DefaultMorphism Text)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: DMU -> DefaultMorphism Text -> [Named ()] -> Result (Text, [Named ()]) Source #

signature_colimit :: DMU -> Gr Text (Int, DefaultMorphism Text) -> Result (Text, Map Int (DefaultMorphism Text)) Source #

qualify :: DMU -> SIMPLE_ID -> LibName -> DefaultMorphism Text -> Text -> Result (DefaultMorphism Text, [Named ()]) Source #

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

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

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

empty_signature :: DMU -> Text Source #

add_symb_to_sign :: DMU -> Text -> () -> Result Text Source #

signature_union :: DMU -> Text -> Text -> Result Text Source #

signatureDiff :: DMU -> Text -> Text -> Result Text Source #

intersection :: DMU -> Text -> Text -> Result Text Source #

final_union :: DMU -> Text -> Text -> Result Text Source #

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

is_subsig :: DMU -> Text -> Text -> Bool Source #

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

generated_sign :: DMU -> Set () -> Text -> Result (DefaultMorphism Text) Source #

cogenerated_sign :: DMU -> Set () -> Text -> Result (DefaultMorphism Text) Source #

induced_from_morphism :: DMU -> EndoMap () -> Text -> Result (DefaultMorphism Text) Source #

induced_from_to_morphism :: DMU -> EndoMap () -> ExtSign Text () -> ExtSign Text () -> Result (DefaultMorphism Text) Source #

is_transportable :: DMU -> DefaultMorphism Text -> Bool Source #

is_injective :: DMU -> DefaultMorphism Text -> Bool Source #

theory_to_taxonomy :: DMU -> TaxoGraphKind -> MMiSSOntology -> Text -> [Named ()] -> Result MMiSSOntology Source #

corresp2th :: DMU -> String -> Bool -> Text -> Text -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Text, [Named ()], Text, Text, EndoMap (), EndoMap ()) Source #

equiv2cospan :: DMU -> Text -> Text -> [()] -> [()] -> Result (Text, Text, Text, EndoMap (), EndoMap ()) Source #

extract_module :: DMU -> [IRI] -> (Text, [Named ()]) -> Result (Text, [Named ()]) Source #

StaticAnalysis SoftFOL [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () Source # 
Instance details

Defined in SoftFOL.Logic_SoftFOL

Methods

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

sen_analysis :: SoftFOL -> Maybe (([TPTP], Sign, Sentence) -> Result Sentence) Source #

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

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

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

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

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

quotient_term_algebra :: SoftFOL -> SoftFOLMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: SoftFOL -> Gr Sign (Int, SoftFOLMorphism) -> Result (Sign, Map Int SoftFOLMorphism) Source #

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

symbol_to_raw :: SoftFOL -> SFSymbol -> () Source #

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

matches :: SoftFOL -> SFSymbol -> () -> Bool Source #

empty_signature :: SoftFOL -> Sign Source #

add_symb_to_sign :: SoftFOL -> Sign -> SFSymbol -> Result Sign Source #

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

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

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

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

morphism_union :: SoftFOL -> SoftFOLMorphism -> SoftFOLMorphism -> Result SoftFOLMorphism Source #

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

subsig_inclusion :: SoftFOL -> Sign -> Sign -> Result SoftFOLMorphism Source #

generated_sign :: SoftFOL -> Set SFSymbol -> Sign -> Result SoftFOLMorphism Source #

cogenerated_sign :: SoftFOL -> Set SFSymbol -> Sign -> Result SoftFOLMorphism Source #

induced_from_morphism :: SoftFOL -> EndoMap () -> Sign -> Result SoftFOLMorphism Source #

induced_from_to_morphism :: SoftFOL -> EndoMap () -> ExtSign Sign SFSymbol -> ExtSign Sign SFSymbol -> Result SoftFOLMorphism Source #

is_transportable :: SoftFOL -> SoftFOLMorphism -> Bool Source #

is_injective :: SoftFOL -> SoftFOLMorphism -> Bool Source #

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

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

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

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

Show a => StaticAnalysis (GenCspCASL a) CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol Source #

Static Analysis for CspCASL

Instance details

Defined in CspCASL.Logic_CspCASL

Methods

basic_analysis :: GenCspCASL a -> Maybe ((CspBasicSpec, CspCASLSign, GlobalAnnos) -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen])) Source #

sen_analysis :: GenCspCASL a -> Maybe ((CspBasicSpec, CspCASLSign, CspCASLSen) -> Result CspCASLSen) Source #

extBasicAnalysis :: GenCspCASL a -> IRI -> LibName -> CspBasicSpec -> CspCASLSign -> GlobalAnnos -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen]) Source #

stat_symb_map_items :: GenCspCASL a -> CspCASLSign -> Maybe CspCASLSign -> [CspSymbMapItems] -> Result (EndoMap CspRawSymbol) Source #

stat_symb_items :: GenCspCASL a -> CspCASLSign -> [CspSymbItems] -> Result [CspRawSymbol] Source #

convertTheory :: GenCspCASL a -> Maybe ((CspCASLSign, [Named CspCASLSen]) -> CspBasicSpec) Source #

ensures_amalgamability :: GenCspCASL a -> ([CASLAmalgOpt], Gr CspCASLSign (Int, CspCASLMorphism), [(Int, CspCASLMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: GenCspCASL a -> CspCASLMorphism -> [Named CspCASLSen] -> Result (CspCASLSign, [Named CspCASLSen]) Source #

signature_colimit :: GenCspCASL a -> Gr CspCASLSign (Int, CspCASLMorphism) -> Result (CspCASLSign, Map Int CspCASLMorphism) Source #

qualify :: GenCspCASL a -> SIMPLE_ID -> LibName -> CspCASLMorphism -> CspCASLSign -> Result (CspCASLMorphism, [Named CspCASLSen]) Source #

symbol_to_raw :: GenCspCASL a -> CspSymbol -> CspRawSymbol Source #

id_to_raw :: GenCspCASL a -> Id -> CspRawSymbol Source #

matches :: GenCspCASL a -> CspSymbol -> CspRawSymbol -> Bool Source #

empty_signature :: GenCspCASL a -> CspCASLSign Source #

add_symb_to_sign :: GenCspCASL a -> CspCASLSign -> CspSymbol -> Result CspCASLSign Source #

signature_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

signatureDiff :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

intersection :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

final_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

morphism_union :: GenCspCASL a -> CspCASLMorphism -> CspCASLMorphism -> Result CspCASLMorphism Source #

is_subsig :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Bool Source #

subsig_inclusion :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLMorphism Source #

generated_sign :: GenCspCASL a -> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism Source #

cogenerated_sign :: GenCspCASL a -> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism Source #

induced_from_morphism :: GenCspCASL a -> EndoMap CspRawSymbol -> CspCASLSign -> Result CspCASLMorphism Source #

induced_from_to_morphism :: GenCspCASL a -> EndoMap CspRawSymbol -> ExtSign CspCASLSign CspSymbol -> ExtSign CspCASLSign CspSymbol -> Result CspCASLMorphism Source #

is_transportable :: GenCspCASL a -> CspCASLMorphism -> Bool Source #

is_injective :: GenCspCASL a -> CspCASLMorphism -> Bool Source #

theory_to_taxonomy :: GenCspCASL a -> TaxoGraphKind -> MMiSSOntology -> CspCASLSign -> [Named CspCASLSen] -> Result MMiSSOntology Source #

corresp2th :: GenCspCASL a -> String -> Bool -> CspCASLSign -> CspCASLSign -> [CspSymbItems] -> [CspSymbItems] -> EndoMap CspSymbol -> EndoMap CspSymbol -> REL_REF -> Result (CspCASLSign, [Named CspCASLSen], CspCASLSign, CspCASLSign, EndoMap CspSymbol, EndoMap CspSymbol) Source #

equiv2cospan :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> [CspSymbItems] -> [CspSymbItems] -> Result (CspCASLSign, CspCASLSign, CspCASLSign, EndoMap CspSymbol, EndoMap CspSymbol) Source #

extract_module :: GenCspCASL a -> [IRI] -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) 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, Ord symbol1, GetRange symbol1, Pretty symbol1, Typeable symbol1, Data sentence2) => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 Source # 
Instance details

Defined in Logic.Morphism

Methods

basic_analysis :: SpanDomain cid -> Maybe (((), sign1, GlobalAnnos) -> Result ((), ExtSign sign1 sign_symbol1, [Named (S2 sentence2)])) Source #

sen_analysis :: SpanDomain cid -> Maybe (((), sign1, S2 sentence2) -> Result (S2 sentence2)) Source #

extBasicAnalysis :: SpanDomain cid -> IRI -> LibName -> () -> sign1 -> GlobalAnnos -> Result ((), ExtSign sign1 sign_symbol1, [Named (S2 sentence2)]) Source #

stat_symb_map_items :: SpanDomain cid -> sign1 -> Maybe sign1 -> [()] -> Result (EndoMap symbol1) Source #

stat_symb_items :: SpanDomain cid -> sign1 -> [()] -> Result [symbol1] Source #

convertTheory :: SpanDomain cid -> Maybe ((sign1, [Named (S2 sentence2)]) -> ()) Source #

ensures_amalgamability :: SpanDomain cid -> ([CASLAmalgOpt], Gr sign1 (Int, morphism1), [(Int, morphism1)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: SpanDomain cid -> morphism1 -> [Named (S2 sentence2)] -> Result (sign1, [Named (S2 sentence2)]) Source #

signature_colimit :: SpanDomain cid -> Gr sign1 (Int, morphism1) -> Result (sign1, Map Int morphism1) Source #

qualify :: SpanDomain cid -> SIMPLE_ID -> LibName -> morphism1 -> sign1 -> Result (morphism1, [Named (S2 sentence2)]) Source #

symbol_to_raw :: SpanDomain cid -> sign_symbol1 -> symbol1 Source #

id_to_raw :: SpanDomain cid -> Id -> symbol1 Source #

matches :: SpanDomain cid -> sign_symbol1 -> symbol1 -> Bool Source #

empty_signature :: SpanDomain cid -> sign1 Source #

add_symb_to_sign :: SpanDomain cid -> sign1 -> sign_symbol1 -> Result sign1 Source #

signature_union :: SpanDomain cid -> sign1 -> sign1 -> Result sign1 Source #

signatureDiff :: SpanDomain cid -> sign1 -> sign1 -> Result sign1 Source #

intersection :: SpanDomain cid -> sign1 -> sign1 -> Result sign1 Source #

final_union :: SpanDomain cid -> sign1 -> sign1 -> Result sign1 Source #

morphism_union :: SpanDomain cid -> morphism1 -> morphism1 -> Result morphism1 Source #

is_subsig :: SpanDomain cid -> sign1 -> sign1 -> Bool Source #

subsig_inclusion :: SpanDomain cid -> sign1 -> sign1 -> Result morphism1 Source #

generated_sign :: SpanDomain cid -> Set sign_symbol1 -> sign1 -> Result morphism1 Source #

cogenerated_sign :: SpanDomain cid -> Set sign_symbol1 -> sign1 -> Result morphism1 Source #

induced_from_morphism :: SpanDomain cid -> EndoMap symbol1 -> sign1 -> Result morphism1 Source #

induced_from_to_morphism :: SpanDomain cid -> EndoMap symbol1 -> ExtSign sign1 sign_symbol1 -> ExtSign sign1 sign_symbol1 -> Result morphism1 Source #

is_transportable :: SpanDomain cid -> morphism1 -> Bool Source #

is_injective :: SpanDomain cid -> morphism1 -> Bool Source #

theory_to_taxonomy :: SpanDomain cid -> TaxoGraphKind -> MMiSSOntology -> sign1 -> [Named (S2 sentence2)] -> Result MMiSSOntology Source #

corresp2th :: SpanDomain cid -> String -> Bool -> sign1 -> sign1 -> [()] -> [()] -> EndoMap sign_symbol1 -> EndoMap sign_symbol1 -> REL_REF -> Result (sign1, [Named (S2 sentence2)], sign1, sign1, EndoMap sign_symbol1, EndoMap sign_symbol1) Source #

equiv2cospan :: SpanDomain cid -> sign1 -> sign1 -> [()] -> [()] -> Result (sign1, sign1, sign1, EndoMap sign_symbol1, EndoMap sign_symbol1) Source #

extract_module :: SpanDomain cid -> [IRI] -> (sign1, [Named (S2 sentence2)]) -> Result (sign1, [Named (S2 sentence2)]) Source #

printTheory :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol => Maybe IRI -> lid -> (sign, [Named sentence]) -> Doc Source #

print a whole theory

inclusion :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol => lid -> sign -> sign -> Result morphism Source #

guarded inclusion

class (Ord l, Show l) => SemiLatticeWithTop l where Source #

semi lattices with top (needed for sublogics). Note that Ord is only used for efficiency and is not related to the partial order given by the lattice. Only Eq is used to define isSubElem

Methods

lub :: l -> l -> l Source #

top :: l Source #

Instances

Instances details
SemiLatticeWithTop () Source # 
Instance details

Defined in Logic.Logic

Methods

lub :: () -> () -> () Source #

top :: () Source #

SemiLatticeWithTop CASL_DL_SL Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

SemiLatticeWithTop CommonLogicSL Source #

Sublogics

Instance details

Defined in CommonLogic.Logic_CommonLogic

SemiLatticeWithTop Sublogic Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

SemiLatticeWithTop HolLightSL Source #

Sublogics

Instance details

Defined in HolLight.Logic_HolLight

SemiLatticeWithTop ProfSub Source # 
Instance details

Defined in OWL2.Logic_OWL2

SemiLatticeWithTop PropSL Source #

Sublogics

Instance details

Defined in Propositional.Logic_Propositional

SemiLatticeWithTop QBFSL Source #

Sublogics

Instance details

Defined in QBF.Logic_QBF

Methods

lub :: QBFSL -> QBFSL -> QBFSL Source #

top :: QBFSL Source #

SemiLatticeWithTop THFSl Source # 
Instance details

Defined in THF.Logic_THF

Methods

lub :: THFSl -> THFSl -> THFSl Source #

top :: THFSl Source #

SemiLatticeWithTop Sublogic Source # 
Instance details

Defined in TPTP.Logic_TPTP

Lattice a => SemiLatticeWithTop (CASL_SL a) Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

lub :: CASL_SL a -> CASL_SL a -> CASL_SL a Source #

top :: CASL_SL a Source #

(SemiLatticeWithTop sublogics1, SemiLatticeWithTop sublogics2) => SemiLatticeWithTop (SublogicsPair sublogics1 sublogics2) Source # 
Instance details

Defined in Logic.Morphism

Methods

lub :: SublogicsPair sublogics1 sublogics2 -> SublogicsPair sublogics1 sublogics2 -> SublogicsPair sublogics1 sublogics2 Source #

top :: SublogicsPair sublogics1 sublogics2 Source #

isSubElem :: SemiLatticeWithTop l => l -> l -> Bool Source #

less or equal for semi lattices

class MinSublogic sublogic item where Source #

class providing the minimal sublogic of an item

Methods

minSublogic :: item -> sublogic Source #

Instances

Instances details
MinSublogic () a Source #

a default instance for no sublogics

Instance details

Defined in Logic.Logic

Methods

minSublogic :: a -> () Source #

MinSublogic CASL_DL_SL SYMB_MAP_ITEMS Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

MinSublogic CASL_DL_SL SYMB_ITEMS Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

MinSublogic CASL_DL_SL DL_BASIC_SPEC Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

MinSublogic CASL_DL_SL Symbol Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

MinSublogic CASL_DL_SL DLSign Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

MinSublogic CASL_DL_SL DLFORMULA Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

MinSublogic CASL_DL_SL DLMor Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

MinSublogic CommonLogicSL SYMB_ITEMS Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

MinSublogic CommonLogicSL SYMB_MAP_ITEMS Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

MinSublogic CommonLogicSL NAME Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

MinSublogic CommonLogicSL TEXT_META Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

MinSublogic CommonLogicSL BASIC_SPEC Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

MinSublogic CommonLogicSL Sign Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

MinSublogic CommonLogicSL Morphism Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

MinSublogic CommonLogicSL Symbol Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

MinSublogic Sublogic SymbMapItems Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

MinSublogic Sublogic SymbItems Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

MinSublogic Sublogic BasicSpec Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

MinSublogic Sublogic Symbol Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

MinSublogic Sublogic Morphism Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

MinSublogic Sublogic Env Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

MinSublogic Sublogic Sentence Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

MinSublogic HolLightSL () Source # 
Instance details

Defined in HolLight.Logic_HolLight

Methods

minSublogic :: () -> HolLightSL Source #

MinSublogic HolLightSL Sign Source # 
Instance details

Defined in HolLight.Logic_HolLight

MinSublogic HolLightSL Sentence Source # 
Instance details

Defined in HolLight.Logic_HolLight

MinSublogic HolLightSL HolLightMorphism Source # 
Instance details

Defined in HolLight.Logic_HolLight

MinSublogic ProfSub OntologyDocument Source # 
Instance details

Defined in OWL2.Logic_OWL2

MinSublogic ProfSub Axiom Source # 
Instance details

Defined in OWL2.Logic_OWL2

MinSublogic ProfSub Entity Source # 
Instance details

Defined in OWL2.Logic_OWL2

MinSublogic ProfSub Sign Source # 
Instance details

Defined in OWL2.Logic_OWL2

MinSublogic ProfSub SymbMapItems Source # 
Instance details

Defined in OWL2.Logic_OWL2

MinSublogic ProfSub SymbItems Source # 
Instance details

Defined in OWL2.Logic_OWL2

MinSublogic ProfSub OWLMorphism Source # 
Instance details

Defined in OWL2.Logic_OWL2

MinSublogic PropSL SYMB_MAP_ITEMS Source # 
Instance details

Defined in Propositional.Logic_Propositional

MinSublogic PropSL SYMB_ITEMS Source # 
Instance details

Defined in Propositional.Logic_Propositional

MinSublogic PropSL FORMULA Source # 
Instance details

Defined in Propositional.Logic_Propositional

MinSublogic PropSL BASIC_SPEC Source # 
Instance details

Defined in Propositional.Logic_Propositional

MinSublogic PropSL Sign Source # 
Instance details

Defined in Propositional.Logic_Propositional

MinSublogic PropSL Morphism Source # 
Instance details

Defined in Propositional.Logic_Propositional

MinSublogic PropSL Symbol Source # 
Instance details

Defined in Propositional.Logic_Propositional

MinSublogic QBFSL Sign Source # 
Instance details

Defined in QBF.Logic_QBF

MinSublogic QBFSL SYMBMAPITEMS Source # 
Instance details

Defined in QBF.Logic_QBF

MinSublogic QBFSL SYMBITEMS Source # 
Instance details

Defined in QBF.Logic_QBF

MinSublogic QBFSL FORMULA Source # 
Instance details

Defined in QBF.Logic_QBF

MinSublogic QBFSL BASICSPEC Source # 
Instance details

Defined in QBF.Logic_QBF

MinSublogic QBFSL Morphism Source # 
Instance details

Defined in QBF.Logic_QBF

MinSublogic QBFSL Symbol Source # 
Instance details

Defined in QBF.Logic_QBF

MinSublogic THFSl () Source # 
Instance details

Defined in THF.Logic_THF

Methods

minSublogic :: () -> THFSl Source #

MinSublogic THFSl DefinedType Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFUnaryConnective Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFPairConnective Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl Quantifier Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFQuantifier Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFSequent Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFAtom Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFBinaryType Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFUnitaryType Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFTopLevelType Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFSubType Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFTypeableFormula Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFTypeFormula Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFTypedConst Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFVariable Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFQuantifiedFormula Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFUnitaryFormula Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFBinaryTuple Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFBinaryFormula Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFLogicFormula Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl THFFormula Source # 
Instance details

Defined in THF.Sublogic

MinSublogic THFSl Kind Source # 
Instance details

Defined in THF.Logic_THF

MinSublogic THFSl Type Source # 
Instance details

Defined in THF.Logic_THF

MinSublogic THFSl SymbolTHF Source # 
Instance details

Defined in THF.Logic_THF

MinSublogic THFSl BasicSpecTHF Source # 
Instance details

Defined in THF.Logic_THF

MinSublogic THFSl SignTHF Source # 
Instance details

Defined in THF.Logic_THF

MinSublogic THFSl MorphismTHF Source # 
Instance details

Defined in THF.Logic_THF

MinSublogic Sublogic () Source # 
Instance details

Defined in TPTP.Logic_TPTP

Methods

minSublogic :: () -> Sublogic Source #

MinSublogic Sublogic BASIC_SPEC Source # 
Instance details

Defined in TPTP.Logic_TPTP

MinSublogic Sublogic Sign Source # 
Instance details

Defined in TPTP.Logic_TPTP

MinSublogic Sublogic Symbol Source # 
Instance details

Defined in TPTP.Logic_TPTP

MinSublogic Sublogic Sentence Source # 
Instance details

Defined in TPTP.Logic_TPTP

MinSublogic Sublogic Morphism Source # 
Instance details

Defined in TPTP.Logic_TPTP

Lattice a => MinSublogic (CASL_SL a) Symbol Source # 
Instance details

Defined in CASL.Logic_CASL

Lattice a => MinSublogic (CASL_SL a) SYMB_MAP_ITEMS Source # 
Instance details

Defined in CASL.Logic_CASL

Lattice a => MinSublogic (CASL_SL a) SYMB_ITEMS Source # 
Instance details

Defined in CASL.Logic_CASL

MinSL a f => MinSublogic (CASL_SL a) (FORMULA f) Source # 
Instance details

Defined in CASL.Logic_CASL

MinSL a e => MinSublogic (CASL_SL a) (Sign f e) Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

minSublogic :: Sign f e -> CASL_SL a Source #

MinSL a e => MinSublogic (CASL_SL a) (Morphism f e m) Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

minSublogic :: Morphism f e m -> CASL_SL a Source #

(MinSL a f, MinSL a s, MinSL a b) => MinSublogic (CASL_SL a) (BASIC_SPEC b s f) Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

minSublogic :: BASIC_SPEC b s f -> CASL_SL a Source #

(MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2) => MinSublogic (SublogicsPair sublogics1 sublogics2) alpha Source # 
Instance details

Defined in Logic.Morphism

Methods

minSublogic :: alpha -> SublogicsPair sublogics1 sublogics2 Source #

(SemiLatticeWithTop sublogics1, MinSublogic sublogics2 sentence2) => MinSublogic (SublogicsPair sublogics1 sublogics2) (S2 sentence2) Source # 
Instance details

Defined in Logic.Morphism

Methods

minSublogic :: S2 sentence2 -> SublogicsPair sublogics1 sublogics2 Source #

class MinSublogic sublogic item => ProjectSublogic sublogic item where Source #

class providing also the projection of an item to a sublogic

Methods

projectSublogic :: sublogic -> item -> item Source #

Instances

Instances details
ProjectSublogic () b Source #

a default instance for no sublogics

Instance details

Defined in Logic.Logic

Methods

projectSublogic :: () -> b -> b Source #

ProjectSublogic CASL_DL_SL DL_BASIC_SPEC Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

ProjectSublogic CASL_DL_SL Symbol Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

ProjectSublogic CASL_DL_SL DLSign Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

ProjectSublogic CASL_DL_SL DLMor Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

ProjectSublogic CommonLogicSL BASIC_SPEC Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

ProjectSublogic CommonLogicSL Sign Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

ProjectSublogic CommonLogicSL Morphism Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

ProjectSublogic Sublogic BasicSpec Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

ProjectSublogic Sublogic Morphism Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

ProjectSublogic Sublogic Env Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

ProjectSublogic HolLightSL () Source # 
Instance details

Defined in HolLight.Logic_HolLight

Methods

projectSublogic :: HolLightSL -> () -> () Source #

ProjectSublogic HolLightSL Sign Source # 
Instance details

Defined in HolLight.Logic_HolLight

ProjectSublogic HolLightSL HolLightMorphism Source # 
Instance details

Defined in HolLight.Logic_HolLight

ProjectSublogic ProfSub OntologyDocument Source # 
Instance details

Defined in OWL2.Logic_OWL2

ProjectSublogic ProfSub Sign Source # 
Instance details

Defined in OWL2.Logic_OWL2

ProjectSublogic ProfSub OWLMorphism Source # 
Instance details

Defined in OWL2.Logic_OWL2

ProjectSublogic PropSL BASIC_SPEC Source # 
Instance details

Defined in Propositional.Logic_Propositional

ProjectSublogic PropSL Sign Source # 
Instance details

Defined in Propositional.Logic_Propositional

ProjectSublogic PropSL Morphism Source # 
Instance details

Defined in Propositional.Logic_Propositional

ProjectSublogic QBFSL Sign Source # 
Instance details

Defined in QBF.Logic_QBF

ProjectSublogic QBFSL BASICSPEC Source # 
Instance details

Defined in QBF.Logic_QBF

ProjectSublogic QBFSL Morphism Source # 
Instance details

Defined in QBF.Logic_QBF

ProjectSublogic THFSl BasicSpecTHF Source # 
Instance details

Defined in THF.Logic_THF

ProjectSublogic THFSl SignTHF Source # 
Instance details

Defined in THF.Logic_THF

ProjectSublogic THFSl MorphismTHF Source # 
Instance details

Defined in THF.Logic_THF

ProjectSublogic Sublogic BASIC_SPEC Source # 
Instance details

Defined in TPTP.Logic_TPTP

ProjectSublogic Sublogic Sign Source # 
Instance details

Defined in TPTP.Logic_TPTP

ProjectSublogic Sublogic Sentence Source # 
Instance details

Defined in TPTP.Logic_TPTP

ProjectSublogic Sublogic Morphism Source # 
Instance details

Defined in TPTP.Logic_TPTP

MinSL a e => ProjectSublogic (CASL_SL a) (Sign f e) Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

projectSublogic :: CASL_SL a -> Sign f e -> Sign f e Source #

MinSL a e => ProjectSublogic (CASL_SL a) (Morphism f e m) Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

projectSublogic :: CASL_SL a -> Morphism f e m -> Morphism f e m Source #

(MinSL a f, MinSL a s, MinSL a b, ProjForm a f, ProjSigItem a s f, ProjBasic a b s f) => ProjectSublogic (CASL_SL a) (BASIC_SPEC b s f) Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

projectSublogic :: CASL_SL a -> BASIC_SPEC b s f -> BASIC_SPEC b s f Source #

(MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2) => ProjectSublogic (SublogicsPair sublogics1 sublogics2) alpha Source # 
Instance details

Defined in Logic.Morphism

Methods

projectSublogic :: SublogicsPair sublogics1 sublogics2 -> alpha -> alpha Source #

class MinSublogic sublogic item => ProjectSublogicM sublogic item where Source #

like ProjectSublogic, but providing a partial projection

Methods

projectSublogicM :: sublogic -> item -> Maybe item Source #

Instances

Instances details
ProjectSublogicM () b Source #

a default instance for no sublogics

Instance details

Defined in Logic.Logic

Methods

projectSublogicM :: () -> b -> Maybe b Source #

ProjectSublogicM CASL_DL_SL SYMB_MAP_ITEMS Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

ProjectSublogicM CASL_DL_SL SYMB_ITEMS Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

ProjectSublogicM CASL_DL_SL Symbol Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

ProjectSublogicM CommonLogicSL SYMB_ITEMS Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

ProjectSublogicM CommonLogicSL SYMB_MAP_ITEMS Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

ProjectSublogicM CommonLogicSL NAME Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

ProjectSublogicM CommonLogicSL Symbol Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

ProjectSublogicM Sublogic SymbMapItems Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

ProjectSublogicM Sublogic SymbItems Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

ProjectSublogicM Sublogic Symbol Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

ProjectSublogicM HolLightSL () Source # 
Instance details

Defined in HolLight.Logic_HolLight

Methods

projectSublogicM :: HolLightSL -> () -> Maybe () Source #

ProjectSublogicM ProfSub Entity Source # 
Instance details

Defined in OWL2.Logic_OWL2

ProjectSublogicM ProfSub SymbMapItems Source # 
Instance details

Defined in OWL2.Logic_OWL2

ProjectSublogicM ProfSub SymbItems Source # 
Instance details

Defined in OWL2.Logic_OWL2

ProjectSublogicM PropSL SYMB_MAP_ITEMS Source # 
Instance details

Defined in Propositional.Logic_Propositional

ProjectSublogicM PropSL SYMB_ITEMS Source # 
Instance details

Defined in Propositional.Logic_Propositional

ProjectSublogicM PropSL FORMULA Source # 
Instance details

Defined in Propositional.Logic_Propositional

ProjectSublogicM PropSL Symbol Source # 
Instance details

Defined in Propositional.Logic_Propositional

ProjectSublogicM QBFSL SYMBMAPITEMS Source # 
Instance details

Defined in QBF.Logic_QBF

ProjectSublogicM QBFSL SYMBITEMS Source # 
Instance details

Defined in QBF.Logic_QBF

ProjectSublogicM QBFSL FORMULA Source # 
Instance details

Defined in QBF.Logic_QBF

ProjectSublogicM QBFSL Symbol Source # 
Instance details

Defined in QBF.Logic_QBF

Methods

projectSublogicM :: QBFSL -> Symbol -> Maybe Symbol Source #

ProjectSublogicM THFSl () Source # 
Instance details

Defined in THF.Logic_THF

Methods

projectSublogicM :: THFSl -> () -> Maybe () Source #

ProjectSublogicM THFSl SymbolTHF Source # 
Instance details

Defined in THF.Logic_THF

ProjectSublogicM Sublogic () Source # 
Instance details

Defined in TPTP.Logic_TPTP

Methods

projectSublogicM :: Sublogic -> () -> Maybe () Source #

ProjectSublogicM Sublogic Symbol Source # 
Instance details

Defined in TPTP.Logic_TPTP

Lattice a => ProjectSublogicM (CASL_SL a) Symbol Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

projectSublogicM :: CASL_SL a -> Symbol -> Maybe Symbol Source #

Lattice a => ProjectSublogicM (CASL_SL a) SYMB_MAP_ITEMS Source # 
Instance details

Defined in CASL.Logic_CASL

Lattice a => ProjectSublogicM (CASL_SL a) SYMB_ITEMS Source # 
Instance details

Defined in CASL.Logic_CASL

(MinSublogic sublogics1 sign1, SemiLatticeWithTop sublogics2) => ProjectSublogicM (SublogicsPair sublogics1 sublogics2) sign1 Source # 
Instance details

Defined in Logic.Morphism

Methods

projectSublogicM :: SublogicsPair sublogics1 sublogics2 -> sign1 -> Maybe sign1 Source #

class SublogicName l where Source #

a class for providing a sublogi name

Methods

sublogicName :: l -> String Source #

Instances

Instances details
SublogicName () Source # 
Instance details

Defined in Logic.Logic

Methods

sublogicName :: () -> String Source #

SublogicName CASL_DL_SL Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Methods

sublogicName :: CASL_DL_SL -> String Source #

SublogicName CommonLogicSL Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

Methods

sublogicName :: CommonLogicSL -> String Source #

SublogicName Sublogic Source # 
Instance details

Defined in HasCASL.Logic_HasCASL

Methods

sublogicName :: Sublogic -> String Source #

SublogicName HolLightSL Source # 
Instance details

Defined in HolLight.Logic_HolLight

Methods

sublogicName :: HolLightSL -> String Source #

SublogicName ProfSub Source # 
Instance details

Defined in OWL2.Logic_OWL2

Methods

sublogicName :: ProfSub -> String Source #

SublogicName PropSL Source # 
Instance details

Defined in Propositional.Logic_Propositional

Methods

sublogicName :: PropSL -> String Source #

SublogicName QBFSL Source # 
Instance details

Defined in QBF.Logic_QBF

Methods

sublogicName :: QBFSL -> String Source #

SublogicName THFSl Source # 
Instance details

Defined in THF.Logic_THF

Methods

sublogicName :: THFSl -> String Source #

SublogicName Sublogic Source # 
Instance details

Defined in TPTP.Logic_TPTP

Methods

sublogicName :: Sublogic -> String Source #

NameSL a => SublogicName (CASL_SL a) Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

sublogicName :: CASL_SL a -> String Source #

(SublogicName sublogics1, SublogicName sublogics2) => SublogicName (SublogicsPair sublogics1 sublogics2) Source # 
Instance details

Defined in Logic.Morphism

Methods

sublogicName :: SublogicsPair sublogics1 sublogics2 -> String Source #

type SyntaxTable = (PrecMap, AssocMap) Source #

a type for syntax information eventually stored in the signature

class (StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol, SemiLatticeWithTop sublogics, MinSublogic sublogics sentence, ProjectSublogic sublogics basic_spec, ProjectSublogicM sublogics symb_items, ProjectSublogicM sublogics symb_map_items, ProjectSublogic sublogics sign, ProjectSublogic sublogics morphism, ProjectSublogicM sublogics symbol, Convertible sublogics, SublogicName sublogics, Ord proof_tree, Show proof_tree, Convertible proof_tree) => Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree | lid -> sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree where Source #

Minimal complete definition

Nothing

Methods

parse_basic_sen :: lid -> Maybe (basic_spec -> AParser st sentence) Source #

stability :: lid -> Stability Source #

stability of the implementation

data_logic :: lid -> Maybe AnyLogic Source #

for a process logic, return its data logic

top_sublogic :: lid -> sublogics Source #

the top sublogic, corresponding to the whole logic

all_sublogics :: lid -> [sublogics] Source #

list all the sublogics of the current logic

bottomSublogic :: lid -> Maybe sublogics Source #

sublogicDimensions :: lid -> [[sublogics]] Source #

parseSublogic :: lid -> String -> Maybe sublogics Source #

parse sublogic (override more efficiently)

proj_sublogic_epsilon :: lid -> sublogics -> sign -> morphism Source #

provide the embedding of a projected signature into the original signature

provers :: lid -> [Prover sign sentence morphism sublogics proof_tree] Source #

several provers can be provided. See module Logic.Prover

default_prover :: lid -> String Source #

name of default prover, empty if none available

cons_checkers :: lid -> [ConsChecker sign sentence sublogics morphism proof_tree] Source #

consistency checkers

conservativityCheck :: lid -> [ConservativityChecker sign sentence morphism] Source #

conservativity checkers

empty_proof_tree :: lid -> proof_tree Source #

the empty proof tree

syntaxTable :: lid -> sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: lid -> Maybe OMCD Source #

export_symToOmdoc :: lid -> NameMap symbol -> symbol -> String -> Result TCElement Source #

export_senToOmdoc :: lid -> NameMap symbol -> sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: lid -> SigMap symbol -> sign -> [Named sentence] -> Result [TCElement] Source #

additional information which has to be exported can be exported by this function

omdocToSym :: lid -> SigMapI symbol -> TCElement -> String -> Result symbol Source #

omdocToSen :: lid -> SigMapI symbol -> TCElement -> String -> Result (Maybe (Named sentence)) Source #

addOMadtToTheory :: lid -> SigMapI symbol -> (sign, [Named sentence]) -> [[OmdADT]] -> Result (sign, [Named sentence]) Source #

Algebraic Data Types are imported with this function. By default the input is returned without changes.

addOmdocToTheory :: lid -> SigMapI symbol -> (sign, [Named sentence]) -> [TCElement] -> Result (sign, [Named sentence]) Source #

additional information which has to be imported can be imported by this function. By default the input is returned without changes.

sublogicOfTheo :: lid -> (sign, [sentence]) -> sublogics Source #

sublogic of a theory

Instances

Instances details
Logic RelScheme () RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol () Source #

Instance of Logic for Relational Schemes

Instance details

Defined in RelationalScheme.Logic_Rel

Methods

parse_basic_sen :: RelScheme -> Maybe (RSScheme -> AParser st Sentence) Source #

stability :: RelScheme -> Stability Source #

data_logic :: RelScheme -> Maybe AnyLogic Source #

top_sublogic :: RelScheme -> () Source #

all_sublogics :: RelScheme -> [()] Source #

bottomSublogic :: RelScheme -> Maybe () Source #

sublogicDimensions :: RelScheme -> [[()]] Source #

parseSublogic :: RelScheme -> String -> Maybe () Source #

proj_sublogic_epsilon :: RelScheme -> () -> Sign -> RSMorphism Source #

provers :: RelScheme -> [Prover Sign Sentence RSMorphism () ()] Source #

default_prover :: RelScheme -> String Source #

cons_checkers :: RelScheme -> [ConsChecker Sign Sentence () RSMorphism ()] Source #

conservativityCheck :: RelScheme -> [ConservativityChecker Sign Sentence RSMorphism] Source #

empty_proof_tree :: RelScheme -> () Source #

syntaxTable :: RelScheme -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: RelScheme -> Maybe OMCD Source #

export_symToOmdoc :: RelScheme -> NameMap RSSymbol -> RSSymbol -> String -> Result TCElement Source #

export_senToOmdoc :: RelScheme -> NameMap RSSymbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: RelScheme -> SigMap RSSymbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: RelScheme -> SigMapI RSSymbol -> TCElement -> String -> Result RSSymbol Source #

omdocToSen :: RelScheme -> SigMapI RSSymbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: RelScheme -> SigMapI RSSymbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: RelScheme -> SigMapI RSSymbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

sublogicOfTheo :: RelScheme -> (Sign, [Sentence]) -> () Source #

Logic RDF RDFSub TurtleDocument Axiom SymbItems SymbMapItems Sign RDFMorphism RDFEntity RawSymb ProofTree Source # 
Instance details

Defined in RDF.Logic_RDF

Methods

parse_basic_sen :: RDF -> Maybe (TurtleDocument -> AParser st Axiom) Source #

stability :: RDF -> Stability Source #

data_logic :: RDF -> Maybe AnyLogic Source #

top_sublogic :: RDF -> RDFSub Source #

all_sublogics :: RDF -> [RDFSub] Source #

bottomSublogic :: RDF -> Maybe RDFSub Source #

sublogicDimensions :: RDF -> [[RDFSub]] Source #

parseSublogic :: RDF -> String -> Maybe RDFSub Source #

proj_sublogic_epsilon :: RDF -> RDFSub -> Sign -> RDFMorphism Source #

provers :: RDF -> [Prover Sign Axiom RDFMorphism RDFSub ProofTree] Source #

default_prover :: RDF -> String Source #

cons_checkers :: RDF -> [ConsChecker Sign Axiom RDFSub RDFMorphism ProofTree] Source #

conservativityCheck :: RDF -> [ConservativityChecker Sign Axiom RDFMorphism] Source #

empty_proof_tree :: RDF -> ProofTree Source #

syntaxTable :: RDF -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: RDF -> Maybe OMCD Source #

export_symToOmdoc :: RDF -> NameMap RDFEntity -> RDFEntity -> String -> Result TCElement Source #

export_senToOmdoc :: RDF -> NameMap RDFEntity -> Axiom -> Result TCorOMElement Source #

export_theoryToOmdoc :: RDF -> SigMap RDFEntity -> Sign -> [Named Axiom] -> Result [TCElement] Source #

omdocToSym :: RDF -> SigMapI RDFEntity -> TCElement -> String -> Result RDFEntity Source #

omdocToSen :: RDF -> SigMapI RDFEntity -> TCElement -> String -> Result (Maybe (Named Axiom)) Source #

addOMadtToTheory :: RDF -> SigMapI RDFEntity -> (Sign, [Named Axiom]) -> [[OmdADT]] -> Result (Sign, [Named Axiom]) Source #

addOmdocToTheory :: RDF -> SigMapI RDFEntity -> (Sign, [Named Axiom]) -> [TCElement] -> Result (Sign, [Named Axiom]) Source #

sublogicOfTheo :: RDF -> (Sign, [Axiom]) -> RDFSub Source #

Logic QVTR () Transformation Sen () () Sign Morphism () () () Source # 
Instance details

Defined in QVTR.Logic_QVTR

Methods

parse_basic_sen :: QVTR -> Maybe (Transformation -> AParser st Sen) Source #

stability :: QVTR -> Stability Source #

data_logic :: QVTR -> Maybe AnyLogic Source #

top_sublogic :: QVTR -> () Source #

all_sublogics :: QVTR -> [()] Source #

bottomSublogic :: QVTR -> Maybe () Source #

sublogicDimensions :: QVTR -> [[()]] Source #

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

proj_sublogic_epsilon :: QVTR -> () -> Sign -> Morphism Source #

provers :: QVTR -> [Prover Sign Sen Morphism () ()] Source #

default_prover :: QVTR -> String Source #

cons_checkers :: QVTR -> [ConsChecker Sign Sen () Morphism ()] Source #

conservativityCheck :: QVTR -> [ConservativityChecker Sign Sen Morphism] Source #

empty_proof_tree :: QVTR -> () Source #

syntaxTable :: QVTR -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: QVTR -> Maybe OMCD Source #

export_symToOmdoc :: QVTR -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: QVTR -> NameMap () -> Sen -> Result TCorOMElement Source #

export_theoryToOmdoc :: QVTR -> SigMap () -> Sign -> [Named Sen] -> Result [TCElement] Source #

omdocToSym :: QVTR -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: QVTR -> SigMapI () -> TCElement -> String -> Result (Maybe (Named Sen)) Source #

addOMadtToTheory :: QVTR -> SigMapI () -> (Sign, [Named Sen]) -> [[OmdADT]] -> Result (Sign, [Named Sen]) Source #

addOmdocToTheory :: QVTR -> SigMapI () -> (Sign, [Named Sen]) -> [TCElement] -> Result (Sign, [Named Sen]) Source #

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

Logic OMDoc_PUN () () () () () OMDoc_Sign OMDoc_Morphism Symbol () () Source # 
Instance details

Defined in OMDoc.Logic_OMDoc

Methods

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

stability :: OMDoc_PUN -> Stability Source #

data_logic :: OMDoc_PUN -> Maybe AnyLogic Source #

top_sublogic :: OMDoc_PUN -> () Source #

all_sublogics :: OMDoc_PUN -> [()] Source #

bottomSublogic :: OMDoc_PUN -> Maybe () Source #

sublogicDimensions :: OMDoc_PUN -> [[()]] Source #

parseSublogic :: OMDoc_PUN -> String -> Maybe () Source #

proj_sublogic_epsilon :: OMDoc_PUN -> () -> OMDoc_Sign -> OMDoc_Morphism Source #

provers :: OMDoc_PUN -> [Prover OMDoc_Sign () OMDoc_Morphism () ()] Source #

default_prover :: OMDoc_PUN -> String Source #

cons_checkers :: OMDoc_PUN -> [ConsChecker OMDoc_Sign () () OMDoc_Morphism ()] Source #

conservativityCheck :: OMDoc_PUN -> [ConservativityChecker OMDoc_Sign () OMDoc_Morphism] Source #

empty_proof_tree :: OMDoc_PUN -> () Source #

syntaxTable :: OMDoc_PUN -> OMDoc_Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: OMDoc_PUN -> Maybe OMCD Source #

export_symToOmdoc :: OMDoc_PUN -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: OMDoc_PUN -> NameMap Symbol -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: OMDoc_PUN -> SigMap Symbol -> OMDoc_Sign -> [Named ()] -> Result [TCElement] Source #

omdocToSym :: OMDoc_PUN -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: OMDoc_PUN -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ())) Source #

addOMadtToTheory :: OMDoc_PUN -> SigMapI Symbol -> (OMDoc_Sign, [Named ()]) -> [[OmdADT]] -> Result (OMDoc_Sign, [Named ()]) Source #

addOmdocToTheory :: OMDoc_PUN -> SigMapI Symbol -> (OMDoc_Sign, [Named ()]) -> [TCElement] -> Result (OMDoc_Sign, [Named ()]) Source #

sublogicOfTheo :: OMDoc_PUN -> (OMDoc_Sign, [()]) -> () Source #

Logic Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () Source #

Instance of Logic for Maude

Instance details

Defined in Maude.Logic_Maude

Methods

parse_basic_sen :: Maude -> Maybe (MaudeText -> AParser st Sentence) Source #

stability :: Maude -> Stability Source #

data_logic :: Maude -> Maybe AnyLogic Source #

top_sublogic :: Maude -> () Source #

all_sublogics :: Maude -> [()] Source #

bottomSublogic :: Maude -> Maybe () Source #

sublogicDimensions :: Maude -> [[()]] Source #

parseSublogic :: Maude -> String -> Maybe () Source #

proj_sublogic_epsilon :: Maude -> () -> Sign -> Morphism Source #

provers :: Maude -> [Prover Sign Sentence Morphism () ()] Source #

default_prover :: Maude -> String Source #

cons_checkers :: Maude -> [ConsChecker Sign Sentence () Morphism ()] Source #

conservativityCheck :: Maude -> [ConservativityChecker Sign Sentence Morphism] Source #

empty_proof_tree :: Maude -> () Source #

syntaxTable :: Maude -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Maude -> Maybe OMCD Source #

export_symToOmdoc :: Maude -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Maude -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: Maude -> SigMap Symbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: Maude -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Maude -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: Maude -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: Maude -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

sublogicOfTheo :: Maude -> (Sign, [Sentence]) -> () Source #

Logic THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Instance details

Defined in THF.Logic_THF

Methods

parse_basic_sen :: THF -> Maybe (BasicSpecTHF -> AParser st THFFormula) Source #

stability :: THF -> Stability Source #

data_logic :: THF -> Maybe AnyLogic Source #

top_sublogic :: THF -> THFSl Source #

all_sublogics :: THF -> [THFSl] Source #

bottomSublogic :: THF -> Maybe THFSl Source #

sublogicDimensions :: THF -> [[THFSl]] Source #

parseSublogic :: THF -> String -> Maybe THFSl Source #

proj_sublogic_epsilon :: THF -> THFSl -> SignTHF -> MorphismTHF Source #

provers :: THF -> [Prover SignTHF THFFormula MorphismTHF THFSl ProofTree] Source #

default_prover :: THF -> String Source #

cons_checkers :: THF -> [ConsChecker SignTHF THFFormula THFSl MorphismTHF ProofTree] Source #

conservativityCheck :: THF -> [ConservativityChecker SignTHF THFFormula MorphismTHF] Source #

empty_proof_tree :: THF -> ProofTree Source #

syntaxTable :: THF -> SignTHF -> Maybe SyntaxTable Source #

omdoc_metatheory :: THF -> Maybe OMCD Source #

export_symToOmdoc :: THF -> NameMap SymbolTHF -> SymbolTHF -> String -> Result TCElement Source #

export_senToOmdoc :: THF -> NameMap SymbolTHF -> THFFormula -> Result TCorOMElement Source #

export_theoryToOmdoc :: THF -> SigMap SymbolTHF -> SignTHF -> [Named THFFormula] -> Result [TCElement] Source #

omdocToSym :: THF -> SigMapI SymbolTHF -> TCElement -> String -> Result SymbolTHF Source #

omdocToSen :: THF -> SigMapI SymbolTHF -> TCElement -> String -> Result (Maybe (Named THFFormula)) Source #

addOMadtToTheory :: THF -> SigMapI SymbolTHF -> (SignTHF, [Named THFFormula]) -> [[OmdADT]] -> Result (SignTHF, [Named THFFormula]) Source #

addOmdocToTheory :: THF -> SigMapI SymbolTHF -> (SignTHF, [Named THFFormula]) -> [TCElement] -> Result (SignTHF, [Named THFFormula]) Source #

sublogicOfTheo :: THF -> (SignTHF, [THFFormula]) -> THFSl Source #

Logic TPTP Sublogic BASIC_SPEC Sentence () () Sign Morphism Symbol () ProofTree Source # 
Instance details

Defined in TPTP.Logic_TPTP

Methods

parse_basic_sen :: TPTP -> Maybe (BASIC_SPEC -> AParser st Sentence) Source #

stability :: TPTP -> Stability Source #

data_logic :: TPTP -> Maybe AnyLogic Source #

top_sublogic :: TPTP -> Sublogic Source #

all_sublogics :: TPTP -> [Sublogic] Source #

bottomSublogic :: TPTP -> Maybe Sublogic Source #

sublogicDimensions :: TPTP -> [[Sublogic]] Source #

parseSublogic :: TPTP -> String -> Maybe Sublogic Source #

proj_sublogic_epsilon :: TPTP -> Sublogic -> Sign -> Morphism Source #

provers :: TPTP -> [Prover Sign Sentence Morphism Sublogic ProofTree] Source #

default_prover :: TPTP -> String Source #

cons_checkers :: TPTP -> [ConsChecker Sign Sentence Sublogic Morphism ProofTree] Source #

conservativityCheck :: TPTP -> [ConservativityChecker Sign Sentence Morphism] Source #

empty_proof_tree :: TPTP -> ProofTree Source #

syntaxTable :: TPTP -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: TPTP -> Maybe OMCD Source #

export_symToOmdoc :: TPTP -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: TPTP -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: TPTP -> SigMap Symbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: TPTP -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: TPTP -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: TPTP -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: TPTP -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

sublogicOfTheo :: TPTP -> (Sign, [Sentence]) -> Sublogic Source #

Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source #

Instance of Logic for propositional logc

Instance details

Defined in QBF.Logic_QBF

Methods

parse_basic_sen :: QBF -> Maybe (BASICSPEC -> AParser st FORMULA) Source #

stability :: QBF -> Stability Source #

data_logic :: QBF -> Maybe AnyLogic Source #

top_sublogic :: QBF -> QBFSL Source #

all_sublogics :: QBF -> [QBFSL] Source #

bottomSublogic :: QBF -> Maybe QBFSL Source #

sublogicDimensions :: QBF -> [[QBFSL]] Source #

parseSublogic :: QBF -> String -> Maybe QBFSL Source #

proj_sublogic_epsilon :: QBF -> QBFSL -> Sign -> Morphism Source #

provers :: QBF -> [Prover Sign FORMULA Morphism QBFSL ProofTree] Source #

default_prover :: QBF -> String Source #

cons_checkers :: QBF -> [ConsChecker Sign FORMULA QBFSL Morphism ProofTree] Source #

conservativityCheck :: QBF -> [ConservativityChecker Sign FORMULA Morphism] Source #

empty_proof_tree :: QBF -> ProofTree Source #

syntaxTable :: QBF -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: QBF -> Maybe OMCD Source #

export_symToOmdoc :: QBF -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: QBF -> NameMap Symbol -> FORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: QBF -> SigMap Symbol -> Sign -> [Named FORMULA] -> Result [TCElement] Source #

omdocToSym :: QBF -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: QBF -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source #

addOMadtToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source #

addOmdocToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source #

sublogicOfTheo :: QBF -> (Sign, [FORMULA]) -> QBFSL Source #

Logic Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #

Instance of Logic for propositional logc

Instance details

Defined in Propositional.Logic_Propositional

Methods

parse_basic_sen :: Propositional -> Maybe (BASIC_SPEC -> AParser st FORMULA) Source #

stability :: Propositional -> Stability Source #

data_logic :: Propositional -> Maybe AnyLogic Source #

top_sublogic :: Propositional -> PropSL Source #

all_sublogics :: Propositional -> [PropSL] Source #

bottomSublogic :: Propositional -> Maybe PropSL Source #

sublogicDimensions :: Propositional -> [[PropSL]] Source #

parseSublogic :: Propositional -> String -> Maybe PropSL Source #

proj_sublogic_epsilon :: Propositional -> PropSL -> Sign -> Morphism Source #

provers :: Propositional -> [Prover Sign FORMULA Morphism PropSL ProofTree] Source #

default_prover :: Propositional -> String Source #

cons_checkers :: Propositional -> [ConsChecker Sign FORMULA PropSL Morphism ProofTree] Source #

conservativityCheck :: Propositional -> [ConservativityChecker Sign FORMULA Morphism] Source #

empty_proof_tree :: Propositional -> ProofTree Source #

syntaxTable :: Propositional -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Propositional -> Maybe OMCD Source #

export_symToOmdoc :: Propositional -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Propositional -> NameMap Symbol -> FORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: Propositional -> SigMap Symbol -> Sign -> [Named FORMULA] -> Result [TCElement] Source #

omdocToSym :: Propositional -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Propositional -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source #

addOMadtToTheory :: Propositional -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source #

addOmdocToTheory :: Propositional -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source #

sublogicOfTheo :: Propositional -> (Sign, [FORMULA]) -> PropSL Source #

Logic OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source # 
Instance details

Defined in OWL2.Logic_OWL2

Methods

parse_basic_sen :: OWL2 -> Maybe (OntologyDocument -> AParser st Axiom) Source #

stability :: OWL2 -> Stability Source #

data_logic :: OWL2 -> Maybe AnyLogic Source #

top_sublogic :: OWL2 -> ProfSub Source #

all_sublogics :: OWL2 -> [ProfSub] Source #

bottomSublogic :: OWL2 -> Maybe ProfSub Source #

sublogicDimensions :: OWL2 -> [[ProfSub]] Source #

parseSublogic :: OWL2 -> String -> Maybe ProfSub Source #

proj_sublogic_epsilon :: OWL2 -> ProfSub -> Sign -> OWLMorphism Source #

provers :: OWL2 -> [Prover Sign Axiom OWLMorphism ProfSub ProofTree] Source #

default_prover :: OWL2 -> String Source #

cons_checkers :: OWL2 -> [ConsChecker Sign Axiom ProfSub OWLMorphism ProofTree] Source #

conservativityCheck :: OWL2 -> [ConservativityChecker Sign Axiom OWLMorphism] Source #

empty_proof_tree :: OWL2 -> ProofTree Source #

syntaxTable :: OWL2 -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: OWL2 -> Maybe OMCD Source #

export_symToOmdoc :: OWL2 -> NameMap Entity -> Entity -> String -> Result TCElement Source #

export_senToOmdoc :: OWL2 -> NameMap Entity -> Axiom -> Result TCorOMElement Source #

export_theoryToOmdoc :: OWL2 -> SigMap Entity -> Sign -> [Named Axiom] -> Result [TCElement] Source #

omdocToSym :: OWL2 -> SigMapI Entity -> TCElement -> String -> Result Entity Source #

omdocToSen :: OWL2 -> SigMapI Entity -> TCElement -> String -> Result (Maybe (Named Axiom)) Source #

addOMadtToTheory :: OWL2 -> SigMapI Entity -> (Sign, [Named Axiom]) -> [[OmdADT]] -> Result (Sign, [Named Axiom]) Source #

addOmdocToTheory :: OWL2 -> SigMapI Entity -> (Sign, [Named Axiom]) -> [TCElement] -> Result (Sign, [Named Axiom]) Source #

sublogicOfTheo :: OWL2 -> (Sign, [Axiom]) -> ProfSub Source #

Logic NeSyPatterns () BASIC_SPEC () SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #

Instance of Logic for propositional logc

Instance details

Defined in NeSyPatterns.Logic_NeSyPatterns

Methods

parse_basic_sen :: NeSyPatterns -> Maybe (BASIC_SPEC -> AParser st ()) Source #

stability :: NeSyPatterns -> Stability Source #

data_logic :: NeSyPatterns -> Maybe AnyLogic Source #

top_sublogic :: NeSyPatterns -> () Source #

all_sublogics :: NeSyPatterns -> [()] Source #

bottomSublogic :: NeSyPatterns -> Maybe () Source #

sublogicDimensions :: NeSyPatterns -> [[()]] Source #

parseSublogic :: NeSyPatterns -> String -> Maybe () Source #

proj_sublogic_epsilon :: NeSyPatterns -> () -> Sign -> Morphism Source #

provers :: NeSyPatterns -> [Prover Sign () Morphism () ProofTree] Source #

default_prover :: NeSyPatterns -> String Source #

cons_checkers :: NeSyPatterns -> [ConsChecker Sign () () Morphism ProofTree] Source #

conservativityCheck :: NeSyPatterns -> [ConservativityChecker Sign () Morphism] Source #

empty_proof_tree :: NeSyPatterns -> ProofTree Source #

syntaxTable :: NeSyPatterns -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: NeSyPatterns -> Maybe OMCD Source #

export_symToOmdoc :: NeSyPatterns -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: NeSyPatterns -> NameMap Symbol -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: NeSyPatterns -> SigMap Symbol -> Sign -> [Named ()] -> Result [TCElement] Source #

omdocToSym :: NeSyPatterns -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: NeSyPatterns -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ())) Source #

addOMadtToTheory :: NeSyPatterns -> SigMapI Symbol -> (Sign, [Named ()]) -> [[OmdADT]] -> Result (Sign, [Named ()]) Source #

addOmdocToTheory :: NeSyPatterns -> SigMapI Symbol -> (Sign, [Named ()]) -> [TCElement] -> Result (Sign, [Named ()]) Source #

sublogicOfTheo :: NeSyPatterns -> (Sign, [()]) -> () Source #

Logic LF () BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RAW_SYM () Source # 
Instance details

Defined in LF.Logic_LF

Methods

parse_basic_sen :: LF -> Maybe (BASIC_SPEC -> AParser st Sentence) Source #

stability :: LF -> Stability Source #

data_logic :: LF -> Maybe AnyLogic Source #

top_sublogic :: LF -> () Source #

all_sublogics :: LF -> [()] Source #

bottomSublogic :: LF -> Maybe () Source #

sublogicDimensions :: LF -> [[()]] Source #

parseSublogic :: LF -> String -> Maybe () Source #

proj_sublogic_epsilon :: LF -> () -> Sign -> Morphism Source #

provers :: LF -> [Prover Sign Sentence Morphism () ()] Source #

default_prover :: LF -> String Source #

cons_checkers :: LF -> [ConsChecker Sign Sentence () Morphism ()] Source #

conservativityCheck :: LF -> [ConservativityChecker Sign Sentence Morphism] Source #

empty_proof_tree :: LF -> () Source #

syntaxTable :: LF -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: LF -> Maybe OMCD Source #

export_symToOmdoc :: LF -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: LF -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: LF -> SigMap Symbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: LF -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: LF -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: LF -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: LF -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

sublogicOfTheo :: LF -> (Sign, [Sentence]) -> () Source #

Logic Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Isabelle.Logic_Isabelle

Methods

parse_basic_sen :: Isabelle -> Maybe (() -> AParser st Sentence) Source #

stability :: Isabelle -> Stability Source #

data_logic :: Isabelle -> Maybe AnyLogic Source #

top_sublogic :: Isabelle -> () Source #

all_sublogics :: Isabelle -> [()] Source #

bottomSublogic :: Isabelle -> Maybe () Source #

sublogicDimensions :: Isabelle -> [[()]] Source #

parseSublogic :: Isabelle -> String -> Maybe () Source #

proj_sublogic_epsilon :: Isabelle -> () -> Sign -> IsabelleMorphism Source #

provers :: Isabelle -> [Prover Sign Sentence IsabelleMorphism () ()] Source #

default_prover :: Isabelle -> String Source #

cons_checkers :: Isabelle -> [ConsChecker Sign Sentence () IsabelleMorphism ()] Source #

conservativityCheck :: Isabelle -> [ConservativityChecker Sign Sentence IsabelleMorphism] Source #

empty_proof_tree :: Isabelle -> () Source #

syntaxTable :: Isabelle -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Isabelle -> Maybe OMCD Source #

export_symToOmdoc :: Isabelle -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: Isabelle -> NameMap () -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: Isabelle -> SigMap () -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: Isabelle -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: Isabelle -> SigMapI () -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: Isabelle -> SigMapI () -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: Isabelle -> SigMapI () -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

sublogicOfTheo :: Isabelle -> (Sign, [Sentence]) -> () Source #

Logic HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Source #

Instance of Logic for propositional logc

Instance details

Defined in HolLight.Logic_HolLight

Methods

parse_basic_sen :: HolLight -> Maybe (() -> AParser st Sentence) Source #

stability :: HolLight -> Stability Source #

data_logic :: HolLight -> Maybe AnyLogic Source #

top_sublogic :: HolLight -> HolLightSL Source #

all_sublogics :: HolLight -> [HolLightSL] Source #

bottomSublogic :: HolLight -> Maybe HolLightSL Source #

sublogicDimensions :: HolLight -> [[HolLightSL]] Source #

parseSublogic :: HolLight -> String -> Maybe HolLightSL Source #

proj_sublogic_epsilon :: HolLight -> HolLightSL -> Sign -> HolLightMorphism Source #

provers :: HolLight -> [Prover Sign Sentence HolLightMorphism HolLightSL ()] Source #

default_prover :: HolLight -> String Source #

cons_checkers :: HolLight -> [ConsChecker Sign Sentence HolLightSL HolLightMorphism ()] Source #

conservativityCheck :: HolLight -> [ConservativityChecker Sign Sentence HolLightMorphism] Source #

empty_proof_tree :: HolLight -> () Source #

syntaxTable :: HolLight -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: HolLight -> Maybe OMCD Source #

export_symToOmdoc :: HolLight -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: HolLight -> NameMap () -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: HolLight -> SigMap () -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: HolLight -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: HolLight -> SigMapI () -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: HolLight -> SigMapI () -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: HolLight -> SigMapI () -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

sublogicOfTheo :: HolLight -> (Sign, [Sentence]) -> HolLightSL Source #

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

Defined in HasCASL.Logic_HasCASL

Methods

parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source #

stability :: HasCASL -> Stability Source #

data_logic :: HasCASL -> Maybe AnyLogic Source #

top_sublogic :: HasCASL -> Sublogic Source #

all_sublogics :: HasCASL -> [Sublogic] Source #

bottomSublogic :: HasCASL -> Maybe Sublogic Source #

sublogicDimensions :: HasCASL -> [[Sublogic]] Source #

parseSublogic :: HasCASL -> String -> Maybe Sublogic Source #

proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source #

provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source #

default_prover :: HasCASL -> String Source #

cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source #

conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source #

empty_proof_tree :: HasCASL -> () Source #

syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source #

omdoc_metatheory :: HasCASL -> Maybe OMCD Source #

export_symToOmdoc :: HasCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source #

addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source #

sublogicOfTheo :: HasCASL -> (Env, [Sentence]) -> Sublogic Source #

Logic FrameworkCom () ComorphismDef () () () ComorphismDef MorphismCom () () () Source # 
Instance details

Defined in Framework.Logic_Framework

Methods

parse_basic_sen :: FrameworkCom -> Maybe (ComorphismDef -> AParser st ()) Source #

stability :: FrameworkCom -> Stability Source #

data_logic :: FrameworkCom -> Maybe AnyLogic Source #

top_sublogic :: FrameworkCom -> () Source #

all_sublogics :: FrameworkCom -> [()] Source #

bottomSublogic :: FrameworkCom -> Maybe () Source #

sublogicDimensions :: FrameworkCom -> [[()]] Source #

parseSublogic :: FrameworkCom -> String -> Maybe () Source #

proj_sublogic_epsilon :: FrameworkCom -> () -> ComorphismDef -> MorphismCom Source #

provers :: FrameworkCom -> [Prover ComorphismDef () MorphismCom () ()] Source #

default_prover :: FrameworkCom -> String Source #

cons_checkers :: FrameworkCom -> [ConsChecker ComorphismDef () () MorphismCom ()] Source #

conservativityCheck :: FrameworkCom -> [ConservativityChecker ComorphismDef () MorphismCom] Source #

empty_proof_tree :: FrameworkCom -> () Source #

syntaxTable :: FrameworkCom -> ComorphismDef -> Maybe SyntaxTable Source #

omdoc_metatheory :: FrameworkCom -> Maybe OMCD Source #

export_symToOmdoc :: FrameworkCom -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: FrameworkCom -> NameMap () -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: FrameworkCom -> SigMap () -> ComorphismDef -> [Named ()] -> Result [TCElement] Source #

omdocToSym :: FrameworkCom -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: FrameworkCom -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source #

addOMadtToTheory :: FrameworkCom -> SigMapI () -> (ComorphismDef, [Named ()]) -> [[OmdADT]] -> Result (ComorphismDef, [Named ()]) Source #

addOmdocToTheory :: FrameworkCom -> SigMapI () -> (ComorphismDef, [Named ()]) -> [TCElement] -> Result (ComorphismDef, [Named ()]) Source #

sublogicOfTheo :: FrameworkCom -> (ComorphismDef, [()]) -> () Source #

Logic Framework () LogicDef () () () LogicDef Morphism () () () Source # 
Instance details

Defined in Framework.Logic_Framework

Methods

parse_basic_sen :: Framework -> Maybe (LogicDef -> AParser st ()) Source #

stability :: Framework -> Stability Source #

data_logic :: Framework -> Maybe AnyLogic Source #

top_sublogic :: Framework -> () Source #

all_sublogics :: Framework -> [()] Source #

bottomSublogic :: Framework -> Maybe () Source #

sublogicDimensions :: Framework -> [[()]] Source #

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

proj_sublogic_epsilon :: Framework -> () -> LogicDef -> Morphism Source #

provers :: Framework -> [Prover LogicDef () Morphism () ()] Source #

default_prover :: Framework -> String Source #

cons_checkers :: Framework -> [ConsChecker LogicDef () () Morphism ()] Source #

conservativityCheck :: Framework -> [ConservativityChecker LogicDef () Morphism] Source #

empty_proof_tree :: Framework -> () Source #

syntaxTable :: Framework -> LogicDef -> Maybe SyntaxTable Source #

omdoc_metatheory :: Framework -> Maybe OMCD Source #

export_symToOmdoc :: Framework -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: Framework -> NameMap () -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: Framework -> SigMap () -> LogicDef -> [Named ()] -> Result [TCElement] Source #

omdocToSym :: Framework -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: Framework -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source #

addOMadtToTheory :: Framework -> SigMapI () -> (LogicDef, [Named ()]) -> [[OmdADT]] -> Result (LogicDef, [Named ()]) Source #

addOmdocToTheory :: Framework -> SigMapI () -> (LogicDef, [Named ()]) -> [TCElement] -> Result (LogicDef, [Named ()]) Source #

sublogicOfTheo :: Framework -> (LogicDef, [()]) -> () Source #

Logic DFOL () BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol () Source # 
Instance details

Defined in DFOL.Logic_DFOL

Methods

parse_basic_sen :: DFOL -> Maybe (BASIC_SPEC -> AParser st FORMULA) Source #

stability :: DFOL -> Stability Source #

data_logic :: DFOL -> Maybe AnyLogic Source #

top_sublogic :: DFOL -> () Source #

all_sublogics :: DFOL -> [()] Source #

bottomSublogic :: DFOL -> Maybe () Source #

sublogicDimensions :: DFOL -> [[()]] Source #

parseSublogic :: DFOL -> String -> Maybe () Source #

proj_sublogic_epsilon :: DFOL -> () -> Sign -> Morphism Source #

provers :: DFOL -> [Prover Sign FORMULA Morphism () ()] Source #

default_prover :: DFOL -> String Source #

cons_checkers :: DFOL -> [ConsChecker Sign FORMULA () Morphism ()] Source #

conservativityCheck :: DFOL -> [ConservativityChecker Sign FORMULA Morphism] Source #

empty_proof_tree :: DFOL -> () Source #

syntaxTable :: DFOL -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: DFOL -> Maybe OMCD Source #

export_symToOmdoc :: DFOL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: DFOL -> NameMap Symbol -> FORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: DFOL -> SigMap Symbol -> Sign -> [Named FORMULA] -> Result [TCElement] Source #

omdocToSym :: DFOL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: DFOL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source #

addOMadtToTheory :: DFOL -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source #

addOmdocToTheory :: DFOL -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source #

sublogicOfTheo :: DFOL -> (Sign, [FORMULA]) -> () Source #

Logic CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Instance details

Defined in CommonLogic.Logic_CommonLogic

Methods

parse_basic_sen :: CommonLogic -> Maybe (BASIC_SPEC -> AParser st TEXT_META) Source #

stability :: CommonLogic -> Stability Source #

data_logic :: CommonLogic -> Maybe AnyLogic Source #

top_sublogic :: CommonLogic -> CommonLogicSL Source #

all_sublogics :: CommonLogic -> [CommonLogicSL] Source #

bottomSublogic :: CommonLogic -> Maybe CommonLogicSL Source #

sublogicDimensions :: CommonLogic -> [[CommonLogicSL]] Source #

parseSublogic :: CommonLogic -> String -> Maybe CommonLogicSL Source #

proj_sublogic_epsilon :: CommonLogic -> CommonLogicSL -> Sign -> Morphism Source #

provers :: CommonLogic -> [Prover Sign TEXT_META Morphism CommonLogicSL ProofTree] Source #

default_prover :: CommonLogic -> String Source #

cons_checkers :: CommonLogic -> [ConsChecker Sign TEXT_META CommonLogicSL Morphism ProofTree] Source #

conservativityCheck :: CommonLogic -> [ConservativityChecker Sign TEXT_META Morphism] Source #

empty_proof_tree :: CommonLogic -> ProofTree Source #

syntaxTable :: CommonLogic -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CommonLogic -> Maybe OMCD Source #

export_symToOmdoc :: CommonLogic -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CommonLogic -> NameMap Symbol -> TEXT_META -> Result TCorOMElement Source #

export_theoryToOmdoc :: CommonLogic -> SigMap Symbol -> Sign -> [Named TEXT_META] -> Result [TCElement] Source #

omdocToSym :: CommonLogic -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CommonLogic -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named TEXT_META)) Source #

addOMadtToTheory :: CommonLogic -> SigMapI Symbol -> (Sign, [Named TEXT_META]) -> [[OmdADT]] -> Result (Sign, [Named TEXT_META]) Source #

addOmdocToTheory :: CommonLogic -> SigMapI Symbol -> (Sign, [Named TEXT_META]) -> [TCElement] -> Result (Sign, [Named TEXT_META]) Source #

sublogicOfTheo :: CommonLogic -> (Sign, [TEXT_META]) -> CommonLogicSL Source #

Logic CSMOF () Metamodel Sen () () Sign Morphism () () () Source # 
Instance details

Defined in CSMOF.Logic_CSMOF

Methods

parse_basic_sen :: CSMOF -> Maybe (Metamodel -> AParser st Sen) Source #

stability :: CSMOF -> Stability Source #

data_logic :: CSMOF -> Maybe AnyLogic Source #

top_sublogic :: CSMOF -> () Source #

all_sublogics :: CSMOF -> [()] Source #

bottomSublogic :: CSMOF -> Maybe () Source #

sublogicDimensions :: CSMOF -> [[()]] Source #

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

proj_sublogic_epsilon :: CSMOF -> () -> Sign -> Morphism Source #

provers :: CSMOF -> [Prover Sign Sen Morphism () ()] Source #

default_prover :: CSMOF -> String Source #

cons_checkers :: CSMOF -> [ConsChecker Sign Sen () Morphism ()] Source #

conservativityCheck :: CSMOF -> [ConservativityChecker Sign Sen Morphism] Source #

empty_proof_tree :: CSMOF -> () Source #

syntaxTable :: CSMOF -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CSMOF -> Maybe OMCD Source #

export_symToOmdoc :: CSMOF -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: CSMOF -> NameMap () -> Sen -> Result TCorOMElement Source #

export_theoryToOmdoc :: CSMOF -> SigMap () -> Sign -> [Named Sen] -> Result [TCElement] Source #

omdocToSym :: CSMOF -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: CSMOF -> SigMapI () -> TCElement -> String -> Result (Maybe (Named Sen)) Source #

addOMadtToTheory :: CSMOF -> SigMapI () -> (Sign, [Named Sen]) -> [[OmdADT]] -> Result (Sign, [Named Sen]) Source #

addOmdocToTheory :: CSMOF -> SigMapI () -> (Sign, [Named Sen]) -> [TCElement] -> Result (Sign, [Named Sen]) Source #

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

Logic Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Adl.Logic_Adl

Methods

parse_basic_sen :: Adl -> Maybe (Context -> AParser st Sen) Source #

stability :: Adl -> Stability Source #

data_logic :: Adl -> Maybe AnyLogic Source #

top_sublogic :: Adl -> () Source #

all_sublogics :: Adl -> [()] Source #

bottomSublogic :: Adl -> Maybe () Source #

sublogicDimensions :: Adl -> [[()]] Source #

parseSublogic :: Adl -> String -> Maybe () Source #

proj_sublogic_epsilon :: Adl -> () -> Sign -> Morphism Source #

provers :: Adl -> [Prover Sign Sen Morphism () ProofTree] Source #

default_prover :: Adl -> String Source #

cons_checkers :: Adl -> [ConsChecker Sign Sen () Morphism ProofTree] Source #

conservativityCheck :: Adl -> [ConservativityChecker Sign Sen Morphism] Source #

empty_proof_tree :: Adl -> ProofTree Source #

syntaxTable :: Adl -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Adl -> Maybe OMCD Source #

export_symToOmdoc :: Adl -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Adl -> NameMap Symbol -> Sen -> Result TCorOMElement Source #

export_theoryToOmdoc :: Adl -> SigMap Symbol -> Sign -> [Named Sen] -> Result [TCElement] Source #

omdocToSym :: Adl -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Adl -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sen)) Source #

addOMadtToTheory :: Adl -> SigMapI Symbol -> (Sign, [Named Sen]) -> [[OmdADT]] -> Result (Sign, [Named Sen]) Source #

addOmdocToTheory :: Adl -> SigMapI Symbol -> (Sign, [Named Sen]) -> [TCElement] -> Result (Sign, [Named Sen]) Source #

sublogicOfTheo :: Adl -> (Sign, [Sen]) -> () Source #

Logic CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

parse_basic_sen :: CASL -> Maybe (CASLBasicSpec -> AParser st CASLFORMULA) Source #

stability :: CASL -> Stability Source #

data_logic :: CASL -> Maybe AnyLogic Source #

top_sublogic :: CASL -> CASL_Sublogics Source #

all_sublogics :: CASL -> [CASL_Sublogics] Source #

bottomSublogic :: CASL -> Maybe CASL_Sublogics Source #

sublogicDimensions :: CASL -> [[CASL_Sublogics]] Source #

parseSublogic :: CASL -> String -> Maybe CASL_Sublogics Source #

proj_sublogic_epsilon :: CASL -> CASL_Sublogics -> CASLSign -> CASLMor Source #

provers :: CASL -> [Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree] Source #

default_prover :: CASL -> String Source #

cons_checkers :: CASL -> [ConsChecker CASLSign CASLFORMULA CASL_Sublogics CASLMor ProofTree] Source #

conservativityCheck :: CASL -> [ConservativityChecker CASLSign CASLFORMULA CASLMor] Source #

empty_proof_tree :: CASL -> ProofTree Source #

syntaxTable :: CASL -> CASLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CASL -> Maybe OMCD Source #

export_symToOmdoc :: CASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CASL -> NameMap Symbol -> CASLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: CASL -> SigMap Symbol -> CASLSign -> [Named CASLFORMULA] -> Result [TCElement] Source #

omdocToSym :: CASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CASLFORMULA)) Source #

addOMadtToTheory :: CASL -> SigMapI Symbol -> (CASLSign, [Named CASLFORMULA]) -> [[OmdADT]] -> Result (CASLSign, [Named CASLFORMULA]) Source #

addOmdocToTheory :: CASL -> SigMapI Symbol -> (CASLSign, [Named CASLFORMULA]) -> [TCElement] -> Result (CASLSign, [Named CASLFORMULA]) Source #

sublogicOfTheo :: CASL -> (CASLSign, [CASLFORMULA]) -> CASL_Sublogics Source #

Logic Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source # 
Instance details

Defined in Modal.Logic_Modal

Methods

parse_basic_sen :: Modal -> Maybe (M_BASIC_SPEC -> AParser st ModalFORMULA) Source #

stability :: Modal -> Stability Source #

data_logic :: Modal -> Maybe AnyLogic Source #

top_sublogic :: Modal -> () Source #

all_sublogics :: Modal -> [()] Source #

bottomSublogic :: Modal -> Maybe () Source #

sublogicDimensions :: Modal -> [[()]] Source #

parseSublogic :: Modal -> String -> Maybe () Source #

proj_sublogic_epsilon :: Modal -> () -> MSign -> ModalMor Source #

provers :: Modal -> [Prover MSign ModalFORMULA ModalMor () ()] Source #

default_prover :: Modal -> String Source #

cons_checkers :: Modal -> [ConsChecker MSign ModalFORMULA () ModalMor ()] Source #

conservativityCheck :: Modal -> [ConservativityChecker MSign ModalFORMULA ModalMor] Source #

empty_proof_tree :: Modal -> () Source #

syntaxTable :: Modal -> MSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Modal -> Maybe OMCD Source #

export_symToOmdoc :: Modal -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Modal -> NameMap Symbol -> ModalFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: Modal -> SigMap Symbol -> MSign -> [Named ModalFORMULA] -> Result [TCElement] Source #

omdocToSym :: Modal -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Modal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ModalFORMULA)) Source #

addOMadtToTheory :: Modal -> SigMapI Symbol -> (MSign, [Named ModalFORMULA]) -> [[OmdADT]] -> Result (MSign, [Named ModalFORMULA]) Source #

addOmdocToTheory :: Modal -> SigMapI Symbol -> (MSign, [Named ModalFORMULA]) -> [TCElement] -> Result (MSign, [Named ModalFORMULA]) Source #

sublogicOfTheo :: Modal -> (MSign, [ModalFORMULA]) -> () Source #

Logic Hybrid () H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol () Source # 
Instance details

Defined in Hybrid.Logic_Hybrid

Methods

parse_basic_sen :: Hybrid -> Maybe (H_BASIC_SPEC -> AParser st HybridFORMULA) Source #

stability :: Hybrid -> Stability Source #

data_logic :: Hybrid -> Maybe AnyLogic Source #

top_sublogic :: Hybrid -> () Source #

all_sublogics :: Hybrid -> [()] Source #

bottomSublogic :: Hybrid -> Maybe () Source #

sublogicDimensions :: Hybrid -> [[()]] Source #

parseSublogic :: Hybrid -> String -> Maybe () Source #

proj_sublogic_epsilon :: Hybrid -> () -> HSign -> HybridMor Source #

provers :: Hybrid -> [Prover HSign HybridFORMULA HybridMor () ()] Source #

default_prover :: Hybrid -> String Source #

cons_checkers :: Hybrid -> [ConsChecker HSign HybridFORMULA () HybridMor ()] Source #

conservativityCheck :: Hybrid -> [ConservativityChecker HSign HybridFORMULA HybridMor] Source #

empty_proof_tree :: Hybrid -> () Source #

syntaxTable :: Hybrid -> HSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Hybrid -> Maybe OMCD Source #

export_symToOmdoc :: Hybrid -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Hybrid -> NameMap Symbol -> HybridFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: Hybrid -> SigMap Symbol -> HSign -> [Named HybridFORMULA] -> Result [TCElement] Source #

omdocToSym :: Hybrid -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Hybrid -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named HybridFORMULA)) Source #

addOMadtToTheory :: Hybrid -> SigMapI Symbol -> (HSign, [Named HybridFORMULA]) -> [[OmdADT]] -> Result (HSign, [Named HybridFORMULA]) Source #

addOmdocToTheory :: Hybrid -> SigMapI Symbol -> (HSign, [Named HybridFORMULA]) -> [TCElement] -> Result (HSign, [Named HybridFORMULA]) Source #

sublogicOfTheo :: Hybrid -> (HSign, [HybridFORMULA]) -> () Source #

Logic Fpl () FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol () Source # 
Instance details

Defined in Fpl.Logic_Fpl

Methods

parse_basic_sen :: Fpl -> Maybe (FplBasicSpec -> AParser st FplForm) Source #

stability :: Fpl -> Stability Source #

data_logic :: Fpl -> Maybe AnyLogic Source #

top_sublogic :: Fpl -> () Source #

all_sublogics :: Fpl -> [()] Source #

bottomSublogic :: Fpl -> Maybe () Source #

sublogicDimensions :: Fpl -> [[()]] Source #

parseSublogic :: Fpl -> String -> Maybe () Source #

proj_sublogic_epsilon :: Fpl -> () -> FplSign -> FplMor Source #

provers :: Fpl -> [Prover FplSign FplForm FplMor () ()] Source #

default_prover :: Fpl -> String Source #

cons_checkers :: Fpl -> [ConsChecker FplSign FplForm () FplMor ()] Source #

conservativityCheck :: Fpl -> [ConservativityChecker FplSign FplForm FplMor] Source #

empty_proof_tree :: Fpl -> () Source #

syntaxTable :: Fpl -> FplSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Fpl -> Maybe OMCD Source #

export_symToOmdoc :: Fpl -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Fpl -> NameMap Symbol -> FplForm -> Result TCorOMElement Source #

export_theoryToOmdoc :: Fpl -> SigMap Symbol -> FplSign -> [Named FplForm] -> Result [TCElement] Source #

omdocToSym :: Fpl -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Fpl -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FplForm)) Source #

addOMadtToTheory :: Fpl -> SigMapI Symbol -> (FplSign, [Named FplForm]) -> [[OmdADT]] -> Result (FplSign, [Named FplForm]) Source #

addOmdocToTheory :: Fpl -> SigMapI Symbol -> (FplSign, [Named FplForm]) -> [TCElement] -> Result (FplSign, [Named FplForm]) Source #

sublogicOfTheo :: Fpl -> (FplSign, [FplForm]) -> () Source #

Logic ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Methods

parse_basic_sen :: ExtModal -> Maybe (EM_BASIC_SPEC -> AParser st ExtModalFORMULA) Source #

stability :: ExtModal -> Stability Source #

data_logic :: ExtModal -> Maybe AnyLogic Source #

top_sublogic :: ExtModal -> ExtModalSL Source #

all_sublogics :: ExtModal -> [ExtModalSL] Source #

bottomSublogic :: ExtModal -> Maybe ExtModalSL Source #

sublogicDimensions :: ExtModal -> [[ExtModalSL]] Source #

parseSublogic :: ExtModal -> String -> Maybe ExtModalSL Source #

proj_sublogic_epsilon :: ExtModal -> ExtModalSL -> ExtModalSign -> ExtModalMorph Source #

provers :: ExtModal -> [Prover ExtModalSign ExtModalFORMULA ExtModalMorph ExtModalSL ()] Source #

default_prover :: ExtModal -> String Source #

cons_checkers :: ExtModal -> [ConsChecker ExtModalSign ExtModalFORMULA ExtModalSL ExtModalMorph ()] Source #

conservativityCheck :: ExtModal -> [ConservativityChecker ExtModalSign ExtModalFORMULA ExtModalMorph] Source #

empty_proof_tree :: ExtModal -> () Source #

syntaxTable :: ExtModal -> ExtModalSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: ExtModal -> Maybe OMCD Source #

export_symToOmdoc :: ExtModal -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: ExtModal -> NameMap Symbol -> ExtModalFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: ExtModal -> SigMap Symbol -> ExtModalSign -> [Named ExtModalFORMULA] -> Result [TCElement] Source #

omdocToSym :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ExtModalFORMULA)) Source #

addOMadtToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [[OmdADT]] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

addOmdocToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [TCElement] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

sublogicOfTheo :: ExtModal -> (ExtModalSign, [ExtModalFORMULA]) -> ExtModalSL Source #

Logic ConstraintCASL CASL_Sublogics ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol () Source # 
Instance details

Defined in ConstraintCASL.Logic_ConstraintCASL

Methods

parse_basic_sen :: ConstraintCASL -> Maybe (ConstraintCASLBasicSpec -> AParser st ConstraintCASLFORMULA) Source #

stability :: ConstraintCASL -> Stability Source #

data_logic :: ConstraintCASL -> Maybe AnyLogic Source #

top_sublogic :: ConstraintCASL -> CASL_Sublogics Source #

all_sublogics :: ConstraintCASL -> [CASL_Sublogics] Source #

bottomSublogic :: ConstraintCASL -> Maybe CASL_Sublogics Source #

sublogicDimensions :: ConstraintCASL -> [[CASL_Sublogics]] Source #

parseSublogic :: ConstraintCASL -> String -> Maybe CASL_Sublogics Source #

proj_sublogic_epsilon :: ConstraintCASL -> CASL_Sublogics -> ConstraintCASLSign -> ConstraintCASLMor Source #

provers :: ConstraintCASL -> [Prover ConstraintCASLSign ConstraintCASLFORMULA ConstraintCASLMor CASL_Sublogics ()] Source #

default_prover :: ConstraintCASL -> String Source #

cons_checkers :: ConstraintCASL -> [ConsChecker ConstraintCASLSign ConstraintCASLFORMULA CASL_Sublogics ConstraintCASLMor ()] Source #

conservativityCheck :: ConstraintCASL -> [ConservativityChecker ConstraintCASLSign ConstraintCASLFORMULA ConstraintCASLMor] Source #

empty_proof_tree :: ConstraintCASL -> () Source #

syntaxTable :: ConstraintCASL -> ConstraintCASLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: ConstraintCASL -> Maybe OMCD Source #

export_symToOmdoc :: ConstraintCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: ConstraintCASL -> NameMap Symbol -> ConstraintCASLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: ConstraintCASL -> SigMap Symbol -> ConstraintCASLSign -> [Named ConstraintCASLFORMULA] -> Result [TCElement] Source #

omdocToSym :: ConstraintCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: ConstraintCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ConstraintCASLFORMULA)) Source #

addOMadtToTheory :: ConstraintCASL -> SigMapI Symbol -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> [[OmdADT]] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #

addOmdocToTheory :: ConstraintCASL -> SigMapI Symbol -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> [TCElement] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #

sublogicOfTheo :: ConstraintCASL -> (ConstraintCASLSign, [ConstraintCASLFORMULA]) -> CASL_Sublogics Source #

Logic CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Methods

parse_basic_sen :: CoCASL -> Maybe (C_BASIC_SPEC -> AParser st CoCASLFORMULA) Source #

stability :: CoCASL -> Stability Source #

data_logic :: CoCASL -> Maybe AnyLogic Source #

top_sublogic :: CoCASL -> CoCASL_Sublogics Source #

all_sublogics :: CoCASL -> [CoCASL_Sublogics] Source #

bottomSublogic :: CoCASL -> Maybe CoCASL_Sublogics Source #

sublogicDimensions :: CoCASL -> [[CoCASL_Sublogics]] Source #

parseSublogic :: CoCASL -> String -> Maybe CoCASL_Sublogics Source #

proj_sublogic_epsilon :: CoCASL -> CoCASL_Sublogics -> CSign -> CoCASLMor Source #

provers :: CoCASL -> [Prover CSign CoCASLFORMULA CoCASLMor CoCASL_Sublogics ()] Source #

default_prover :: CoCASL -> String Source #

cons_checkers :: CoCASL -> [ConsChecker CSign CoCASLFORMULA CoCASL_Sublogics CoCASLMor ()] Source #

conservativityCheck :: CoCASL -> [ConservativityChecker CSign CoCASLFORMULA CoCASLMor] Source #

empty_proof_tree :: CoCASL -> () Source #

syntaxTable :: CoCASL -> CSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CoCASL -> Maybe OMCD Source #

export_symToOmdoc :: CoCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CoCASL -> NameMap Symbol -> CoCASLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: CoCASL -> SigMap Symbol -> CSign -> [Named CoCASLFORMULA] -> Result [TCElement] Source #

omdocToSym :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CoCASLFORMULA)) Source #

addOMadtToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [[OmdADT]] -> Result (CSign, [Named CoCASLFORMULA]) Source #

addOmdocToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [TCElement] -> Result (CSign, [Named CoCASLFORMULA]) Source #

sublogicOfTheo :: CoCASL -> (CSign, [CoCASLFORMULA]) -> CoCASL_Sublogics Source #

Logic COL () C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol () Source # 
Instance details

Defined in COL.Logic_COL

Methods

parse_basic_sen :: COL -> Maybe (C_BASIC_SPEC -> AParser st COLFORMULA) Source #

stability :: COL -> Stability Source #

data_logic :: COL -> Maybe AnyLogic Source #

top_sublogic :: COL -> () Source #

all_sublogics :: COL -> [()] Source #

bottomSublogic :: COL -> Maybe () Source #

sublogicDimensions :: COL -> [[()]] Source #

parseSublogic :: COL -> String -> Maybe () Source #

proj_sublogic_epsilon :: COL -> () -> CSign -> COLMor Source #

provers :: COL -> [Prover CSign COLFORMULA COLMor () ()] Source #

default_prover :: COL -> String Source #

cons_checkers :: COL -> [ConsChecker CSign COLFORMULA () COLMor ()] Source #

conservativityCheck :: COL -> [ConservativityChecker CSign COLFORMULA COLMor] Source #

empty_proof_tree :: COL -> () Source #

syntaxTable :: COL -> CSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: COL -> Maybe OMCD Source #

export_symToOmdoc :: COL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: COL -> NameMap Symbol -> COLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: COL -> SigMap Symbol -> CSign -> [Named COLFORMULA] -> Result [TCElement] Source #

omdocToSym :: COL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: COL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named COLFORMULA)) Source #

addOMadtToTheory :: COL -> SigMapI Symbol -> (CSign, [Named COLFORMULA]) -> [[OmdADT]] -> Result (CSign, [Named COLFORMULA]) Source #

addOmdocToTheory :: COL -> SigMapI Symbol -> (CSign, [Named COLFORMULA]) -> [TCElement] -> Result (CSign, [Named COLFORMULA]) Source #

sublogicOfTheo :: COL -> (CSign, [COLFORMULA]) -> () Source #

Logic CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Methods

parse_basic_sen :: CASL_DL -> Maybe (DL_BASIC_SPEC -> AParser st DLFORMULA) Source #

stability :: CASL_DL -> Stability Source #

data_logic :: CASL_DL -> Maybe AnyLogic Source #

top_sublogic :: CASL_DL -> CASL_DL_SL Source #

all_sublogics :: CASL_DL -> [CASL_DL_SL] Source #

bottomSublogic :: CASL_DL -> Maybe CASL_DL_SL Source #

sublogicDimensions :: CASL_DL -> [[CASL_DL_SL]] Source #

parseSublogic :: CASL_DL -> String -> Maybe CASL_DL_SL Source #

proj_sublogic_epsilon :: CASL_DL -> CASL_DL_SL -> DLSign -> DLMor Source #

provers :: CASL_DL -> [Prover DLSign DLFORMULA DLMor CASL_DL_SL ProofTree] Source #

default_prover :: CASL_DL -> String Source #

cons_checkers :: CASL_DL -> [ConsChecker DLSign DLFORMULA CASL_DL_SL DLMor ProofTree] Source #

conservativityCheck :: CASL_DL -> [ConservativityChecker DLSign DLFORMULA DLMor] Source #

empty_proof_tree :: CASL_DL -> ProofTree Source #

syntaxTable :: CASL_DL -> DLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CASL_DL -> Maybe OMCD Source #

export_symToOmdoc :: CASL_DL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CASL_DL -> NameMap Symbol -> DLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: CASL_DL -> SigMap Symbol -> DLSign -> [Named DLFORMULA] -> Result [TCElement] Source #

omdocToSym :: CASL_DL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CASL_DL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named DLFORMULA)) Source #

addOMadtToTheory :: CASL_DL -> SigMapI Symbol -> (DLSign, [Named DLFORMULA]) -> [[OmdADT]] -> Result (DLSign, [Named DLFORMULA]) Source #

addOmdocToTheory :: CASL_DL -> SigMapI Symbol -> (DLSign, [Named DLFORMULA]) -> [TCElement] -> Result (DLSign, [Named DLFORMULA]) Source #

sublogicOfTheo :: CASL_DL -> (DLSign, [DLFORMULA]) -> CASL_DL_SL Source #

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

Instance of Logic for propositional logc

Instance details

Defined in Temporal.Logic_Temporal

Methods

parse_basic_sen :: Temporal -> Maybe (BASIC_SPEC -> AParser st FORMULA) Source #

stability :: Temporal -> Stability Source #

data_logic :: Temporal -> Maybe AnyLogic Source #

top_sublogic :: Temporal -> () Source #

all_sublogics :: Temporal -> [()] Source #

bottomSublogic :: Temporal -> Maybe () Source #

sublogicDimensions :: Temporal -> [[()]] Source #

parseSublogic :: Temporal -> String -> Maybe () Source #

proj_sublogic_epsilon :: Temporal -> () -> Sign -> Morphism Source #

provers :: Temporal -> [Prover Sign FORMULA Morphism () ()] Source #

default_prover :: Temporal -> String Source #

cons_checkers :: Temporal -> [ConsChecker Sign FORMULA () Morphism ()] Source #

conservativityCheck :: Temporal -> [ConservativityChecker Sign FORMULA Morphism] Source #

empty_proof_tree :: Temporal -> () Source #

syntaxTable :: Temporal -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Temporal -> Maybe OMCD Source #

export_symToOmdoc :: Temporal -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Temporal -> NameMap Symbol -> FORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: Temporal -> SigMap Symbol -> Sign -> [Named FORMULA] -> Result [TCElement] Source #

omdocToSym :: Temporal -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Temporal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source #

addOMadtToTheory :: Temporal -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source #

addOmdocToTheory :: Temporal -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source #

sublogicOfTheo :: Temporal -> (Sign, [FORMULA]) -> () Source #

Logic Hybridize () Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS Sgn_Wrap Mor Symbol RawSymbol () Source # 
Instance details

Defined in TopHybrid.Logic_TopHybrid

Methods

parse_basic_sen :: Hybridize -> Maybe (Spc_Wrap -> AParser st Frm_Wrap) Source #

stability :: Hybridize -> Stability Source #

data_logic :: Hybridize -> Maybe AnyLogic Source #

top_sublogic :: Hybridize -> () Source #

all_sublogics :: Hybridize -> [()] Source #

bottomSublogic :: Hybridize -> Maybe () Source #

sublogicDimensions :: Hybridize -> [[()]] Source #

parseSublogic :: Hybridize -> String -> Maybe () Source #

proj_sublogic_epsilon :: Hybridize -> () -> Sgn_Wrap -> Mor Source #

provers :: Hybridize -> [Prover Sgn_Wrap Frm_Wrap Mor () ()] Source #

default_prover :: Hybridize -> String Source #

cons_checkers :: Hybridize -> [ConsChecker Sgn_Wrap Frm_Wrap () Mor ()] Source #

conservativityCheck :: Hybridize -> [ConservativityChecker Sgn_Wrap Frm_Wrap Mor] Source #

empty_proof_tree :: Hybridize -> () Source #

syntaxTable :: Hybridize -> Sgn_Wrap -> Maybe SyntaxTable Source #

omdoc_metatheory :: Hybridize -> Maybe OMCD Source #

export_symToOmdoc :: Hybridize -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Hybridize -> NameMap Symbol -> Frm_Wrap -> Result TCorOMElement Source #

export_theoryToOmdoc :: Hybridize -> SigMap Symbol -> Sgn_Wrap -> [Named Frm_Wrap] -> Result [TCElement] Source #

omdocToSym :: Hybridize -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Hybridize -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Frm_Wrap)) Source #

addOMadtToTheory :: Hybridize -> SigMapI Symbol -> (Sgn_Wrap, [Named Frm_Wrap]) -> [[OmdADT]] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source #

addOmdocToTheory :: Hybridize -> SigMapI Symbol -> (Sgn_Wrap, [Named Frm_Wrap]) -> [TCElement] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source #

sublogicOfTheo :: Hybridize -> (Sgn_Wrap, [Frm_Wrap]) -> () Source #

Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Instance details

Defined in VSE.Logic_VSE

Methods

parse_basic_sen :: VSE -> Maybe (VSEBasicSpec -> AParser st Sentence) Source #

stability :: VSE -> Stability Source #

data_logic :: VSE -> Maybe AnyLogic Source #

top_sublogic :: VSE -> () Source #

all_sublogics :: VSE -> [()] Source #

bottomSublogic :: VSE -> Maybe () Source #

sublogicDimensions :: VSE -> [[()]] Source #

parseSublogic :: VSE -> String -> Maybe () Source #

proj_sublogic_epsilon :: VSE -> () -> VSESign -> VSEMor Source #

provers :: VSE -> [Prover VSESign Sentence VSEMor () ()] Source #

default_prover :: VSE -> String Source #

cons_checkers :: VSE -> [ConsChecker VSESign Sentence () VSEMor ()] Source #

conservativityCheck :: VSE -> [ConservativityChecker VSESign Sentence VSEMor] Source #

empty_proof_tree :: VSE -> () Source #

syntaxTable :: VSE -> VSESign -> Maybe SyntaxTable Source #

omdoc_metatheory :: VSE -> Maybe OMCD Source #

export_symToOmdoc :: VSE -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: VSE -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: VSE -> SigMap Symbol -> VSESign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: VSE -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: VSE -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [[OmdADT]] -> Result (VSESign, [Named Sentence]) Source #

addOmdocToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [TCElement] -> Result (VSESign, [Named Sentence]) Source #

sublogicOfTheo :: VSE -> (VSESign, [Sentence]) -> () Source #

Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION] Source #

Instance of Logic for reduce logc

Instance details

Defined in CSL.Logic_CSL

Methods

parse_basic_sen :: CSL -> Maybe (BASIC_SPEC -> AParser st CMD) Source #

stability :: CSL -> Stability Source #

data_logic :: CSL -> Maybe AnyLogic Source #

top_sublogic :: CSL -> () Source #

all_sublogics :: CSL -> [()] Source #

bottomSublogic :: CSL -> Maybe () Source #

sublogicDimensions :: CSL -> [[()]] Source #

parseSublogic :: CSL -> String -> Maybe () Source #

proj_sublogic_epsilon :: CSL -> () -> Sign -> Morphism Source #

provers :: CSL -> [Prover Sign CMD Morphism () [EXPRESSION]] Source #

default_prover :: CSL -> String Source #

cons_checkers :: CSL -> [ConsChecker Sign CMD () Morphism [EXPRESSION]] Source #

conservativityCheck :: CSL -> [ConservativityChecker Sign CMD Morphism] Source #

empty_proof_tree :: CSL -> [EXPRESSION] Source #

syntaxTable :: CSL -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CSL -> Maybe OMCD Source #

export_symToOmdoc :: CSL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CSL -> NameMap Symbol -> CMD -> Result TCorOMElement Source #

export_theoryToOmdoc :: CSL -> SigMap Symbol -> Sign -> [Named CMD] -> Result [TCElement] Source #

omdocToSym :: CSL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CSL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CMD)) Source #

addOMadtToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [[OmdADT]] -> Result (Sign, [Named CMD]) Source #

addOmdocToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [TCElement] -> Result (Sign, [Named CMD]) Source #

sublogicOfTheo :: CSL -> (Sign, [CMD]) -> () Source #

Logic FreeCAD () Document () () () Sign (DefaultMorphism Sign) () () () Source # 
Instance details

Defined in FreeCAD.Logic_FreeCAD

Methods

parse_basic_sen :: FreeCAD -> Maybe (Document -> AParser st ()) Source #

stability :: FreeCAD -> Stability Source #

data_logic :: FreeCAD -> Maybe AnyLogic Source #

top_sublogic :: FreeCAD -> () Source #

all_sublogics :: FreeCAD -> [()] Source #

bottomSublogic :: FreeCAD -> Maybe () Source #

sublogicDimensions :: FreeCAD -> [[()]] Source #

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

proj_sublogic_epsilon :: FreeCAD -> () -> Sign -> DefaultMorphism Sign Source #

provers :: FreeCAD -> [Prover Sign () (DefaultMorphism Sign) () ()] Source #

default_prover :: FreeCAD -> String Source #

cons_checkers :: FreeCAD -> [ConsChecker Sign () () (DefaultMorphism Sign) ()] Source #

conservativityCheck :: FreeCAD -> [ConservativityChecker Sign () (DefaultMorphism Sign)] Source #

empty_proof_tree :: FreeCAD -> () Source #

syntaxTable :: FreeCAD -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: FreeCAD -> Maybe OMCD Source #

export_symToOmdoc :: FreeCAD -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: FreeCAD -> NameMap () -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: FreeCAD -> SigMap () -> Sign -> [Named ()] -> Result [TCElement] Source #

omdocToSym :: FreeCAD -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: FreeCAD -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source #

addOMadtToTheory :: FreeCAD -> SigMapI () -> (Sign, [Named ()]) -> [[OmdADT]] -> Result (Sign, [Named ()]) Source #

addOmdocToTheory :: FreeCAD -> SigMapI () -> (Sign, [Named ()]) -> [TCElement] -> Result (Sign, [Named ()]) Source #

sublogicOfTheo :: FreeCAD -> (Sign, [()]) -> () Source #

Logic DMU () Text () () () Text (DefaultMorphism Text) () () () Source # 
Instance details

Defined in DMU.Logic_DMU

Methods

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

stability :: DMU -> Stability Source #

data_logic :: DMU -> Maybe AnyLogic Source #

top_sublogic :: DMU -> () Source #

all_sublogics :: DMU -> [()] Source #

bottomSublogic :: DMU -> Maybe () Source #

sublogicDimensions :: DMU -> [[()]] Source #

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

proj_sublogic_epsilon :: DMU -> () -> Text -> DefaultMorphism Text Source #

provers :: DMU -> [Prover Text () (DefaultMorphism Text) () ()] Source #

default_prover :: DMU -> String Source #

cons_checkers :: DMU -> [ConsChecker Text () () (DefaultMorphism Text) ()] Source #

conservativityCheck :: DMU -> [ConservativityChecker Text () (DefaultMorphism Text)] Source #

empty_proof_tree :: DMU -> () Source #

syntaxTable :: DMU -> Text -> Maybe SyntaxTable Source #

omdoc_metatheory :: DMU -> Maybe OMCD Source #

export_symToOmdoc :: DMU -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: DMU -> NameMap () -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: DMU -> SigMap () -> Text -> [Named ()] -> Result [TCElement] Source #

omdocToSym :: DMU -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: DMU -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source #

addOMadtToTheory :: DMU -> SigMapI () -> (Text, [Named ()]) -> [[OmdADT]] -> Result (Text, [Named ()]) Source #

addOmdocToTheory :: DMU -> SigMapI () -> (Text, [Named ()]) -> [TCElement] -> Result (Text, [Named ()]) Source #

sublogicOfTheo :: DMU -> (Text, [()]) -> () Source #

Logic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree Source # 
Instance details

Defined in SoftFOL.Logic_SoftFOL

Methods

parse_basic_sen :: SoftFOL -> Maybe ([TPTP] -> AParser st Sentence) Source #

stability :: SoftFOL -> Stability Source #

data_logic :: SoftFOL -> Maybe AnyLogic Source #

top_sublogic :: SoftFOL -> () Source #

all_sublogics :: SoftFOL -> [()] Source #

bottomSublogic :: SoftFOL -> Maybe () Source #

sublogicDimensions :: SoftFOL -> [[()]] Source #

parseSublogic :: SoftFOL -> String -> Maybe () Source #

proj_sublogic_epsilon :: SoftFOL -> () -> Sign -> SoftFOLMorphism Source #

provers :: SoftFOL -> [Prover Sign Sentence SoftFOLMorphism () ProofTree] Source #

default_prover :: SoftFOL -> String Source #

cons_checkers :: SoftFOL -> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree] Source #

conservativityCheck :: SoftFOL -> [ConservativityChecker Sign Sentence SoftFOLMorphism] Source #

empty_proof_tree :: SoftFOL -> ProofTree Source #

syntaxTable :: SoftFOL -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: SoftFOL -> Maybe OMCD Source #

export_symToOmdoc :: SoftFOL -> NameMap SFSymbol -> SFSymbol -> String -> Result TCElement Source #

export_senToOmdoc :: SoftFOL -> NameMap SFSymbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: SoftFOL -> SigMap SFSymbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result SFSymbol Source #

omdocToSen :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: SoftFOL -> SigMapI SFSymbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: SoftFOL -> SigMapI SFSymbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

sublogicOfTheo :: SoftFOL -> (Sign, [Sentence]) -> () Source #

CspCASLSemantics a => Logic (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source #

Instance of Logic for CspCASL

Instance details

Defined in CspCASL.Logic_CspCASL

Methods

parse_basic_sen :: GenCspCASL a -> Maybe (CspBasicSpec -> AParser st CspCASLSen) Source #

stability :: GenCspCASL a -> Stability Source #

data_logic :: GenCspCASL a -> Maybe AnyLogic Source #

top_sublogic :: GenCspCASL a -> () Source #

all_sublogics :: GenCspCASL a -> [()] Source #

bottomSublogic :: GenCspCASL a -> Maybe () Source #

sublogicDimensions :: GenCspCASL a -> [[()]] Source #

parseSublogic :: GenCspCASL a -> String -> Maybe () Source #

proj_sublogic_epsilon :: GenCspCASL a -> () -> CspCASLSign -> CspCASLMorphism Source #

provers :: GenCspCASL a -> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()] Source #

default_prover :: GenCspCASL a -> String Source #

cons_checkers :: GenCspCASL a -> [ConsChecker CspCASLSign CspCASLSen () CspCASLMorphism ()] Source #

conservativityCheck :: GenCspCASL a -> [ConservativityChecker CspCASLSign CspCASLSen CspCASLMorphism] Source #

empty_proof_tree :: GenCspCASL a -> () Source #

syntaxTable :: GenCspCASL a -> CspCASLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: GenCspCASL a -> Maybe OMCD Source #

export_symToOmdoc :: GenCspCASL a -> NameMap CspSymbol -> CspSymbol -> String -> Result TCElement Source #

export_senToOmdoc :: GenCspCASL a -> NameMap CspSymbol -> CspCASLSen -> Result TCorOMElement Source #

export_theoryToOmdoc :: GenCspCASL a -> SigMap CspSymbol -> CspCASLSign -> [Named CspCASLSen] -> Result [TCElement] Source #

omdocToSym :: GenCspCASL a -> SigMapI CspSymbol -> TCElement -> String -> Result CspSymbol Source #

omdocToSen :: GenCspCASL a -> SigMapI CspSymbol -> TCElement -> String -> Result (Maybe (Named CspCASLSen)) Source #

addOMadtToTheory :: GenCspCASL a -> SigMapI CspSymbol -> (CspCASLSign, [Named CspCASLSen]) -> [[OmdADT]] -> Result (CspCASLSign, [Named CspCASLSen]) Source #

addOmdocToTheory :: GenCspCASL a -> SigMapI CspSymbol -> (CspCASLSign, [Named CspCASLSen]) -> [TCElement] -> Result (CspCASLSign, [Named CspCASLSen]) Source #

sublogicOfTheo :: GenCspCASL a -> (CspCASLSign, [CspCASLSen]) -> () Source #

(MinSublogic sublogics1 (), 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, Ord proof_tree2, Show proof_tree2, Data sentence2) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2 Source # 
Instance details

Defined in Logic.Morphism

Methods

parse_basic_sen :: SpanDomain cid -> Maybe (() -> AParser st (S2 sentence2)) Source #

stability :: SpanDomain cid -> Stability Source #

data_logic :: SpanDomain cid -> Maybe AnyLogic Source #

top_sublogic :: SpanDomain cid -> SublogicsPair sublogics1 sublogics2 Source #

all_sublogics :: SpanDomain cid -> [SublogicsPair sublogics1 sublogics2] Source #

bottomSublogic :: SpanDomain cid -> Maybe (SublogicsPair sublogics1 sublogics2) Source #

sublogicDimensions :: SpanDomain cid -> [[SublogicsPair sublogics1 sublogics2]] Source #

parseSublogic :: SpanDomain cid -> String -> Maybe (SublogicsPair sublogics1 sublogics2) Source #

proj_sublogic_epsilon :: SpanDomain cid -> SublogicsPair sublogics1 sublogics2 -> sign1 -> morphism1 Source #

provers :: SpanDomain cid -> [Prover sign1 (S2 sentence2) morphism1 (SublogicsPair sublogics1 sublogics2) proof_tree2] Source #

default_prover :: SpanDomain cid -> String Source #

cons_checkers :: SpanDomain cid -> [ConsChecker sign1 (S2 sentence2) (SublogicsPair sublogics1 sublogics2) morphism1 proof_tree2] Source #

conservativityCheck :: SpanDomain cid -> [ConservativityChecker sign1 (S2 sentence2) morphism1] Source #

empty_proof_tree :: SpanDomain cid -> proof_tree2 Source #

syntaxTable :: SpanDomain cid -> sign1 -> Maybe SyntaxTable Source #

omdoc_metatheory :: SpanDomain cid -> Maybe OMCD Source #

export_symToOmdoc :: SpanDomain cid -> NameMap sign_symbol1 -> sign_symbol1 -> String -> Result TCElement Source #

export_senToOmdoc :: SpanDomain cid -> NameMap sign_symbol1 -> S2 sentence2 -> Result TCorOMElement Source #

export_theoryToOmdoc :: SpanDomain cid -> SigMap sign_symbol1 -> sign1 -> [Named (S2 sentence2)] -> Result [TCElement] Source #

omdocToSym :: SpanDomain cid -> SigMapI sign_symbol1 -> TCElement -> String -> Result sign_symbol1 Source #

omdocToSen :: SpanDomain cid -> SigMapI sign_symbol1 -> TCElement -> String -> Result (Maybe (Named (S2 sentence2))) Source #

addOMadtToTheory :: SpanDomain cid -> SigMapI sign_symbol1 -> (sign1, [Named (S2 sentence2)]) -> [[OmdADT]] -> Result (sign1, [Named (S2 sentence2)]) Source #

addOmdocToTheory :: SpanDomain cid -> SigMapI sign_symbol1 -> (sign1, [Named (S2 sentence2)]) -> [TCElement] -> Result (sign1, [Named (S2 sentence2)]) Source #

sublogicOfTheo :: SpanDomain cid -> (sign1, [S2 sentence2]) -> SublogicsPair sublogics1 sublogics2 Source #

class Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => LogicalFramework lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree | lid -> sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree where Source #

Minimal complete definition

Nothing

Methods

base_sig :: lid -> sign Source #

the base signature

write_logic :: lid -> String -> String Source #

generation of the object logic instances second argument is object logic name

write_syntax :: lid -> String -> morphism -> String Source #

generation of the Ltruth morphism declaration second argument is the object logic name third argument is the Ltruth morphism

write_proof :: lid -> String -> morphism -> String Source #

write_model :: lid -> String -> morphism -> String Source #

read_morphism :: lid -> FilePath -> morphism Source #

write_comorphism :: lid -> String -> String -> String -> morphism -> morphism -> morphism -> String Source #

Instances

Instances details
LogicalFramework Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () Source # 
Instance details

Defined in Maude.Logic_Maude

Methods

base_sig :: Maude -> Sign Source #

write_logic :: Maude -> String -> String Source #

write_syntax :: Maude -> String -> Morphism -> String Source #

write_proof :: Maude -> String -> Morphism -> String Source #

write_model :: Maude -> String -> Morphism -> String Source #

read_morphism :: Maude -> FilePath -> Morphism Source #

write_comorphism :: Maude -> String -> String -> String -> Morphism -> Morphism -> Morphism -> String Source #

LogicalFramework LF () BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RAW_SYM () Source # 
Instance details

Defined in LF.Logic_LF

Methods

base_sig :: LF -> Sign Source #

write_logic :: LF -> String -> String Source #

write_syntax :: LF -> String -> Morphism -> String Source #

write_proof :: LF -> String -> Morphism -> String Source #

write_model :: LF -> String -> Morphism -> String Source #

read_morphism :: LF -> FilePath -> Morphism Source #

write_comorphism :: LF -> String -> String -> String -> Morphism -> Morphism -> Morphism -> String Source #

LogicalFramework Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Isabelle.Logic_Isabelle

Methods

base_sig :: Isabelle -> Sign Source #

write_logic :: Isabelle -> String -> String Source #

write_syntax :: Isabelle -> String -> IsabelleMorphism -> String Source #

write_proof :: Isabelle -> String -> IsabelleMorphism -> String Source #

write_model :: Isabelle -> String -> IsabelleMorphism -> String Source #

read_morphism :: Isabelle -> FilePath -> IsabelleMorphism Source #

write_comorphism :: Isabelle -> String -> String -> String -> IsabelleMorphism -> IsabelleMorphism -> IsabelleMorphism -> String Source #

emptyTheory :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol => lid -> Theory sign sentence proof_tree Source #

the empty theory

data AnyLogic Source #

the disjoint union of all logics

Constructors

forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree.Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => Logic lid 

Instances

Instances details
Eq AnyLogic Source # 
Instance details

Defined in Logic.Logic

Methods

(==) :: AnyLogic -> AnyLogic -> Bool

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

Ord AnyLogic Source # 
Instance details

Defined in Logic.Logic

Methods

compare :: AnyLogic -> AnyLogic -> Ordering

(<) :: AnyLogic -> AnyLogic -> Bool

(<=) :: AnyLogic -> AnyLogic -> Bool

(>) :: AnyLogic -> AnyLogic -> Bool

(>=) :: AnyLogic -> AnyLogic -> Bool

max :: AnyLogic -> AnyLogic -> AnyLogic

min :: AnyLogic -> AnyLogic -> AnyLogic

Show AnyLogic Source # 
Instance details

Defined in Logic.Logic

Methods

showsPrec :: Int -> AnyLogic -> ShowS

show :: AnyLogic -> String

showList :: [AnyLogic] -> ShowS

GetRange AnyLogic Source # 
Instance details

Defined in Logic.Logic

ShATermLG AnyLogic Source # 
Instance details

Defined in ATC.Grothendieck

Methods

toShATermLG :: ATermTable -> AnyLogic -> IO (ATermTable, Int) Source #

fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, AnyLogic) Source #