c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu{-# OPTIONS -fallow-undecidable-instances #-}

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner{- |

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuModule : $Header$

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuDescription : central interface (type class) for logics in Hets

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2006

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuMaintainer : till@tzi.de

402ffc909b645ddb2d5c76343bf74a6cb33c6205Christian MaederStability : provisional

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuPortability : non-portable (various -fglasgow-exts extensions)

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuCentral interface (type class) for logics in Hets

90d7cac36f60438bd35124e3389b5bce6d114b46Christian Maeder

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuProvides data structures for logics (with symbols). Logics are

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu a type class with an /identity/ type (usually interpreted

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu by a singleton set) which serves to treat logics as

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu data. All the functions in the type class take the

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu identity as first argument in order to determine the logic.

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder For logic (co)morphisms see "Logic.Comorphism"

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu

392634badbe11a21c7825ee0e1ee132220a2539eMihai Codescu This module uses multiparameter type classes

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (<http://haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#multi-param-type-classes>)

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu with functional dependencies (<http://haskell.org/hawiki/FunDeps>)

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu for defining an interface for the notion of logic. Multiparameter type

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu classes are needed because a logic consists of a collection of types,

5418aa59492005c2ca40436ab84c4029cd2922a5Christian Maeder together with operations on these. Functional dependencies

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski are needed because no operation will involve all types of

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu the multiparameter type class; hence we need a method to derive

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

5418aa59492005c2ca40436ab84c4029cd2922a5Christian Maeder introduce a new singleton type that constitutes the identity

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu of the logic. All other types of the multiparameter type class

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu depend on this 'identy constituting' type, and all operations take

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu the 'identity constituting' type as first arguments. The value

3bc502518f75cd5a21aa2f608a31f50c19134db0Christian Maeder of the argument of the 'identity constituting' type is irrelevant

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu (note that there is only one value of such a type anyway).

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu References:

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai Codescu J. A. Goguen and R. M. Burstall

7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai Codescu Institutions: Abstract Model Theory for Specification and

7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai Codescu Programming

7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai Codescu JACM 39, p. 95--146, 1992

7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai Codescu (general notion of logic - model theory only)

7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu J. Meseguer

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu General Logics

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu Logic Colloquium 87, p. 275--329, North Holland, 1989

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu (general notion of logic - also entailment\/proof theory;

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder notion of logic representation, called map there)

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu T. Mossakowski:

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu Specification in an arbitrary institution with symbols

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 14th WADT 1999, LNCS 1827, p. 252--270

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu (treatment of symbols and raw symbols, see also CASL semantics

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu in the CASL reference manual)

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu T. Mossakowski, B. Klin:

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu Institution Independent Static Analysis for CASL

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu 15h WADT 2001, LNCS 2267, p. 221-237, 2002.

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu (what is needed for static anaylsis)

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu S. Autexier and T. Mossakowski

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu Integrating HOLCASL into the Development Graph Manager MAYA

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu FroCoS 2002, LNCS 2309, p. 2-17, 2002.

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu (interface to provers)

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu CoFI (ed.): CASL Reference Manual, LNCS 2960, Springer Verlag, 2004.

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu (static semantics of CASL structured and architectural specifications)

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu T. Mossakowski

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu Heterogeneous specification and the heterogeneous tool set

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu Habilitation thesis, University of Bremen, 2005

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu (the general picture of heterogeneous specification)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

272a5a82588ab4115dac5eb81d43d74929e99ad7Till Mossakowski-}

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescumodule Logic.Logic where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport Common.Id

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport Common.GlobalAnnotations

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport qualified Common.Lib.Set as Set

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport qualified Common.Lib.Map as Map

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport Common.Lib.Graph as Tree

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport Common.AnnoState

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport Common.Result

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport Common.AS_Annotation

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport Common.Doc

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport Common.DocUtils

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport Logic.Prover -- for one half of class Sentences

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport Common.DynamicUtils

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport Common.ATerm.Lib -- (ShATermConvertible)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport ATC.DefaultMorphism()

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport Common.Amalgamate -- passed to ensures_amalgamability

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.Taxonomy

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Taxonomy.MMiSSOntology (MMiSSOntology)

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | Stability of logic implementations

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescudata Stability = Stable | Testing | Unstable | Experimental

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder deriving (Eq, Show)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu-- | shortcut for class constraints

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederclass (Show a, Pretty a, Typeable a, ShATermConvertible a)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder => PrintTypeConv a

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu-- | shortcut for class constraints with equality

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuclass (Eq a, PrintTypeConv a) => EqPrintTypeConv a

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu

96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescuinstance (Show a, Pretty a, Typeable a,

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu ShATermConvertible a) => PrintTypeConv a

803425dfe6a5da41b9cea480788980fa104545adMihai Codescuinstance (Eq a, PrintTypeConv a) => EqPrintTypeConv a

96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu-- | maps from a to a

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskitype EndoMap a = Map.Map a a

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski{- | the name of a logic.

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu Define instances like "data CASL = CASL deriving Show"

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu-}

803425dfe6a5da41b9cea480788980fa104545adMihai Codescuclass Show lid => Language lid where

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu language_name :: lid -> String

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder language_name i = show i

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder description :: lid -> String

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu -- default implementation

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu description _ = "No description available"

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu{- | Categories are given as usual: objects, morphisms, identities,

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu domain, codomain and composition. The type id is the name, or

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu the identity of the category. It is an argument to all functions

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder of the type class, serving disambiguation among instances

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (via the functional dependency lid -> sign morphism).

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

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu subtypes, using legal_obj and legal_mor. For example, for the

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu category of sets and injective maps, legal_mor would check

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu injectivity. Since Eq is a subclass of Category, it is also

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu possible to impose a quotient on the types for objects and morphisms.

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu-}

803425dfe6a5da41b9cea480788980fa104545adMihai Codescuclass (Language lid, Eq sign, Eq morphism)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder => Category lid sign morphism | lid -> sign morphism where

96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- | identity morphisms

96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu ide :: lid -> sign -> morphism

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu -- | composition, in diagrammatic order

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu comp :: lid -> morphism -> morphism -> Result morphism

96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- | domain and codomain of morphisms

b7f625188b6bf3d708b2a1b64a6cea7880708adbChristian Maeder dom, cod :: lid -> morphism -> sign

b7f625188b6bf3d708b2a1b64a6cea7880708adbChristian Maeder -- | is a value of type sign denoting a legal signature?

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder legal_obj :: lid -> sign -> Bool

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- | is a value of type morphism denoting a legal signature morphism?

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu legal_mor :: lid -> morphism -> Bool

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu{- | Abstract syntax, parsing and printing.

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu There are three types for abstract syntax:

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder basic_spec is for basic specifications (see CASL RefMan p. 5ff.),

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu 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 (Category lid sign morphism, Ord sentence,

Ord symbol, -- for efficient lookup

PrintTypeConv sign, PrintTypeConv morphism,

PrintTypeConv sentence, PrintTypeConv symbol,

Eq proof_tree, Show proof_tree, ShATermConvertible proof_tree,

Ord proof_tree, Typeable proof_tree)

=> Sentences lid sentence proof_tree sign morphism symbol

| lid -> sentence proof_tree sign morphism symbol

where

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

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

-- | symbol map for a signature morphism

symmap_of :: lid -> morphism -> EndoMap symbol

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

sym_name :: lid -> symbol -> Id

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

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

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

provers _ = [] -- default implementation

-- | consistency checkers

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

cons_checkers _ = [] -- default implementation

-- | conservativity checkers

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

morphism -> [Named sentence] -> Result (Maybe Bool)

conservativityCheck l _ _ _ = statErr l "conservativityCheck"

-- | the empty proof tree

empty_proof_tree :: proof_tree

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

inlineAxioms :: StaticAnalysis lid

basic_spec sentence proof_tree symb_items symb_map_items

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

inlineAxioms _ _ = error "inlineAxioms"

-- error function for static analysis

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

statErr lid str = fail ("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 proof_tree sign morphism symbol

, Ord raw_symbol, Pretty raw_symbol, Typeable raw_symbol)

=> StaticAnalysis lid

basic_spec sentence proof_tree symb_items symb_map_items

sign morphism symbol raw_symbol

| lid -> basic_spec sentence proof_tree 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.

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, sign, [Named sentence]))

-- default implementation

basic_analysis _ = Nothing

-- | one-sided inverse for static analysis

sign_to_basic_spec :: lid -> sign -> [Named sentence] -> basic_spec

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

weaklyAmalgamableCocone :: lid -> Tree.Gr sign morphism

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

weaklyAmalgamableCocone l _ = statErr l "weaklyAmalgamableCocone"

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

ensures_amalgamability :: lid ->

([CASLAmalgOpt], -- the program options

Tree.Gr sign morphism, -- the diagram to be analyzed

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

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

-> Result Amalgamates

ensures_amalgamability l _ = statErr l "ensures_amalgamability"

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

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

See CASL RefMan p. 192, function IDAsSym -}

id_to_raw :: lid -> Id -> raw_symbol

{- | 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

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

{- | Compute the difference of signatures. The first

signature must be an inclusion of the second. The resulting

signature might be an unclosed signature that should only be

used with care, though the following property should hold:

is_subsig s1 s2 => union s1 (difference s2 s1) = s2

(Unions are supposed to be symmetric and associative.) -}

signature_difference :: lid -> sign -> sign -> Result sign

signature_difference l _ _ = statErr l "signature_difference"

-- | subsignatures, see CASL RefMan p. 194

is_subsig :: lid -> sign -> sign -> Bool

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

-- | semi lattices with top (needed for sublogics)

class (Eq 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 _ = ()

{-

instance SemiLatticeWithTop s => MinSublogic s a where

minSublogic _ = top

-}

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

{-

instance MinSublogic a b => ProjectSublogic a 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

{-

instance (SemiLatticeWithTop a, MinSublogic a b) => ProjectSublogicM a b where

projectSublogicM l i = if isSubElem (minSublogic i) l

then Just i else Nothing

-}

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

=> 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 li _ s = ide li s

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

-- Derived functions

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

-- | the empty theory

empty_theory :: StaticAnalysis lid

basic_spec sentence proof_tree 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

instance Show AnyLogic where

show (Logic lid) = language_name lid

instance Eq AnyLogic where

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

tyconAnyLogic :: TyCon

tyconAnyLogic = mkTyCon "Logic.Logic.AnyLogic"

instance Typeable AnyLogic where

typeOf _ = mkTyConApp tyconAnyLogic []

{- class hierarchy:

Language

__________/

Category

| /

Sentences Syntax

\ /

StaticAnalysis (no sublogics)

\

\

Logic

-}