bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveDataTypeable

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner , FlexibleInstances, UndecidableInstances, ExistentialQuantification #-}

81d182b21020b815887e9057959228546cf61b6bChristian Maeder{- |

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederModule : ./Logic/Logic.hs

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuDescription : central interface (type class) for logics in Hets

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

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederMaintainer : till@informatik.uni-bremen.de

fbb66ee3e170624835b99f7aa91980753cb5b472Christian MaederStability : provisional

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

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederCentral interface (type class) for logics in Hets

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

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

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder a type class with an /identity type/ (usually interpreted

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

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

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

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder For logic (co)morphisms see "Logic.Comorphism"

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder

722e8a91f69209ba0e99bf799c4989801d78cf16Christian Maeder This module uses multiparameter type classes with functional dependencies

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder (<http://www.haskell.org/haskellwiki/Functional_dependencies>)

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

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder classes are needed because a logic consists of a collection of types,

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder together with operations on these. Functional dependencies

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

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder the multiparameter type class; hence we need a method to derive

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

33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maeder introduce a new singleton type that is the name, or constitutes the identity

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder of the logic. All other types of the multiparameter type class

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder depend on this /identity constituting/ type, and all operations take

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder the 'identity constituting' type as first arguments. The value

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder of the argument of the /identity constituting/ type is irrelevant

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

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder Note that we tend to use @lid@ both for the /identity type/

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

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder

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

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder * sign: signatures, that is, contexts, or non-logical vocabularies,

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder typically consisting of a set of declared sorts, predicates,

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder function symbols, propositional letters etc., together with their

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder typing.

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder * sentence: logical formulas.

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski * basic_spec: abstract syntax of basic specifications. The latter are

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder human-readable presentations of a signature together with some sentences.

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder

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

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder with their types

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder

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

60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder or partially qualified

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder

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

60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder

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

60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder symbols of a signature as hidden.

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder

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

4cf9b5b0484a15c0f071ef7898cdcc3a44a15429Christian Maeder presentations of signature morphisms.

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder

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

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder record of Boolean flags, indicating whether some feature is

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder present in the sublogi of not.

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder * proof_tree: proof trees.

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder References:

60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder

60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder J. A. Goguen and R. M. Burstall

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder Institutions: Abstract Model Theory for Specification and

60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder Programming

60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder JACM 39, p. 95-146, 1992

60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder (general notion of logic - model theory only)

60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder J. Meseguer

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder General Logics

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

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

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder notion of logic representation, called map there)

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder T. Mossakowski:

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Specification in an arbitrary institution with symbols

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

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

60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder in the CASL reference manual)

60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder T. Mossakowski, B. Klin:

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder Institution Independent Static Analysis for CASL

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

60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder (what is needed for static anaylsis)

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder S. Autexier and T. Mossakowski

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder Integrating HOLCASL into the Development Graph Manager MAYA

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder FroCoS 2002, LNCS 2309, p. 2-17, 2002.

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder (interface to provers)

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder

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

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder (static semantics of CASL structured and architectural specifications)

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder T. Mossakowski

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder Heterogeneous specification and the heterogeneous tool set

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder Habilitation thesis, University of Bremen, 2005

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder (the general picture of heterogeneous specification)

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder-}

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maedermodule Logic.Logic where

df2a122c5ecd7d995323c3f0754e1a2a4e3dc0a8Christian Maeder

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maederimport Logic.Prover (Prover, ConsChecker, Theory (..))

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maederimport Logic.KnownIris

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maederimport Taxonomy.MMiSSOntology (MMiSSOntology)

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport ATC.DefaultMorphism ()

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maederimport qualified OMDoc.DataTypes as OMDoc

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder ( TCElement

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder , TCorOMElement

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder , NameMap

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder , SigMap

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder , SigMapI

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder , OMCD

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder , OmdADT)

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maederimport ATerm.Lib (ShATermConvertible)

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.AS_Annotation

5964438458028e61fdabfa74ca3b4210206cdba6Christian Maederimport Common.Amalgamate

5964438458028e61fdabfa74ca3b4210206cdba6Christian Maederimport Common.AnnoState

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maederimport Common.Consistency

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maederimport Common.DefaultMorphism

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport Common.Doc

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maederimport Common.DocUtils

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maederimport Common.ExtSign

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport Common.GlobalAnnotations

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport Common.Id

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maederimport Common.IRI

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maederimport Common.Item

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maederimport Common.Json

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maederimport Common.Lib.Graph

d48085f765fca838c1d972d2123601997174583dChristian Maederimport Common.LibName

797f811e57952d59e73b8cd03b667eef276db972Christian Maederimport Common.Prec (PrecMap)

f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maederimport Common.Result

f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maederimport Common.Taxonomy

f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maederimport Common.ToXml

f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder

f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maederimport qualified Data.Set as Set

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maederimport qualified Data.Map as Map

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Data.Monoid

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maederimport Data.Ord

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maederimport Data.Typeable

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maederimport Control.Monad (unless)

f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder

f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder-- | Stability of logic implementations

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maederdata Stability = Stable | Testing | Unstable | Experimental

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder deriving (Eq, Show)

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder-- | shortcut for class constraints

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederclass ShATermConvertible a => Convertible a

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederinstance ShATermConvertible a => Convertible a

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder-- | shortcut for class constraints

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maederclass (Pretty a, Convertible a) => PrintTypeConv a

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maederinstance (Pretty a, Convertible a) => PrintTypeConv a

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder-- | shortcut for class constraints with equality

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maederclass (Eq a, PrintTypeConv a) => EqPrintTypeConv a

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maederinstance (Eq a, PrintTypeConv a) => EqPrintTypeConv a

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder

89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder-- | maps from a to a

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maedertype EndoMap a = Map.Map a a

304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder

7344fe509f1a733c88a72b05f9beff070af4701aChristian Maeder{- | the name of a logic.

304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder Define instances like "data CASL = CASL deriving (Show, Typeable, Data)"

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-}

304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maederclass Show lid => Language lid where

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder language_name :: lid -> String

7344fe509f1a733c88a72b05f9beff070af4701aChristian Maeder language_name = show

7344fe509f1a733c88a72b05f9beff070af4701aChristian Maeder description :: lid -> String

7344fe509f1a733c88a72b05f9beff070af4701aChristian Maeder -- default implementation

7344fe509f1a733c88a72b05f9beff070af4701aChristian Maeder description _ = ""

7344fe509f1a733c88a72b05f9beff070af4701aChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder-- short description = first line of description

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maedershort_description :: Language lid => lid -> String

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maedershort_description l = head ((lines $ description l) ++ [""])

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder

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

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

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

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder of the type class, serving disambiguation among instances

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

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

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

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

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

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

7344fe509f1a733c88a72b05f9beff070af4701aChristian Maeder Require Ord instances only for efficiency, i.e. in sets or maps.

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder-}

d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maederclass (Ord object, Ord morphism)

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder => Category object morphism | morphism -> object where

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder -- | identity morphisms

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder ide :: object -> morphism

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder {- | composition, in diagrammatic order,

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder if intermediate objects are equal (not checked!) -}

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder composeMorphisms :: morphism -> morphism -> Result morphism

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder -- | domain and codomain of morphisms

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder dom, cod :: morphism -> object

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder -- | the inverse of a morphism

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder inverse :: morphism -> Result morphism

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder inverse _ = fail "Logic.Logic.Category.inverse not implemented"

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder -- | test if the signature morphism an inclusion

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder isInclusion :: morphism -> Bool

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder isInclusion _ = False -- in general no inclusion

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder -- | is a value of type morphism denoting a legal morphism?

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder legal_mor :: morphism -> Result ()

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder legal_mor _ = return ()

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder-- | test if the signature morphism is the identity

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederisIdentity :: Category object morphism => morphism -> Bool

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederisIdentity m = isInclusion m && dom m == cod m

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maedercomp :: Category object morphism => morphism -> morphism -> Result morphism

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maedercomp m1 m2 = if cod m1 == dom m2 then composeMorphisms m1 m2 else

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder fail "target of first and source of second morphism are different"

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder

bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maederinstance Ord sign => Category sign (DefaultMorphism sign) where

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder dom = domOfDefaultMorphism

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder cod = codOfDefaultMorphism

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder ide = ideOfDefaultMorphism

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder isInclusion = const True

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder composeMorphisms = compOfDefaultMorphism

60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder{- | Abstract syntax, parsing and printing.

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder There are three types for abstract syntax:

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

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

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

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder-}

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maederclass (Language lid, PrintTypeConv basic_spec, GetRange basic_spec,

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder Monoid basic_spec, -- for joining converted signatures and sentences

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder Pretty symbol,

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder EqPrintTypeConv symb_items,

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder EqPrintTypeConv symb_map_items)

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder => Syntax lid basic_spec symbol symb_items symb_map_items

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder | lid -> basic_spec symbol symb_items symb_map_items

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder where

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder -- | parsers and printers

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder parsersAndPrinters :: lid -> Map.Map String

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder parsersAndPrinters li = case parse_basic_spec li of

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder Nothing -> Map.empty

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder Just p -> makeDefault (p, pretty)

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder -- | parser for basic specifications

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder parse_basic_spec :: lid -> Maybe (PrefixMap -> AParser st basic_spec)

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder -- | parser for a single symbol returned as list

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder parseSingleSymbItem :: lid -> Maybe (AParser st symb_items)

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder -- | parser for symbol lists

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder parse_symb_items :: lid -> Maybe (AParser st symb_items)

54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder -- | parser for symbol maps

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder parse_symb_map_items :: lid -> Maybe (AParser st symb_map_items)

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder toItem :: lid -> basic_spec -> Item

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder symb_items_name :: lid -> symb_items -> [String]

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder -- default implementations

66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder parse_basic_spec _ = Nothing

parseSingleSymbItem _ = Nothing

parse_symb_items _ = Nothing

parse_symb_map_items _ = Nothing

symb_items_name _ _ = [""]

toItem _ bs = mkFlatItem ("Basicspec", pretty bs) $ getRangeSpan bs

basicSpecParser :: Syntax lid basic_spec symbol symb_items symb_map_items

=> Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec)

basicSpecParser sm = fmap fst . parserAndPrinter sm

basicSpecPrinter :: Syntax lid basic_spec symbol symb_items symb_map_items

=> Maybe IRI -> lid -> Maybe (basic_spec -> Doc)

basicSpecPrinter sm = fmap snd . parserAndPrinter sm

basicSpecSyntaxes :: Syntax lid basic_spec symbol symb_items symb_map_items

=> lid -> [String]

basicSpecSyntaxes = Map.keys . serializations . language_name

parserAndPrinter :: Syntax lid basic_spec symbol symb_items symb_map_items

=> Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec,

basic_spec -> Doc)

parserAndPrinter sm l = lookupDefault l sm (parsersAndPrinters l)

-- | function to lookup parser or printer

lookupDefault :: Syntax lid basic_spec symbol symb_items symb_map_items

=> lid -> Maybe IRI -> Map.Map String b -> Maybe b

lookupDefault l im m = case im of

Just i -> do

let s = iriToStringUnsecure i

ser <- if isSimple i then return s

else lookupSerialization (language_name l) s

Map.lookup ser m

Nothing -> if Map.size m == 1 then Just $ head $ Map.elems m

else Map.lookup "" m

showSyntax :: Language lid => lid -> Maybe IRI -> String

showSyntax lid = (("logic " ++ language_name lid) ++)

. maybe "" ((" serialization " ++) . iriToStringUnsecure)

makeDefault :: b -> Map.Map String b

makeDefault = Map.singleton ""

addSyntax :: String -> b -> Map.Map String b -> Map.Map String b

addSyntax = Map.insert

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

GetRange sentence, GetRange symbol,

PrintTypeConv sentence, ToJson sentence,

ToXml sentence, PrintTypeConv symbol)

=> Sentences lid sentence sign morphism symbol

| lid -> sentence sign morphism symbol

where

-- | sentence translation along a signature morphism

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

map_sen l _ _ = statFail l "map_sen"

-- | simplification of sentences (leave out qualifications)

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

simplify_sen _ _ = id

-- | negation of a sentence for disproving

negation :: lid -> sentence -> Maybe sentence

negation _ _ = Nothing

-- | modified signature printing when followed by sentences

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

-- | dependency ordered list of symbol sets for a signature

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

sym_of _ _ = []

{- | Dependency ordered list of a bigger symbol set for a

signature. This function contains more symbols than those being subject

to hiding and renaming (given by 'sym_of') to better represent a

signature as a set of symbols given within xml files. At least for CASL

additional symbols for (direct) subsorts will be created, but note, that

no symbol for a partial function will be created, if the signature

contains this function as total, although a signature with just that

partial function would be a subsignature. This function is supposed to

work over partial signatures created by 'signatureDiff'. -}

mostSymsOf :: lid -> sign -> [symbol]

mostSymsOf l = concatMap Set.toList . sym_of l

-- | 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 _ = statError l "sym_name"

-- | some symbols have a label for better readability

sym_label :: lid -> symbol -> Maybe String

sym_label _ _ = Nothing

-- | the fully qualified name for XML output (i.e. of OWL2)

fullSymName :: lid -> symbol -> String

fullSymName l = show . sym_name l

-- | a logic dependent kind of a symbol

symKind :: lid -> symbol -> String

symKind _ _ = "defaultKind"

-- | the symbols occuring in a sentence (any order)

symsOfSen :: lid -> sign -> sentence -> [symbol]

symsOfSen _ _ _ = []

-- | combine two symbols into another one

pair_symbols :: lid -> symbol -> symbol -> Result symbol

pair_symbols lid _ _ = error $ "pair_symbols nyi for logic " ++ show lid

-- | makes a singleton list from the given value

singletonList :: a -> [a]

singletonList x = [x]

-- | set of symbols for a signature

symset_of :: forall lid sentence sign morphism symbol .

Sentences lid sentence sign morphism symbol =>

lid -> sign -> Set.Set symbol

symset_of lid sig = Set.unions $ sym_of lid sig

-- | dependency ordered list of symbols for a signature

symlist_of :: forall lid sentence sign morphism symbol .

Sentences lid sentence sign morphism symbol =>

lid -> sign -> [symbol]

symlist_of lid sig = concatMap Set.toList $ sym_of lid sig

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

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

statFail lid = fail . statErrMsg lid

statError :: Language lid => lid -> String -> a

statError lid = error . statErrMsg lid

-- | error message for static analysis

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

statErrMsg lid str =

"Logic." ++ str ++ " not implemented 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.)

-}

data REL_REF = Subs | IsSubs | Equiv | Incomp

| HasInst | InstOf | DefRel

| RelName IRI

deriving (Show, Eq)

class ( Syntax lid basic_spec symbol symb_items symb_map_items

, Sentences lid sentence sign morphism symbol

, GetRange raw_symbol, Ord raw_symbol, Pretty raw_symbol

, Typeable raw_symbol)

=> StaticAnalysis lid

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol

| lid -> basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol

where

{- | 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, sign, GlobalAnnos)

-> Result (basic_spec, ExtSign sign symbol, [Named sentence]))

basic_analysis _ = Nothing

-- | Analysis of just sentences

sen_analysis :: lid

-> Maybe ((basic_spec, sign, sentence) -> Result sentence)

sen_analysis _ = Nothing

-- | a basic analysis with additional arguments

extBasicAnalysis :: lid -> IRI -> LibName

-> basic_spec -> sign -> GlobalAnnos

-> Result (basic_spec, ExtSign sign symbol, [Named sentence])

extBasicAnalysis l _ _ b s g = case basic_analysis l of

Nothing -> statFail l "basic_analysis"

Just ba -> ba (b, s, g)

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

stat_symb_map_items :: lid -> sign -> Maybe sign -> [symb_map_items]

-> Result (EndoMap raw_symbol)

stat_symb_map_items l _ _ _ = statFail l "stat_symb_map_items"

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

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

stat_symb_items l _ _ = statFail l "stat_symb_items"

-- | convert a theory to basic specs for different serializations

convertTheory :: lid -> Maybe ((sign, [Named sentence]) -> basic_spec)

convertTheory _ = Nothing

{- ----------------------- amalgamation ---------------------------

Computation of colimits of signature diagram.

Indeed, it suffices to compute a cocone 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

-- | quotient term algebra for normalization of freeness

quotient_term_algebra :: lid -- the logic

-> morphism -- sigma : Sigma -> SigmaM

-> [Named sentence] -- Th(M)

-> Result

(sign, -- SigmaK

[Named sentence] -- Ax(K)

)

quotient_term_algebra l _ _ = statFail l "quotient_term_algebra"

-- | signature colimits

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

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

signature_colimit l _ = statFail l "signature_colimit"

{- | rename and qualify the symbols considering a united incoming

morphisms, code out overloading and

create sentences for the overloading relation -}

qualify :: lid -> SIMPLE_ID -> LibName -> morphism -> sign

-> Result (morphism, [Named sentence])

qualify l _ _ _ _ = statFail 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 _ = statError 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 _ = statError l "id_to_raw"

{- | Check whether 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 _ _ _ = True

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

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

empty_signature :: lid -> sign

-- | adds a symbol to a given signature

add_symb_to_sign :: lid -> sign -> symbol -> Result sign

add_symb_to_sign l _ _ = statFail l "add_symb_to_sign"

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

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

signature_union l _ _ = statFail l "signature_union"

-- | difference of signatures resulting in unclosed pre-signatures

signatureDiff :: lid -> sign -> sign -> Result sign

signatureDiff l _ _ = statFail l "signatureDiff"

-- | intersection of signatures

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

intersection l _ _ = statFail l "intersection"

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

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

final_union l _ _ = statFail l "final_union"

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

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

morphism_union l _ _ = statFail l "morphism_union"

-- | subsignatures, see CASL RefMan p. 194

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

is_subsig _ _ _ = False

{- | construct the inclusion morphisms between subsignatures,

see CASL RefMan p. 194 -}

subsig_inclusion :: lid -> sign -> sign -> Result morphism

subsig_inclusion l _ _ = statFail l "subsig_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 _ _ = statFail l "generated_sign"

cogenerated_sign l _ _ = statFail 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 _ _ = statFail 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 rm (ExtSign sig _) (ExtSign tar _) = do

mor <- induced_from_morphism l rm sig

inclusion l (cod mor) tar >>= composeMorphisms mor

{- | Check whether a signature morphism is transportable.

See CASL RefMan p. 304f. -}

is_transportable :: lid -> morphism -> Bool

is_transportable _ _ = False

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

is injective -}

is_injective :: lid -> morphism -> Bool

is_injective _ _ = False

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

theory_to_taxonomy :: lid

-> TaxoGraphKind

-> MMiSSOntology

-> sign -> [Named sentence]

-> Result MMiSSOntology

theory_to_taxonomy l _ _ _ _ = statFail l "theory_to_taxonomy"

-- | create a theory from a correspondence

corresp2th :: lid

-> String -- the name of the alignment

-> Bool -- flag: should we disambiguate in the bridge

-> sign

-> sign

-> [symb_items]

-> [symb_items]

-> EndoMap symbol

-> EndoMap symbol

-> REL_REF

-> Result (sign, [Named sentence], sign, sign,

EndoMap symbol, EndoMap symbol)

corresp2th _ _ _ _ _ _ _ _ _ = error "c2th nyi"

-- | create a co-span fragment from an equivalence

equiv2cospan :: lid -> sign -> sign -> [symb_items] -> [symb_items]

-> Result (sign, sign, sign, EndoMap symbol, EndoMap symbol)

equiv2cospan _ _ _ _ _ = error "equiv2cospan nyi"

-- | extract the module

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

-> Result (sign, [Named sentence])

extract_module _ _ = return

-- | print a whole theory

printTheory :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol

=> Maybe IRI -> lid -> (sign, [Named sentence]) -> Doc

printTheory sm lid th@(s, l) = case

(convertTheory lid, basicSpecPrinter sm lid) of

(Just c, Just p) -> p (c th)

_ -> print_sign lid s $++$ vsep (map (print_named lid) l)

-- | guarded inclusion

inclusion :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol

=> lid -> sign -> sign -> Result morphism

inclusion l s1 s2 = if is_subsig l s1 s2 then subsig_inclusion l s1 s2

else fail $ show $ fsep

[ text (language_name l)

, text "cannot construct inclusion. Symbol(s) missing in target:"

, pretty $ Set.difference (symset_of l s1) $ symset_of l s2

, text "\nSource is: "

, pretty $ symset_of l s1

, text "\nTarget is: "

, pretty $ symset_of l s2 ]

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

lub :: l -> l -> l -- least upper bound or "join"

top :: l

instance SemiLatticeWithTop () where

lub _ _ = ()

top = ()

-- | less or equal for semi lattices

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

isSubElem a b = lub 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

-- | a class for providing a sublogi name

class SublogicName l where

sublogicName :: l -> String

instance SublogicName () where

sublogicName () = ""

-- | a type for syntax information eventually stored in the signature

type SyntaxTable = (PrecMap, AssocMap)

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

Convertible sublogics,

SublogicName sublogics,

Ord proof_tree, Show proof_tree,

Convertible 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

-- Parser of sentence (Added for Hybridized logics)

parse_basic_sen :: lid -> Maybe (basic_spec -> AParser st sentence)

parse_basic_sen _ = Nothing

-- | stability of the implementation

stability :: lid -> Stability

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]

{- a bottom sublogic can be extended along several dimensions

joining all last elements of a dimension should yield the top-sublogic

-}

bottomSublogic :: lid -> Maybe sublogics

bottomSublogic _ = Nothing

sublogicDimensions :: lid -> [[sublogics]]

sublogicDimensions li = [all_sublogics li]

-- | parse sublogic (override more efficiently)

parseSublogic :: lid -> String -> Maybe sublogics

parseSublogic li s = lookup s $ map (\ l -> (sublogicName l, l))

$ all_sublogics li

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

original signature -}

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

proj_sublogic_epsilon _ _ = ide

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

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

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

provers _ = []

-- | consistency checkers

cons_checkers :: lid

-> [ConsChecker sign sentence

sublogics morphism proof_tree]

cons_checkers _ = []

-- | conservativity checkers

conservativityCheck :: lid

-> [ConservativityChecker sign sentence morphism]

conservativityCheck _ = []

-- | the empty proof tree

empty_proof_tree :: lid -> proof_tree

empty_proof_tree l = statError l "empty_proof_tree"

-- --------------------- OMDoc ---------------------------

syntaxTable :: lid -> sign -> Maybe SyntaxTable

syntaxTable _ _ = Nothing

omdoc_metatheory :: lid -> Maybe OMDoc.OMCD

{- default implementation, no logic should throw an error here

and the base of omcd should be a parseable URI -}

omdoc_metatheory _ = Nothing

export_symToOmdoc :: lid -> OMDoc.NameMap symbol

-> symbol -> String -> Result OMDoc.TCElement

export_symToOmdoc l _ _ = statFail l "export_symToOmdoc"

export_senToOmdoc :: lid -> OMDoc.NameMap symbol

-> sentence -> Result OMDoc.TCorOMElement

export_senToOmdoc l _ _ = statFail l "export_senToOmdoc"

{- | additional information which has to be exported can be

exported by this function -}

export_theoryToOmdoc :: lid -> OMDoc.SigMap symbol -> sign

-> [Named sentence] -> Result [OMDoc.TCElement]

{- default implementation does no extra export

, sufficient in some cases -}

export_theoryToOmdoc _ _ _ _ = return []

omdocToSym :: lid -> OMDoc.SigMapI symbol -> OMDoc.TCElement

-> String -> Result symbol

omdocToSym l _ _ _ = statFail l "omdocToSym"

omdocToSen :: lid -> OMDoc.SigMapI symbol -> OMDoc.TCElement

-> String -> Result (Maybe (Named sentence))

omdocToSen l _ _ _ = statFail l "omdocToSen"

{- | Algebraic Data Types are imported with this function.

By default the input is returned without changes. -}

addOMadtToTheory :: lid -> OMDoc.SigMapI symbol

-> (sign, [Named sentence]) -> [[OMDoc.OmdADT]]

-> Result (sign, [Named sentence])

-- no logic should throw an error here

addOMadtToTheory l _ t adts = do

unless (null adts) $ warning ()

(concat [ "ADT handling not implemented for logic "

, show l, " but some adts have to be handled" ])

nullRange

return t

{- | additional information which has to be imported can be

imported by this function. By default the input is returned

without changes. -}

addOmdocToTheory :: lid -> OMDoc.SigMapI symbol

-> (sign, [Named sentence]) -> [OMDoc.TCElement]

-> Result (sign, [Named sentence])

-- no logic should throw an error here

addOmdocToTheory _ _ t _ = return t

-- | sublogic of a theory

sublogicOfTheo :: (Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree) =>

lid -> (sign, [sentence]) -> sublogics

sublogicOfTheo _ (sig, axs) =

foldl lub (minSublogic sig) $

map minSublogic axs

{- The class of logics which can be used as logical frameworks, in which object

logics can be specified by the user. Currently the only logics implementing

this class are LF, Maude, and Isabelle, with the latter two only having

dummy implementations.

The function "base_sig" returns the base signature of the framework -

for details see Integrating Logical Frameworks in Hets by M. Codescu et al

(WADT10).

The function "write_logic" constructs the contents of the Logic_L

file, where L is the name of the object logic passed as an argument.

Typically, this file will declare the lid of the object logic L and

instances of the classes Language, Syntax, Sentences, Logic, and

StaticAnalysis. The instance of Category is usually inherited from

the framework itself as the object logic reuses the signatures and

morphisms of the framework.

The function "write_syntax" constructs the contents of the file declaring

the Ltruth morphism (see the reference given above). If proofs and models

are later integrated into Hets, there should be analogous functions

"write_proofs" and "write_models" added, declaring the Lpf and

Lmod morphisms respectively. -}

class Logic lid sublogics basic_spec sentence

symb_items symb_map_items sign

morphism symbol raw_symbol proof_tree

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

-- | the base signature

base_sig :: lid -> sign

base_sig l = error $ "Function base_sig nyi for logic " ++ shows l "."

{- | generation of the object logic instances

second argument is object logic name -}

write_logic :: lid -> String -> String

write_logic l = error

$ "Function write_logic nyi for logic " ++ shows l "."

{- | generation of the Ltruth morphism declaration

second argument is the object logic name

third argument is the Ltruth morphism -}

write_syntax :: lid -> String -> morphism -> String

write_syntax l = error $

"Function write_syntax nyi for logic " ++ shows l "."

write_proof :: lid -> String -> morphism -> String

write_proof l = error $

"Function write_proof nyi for logic " ++ shows l "."

write_model :: lid -> String -> morphism -> String

write_model l = error $

"Function write_model nyi for logic " ++ shows l "."

read_morphism :: lid -> FilePath -> morphism

read_morphism l _ = error $

"Function read_morphism nyi for logic " ++ shows l "."

write_comorphism :: lid -> String -> String -> String

-> morphism -> morphism -> morphism

-> String

write_comorphism l = error $

"Function write_comorphism nyi for logic " ++ shows l "."

{- --------------------------------------------------------------

Derived functions

-------------------------------------------------------------- -}

-- | the empty theory

emptyTheory :: StaticAnalysis lid

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol =>

lid -> Theory sign sentence proof_tree

emptyTheory 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 GetRange AnyLogic

instance Show AnyLogic where

show (Logic lid) = language_name lid

instance Eq AnyLogic where

a == b = compare a b == EQ

instance Ord AnyLogic where

compare = comparing show

{- class hierarchy:

Language

__________/

Category

| /

Sentences Syntax

\ /

StaticAnalysis (no sublogics)

|

|

Logic

-}