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