4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{-# OPTIONS -fallow-undecidable-instances #-}

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |

e47d29b522739fbf08aac80c6faa447dde113fbcChristian MaederModule : $Header$

11d6ec73ee5550e00cb56b221bdbeb709142e779Christian MaederDescription : central interface (type class) for logics in Hets

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2006

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : till@informatik.uni-bremen.de

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : provisional

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian MaederPortability : non-portable (various -fglasgow-exts extensions)

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederCentral interface (type class) for logics in Hets

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian MaederProvides data structures for logics (with symbols). Logics are

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder a type class with an /identity type/ (usually interpreted

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder by a singleton set) which serves to treat logics as

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder data. All the functions in the type class take the

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder identity as first argument in order to determine the logic.

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder For logic (co)morphisms see "Logic.Comorphism"

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder This module uses multiparameter type classes with functional dependencies

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder (<http://www.haskell.org/haskellwiki/Functional_dependencies>)

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder for defining an interface for the notion of logic. Multiparameter type

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder classes are needed because a logic consists of a collection of types,

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder together with operations on these. Functional dependencies

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder are needed because no operation will involve all types of

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder the multiparameter type class; hence we need a method to derive

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder the missing types. We chose an easy way: for each logic, we

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder introduce a new singleton type that is the name, or constitutes the identity

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder of the logic. All other types of the multiparameter type class

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder depend on this /identity constituting/ type, and all operations take

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder the 'identity constituting' type as first arguments. The value

62925f4a144f45b5ed1e7c841f891d13f51e553dChristian Maeder of the argument of the /identity constituting/ type is irrelevant

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder (note that there is only one value of such a type anyway).

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Note that we tend to use @lid@ both for the /identity type/

cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian Maeder of a logic, as well as for its unique inhabitant, i.e. @lid :: lid@.

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder The other types involved in the definition of logic are as follows:

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder * sign: signatures, that is, contexts, or non-logical vocabularies,

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder typically consisting of a set of declared sorts, predicates,

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder function symbols, propositional letters etc., together with their

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder typing.

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder * sentence: logical formulas.

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder * basic_spec: abstract syntax of basic specifications. The latter are

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder human-readable presentations of a signature together with some sentences.

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder * symbol: symbols that may occur in a signature, fully qualified

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder with their types

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder * raw_symbol: symbols that may occur in a signature, possibly not

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder or partially qualified

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder * morphism: maps between signatures (typically preserving the structure).

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder * symb_items: abstract syntax of symbol lists, used for declaring some

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder symbols of a signature as hidden.

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder * symb_map_items: abstract syntax of symbol maps, i.e. human-readable

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder presentations of signature morphisms.

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder * sublogics: sublogics of the given logic. This type might be a

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder record of Boolean flags, indicating whether some feature is

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder present in the sublogi of not.

fa45d098e1c9d468f128be9505eb7e5b2705b304Christian Maeder

25612a7b3ce708909298d5426406592473880a20Christian Maeder * proof_tree: proof trees.

d48085f765fca838c1d972d2123601997174583dChristian Maeder

c1db3d36c29a6324745a86dbcba18b8e4cd9f338Christian Maeder References:

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder J. A. Goguen and R. M. Burstall

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder Institutions: Abstract Model Theory for Specification and

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder Programming

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder JACM 39, p. 95-146, 1992

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (general notion of logic - model theory only)

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder

18b709ce961d68328da768318dcc70067f066d86Christian Maeder J. Meseguer

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder General Logics

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder Logic Colloquium 87, p. 275-329, North Holland, 1989

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder (general notion of logic - also proof theory;

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder notion of logic representation, called map there)

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder T. Mossakowski:

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder Specification in an arbitrary institution with symbols

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder 14th WADT 1999, LNCS 1827, p. 252-270

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder (treatment of symbols and raw symbols, see also CASL semantics

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder in the CASL reference manual)

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder T. Mossakowski, B. Klin:

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder Institution Independent Static Analysis for CASL

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder 15h WADT 2001, LNCS 2267, p. 221-237, 2002.

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder (what is needed for static anaylsis)

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder S. Autexier and T. Mossakowski

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder Integrating HOLCASL into the Development Graph Manager MAYA

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder FroCoS 2002, LNCS 2309, p. 2-17, 2002.

18b709ce961d68328da768318dcc70067f066d86Christian Maeder (interface to provers)

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder CoFI (ed.): CASL Reference Manual, LNCS 2960, Springer Verlag, 2004.

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder (static semantics of CASL structured and architectural specifications)

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder T. Mossakowski

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Heterogeneous specification and the heterogeneous tool set

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder Habilitation thesis, University of Bremen, 2005

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder (the general picture of heterogeneous specification)

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder-}

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder

797f811e57952d59e73b8cd03b667eef276db972Christian Maedermodule Logic.Logic where

11d6ec73ee5550e00cb56b221bdbeb709142e779Christian Maeder

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maederimport Logic.Prover (Prover, ConsChecker, Theory(..))

797f811e57952d59e73b8cd03b667eef276db972Christian Maederimport Taxonomy.MMiSSOntology (MMiSSOntology)

797f811e57952d59e73b8cd03b667eef276db972Christian Maederimport ATC.DefaultMorphism ()

18b709ce961d68328da768318dcc70067f066d86Christian Maeder

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiimport Common.AS_Annotation

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maederimport Common.ATerm.Lib (ShATermConvertible)

b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maederimport Common.Amalgamate

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport Common.AnnoState

18b709ce961d68328da768318dcc70067f066d86Christian Maederimport Common.Consistency

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maederimport Common.DefaultMorphism

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maederimport Common.Doc

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maederimport Common.DocUtils

b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maederimport Common.ExtSign

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport Common.GlobalAnnotations

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport Common.Id

d5c415f6373274fed04d83b9322891f3b82e9c26Christian Maederimport Common.Lib.Graph

22fc8a1bd14dc53c5c7f482d2e0c04eb5ee4beb4Christian Maederimport Common.LibName

22fc8a1bd14dc53c5c7f482d2e0c04eb5ee4beb4Christian Maederimport Common.Result

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport Common.Taxonomy

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport qualified Data.Set as Set

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport qualified Data.Map as Map

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Data.Typeable

b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder-- | Stability of logic implementations

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederdata Stability = Stable | Testing | Unstable | Experimental

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder deriving (Eq, Show)

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder-- | shortcut for class constraints

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederclass (Show a, Pretty a, Typeable a, ShATermConvertible a)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder => PrintTypeConv a

b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder

65835942d66905c377fa503e0d577df5aade58feChristian Maeder-- | shortcut for class constraints with equality

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maederclass (Eq a, PrintTypeConv a) => EqPrintTypeConv a

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maederinstance (Show a, Pretty a, Typeable a,

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder ShATermConvertible a) => PrintTypeConv a

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maederinstance (Eq a, PrintTypeConv a) => EqPrintTypeConv a

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder

11d6ec73ee5550e00cb56b221bdbeb709142e779Christian Maeder-- | maps from a to a

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maedertype EndoMap a = Map.Map a a

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder{- | the name of a logic.

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder Define instances like "data CASL = CASL deriving Show"

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder-}

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maederclass Show lid => Language lid where

b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder language_name :: lid -> String

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder language_name i = show i

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder description :: lid -> String

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder -- default implementation

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder description _ = "No description available"

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder{- | Categories are given as usual: objects, morphisms, identities,

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder domain, codomain and composition. The type id is the name, or

b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder the identity of the category. It is an argument to all functions

65835942d66905c377fa503e0d577df5aade58feChristian Maeder of the type class, serving disambiguation among instances

65835942d66905c377fa503e0d577df5aade58feChristian Maeder (via the functional dependency lid -> object morphism).

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder The types for objects and morphisms may be restricted to

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder subtypes, using legal_obj and legal_mor. For example, for the

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder category of sets and injective maps, legal_mor would check

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder injectivity. Since Eq is a subclass of Category, it is also

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder possible to impose a quotient on the types for objects and morphisms.

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder-}

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederclass (Eq object, Eq morphism)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder => Category object morphism | morphism -> object where

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -- | identity morphisms

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder ide :: object -> morphism

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder -- | composition, in diagrammatic order

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder comp :: morphism -> morphism -> Result morphism

-- | domain and codomain of morphisms

dom, cod :: morphism -> object

-- | test if the signature morphism an inclusion

isInclusion :: morphism -> Bool

isInclusion _ = False -- in general no inclusion

-- | is a value of type morphism denoting a legal morphism?

legal_mor :: morphism -> Bool

instance Eq sign => Category sign (DefaultMorphism sign) where

dom = domOfDefaultMorphism

cod = codOfDefaultMorphism

ide = ideOfDefaultMorphism

isInclusion = isInclusionDefaultMorphism

comp = compOfDefaultMorphism

legal_mor = legalDefaultMorphism (const True)

{- | Abstract syntax, parsing and printing.

There are three types for abstract syntax:

basic_spec is for basic specifications (see CASL RefMan p. 5ff.),

symb_items is for symbol lists (see CASL RefMan p. 35ff.),

symb_map_items is for symbol maps (see CASL RefMan p. 35ff.).

-}

class (Language lid, PrintTypeConv basic_spec,

EqPrintTypeConv symb_items,

EqPrintTypeConv symb_map_items)

=> Syntax lid basic_spec symb_items symb_map_items

| lid -> basic_spec symb_items symb_map_items

where

-- | parser for basic specifications

parse_basic_spec :: lid -> Maybe(AParser st basic_spec)

-- | parser for symbol lists

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

-- | parser for symbol maps

parse_symb_map_items :: lid -> Maybe(AParser st symb_map_items)

-- default implementations

parse_basic_spec _ = Nothing

parse_symb_items _ = Nothing

parse_symb_map_items _ = Nothing

{- | Sentences, provers and symbols.

Provers capture the entailment relation between sets of sentences

and sentences. They may return proof trees witnessing proofs.

Signatures are equipped with underlying sets of symbols

(such that the category of signatures becomes a concrete category),

see CASL RefMan p. 191ff.

-}

class (Language lid, Category sign morphism, Ord sentence,

Ord symbol, -- for efficient lookup

PrintTypeConv sign, PrintTypeConv morphism,

PrintTypeConv sentence, PrintTypeConv symbol)

=> Sentences lid sentence sign morphism symbol

| lid -> sentence sign morphism symbol

where

----------------------- sentences ---------------------------

-- | check whether a sentence belongs to a signature

is_of_sign :: lid -> sentence -> signature -> Bool

is_of_sign l _ _ = error $ statErrMsg l "is_of_sign"

-- | sentence translation along a signature morphism

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

map_sen l _ _ = statErr l "map_sen"

-- | simplification of sentences (leave out qualifications)

simplify_sen :: lid -> sign -> sentence -> sentence

simplify_sen _ _ = id -- default implementation

-- | parsing of sentences

parse_sentence :: lid -> Maybe (AParser st sentence)

parse_sentence _ = Nothing

print_sign :: lid -> sign -> Doc

print_sign _ = pretty

-- | print a sentence with comments

print_named :: lid -> Named sentence -> Doc

print_named _ = printAnnoted (addBullet . pretty) . fromLabelledSen

----------------------- symbols ---------------------------

-- | set of symbols for a signature

sym_of :: lid -> sign -> Set.Set symbol

sym_of _ _ = Set.empty

-- | symbol map for a signature morphism

symmap_of :: lid -> morphism -> EndoMap symbol

symmap_of _ _ = Map.empty

-- | symbols have a name, see CASL RefMan p. 192

sym_name :: lid -> symbol -> Id

sym_name l _ = error $ statErrMsg l "sym_name"

-- | a dummy static analysis function to allow type checking *.inline.hs files

inlineAxioms :: StaticAnalysis lid

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol => lid -> String -> [Named sentence]

inlineAxioms _ _ = error "inlineAxioms"

-- | fail function for static analysis

statErr :: (Language lid, Monad m) => lid -> String -> m a

statErr lid = fail . statErrMsg lid

-- | error message for static analysis

statErrMsg :: (Language lid) => lid -> String -> String

statErrMsg lid str = "Logic." ++ str ++ " nyi for: " ++ language_name lid

{- static analysis

This type class provides the data needed for an institution with symbols,

as explained in the structured specification semantics in the CASL

reference manual, chapter III.4.

The static analysis computes signatures from basic specifications,

and signature morphisms from symbol lists and symbol maps. The latter

needs an intermediate stage, so-called raw symbols, which are possibly

unqualified symbols. Normal symbols are always fully qualified.

In the CASL reference manual, our symbols are called "signature symbols",

and our raw symbols are called "symbols". (Terminology should be adapted.)

-}

class ( Syntax lid basic_spec symb_items symb_map_items

, Sentences lid sentence sign morphism symbol

, Ord raw_symbol, Pretty raw_symbol, Typeable raw_symbol)

=> StaticAnalysis lid

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol

| lid -> basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol

where

----------------------- static analysis ---------------------------

{- | static analysis of basic specifications and symbol maps.

The resulting bspec has analyzed axioms in it.

The resulting sign is an extension of the input sign

plus newly declared or redeclared symbols.

See CASL RefMan p. 138 ff. -}

basic_analysis :: lid ->

Maybe((basic_spec, -- abstract syntax tree

sign, -- input signature, for the local

-- environment, carrying the previously

-- declared symbols

GlobalAnnos) -> -- global annotations

Result (basic_spec, ExtSign sign symbol

, [Named sentence]))

-- default implementation

basic_analysis _ = Nothing

-- | static analysis of symbol maps, see CASL RefMan p. 222f.

stat_symb_map_items ::

lid -> [symb_map_items] -> Result (EndoMap raw_symbol)

stat_symb_map_items l _ = statErr l "stat_symb_map_items"

-- | static analysis of symbol lists, see CASL RefMan p. 221f.

stat_symb_items :: lid -> [symb_items] -> Result [raw_symbol]

stat_symb_items l _ = statErr l "stat_symb_items"

------------------------- amalgamation ---------------------------

{- | Computation of colimits of signature diagram.

Indeed, it suffices to compute a coconce that is weakly amalgamable

see Till Mossakowski,

Heterogeneous specification and the heterogeneous tool set

p. 25ff. -}

-- | architectural sharing analysis, see CASL RefMan p. 247ff.

ensures_amalgamability :: lid ->

([CASLAmalgOpt], -- the program options

Gr sign (Int,morphism), -- the diagram to be analyzed

[(Int, morphism)], -- the sink

Gr String String) -- the descriptions of nodes and edges

-> Result Amalgamates

ensures_amalgamability l _ = warning Amalgamates

("amalgamability test not implemented for logic " ++ show l)

nullRange

-- | signature colimits

signature_colimit :: lid -> Gr sign (Int, morphism)

-> Result (sign, Map.Map Int morphism)

signature_colimit l _ = statErr l "signature_colimit"

{- | rename and qualify the symbols, code out overloading,

create sentences for the overloading relation and also return

the inverse morphism -}

qualify :: lid -> SIMPLE_ID -> LIB_ID -> sign

-> Result (morphism, [Named sentence], morphism)

qualify l _ _ _ = statErr l "qualify"

-------------------- symbols and raw symbols ---------------------

{- | Construe a symbol, like f:->t, as a raw symbol.

This is a one-sided inverse to the function SymSySigSym

in the CASL RefMan p. 192. -}

symbol_to_raw :: lid -> symbol -> raw_symbol

symbol_to_raw l _ = error $ statErrMsg l "symbol_to_raw"

{- | Construe an identifier, like f, as a raw symbol.

See CASL RefMan p. 192, function IDAsSym -}

id_to_raw :: lid -> Id -> raw_symbol

id_to_raw l _ = error $ statErrMsg l "id_to_raw"

{- | Check wether a symbol matches a raw symbol, for

example, f:s->t matches f. See CASL RefMan p. 192 -}

matches :: lid -> symbol -> raw_symbol -> Bool

matches l _ _ = error $ statErrMsg l "matches"

--------------- operations on signatures and morphisms -----------

-- | the empty (initial) signature, see CASL RefMan p. 193

empty_signature :: lid -> sign

-- | union of signatures, see CASL RefMan p. 193

signature_union :: lid -> sign -> sign -> Result sign

signature_union l _ _ = statErr l "signature_union"

-- | intersection of signatures

intersection :: lid -> sign -> sign -> Result sign

intersection l _ _ = statErr l "intersection"

-- | final union of signatures, see CASL RefMan p. 194

final_union :: lid -> sign -> sign -> Result sign

final_union l _ _ = statErr l "final_union"

-- | union of signature morphims, see CASL RefMan p. 196

morphism_union :: lid -> morphism -> morphism -> Result morphism

morphism_union l _ _ = statErr l "morphism_union"

{- | construct the inclusion morphisms between subsignatures,

see CASL RefMan p. 194 -}

inclusion :: lid -> sign -> sign -> Result morphism

inclusion l _ _ = statErr l "inclusion"

{- | the signature (co)generated by a set of symbols in another

signature is the smallest (largest) signature containing

(excluding) the set of symbols. Needed for revealing and

hiding, see CASL RefMan p. 197ff. -}

generated_sign, cogenerated_sign ::

lid -> Set.Set symbol -> sign -> Result morphism

generated_sign l _ _ = statErr l "generated_sign"

cogenerated_sign l _ _ = statErr l "cogenerated_sign"

{- | Induce a signature morphism from a source signature and

a raw symbol map. Needed for translation (SP with SM).

See CASL RefMan p. 198 -}

induced_from_morphism ::

lid -> EndoMap raw_symbol -> sign -> Result morphism

induced_from_morphism l _ _ = statErr l "induced_from_morphism"

{- | Induce a signature morphism between two signatures by a

raw symbol map. Needed for instantiation and views.

See CASL RefMan p. 198f. -}

induced_from_to_morphism ::

lid -> EndoMap raw_symbol -> ExtSign sign symbol

-> ExtSign sign symbol -> Result morphism

induced_from_to_morphism l _ _ _ =

statErr l "induced_from_to_morphism"

{- | Check whether a signature morphism is transportable.

See CASL RefMan p. 304f. -}

is_transportable :: lid -> morphism -> Bool

is_transportable _ _ = False -- safe default

{- | Check whether the underlying symbol map of a signature morphism

is injective -}

is_injective :: lid -> morphism -> Bool

is_injective _ _ = False -- safe default

------------------- generate taxonomy from theory ----------------

-- | generate an ontological taxonomy, if this makes sense

theory_to_taxonomy :: lid

-> TaxoGraphKind

-> MMiSSOntology

-> sign -> [Named sentence]

-> Result MMiSSOntology

theory_to_taxonomy l _ _ _ _ = statErr l "theory_to_taxonomy"

-- | subsignatures, see CASL RefMan p. 194

is_subsig :: StaticAnalysis lid

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol => lid -> sign -> sign -> Bool

is_subsig lid s = maybe False (const True) . maybeResult . inclusion lid s

{- | semi lattices with top (needed for sublogics). Note that `Ord` is

only used for efficiency and is not related to the /partial/ order given

by the lattice. Only `Eq` is used to define `isSubElem` -}

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

join :: l -> l -> l

top :: l

instance SemiLatticeWithTop () where

join _ _ = ()

top = ()

-- | less or equal for semi lattices

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

isSubElem a b = join a b == b

-- | class providing the minimal sublogic of an item

class MinSublogic sublogic item where

minSublogic :: item -> sublogic

-- | a default instance for no sublogics

instance MinSublogic () a where

minSublogic _ = ()

-- | class providing also the projection of an item to a sublogic

class MinSublogic sublogic item => ProjectSublogic sublogic item where

projectSublogic :: sublogic -> item -> item

-- | a default instance for no sublogics

instance ProjectSublogic () b where

projectSublogic _ = id

-- | like ProjectSublogic, but providing a partial projection

class MinSublogic sublogic item => ProjectSublogicM sublogic item where

projectSublogicM :: sublogic -> item -> Maybe item

-- | a default instance for no sublogics

instance ProjectSublogicM () b where

projectSublogicM _ = Just

-- | class for providing a list of sublogic names

class Sublogics l where

sublogic_names :: l -> [String]

instance Sublogics () where

sublogic_names () = [""]

{- Type class logic. The central type class of Hets, providing the

interface for logics. This type class is instantiated for many logics,

and it is used for the logic independent parts of Hets.

It hence provides an sbatraction barrier between logic specific and

logic indepdendent code.

This type class extends the class StaticAnalysis by a sublogic mechanism.

Sublogics are important since they avoid the need to provide an own

instance of the class logic for each sublogic. Instead, the sublogic

can use the datastructures and operations of the main logic, and

functions are provided to test whether a given item lies within the

sublogic. Also, projection functions from a super-logic to a sublogic

are provided.

-}

class (StaticAnalysis lid

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol,

SemiLatticeWithTop sublogics,

MinSublogic sublogics sentence,

ProjectSublogic sublogics basic_spec,

ProjectSublogicM sublogics symb_items,

ProjectSublogicM sublogics symb_map_items,

ProjectSublogic sublogics sign,

ProjectSublogic sublogics morphism,

ProjectSublogicM sublogics symbol,

Typeable sublogics,

ShATermConvertible sublogics,

Sublogics sublogics,

Eq proof_tree, Show proof_tree, ShATermConvertible proof_tree,

Ord proof_tree, Typeable proof_tree)

=> Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

| lid -> sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

where

-- | stability of the implementation

stability :: lid -> Stability

-- default

stability _ = Experimental

-- | for a process logic, return its data logic

data_logic :: lid -> Maybe AnyLogic

data_logic _ = Nothing

-- | the top sublogic, corresponding to the whole logic

top_sublogic :: lid -> sublogics

top_sublogic _ = top

-- | list all the sublogics of the current logic

all_sublogics :: lid -> [sublogics]

all_sublogics li = [top_sublogic li]

{- | provide the embedding of a projected signature into the

original signature -}

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

proj_sublogic_epsilon _ _ s = ide s

----------------------- provers ---------------------------

-- | several provers can be provided. See module "Logic.Prover"

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

provers _ = [] -- default implementation

-- | consistency checkers

cons_checkers :: lid

-> [ConsChecker sign sentence

sublogics morphism proof_tree]

cons_checkers _ = [] -- default implementation

-- | conservativity checkers

conservativityCheck :: lid -> (sign, [Named sentence]) ->

morphism -> [Named sentence]

-> Result (Maybe (ConsistencyStatus,[sentence]))

conservativityCheck l _ _ _ = statErr l "conservativityCheck"

-- | the empty proof tree

empty_proof_tree :: lid -> proof_tree

empty_proof_tree l = error $ statErrMsg l "empty_proof_tree"

----------------------------------------------------------------

-- Derived functions

----------------------------------------------------------------

-- | the empty theory

empty_theory :: StaticAnalysis lid

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol =>

lid -> Theory sign sentence proof_tree

empty_theory lid = Theory (empty_signature lid) Map.empty

----------------------------------------------------------------

-- Existential type covering any logic

----------------------------------------------------------------

-- | the disjoint union of all logics

data AnyLogic = forall lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree .

Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

Logic lid

deriving Typeable

instance Show AnyLogic where

show (Logic lid) = language_name lid

instance Eq AnyLogic where

Logic lid1 == Logic lid2 = language_name lid1 == language_name lid2

{- class hierarchy:

Language

__________/

Category

| /

Sentences Syntax

\ /

StaticAnalysis (no sublogics)

\

\

Logic

-}