Logic.hs revision a7be28e157e9ceeec73a8fd0e642c36ea29d4218
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder{-# LANGUAGE UndecidableInstances #-}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederDescription : central interface (type class) for logics in Hets
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2006
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : till@informatik.uni-bremen.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederPortability : non-portable (various -fglasgow-exts extensions)
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaederCentral interface (type class) for logics in Hets
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiProvides data structures for logics (with symbols). Logics are
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski a type class with an /identity type/ (usually interpreted
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder by a singleton set) which serves to treat logics as
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder data. All the functions in the type class take the
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder identity as first argument in order to determine the logic.
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder For logic (co)morphisms see "Logic.Comorphism"
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder This module uses multiparameter type classes with functional dependencies
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder (<http://www.haskell.org/haskellwiki/Functional_dependencies>)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder for defining an interface for the notion of logic. Multiparameter type
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder classes are needed because a logic consists of a collection of types,
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder together with operations on these. Functional dependencies
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder are needed because no operation will involve all types of
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder the multiparameter type class; hence we need a method to derive
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder the missing types. We chose an easy way: for each logic, we
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder introduce a new singleton type that is the name, or constitutes the identity
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder of the logic. All other types of the multiparameter type class
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder depend on this /identity constituting/ type, and all operations take
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder the 'identity constituting' type as first arguments. The value
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder of the argument of the /identity constituting/ type is irrelevant
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder (note that there is only one value of such a type anyway).
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder Note that we tend to use @lid@ both for the /identity type/
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder of a logic, as well as for its unique inhabitant, i.e. @lid :: lid@.
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder The other types involved in the definition of logic are as follows:
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder * sign: signatures, that is, contexts, or non-logical vocabularies,
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder typically consisting of a set of declared sorts, predicates,
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder function symbols, propositional letters etc., together with their
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder * sentence: logical formulas.
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder * basic_spec: abstract syntax of basic specifications. The latter are
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder human-readable presentations of a signature together with some sentences.
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder * symbol: symbols that may occur in a signature, fully qualified
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder with their types
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder * raw_symbol: symbols that may occur in a signature, possibly not
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder or partially qualified
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder * morphism: maps between signatures (typically preserving the structure).
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder * symb_items: abstract syntax of symbol lists, used for declaring some
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder symbols of a signature as hidden.
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder * symb_map_items: abstract syntax of symbol maps, i.e. human-readable
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder presentations of signature morphisms.
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder * sublogics: sublogics of the given logic. This type might be a
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder record of Boolean flags, indicating whether some feature is
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder present in the sublogi of not.
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder * proof_tree: proof trees.
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder J. A. Goguen and R. M. Burstall
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder Institutions: Abstract Model Theory for Specification and
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang JACM 39, p. 95-146, 1992
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder (general notion of logic - model theory only)
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder General Logics
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Logic Colloquium 87, p. 275-329, North Holland, 1989
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder (general notion of logic - also proof theory;
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder notion of logic representation, called map there)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder T. Mossakowski:
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Specification in an arbitrary institution with symbols
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder 14th WADT 1999, LNCS 1827, p. 252-270
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (treatment of symbols and raw symbols, see also CASL semantics
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder in the CASL reference manual)
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder T. Mossakowski, B. Klin:
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich Institution Independent Static Analysis for CASL
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder 15h WADT 2001, LNCS 2267, p. 221-237, 2002.
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich (what is needed for static anaylsis)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski S. Autexier and T. Mossakowski
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Integrating HOLCASL into the Development Graph Manager MAYA
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu FroCoS 2002, LNCS 2309, p. 2-17, 2002.
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder (interface to provers)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder CoFI (ed.): CASL Reference Manual, LNCS 2960, Springer Verlag, 2004.
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder (static semantics of CASL structured and architectural specifications)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder T. Mossakowski
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Heterogeneous specification and the heterogeneous tool set
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Habilitation thesis, University of Bremen, 2005
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (the general picture of heterogeneous specification)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maederimport Logic.Prover (Prover, ConsChecker, Theory(..))
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maederimport Taxonomy.MMiSSOntology (MMiSSOntology)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maederimport Common.ATerm.Lib (ShATermConvertible)
9a6779c8495854bdf36e4a87f98f095e8d0a6e45Christian Maederimport qualified Data.Set as Set
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maederimport qualified Data.Map as Map
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maederimport qualified OMDoc.DataTypes as OMDoc
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder-- | Stability of logic implementations
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maederdata Stability = Stable | Testing | Unstable | Experimental
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder deriving (Eq, Show)
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder-- | shortcut for class constraints
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maederclass (Show a, Pretty a, Typeable a, ShATermConvertible a)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder => PrintTypeConv a
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder-- | shortcut for class constraints with equality
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maederclass (Eq a, PrintTypeConv a) => EqPrintTypeConv a
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maederinstance (Show a, Pretty a, Typeable a,
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder ShATermConvertible a) => PrintTypeConv a
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maederinstance (Eq a, PrintTypeConv a) => EqPrintTypeConv a
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder-- | maps from a to a
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedertype EndoMap a = Map.Map a a
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder{- | the name of a logic.
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Define instances like "data CASL = CASL deriving Show"
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederclass Show lid => Language lid where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder language_name :: lid -> String
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder language_name i = show i
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder description :: lid -> String
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -- default implementation
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder description _ = "No description available"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder{- | Categories are given as usual: objects, morphisms, identities,
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder domain, codomain and composition. The type id is the name, or
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder the identity of the category. It is an argument to all functions
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder of the type class, serving disambiguation among instances
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder (via the functional dependency lid -> object morphism).
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder The types for objects and morphisms may be restricted to
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder subtypes, using legal_obj and legal_mor. For example, for the
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski category of sets and injective maps, legal_mor would check
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder injectivity. Since Eq is a subclass of Category, it is also
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski possible to impose a quotient on the types for objects and morphisms.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Require Ord instances only for efficiency, i.e. in sets or maps.
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maederclass (Ord object, Ord morphism)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder => Category object morphism | morphism -> object where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- | identity morphisms
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder ide :: object -> morphism
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder -- | composition, in diagrammatic order
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder comp :: morphism -> morphism -> Result morphism
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -- | domain and codomain of morphisms
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder dom, cod :: morphism -> object
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- | the inverse of a morphism
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder inverse :: morphism -> Result morphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder inverse _ = fail "Logic.Logic.Category.inverse not implemented"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- | test if the signature morphism an inclusion
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder isInclusion :: morphism -> Bool
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder isInclusion _ = False -- in general no inclusion
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- | is a value of type morphism denoting a legal morphism?
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder legal_mor :: morphism -> Bool
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maederinstance Ord sign => Category sign (DefaultMorphism sign) where
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder dom = domOfDefaultMorphism
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder cod = codOfDefaultMorphism
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder ide = ideOfDefaultMorphism
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder isInclusion = isInclusionDefaultMorphism
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder comp = compOfDefaultMorphism
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder legal_mor = legalDefaultMorphism (const True)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{- | Abstract syntax, parsing and printing.
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder There are three types for abstract syntax:
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder basic_spec is for basic specifications (see CASL RefMan p. 5ff.),
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder symb_items is for symbol lists (see CASL RefMan p. 35ff.),
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder symb_map_items is for symbol maps (see CASL RefMan p. 35ff.).
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederclass (Language lid, PrintTypeConv basic_spec,
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder EqPrintTypeConv symb_items,
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder EqPrintTypeConv symb_map_items)
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder => Syntax lid basic_spec symb_items symb_map_items
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski | lid -> basic_spec symb_items symb_map_items
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder -- | parser for basic specifications
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder parse_basic_spec :: lid -> Maybe(AParser st basic_spec)
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder -- | parser for symbol lists
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder parse_symb_items :: lid -> Maybe(AParser st symb_items)
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder -- | parser for symbol maps
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder parse_symb_map_items :: lid -> Maybe(AParser st symb_map_items)
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder -- default implementations
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz parse_basic_spec _ = Nothing
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder parse_symb_items _ = Nothing
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder parse_symb_map_items _ = Nothing
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder{- | Sentences, provers and symbols.
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder Provers capture the entailment relation between sets of sentences
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder and sentences. They may return proof trees witnessing proofs.
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder Signatures are equipped with underlying sets of symbols
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder (such that the category of signatures becomes a concrete category),
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder see CASL RefMan p. 191ff.
4e3c46a1ca40d50a045342c5fab25b5db4fa9a87Christian Maederclass (Language lid, Category sign morphism, Ord sentence,
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder Ord symbol, -- for efficient lookup
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder PrintTypeConv sign, PrintTypeConv morphism,
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz PrintTypeConv sentence, PrintTypeConv symbol)
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz => Sentences lid sentence sign morphism symbol
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz | lid -> sentence sign morphism symbol
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ----------------------- sentences ---------------------------
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- | check whether a sentence belongs to a signature
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder is_of_sign :: lid -> sentence -> signature -> Bool
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder is_of_sign l _ _ = error $ statErrMsg l "is_of_sign"
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- | sentence translation along a signature morphism
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder map_sen :: lid -> morphism -> sentence -> Result sentence
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder map_sen l _ _ = statErr l "map_sen"
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- | simplification of sentences (leave out qualifications)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder simplify_sen :: lid -> sign -> sentence -> sentence
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder simplify_sen _ _ = id -- default implementation
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -- | parsing of sentences
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder parse_sentence :: lid -> Maybe (AParser st sentence)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder parse_sentence _ = Nothing
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder print_sign :: lid -> sign -> Doc
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder print_sign _ = pretty
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -- | print a sentence with comments
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder print_named :: lid -> Named sentence -> Doc
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder print_named _ = printAnnoted (addBullet . pretty) . fromLabelledSen
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder ----------------------- symbols ---------------------------
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder -- | set of symbols for a signature
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder sym_of :: lid -> sign -> Set.Set symbol
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder sym_of l _ = error $ statErrMsg l "sym_of"
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -- | symbol map for a signature morphism
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder symmap_of :: lid -> morphism -> EndoMap symbol
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder symmap_of l _ = error $ statErrMsg l "symmap_of"
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder -- | symbols have a name, see CASL RefMan p. 192
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder sym_name :: lid -> symbol -> Id
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder sym_name l _ = error $ statErrMsg l "sym_name"
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder-- | a dummy static analysis function to allow type checking *.inline.hs files
568da6120906d5283c4322114eee10f24ea8dd6dChristian MaederinlineAxioms :: StaticAnalysis lid
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder basic_spec sentence symb_items symb_map_items
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder sign morphism symbol raw_symbol => lid -> String -> [Named sentence]
4e144aa4be1f50519f8fa377a7883edfbc76d406Christian MaederinlineAxioms _ _ = error "inlineAxioms"
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder-- | fail function for static analysis
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaederstatErr :: (Language lid, Monad m) => lid -> String -> m a
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederstatErr lid = fail . statErrMsg lid
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- | error message for static analysis
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaederstatErrMsg :: (Language lid) => lid -> String -> String
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederstatErrMsg lid str = "Logic." ++ str ++ " nyi for: " ++ language_name lid
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder{- static analysis
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder This type class provides the data needed for an institution with symbols,
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder as explained in the structured specification semantics in the CASL
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder reference manual, chapter III.4.
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder The static analysis computes signatures from basic specifications,
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder and signature morphisms from symbol lists and symbol maps. The latter
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder needs an intermediate stage, so-called raw symbols, which are possibly
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder unqualified symbols. Normal symbols are always fully qualified.
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder In the CASL reference manual, our symbols are called "signature symbols",
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder and our raw symbols are called "symbols". (Terminology should be adapted.)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maederclass ( Syntax lid basic_spec symb_items symb_map_items
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , Sentences lid sentence sign morphism symbol
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder , Ord raw_symbol, Pretty raw_symbol, Typeable raw_symbol)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder => StaticAnalysis lid
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder basic_spec sentence symb_items symb_map_items
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder sign morphism symbol raw_symbol
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder | lid -> basic_spec sentence symb_items symb_map_items
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder sign morphism symbol raw_symbol
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder ----------------------- static analysis ---------------------------
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder {- | static analysis of basic specifications and symbol maps.
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder The resulting bspec has analyzed axioms in it.
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder The resulting sign is an extension of the input sign
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder plus newly declared or redeclared symbols.
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder See CASL RefMan p. 138 ff. -}
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder basic_analysis :: lid ->
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Maybe((basic_spec, -- abstract syntax tree
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder sign, -- input signature, for the local
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- environment, carrying the previously
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- declared symbols
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder GlobalAnnos) -> -- global annotations
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder Result (basic_spec, ExtSign sign symbol
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder , [Named sentence]))
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- default implementation
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder basic_analysis _ = Nothing
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- | static analysis of symbol maps, see CASL RefMan p. 222f.
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder stat_symb_map_items ::
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder lid -> [symb_map_items] -> Result (EndoMap raw_symbol)
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder stat_symb_map_items l _ = statErr l "stat_symb_map_items"
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- | static analysis of symbol lists, see CASL RefMan p. 221f.
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder stat_symb_items :: lid -> [symb_items] -> Result [raw_symbol]
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder stat_symb_items l _ = statErr l "stat_symb_items"
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder ------------------------- amalgamation ---------------------------
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder {- | Computation of colimits of signature diagram.
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Indeed, it suffices to compute a coconce that is weakly amalgamable
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder see Till Mossakowski,
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Heterogeneous specification and the heterogeneous tool set
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- | architectural sharing analysis, see CASL RefMan p. 247ff.
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ensures_amalgamability :: lid ->
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ([CASLAmalgOpt], -- the program options
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Gr sign (Int,morphism), -- the diagram to be analyzed
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder [(Int, morphism)], -- the sink
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Gr String String) -- the descriptions of nodes and edges
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> Result Amalgamates
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ensures_amalgamability l _ = warning Amalgamates
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ("amalgamability test not implemented for logic " ++ show l)
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder -- | signature colimits
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder signature_colimit :: lid -> Gr sign (Int, morphism)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> Result (sign, Map.Map Int morphism)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski signature_colimit l _ = statErr l "signature_colimit"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder {- | rename and qualify the symbols considering a united incoming
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder morphisms, code out overloading and
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder create sentences for the overloading relation -}
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder qualify :: lid -> SIMPLE_ID -> LIB_ID -> morphism -> sign
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> Result (morphism, [Named sentence])
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder qualify l _ _ _ _ = statErr l "qualify"
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder -------------------- symbols and raw symbols ---------------------
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder {- | Construe a symbol, like f:->t, as a raw symbol.
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder This is a one-sided inverse to the function SymSySigSym
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in the CASL RefMan p. 192. -}
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder symbol_to_raw :: lid -> symbol -> raw_symbol
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder symbol_to_raw l _ = error $ statErrMsg l "symbol_to_raw"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder {- | Construe an identifier, like f, as a raw symbol.
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder See CASL RefMan p. 192, function IDAsSym -}
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder id_to_raw :: lid -> Id -> raw_symbol
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder id_to_raw l _ = error $ statErrMsg l "id_to_raw"
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder {- | Check wether a symbol matches a raw symbol, for
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder example, f:s->t matches f. See CASL RefMan p. 192 -}
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder matches :: lid -> symbol -> raw_symbol -> Bool
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder matches l _ _ = error $ statErrMsg l "matches"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder --------------- operations on signatures and morphisms -----------
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- | the empty (initial) signature, see CASL RefMan p. 193
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder empty_signature :: lid -> sign
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- | union of signatures, see CASL RefMan p. 193
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder signature_union :: lid -> sign -> sign -> Result sign
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder signature_union l _ _ = statErr l "signature_union"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- | intersection of signatures
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder intersection :: lid -> sign -> sign -> Result sign
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder intersection l _ _ = statErr l "intersection"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- | final union of signatures, see CASL RefMan p. 194
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder final_union :: lid -> sign -> sign -> Result sign
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder final_union l _ _ = statErr l "final_union"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- | union of signature morphims, see CASL RefMan p. 196
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder morphism_union :: lid -> morphism -> morphism -> Result morphism
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder morphism_union l _ _ = statErr l "morphism_union"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- | subsignatures, see CASL RefMan p. 194
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder is_subsig :: lid -> sign -> sign -> Bool
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder is_subsig _ _ _ = False
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder {- | construct the inclusion morphisms between subsignatures,
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder see CASL RefMan p. 194 -}
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder subsig_inclusion :: lid -> sign -> sign -> Result morphism
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder subsig_inclusion l _ _ = statErr l "subsig_inclusion"
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder {- | the signature (co)generated by a set of symbols in another
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder signature is the smallest (largest) signature containing
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (excluding) the set of symbols. Needed for revealing and
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder hiding, see CASL RefMan p. 197ff. -}
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder generated_sign, cogenerated_sign ::
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder lid -> Set.Set symbol -> sign -> Result morphism
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder generated_sign l _ _ = statErr l "generated_sign"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder cogenerated_sign l _ _ = statErr l "cogenerated_sign"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder {- | Induce a signature morphism from a source signature and
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder a raw symbol map. Needed for translation (SP with SM).
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder See CASL RefMan p. 198 -}
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder induced_from_morphism ::
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder lid -> EndoMap raw_symbol -> sign -> Result morphism
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder induced_from_morphism l _ _ = statErr l "induced_from_morphism"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder {- | Induce a signature morphism between two signatures by a
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder raw symbol map. Needed for instantiation and views.
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder See CASL RefMan p. 198f. -}
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder induced_from_to_morphism ::
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder lid -> EndoMap raw_symbol -> ExtSign sign symbol
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> ExtSign sign symbol -> Result morphism
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder induced_from_to_morphism l _ _ _ =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder statErr l "induced_from_to_morphism"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder {- | Check whether a signature morphism is transportable.
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder See CASL RefMan p. 304f. -}
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder is_transportable :: lid -> morphism -> Bool
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder is_transportable _ _ = False -- safe default
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder {- | Check whether the underlying symbol map of a signature morphism
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder is injective -}
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder is_injective :: lid -> morphism -> Bool
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder is_injective _ _ = False -- safe default
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ------------------- generate taxonomy from theory ----------------
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- | generate an ontological taxonomy, if this makes sense
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder theory_to_taxonomy :: lid
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -> TaxoGraphKind
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -> MMiSSOntology
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -> sign -> [Named sentence]
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -> Result MMiSSOntology
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder theory_to_taxonomy l _ _ _ _ = statErr l "theory_to_taxonomy"
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder-- | subsignatures, see CASL RefMan p. 194
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederinclusion :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder sign morphism symbol raw_symbol
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder => lid -> sign -> sign -> Result morphism
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maederinclusion lid s1 s2 = if is_subsig lid s1 s2 then subsig_inclusion lid s1 s2
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder else fail $ "Attempt to construct inclusion between non-subsignatures:\n"
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder ++ showDoc (Set.difference (sym_of lid s1) $ sym_of lid s2) ""
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder{- | semi lattices with top (needed for sublogics). Note that `Ord` is
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maederonly used for efficiency and is not related to the /partial/ order given
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maederby the lattice. Only `Eq` is used to define `isSubElem` -}
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederclass (Ord l, Show l) => SemiLatticeWithTop l where
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder join :: l -> l -> l
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maederinstance SemiLatticeWithTop () where
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder join _ _ = ()
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | less or equal for semi lattices
fa167e362877db231378e17ba49c66fbb84862fcChristian MaederisSubElem :: SemiLatticeWithTop l => l -> l -> Bool
fa167e362877db231378e17ba49c66fbb84862fcChristian MaederisSubElem a b = join a b == b
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder-- | class providing the minimal sublogic of an item
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maederclass MinSublogic sublogic item where
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder minSublogic :: item -> sublogic
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder-- | a default instance for no sublogics
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maederinstance MinSublogic () a where
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder minSublogic _ = ()
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- | class providing also the projection of an item to a sublogic
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maederclass MinSublogic sublogic item => ProjectSublogic sublogic item where
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder projectSublogic :: sublogic -> item -> item
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder-- | a default instance for no sublogics
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maederinstance ProjectSublogic () b where
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder projectSublogic _ = id
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder-- | like ProjectSublogic, but providing a partial projection
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maederclass MinSublogic sublogic item => ProjectSublogicM sublogic item where
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder projectSublogicM :: sublogic -> item -> Maybe item
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder-- | a default instance for no sublogics
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederinstance ProjectSublogicM () b where
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder projectSublogicM _ = Just
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder-- | a class for providing a sublogi name
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maederclass SublogicName l where
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder sublogicName :: l -> String
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maederinstance SublogicName () where
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder sublogicName () = ""
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder{- Type class logic. The central type class of Hets, providing the
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder interface for logics. This type class is instantiated for many logics,
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder and it is used for the logic independent parts of Hets.
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder It hence provides an abstraction barrier between logic specific and
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder logic indepdendent code.
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder This type class extends the class StaticAnalysis by a sublogic mechanism.
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder Sublogics are important since they avoid the need to provide an own
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder instance of the class logic for each sublogic. Instead, the sublogic
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder can use the datastructures and operations of the main logic, and
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder functions are provided to test whether a given item lies within the
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder sublogic. Also, projection functions from a super-logic to a sublogic
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder are provided.
74d9a385499bf903b24848dff450a153f525bda7Christian Maederclass (StaticAnalysis lid
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder basic_spec sentence symb_items symb_map_items
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder sign morphism symbol raw_symbol,
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder SemiLatticeWithTop sublogics,
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski MinSublogic sublogics sentence,
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski ProjectSublogic sublogics basic_spec,
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder ProjectSublogicM sublogics symb_items,
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder ProjectSublogicM sublogics symb_map_items,
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ProjectSublogic sublogics sign,
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski ProjectSublogic sublogics morphism,
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder ProjectSublogicM sublogics symbol,
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder Typeable sublogics,
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder ShATermConvertible sublogics,
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder SublogicName sublogics,
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder Eq proof_tree, Show proof_tree, ShATermConvertible proof_tree,
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder Ord proof_tree, Typeable proof_tree)
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder => Logic lid sublogics
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder basic_spec sentence symb_items symb_map_items
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder sign morphism symbol raw_symbol proof_tree
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder | lid -> sublogics
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder basic_spec sentence symb_items symb_map_items
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder sign morphism symbol raw_symbol proof_tree
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder -- | stability of the implementation
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder stability :: lid -> Stability
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder stability _ = Experimental
b2eb5854497af395cbf17a08c7ace5ab73e7eea2Christian Maeder -- | for a process logic, return its data logic
b2eb5854497af395cbf17a08c7ace5ab73e7eea2Christian Maeder data_logic :: lid -> Maybe AnyLogic
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder data_logic _ = Nothing
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder -- | the top sublogic, corresponding to the whole logic
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder top_sublogic :: lid -> sublogics
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder top_sublogic _ = top
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder -- | list all the sublogics of the current logic
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder all_sublogics :: lid -> [sublogics]
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder all_sublogics li = [top_sublogic li]
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder {- | provide the embedding of a projected signature into the
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder original signature -}
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder proj_sublogic_epsilon :: lid -> sublogics -> sign -> morphism
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder proj_sublogic_epsilon _ _ s = ide s
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ----------------------- provers ---------------------------
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder -- | several provers can be provided. See module "Logic.Prover"
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder provers :: lid -> [Prover sign sentence morphism sublogics proof_tree]
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder provers _ = [] -- default implementation
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder -- | consistency checkers
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder cons_checkers :: lid
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder -> [ConsChecker sign sentence
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder sublogics morphism proof_tree]
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder cons_checkers _ = [] -- default implementation
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder -- | conservativity checkers
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder conservativityCheck :: lid
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder -> [ConservativityChecker sign sentence morphism]
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder conservativityCheck _ = []
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder -- | the empty proof tree
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder empty_proof_tree :: lid -> proof_tree
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder empty_proof_tree l = error $ statErrMsg l "empty_proof_tree"
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski ----------------------- OMDoc ---------------------------
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder export_signToOmdoc :: lid -> SIMPLE_ID -> LIB_ID -> sign
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder -- default implementation
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder export_signToOmdoc lid _ _ _ =
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder error $ "exportSignToOmdoc not yet implemented "
5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder ++ "for logic " ++ (show lid)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder export_morphismToOmdoc :: lid -> SIMPLE_ID -> LIB_ID -> morphism
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder -- default implementation
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder export_morphismToOmdoc lid _ _ _ =
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski error $ "exportMorphismToOmdoc not yet implemented "
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder ++ "for logic " ++ (show lid)
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder export_senToOmdoc :: lid -> SIMPLE_ID -> LIB_ID -> sign
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder -> Named sentence -> [OMDoc.TCElement]
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder -- default implementation
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder export_senToOmdoc lid _ _ _ _ =
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder error $ "exportSenToOmdoc not yet implemented "
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder ++ "for logic " ++ (show lid)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder----------------------------------------------------------------
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder-- Derived functions
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder----------------------------------------------------------------
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder-- | the empty theory
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian Maederempty_theory :: StaticAnalysis lid
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder basic_spec sentence symb_items symb_map_items
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder sign morphism symbol raw_symbol =>
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder lid -> Theory sign sentence proof_tree
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiempty_theory lid = Theory (empty_signature lid) Map.empty
32562a567baac248a00782d2727716c13117dc4aChristian Maeder----------------------------------------------------------------
32562a567baac248a00782d2727716c13117dc4aChristian Maeder-- Existential type covering any logic
32562a567baac248a00782d2727716c13117dc4aChristian Maeder----------------------------------------------------------------
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder-- | the disjoint union of all logics
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maederdata AnyLogic = forall lid sublogics
fa373bc327620e08861294716b4454be8d25669fChristian Maeder basic_spec sentence symb_items symb_map_items
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder sign morphism symbol raw_symbol proof_tree .
fa373bc327620e08861294716b4454be8d25669fChristian Maeder Logic lid sublogics
fa373bc327620e08861294716b4454be8d25669fChristian Maeder basic_spec sentence symb_items symb_map_items
fa373bc327620e08861294716b4454be8d25669fChristian Maeder sign morphism symbol raw_symbol proof_tree =>
fa373bc327620e08861294716b4454be8d25669fChristian Maeder deriving Typeable
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maederinstance Show AnyLogic where
32562a567baac248a00782d2727716c13117dc4aChristian Maeder show (Logic lid) = language_name lid
32562a567baac248a00782d2727716c13117dc4aChristian Maederinstance Eq AnyLogic where
32562a567baac248a00782d2727716c13117dc4aChristian Maeder Logic lid1 == Logic lid2 = language_name lid1 == language_name lid2
fa373bc327620e08861294716b4454be8d25669fChristian Maeder{- class hierarchy:
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Sentences Syntax
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder StaticAnalysis (no sublogics)