Logic.hs revision 33b2195dac69479b30c95fdfe83f97bab937f9e9
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{-# LANGUAGE UndecidableInstances #-}
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettModule : $Header$
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyDescription : central interface (type class) for logics in Hets
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachMaintainer : till@informatik.uni-bremen.de
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettStability : provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : non-portable (various -fglasgow-exts extensions)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachCentral interface (type class) for logics in Hets
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettProvides data structures for logics (with symbols). Logics are
78718c37b1a50086a27e0f031db4cf82bea934aeChristian Maeder a type class with an /identity type/ (usually interpreted
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach by a singleton set) which serves to treat logics as
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach data. All the functions in the type class take the
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach identity as first argument in order to determine the logic.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach For logic (co)morphisms see "Logic.Comorphism"
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett This module uses multiparameter type classes with functional dependencies
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder (<http://www.haskell.org/haskellwiki/Functional_dependencies>)
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett for defining an interface for the notion of logic. Multiparameter type
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach classes are needed because a logic consists of a collection of types,
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder together with operations on these. Functional dependencies
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder are needed because no operation will involve all types of
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett the multiparameter type class; hence we need a method to derive
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach the missing types. We chose an easy way: for each logic, we
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach introduce a new singleton type that is the name, or constitutes the identity
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder of the logic. All other types of the multiparameter type class
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly depend on this /identity constituting/ type, and all operations take
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach the 'identity constituting' type as first arguments. The value
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder of the argument of the /identity constituting/ type is irrelevant
0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblett (note that there is only one value of such a type anyway).
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett Note that we tend to use @lid@ both for the /identity type/
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly of a logic, as well as for its unique inhabitant, i.e. @lid :: lid@.
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett The other types involved in the definition of logic are as follows:
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder * sign: signatures, that is, contexts, or non-logical vocabularies,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly typically consisting of a set of declared sorts, predicates,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly function symbols, propositional letters etc., together with their
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder * sentence: logical formulas.
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett * basic_spec: abstract syntax of basic specifications. The latter are
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly human-readable presentations of a signature together with some sentences.
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly * symbol: symbols that may occur in a signature, fully qualified
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly with their types
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett * raw_symbol: symbols that may occur in a signature, possibly not
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder or partially qualified
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly * morphism: maps between signatures (typically preserving the structure).
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder * symb_items: abstract syntax of symbol lists, used for declaring some
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder symbols of a signature as hidden.
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder * symb_map_items: abstract syntax of symbol maps, i.e. human-readable
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly presentations of signature morphisms.
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly * sublogics: sublogics of the given logic. This type might be a
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly record of Boolean flags, indicating whether some feature is
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly present in the sublogi of not.
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder * proof_tree: proof trees.
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder J. A. Goguen and R. M. Burstall
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder Institutions: Abstract Model Theory for Specification and
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett JACM 39, p. 95-146, 1992
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett (general notion of logic - model theory only)
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett General Logics
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett Logic Colloquium 87, p. 275-329, North Holland, 1989
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (general notion of logic - also proof theory;
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett notion of logic representation, called map there)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett T. Mossakowski:
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett Specification in an arbitrary institution with symbols
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett 14th WADT 1999, LNCS 1827, p. 252-270
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett (treatment of symbols and raw symbols, see also CASL semantics
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly in the CASL reference manual)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly T. Mossakowski, B. Klin:
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Institution Independent Static Analysis for CASL
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett 15h WADT 2001, LNCS 2267, p. 221-237, 2002.
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett (what is needed for static anaylsis)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett S. Autexier and T. Mossakowski
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Integrating HOLCASL into the Development Graph Manager MAYA
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly FroCoS 2002, LNCS 2309, p. 2-17, 2002.
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett (interface to provers)
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett CoFI (ed.): CASL Reference Manual, LNCS 2960, Springer Verlag, 2004.
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett (static semantics of CASL structured and architectural specifications)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder T. Mossakowski
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder Heterogeneous specification and the heterogeneous tool set
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder Habilitation thesis, University of Bremen, 2005
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett (the general picture of heterogeneous specification)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettimport Logic.Prover (Prover, ConsChecker, Theory(..))
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport Taxonomy.MMiSSOntology (MMiSSOntology)
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport ATerm.Lib (ShATermConvertible)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettimport qualified Data.Set as Set
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettimport qualified Data.Map as Map
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport qualified OMDoc.DataTypes as OMDoc ( TCElement
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett , TCorOMElement
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | Stability of logic implementations
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillydata Stability = Stable | Testing | Unstable | Experimental
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly deriving (Eq, Show)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | shortcut for class constraints
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyclass ShATermConvertible a => Convertible a
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance ShATermConvertible a => Convertible a
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | shortcut for class constraints
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyclass (Pretty a, Convertible a) => PrintTypeConv a
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance (Pretty a, Convertible a) => PrintTypeConv a
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | shortcut for class constraints with equality
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyclass (Eq a, PrintTypeConv a) => EqPrintTypeConv a
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance (Eq a, PrintTypeConv a) => EqPrintTypeConv a
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | maps from a to a
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maedertype EndoMap a = Map.Map a a
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett{- | the name of a logic.
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Define instances like "data CASL = CASL deriving Show"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyclass Show lid => Language lid where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly language_name :: lid -> String
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly language_name = show
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly description :: lid -> String
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- default implementation
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly description _ = "No description available"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly{- | Categories are given as usual: objects, morphisms, identities,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly domain, codomain and composition. The type id is the name, or
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly the identity of the category. It is an argument to all functions
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly of the type class, serving disambiguation among instances
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (via the functional dependency lid -> object morphism).
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly The types for objects and morphisms may be restricted to
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly subtypes, using legal_obj and legal_mor. For example, for the
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly category of sets and injective maps, legal_mor would check
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly injectivity. Since Eq is a subclass of Category, it is also
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly possible to impose a quotient on the types for objects and morphisms.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Require Ord instances only for efficiency, i.e. in sets or maps.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyclass (Ord object, Ord morphism)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly => Category object morphism | morphism -> object where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- | identity morphisms
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ide :: object -> morphism
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- | composition, in diagrammatic order,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- if intermediate objects are equal (not checked!)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly composeMorphisms :: morphism -> morphism -> Result morphism
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- | domain and codomain of morphisms
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly dom, cod :: morphism -> object
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- | the inverse of a morphism
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly inverse :: morphism -> Result morphism
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly inverse _ = fail "Logic.Logic.Category.inverse not implemented"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- | test if the signature morphism an inclusion
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly isInclusion :: morphism -> Bool
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly isInclusion _ = False -- in general no inclusion
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- | is a value of type morphism denoting a legal morphism?
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly legal_mor :: morphism -> Bool
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillycomp :: Category object morphism => morphism -> morphism -> Result morphism
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillycomp m1 m2 = if cod m1 == dom m2 then composeMorphisms m1 m2 else
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly fail "target of first and source of second morphism are different"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance Ord sign => Category sign (DefaultMorphism sign) where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly dom = domOfDefaultMorphism
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly cod = codOfDefaultMorphism
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ide = ideOfDefaultMorphism
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly isInclusion = const True
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly composeMorphisms = compOfDefaultMorphism
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett legal_mor = legalDefaultMorphism (const True)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly{- | Abstract syntax, parsing and printing.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly There are three types for abstract syntax:
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly basic_spec is for basic specifications (see CASL RefMan p. 5ff.),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly symb_items is for symbol lists (see CASL RefMan p. 35ff.),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly symb_map_items is for symbol maps (see CASL RefMan p. 35ff.).
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblettclass (Language lid, PrintTypeConv basic_spec, GetRange basic_spec,
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly EqPrintTypeConv symb_items,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly EqPrintTypeConv symb_map_items)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly => Syntax lid basic_spec symb_items symb_map_items
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly | lid -> basic_spec symb_items symb_map_items
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- | parser for basic specifications
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly parse_basic_spec :: lid -> Maybe(AParser st basic_spec)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- | parser for symbol lists
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly parse_symb_items :: lid -> Maybe(AParser st symb_items)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- | parser for symbol maps
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly parse_symb_map_items :: lid -> Maybe(AParser st symb_map_items)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly toItem :: lid -> basic_spec -> Item
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- default implementations
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly parse_basic_spec _ = Nothing
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly parse_symb_items _ = Nothing
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly parse_symb_map_items _ = Nothing
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly toItem _ bs = mkFlatItem ("Basicspec", pretty bs) $ getRangeSpan bs
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly{- | Sentences, provers and symbols.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Provers capture the entailment relation between sets of sentences
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly and sentences. They may return proof trees witnessing proofs.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Signatures are equipped with underlying sets of symbols
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (such that the category of signatures becomes a concrete category),
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly see CASL RefMan p. 191ff.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyclass (Language lid, Category sign morphism, Ord sentence,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Ord symbol, -- for efficient lookup
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly PrintTypeConv sign, PrintTypeConv morphism,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly GetRange sentence, GetRange symbol,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly PrintTypeConv sentence, PrintTypeConv symbol)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly => Sentences lid sentence sign morphism symbol
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly | lid -> sentence sign morphism symbol
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ----------------------- sentences ---------------------------
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- | sentence translation along a signature morphism
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly map_sen :: lid -> morphism -> sentence -> Result sentence
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly map_sen l _ _ = statFail l "map_sen"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- | simplification of sentences (leave out qualifications)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly simplify_sen :: lid -> sign -> sentence -> sentence
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly simplify_sen _ _ = id -- default implementation
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- | negation of a sentence for disproving
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly negation :: lid -> sentence -> Maybe sentence
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett negation _ _ = Nothing
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -- | parsing of sentences
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett parse_sentence :: lid -> Maybe (AParser st sentence)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett parse_sentence _ = Nothing
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly print_sign :: lid -> sign -> Doc
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly print_sign _ = pretty
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly -- | print a sentence with comments
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly print_named :: lid -> Named sentence -> Doc
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly print_named _ = printAnnoted (addBullet . pretty) . fromLabelledSen
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ----------------------- symbols ---------------------------
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- | set of symbols for a signature
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sym_of :: lid -> sign -> Set.Set symbol
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly sym_of l _ = statError l "sym_of"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- | symbol map for a signature morphism
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly symmap_of :: lid -> morphism -> EndoMap symbol
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly symmap_of l _ = statError l "symmap_of"
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- | symbols have a name, see CASL RefMan p. 192
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sym_name :: lid -> symbol -> Id
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett sym_name l _ = statError l "sym_name"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- | a dummy static analysis function to allow type checking *.inline.hs files
e95030058b77cb83593c85aa4c506caf154f63b7Andy GimblettinlineAxioms :: StaticAnalysis lid
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly basic_spec sentence symb_items symb_map_items
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sign morphism symbol raw_symbol => lid -> String -> [Named sentence]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyinlineAxioms _ _ = error "inlineAxioms"
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly-- | fail function for static analysis
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy GimblettstatFail :: (Language lid, Monad m) => lid -> String -> m a
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettstatFail lid = fail . statErrMsg lid
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillystatError :: Language lid => lid -> String -> a
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillystatError lid = error . statErrMsg lid
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- | error message for static analysis
5858e6262048894b0e933b547852f04aed009b58Andy GimblettstatErrMsg :: Language lid => lid -> String -> String
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillystatErrMsg lid str =
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett "Logic." ++ str ++ " not implemented for: " ++ language_name lid
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett{- static analysis
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly This type class provides the data needed for an institution with symbols,
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly as explained in the structured specification semantics in the CASL
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly reference manual, chapter III.4.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly The static analysis computes signatures from basic specifications,
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett and signature morphisms from symbol lists and symbol maps. The latter
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder needs an intermediate stage, so-called raw symbols, which are possibly
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder unqualified symbols. Normal symbols are always fully qualified.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly In the CASL reference manual, our symbols are called "signature symbols",
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett and our raw symbols are called "symbols". (Terminology should be adapted.)
842ae753ab848a8508c4832ab64296b929167a97Christian Maederclass ( Syntax lid basic_spec symb_items symb_map_items
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , Sentences lid sentence sign morphism symbol
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett , GetRange raw_symbol, Ord raw_symbol, Pretty raw_symbol
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , Typeable raw_symbol)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder => StaticAnalysis lid
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly basic_spec sentence symb_items symb_map_items
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett sign morphism symbol raw_symbol
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly | lid -> basic_spec sentence symb_items symb_map_items
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly sign morphism symbol raw_symbol
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ----------------------- static analysis ---------------------------
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett {- | static analysis of basic specifications and symbol maps.
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly The resulting bspec has analyzed axioms in it.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly The resulting sign is an extension of the input sign
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly plus newly declared or redeclared symbols.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly See CASL RefMan p. 138 ff. -}
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett basic_analysis :: lid ->
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly Maybe((basic_spec, -- abstract syntax tree
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign, -- input signature, for the local
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- environment, carrying the previously
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly -- declared symbols
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly GlobalAnnos) -> -- global annotations
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Result (basic_spec, ExtSign sign symbol
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett , [Named sentence]))
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -- default implementation
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly basic_analysis _ = Nothing
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- | static analysis of symbol maps, see CASL RefMan p. 222f.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly stat_symb_map_items ::
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly lid -> [symb_map_items] -> Result (EndoMap raw_symbol)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly stat_symb_map_items l _ = statFail l "stat_symb_map_items"
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett -- | static analysis of symbol lists, see CASL RefMan p. 221f.
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly stat_symb_items :: lid -> [symb_items] -> Result [raw_symbol]
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly stat_symb_items l _ = statFail l "stat_symb_items"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ------------------------- amalgamation ---------------------------
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly {- | Computation of colimits of signature diagram.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Indeed, it suffices to compute a coconce that is weakly amalgamable
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett see Till Mossakowski,
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Heterogeneous specification and the heterogeneous tool set
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- | architectural sharing analysis, see CASL RefMan p. 247ff.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ensures_amalgamability :: lid ->
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly ([CASLAmalgOpt], -- the program options
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Gr sign (Int,morphism), -- the diagram to be analyzed
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett [(Int, morphism)], -- the sink
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Gr String String) -- the descriptions of nodes and edges
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> Result Amalgamates
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ensures_amalgamability l _ = warning Amalgamates
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ("amalgamability test not implemented for logic " ++ show l)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly -- | quotient term algebra for normalization of freeness
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett quotient_term_algebra :: lid -- the logic
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> morphism -- sigma : Sigma -> SigmaM
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> [Named sentence] -- Th(M)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (sign, -- SigmaK
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly [Named sentence] -- Ax(K)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly quotient_term_algebra l _ _ = statFail l "quotient_term_algebra"
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett -- | signature colimits
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly signature_colimit :: lid -> Gr sign (Int, morphism)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly -> Result (sign, Map.Map Int morphism)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly signature_colimit l _ = statFail l "signature_colimit"
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder {- | rename and qualify the symbols considering a united incoming
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly morphisms, code out overloading and
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly create sentences for the overloading relation -}
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly qualify :: lid -> SIMPLE_ID -> LibId -> morphism -> sign
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly -> Result (morphism, [Named sentence])
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett qualify l _ _ _ _ = statFail l "qualify"
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly -------------------- symbols and raw symbols ---------------------
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly {- | Construe a symbol, like f:->t, as a raw symbol.
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly This is a one-sided inverse to the function SymSySigSym
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly in the CASL RefMan p. 192. -}
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett symbol_to_raw :: lid -> symbol -> raw_symbol
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett symbol_to_raw l _ = statError l "symbol_to_raw"
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder {- | Construe an identifier, like f, as a raw symbol.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly See CASL RefMan p. 192, function IDAsSym -}
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly id_to_raw :: lid -> Id -> raw_symbol
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly id_to_raw l _ = statError l "id_to_raw"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly {- | Check wether a symbol matches a raw symbol, for
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett example, f:s->t matches f. See CASL RefMan p. 192 -}
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly matches :: lid -> symbol -> raw_symbol -> Bool
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly matches l _ _ = statError l "matches"
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder --------------- operations on signatures and morphisms -----------
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- | the empty (initial) signature, see CASL RefMan p. 193
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly empty_signature :: lid -> sign
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett -- | union of signatures, see CASL RefMan p. 193
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly signature_union :: lid -> sign -> sign -> Result sign
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly signature_union l _ _ = statFail l "signature_union"
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- | intersection of signatures
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly intersection :: lid -> sign -> sign -> Result sign
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder intersection l _ _ = statFail l "intersection"
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly -- | final union of signatures, see CASL RefMan p. 194
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly final_union :: lid -> sign -> sign -> Result sign
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett final_union l _ _ = statFail l "final_union"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -- | union of signature morphims, see CASL RefMan p. 196
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly morphism_union :: lid -> morphism -> morphism -> Result morphism
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly morphism_union l _ _ = statFail l "morphism_union"
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett -- | subsignatures, see CASL RefMan p. 194
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly is_subsig :: lid -> sign -> sign -> Bool
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly is_subsig _ _ _ = False
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly {- | construct the inclusion morphisms between subsignatures,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly see CASL RefMan p. 194 -}
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly subsig_inclusion :: lid -> sign -> sign -> Result morphism
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly subsig_inclusion l _ _ = statFail l "subsig_inclusion"
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly {- | the signature (co)generated by a set of symbols in another
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett signature is the smallest (largest) signature containing
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (excluding) the set of symbols. Needed for revealing and
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett hiding, see CASL RefMan p. 197ff. -}
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder generated_sign, cogenerated_sign ::
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly lid -> Set.Set symbol -> sign -> Result morphism
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly generated_sign l _ _ = statFail l "generated_sign"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly cogenerated_sign l _ _ = statFail l "cogenerated_sign"
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly {- | Induce a signature morphism from a source signature and
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly a raw symbol map. Needed for translation (SP with SM).
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly See CASL RefMan p. 198 -}
a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett induced_from_morphism ::
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly lid -> EndoMap raw_symbol -> sign -> Result morphism
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly induced_from_morphism l _ _ = statFail l "induced_from_morphism"
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly {- | Induce a signature morphism between two signatures by a
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly raw symbol map. Needed for instantiation and views.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly See CASL RefMan p. 198f. -}
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly induced_from_to_morphism ::
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett lid -> EndoMap raw_symbol -> ExtSign sign symbol
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -> ExtSign sign symbol -> Result morphism
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly induced_from_to_morphism l _ _ _ =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly statFail l "induced_from_to_morphism"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly {- | Check whether a signature morphism is transportable.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly See CASL RefMan p. 304f. -}
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly is_transportable :: lid -> morphism -> Bool
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly is_transportable _ _ = False -- safe default
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly {- | Check whether the underlying symbol map of a signature morphism
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly is injective -}
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly is_injective :: lid -> morphism -> Bool
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly is_injective _ _ = False -- safe default
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- | generate an ontological taxonomy, if this makes sense
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly theory_to_taxonomy :: lid
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -> TaxoGraphKind
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -> MMiSSOntology
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -> sign -> [Named sentence]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -> Result MMiSSOntology
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly theory_to_taxonomy l _ _ _ _ = statFail l "theory_to_taxonomy"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | guarded inclusion
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinclusion :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly sign morphism symbol raw_symbol
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly => lid -> sign -> sign -> Result morphism
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reillyinclusion lid s1 s2 = if is_subsig lid s1 s2 then subsig_inclusion lid s1 s2
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly else fail $ "Attempt to construct inclusion between non-subsignatures:\n"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ++ showDoc (Set.difference (sym_of lid s1) $ sym_of lid s2) ""
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly{- | semi lattices with top (needed for sublogics). Note that `Ord` is
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reillyonly used for efficiency and is not related to the /partial/ order given
842ae753ab848a8508c4832ab64296b929167a97Christian Maederby the lattice. Only `Eq` is used to define `isSubElem` -}
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblettclass (Ord l, Show l) => SemiLatticeWithTop l where
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett join :: l -> l -> l
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance SemiLatticeWithTop () where
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett join _ _ = ()
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett-- | less or equal for semi lattices
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'ReillyisSubElem :: SemiLatticeWithTop l => l -> l -> Bool
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'ReillyisSubElem a b = join a b == b
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | class providing the minimal sublogic of an item
842ae753ab848a8508c4832ab64296b929167a97Christian Maederclass MinSublogic sublogic item where
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder minSublogic :: item -> sublogic
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | a default instance for no sublogics
842ae753ab848a8508c4832ab64296b929167a97Christian Maederinstance MinSublogic () a where
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder minSublogic _ = ()
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | class providing also the projection of an item to a sublogic
842ae753ab848a8508c4832ab64296b929167a97Christian Maederclass MinSublogic sublogic item => ProjectSublogic sublogic item where
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder projectSublogic :: sublogic -> item -> item
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett-- | a default instance for no sublogics
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettinstance ProjectSublogic () b where
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett projectSublogic _ = id
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly-- | like ProjectSublogic, but providing a partial projection
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyclass MinSublogic sublogic item => ProjectSublogicM sublogic item where
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly projectSublogicM :: sublogic -> item -> Maybe item
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly-- | a default instance for no sublogics
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyinstance ProjectSublogicM () b where
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly projectSublogicM _ = Just
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | a class for providing a sublogi name
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyclass SublogicName l where
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sublogicName :: l -> String
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyinstance SublogicName () where
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sublogicName () = ""
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly{- Type class logic. The central type class of Hets, providing the
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly interface for logics. This type class is instantiated for many logics,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly and it is used for the logic independent parts of Hets.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly It hence provides an abstraction barrier between logic specific and
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly logic indepdendent code.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly This type class extends the class StaticAnalysis by a sublogic mechanism.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Sublogics are important since they avoid the need to provide an own
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly instance of the class logic for each sublogic. Instead, the sublogic
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly can use the datastructures and operations of the main logic, and
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly functions are provided to test whether a given item lies within the
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly sublogic. Also, projection functions from a super-logic to a sublogic
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly are provided.
842ae753ab848a8508c4832ab64296b929167a97Christian Maederclass (StaticAnalysis lid
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly basic_spec sentence symb_items symb_map_items
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly sign morphism symbol raw_symbol,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly SemiLatticeWithTop sublogics,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly MinSublogic sublogics sentence,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ProjectSublogic sublogics basic_spec,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ProjectSublogicM sublogics symb_items,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ProjectSublogicM sublogics symb_map_items,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ProjectSublogic sublogics sign,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ProjectSublogic sublogics morphism,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ProjectSublogicM sublogics symbol,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Convertible sublogics,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly SublogicName sublogics,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Ord proof_tree, Show proof_tree,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Convertible proof_tree)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder => Logic lid sublogics
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder basic_spec sentence symb_items symb_map_items
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett sign morphism symbol raw_symbol proof_tree
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder | lid -> sublogics
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder basic_spec sentence symb_items symb_map_items
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder sign morphism symbol raw_symbol proof_tree
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly -- | stability of the implementation
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly stability :: lid -> Stability
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder stability _ = Experimental
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- | for a process logic, return its data logic
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder data_logic :: lid -> Maybe AnyLogic
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder data_logic _ = Nothing
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett -- | the top sublogic, corresponding to the whole logic
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett top_sublogic :: lid -> sublogics
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett top_sublogic _ = top
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly -- | list all the sublogics of the current logic
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly all_sublogics :: lid -> [sublogics]
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly all_sublogics li = [top_sublogic li]
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly {- | provide the embedding of a projected signature into the
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly original signature -}
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly proj_sublogic_epsilon :: lid -> sublogics -> sign -> morphism
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly proj_sublogic_epsilon _ _ = ide
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ----------------------- provers ---------------------------
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -- | several provers can be provided. See module "Logic.Prover"
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly provers :: lid -> [Prover sign sentence morphism sublogics proof_tree]
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly provers _ = [] -- default implementation
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -- | consistency checkers
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly cons_checkers :: lid
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -> [ConsChecker sign sentence
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly sublogics morphism proof_tree]
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly cons_checkers _ = [] -- default implementation
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -- | conservativity checkers
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly conservativityCheck :: lid
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly -> [ConservativityChecker sign sentence morphism]
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly conservativityCheck _ = []
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -- | the empty proof tree
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly empty_proof_tree :: lid -> proof_tree
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly empty_proof_tree l = statError l "empty_proof_tree"
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly ----------------------- OMDoc ---------------------------
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly export_symToOmdoc :: lid -> OMDoc.NameMap symbol
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -> symbol -> String -> Result OMDoc.TCElement
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly -- default implementation
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly export_symToOmdoc l _ _ = statError l "export_symToOmdoc"
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly export_senToOmdoc :: lid -> OMDoc.NameMap symbol
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -> sentence -> Result OMDoc.TCorOMElement
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -- default implementation
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly export_senToOmdoc l _ _ = statError l "export_senToOmdoc"
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -- | additional information which have to be exported can be
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -- exported by this function
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly export_theoryToOmdoc :: lid -> OMDoc.SigMap symbol -> sign
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -> [Named sentence] -> Result [OMDoc.TCElement]
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -- default implementation does no extra export
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -- , sufficient in some cases
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly export_theoryToOmdoc _ _ _ _ = return []
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly omdoc_metatheory :: lid -> Maybe OMDoc.OMCD
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly -- default implementation, no logic should throw an error here
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly -- and the base of omcd should be a parseable URI
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly omdoc_metatheory _lid = Nothing
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly----------------------------------------------------------------
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett-- Derived functions
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly----------------------------------------------------------------
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett-- | the empty theory
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'ReillyemptyTheory :: StaticAnalysis lid
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly basic_spec sentence symb_items symb_map_items
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly sign morphism symbol raw_symbol =>
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly lid -> Theory sign sentence proof_tree
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'ReillyemptyTheory lid = Theory (empty_signature lid) Map.empty
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly----------------------------------------------------------------
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly-- Existential type covering any logic
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly----------------------------------------------------------------
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly-- | the disjoint union of all logics
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reillydata AnyLogic = forall lid sublogics
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly basic_spec sentence symb_items symb_map_items
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly sign morphism symbol raw_symbol proof_tree .
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly Logic lid sublogics
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly basic_spec sentence symb_items symb_map_items
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder sign morphism symbol raw_symbol proof_tree =>
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly deriving Typeable
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reillyinstance GetRange AnyLogic
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reillyinstance Show AnyLogic where
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly show (Logic lid) = language_name lid
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reillyinstance Eq AnyLogic where
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett Logic lid1 == Logic lid2 = language_name lid1 == language_name lid2
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly{- class hierarchy:
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Sentences Syntax
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly StaticAnalysis (no sublogics)