a78048ccbdb6256da15e6b0e7e95355e480c2301nd{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveDataTypeable

a78048ccbdb6256da15e6b0e7e95355e480c2301nd , FlexibleInstances, UndecidableInstances, ExistentialQuantification #-}

fd9abdda70912b99b24e3bf1a38f26fde908a74cnd{- |

fd9abdda70912b99b24e3bf1a38f26fde908a74cndModule : $Header$

fd9abdda70912b99b24e3bf1a38f26fde908a74cndDescription : central interface (type class) for logics in Hets

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

a78048ccbdb6256da15e6b0e7e95355e480c2301ndLicense : GPLv2 or higher, see LICENSE.txt

a78048ccbdb6256da15e6b0e7e95355e480c2301ndMaintainer : till@informatik.uni-bremen.de

a78048ccbdb6256da15e6b0e7e95355e480c2301ndStability : provisional

96ad5d81ee4a2cc66a4ae19893efc8aa6d06fae7jailletcPortability : non-portable (various -fglasgow-exts extensions)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndCentral interface (type class) for logics in Hets

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen

2e545ce2450a9953665f701bb05350f0d3f26275ndProvides data structures for logics (with symbols). Logics are

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen a type class with an /identity type/ (usually interpreted

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen by a singleton set) which serves to treat logics as

a78048ccbdb6256da15e6b0e7e95355e480c2301nd data. All the functions in the type class take the

a78048ccbdb6256da15e6b0e7e95355e480c2301nd identity as first argument in order to determine the logic.

af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowen

3f08db06526d6901aa08c110b5bc7dde6bc39905nd For logic (co)morphisms see "Logic.Comorphism"

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd This module uses multiparameter type classes with functional dependencies

a78048ccbdb6256da15e6b0e7e95355e480c2301nd (<http://www.haskell.org/haskellwiki/Functional_dependencies>)

3f08db06526d6901aa08c110b5bc7dde6bc39905nd for defining an interface for the notion of logic. Multiparameter type

a78048ccbdb6256da15e6b0e7e95355e480c2301nd classes are needed because a logic consists of a collection of types,

a78048ccbdb6256da15e6b0e7e95355e480c2301nd together with operations on these. Functional dependencies

f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjung are needed because no operation will involve all types of

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

4b575a6b6704b516f22d65a3ad35696d7b9ba372rpluem the missing types. We chose an easy way: for each logic, we

4b575a6b6704b516f22d65a3ad35696d7b9ba372rpluem introduce a new singleton type that is the name, or constitutes the identity

a78048ccbdb6256da15e6b0e7e95355e480c2301nd of the logic. All other types of the multiparameter type class

a78048ccbdb6256da15e6b0e7e95355e480c2301nd depend on this /identity constituting/ type, and all operations take

a78048ccbdb6256da15e6b0e7e95355e480c2301nd the 'identity constituting' type as first arguments. The value

a78048ccbdb6256da15e6b0e7e95355e480c2301nd of the argument of the /identity constituting/ type is irrelevant

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Note that we tend to use @lid@ both for the /identity type/

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

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

30471a4650391f57975f60bbb6e4a90be7b284bfhumbedooh

a78048ccbdb6256da15e6b0e7e95355e480c2301nd * sign: signatures, that is, contexts, or non-logical vocabularies,

a78048ccbdb6256da15e6b0e7e95355e480c2301nd typically consisting of a set of declared sorts, predicates,

a78048ccbdb6256da15e6b0e7e95355e480c2301nd function symbols, propositional letters etc., together with their

a78048ccbdb6256da15e6b0e7e95355e480c2301nd typing.

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd * sentence: logical formulas.

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd * basic_spec: abstract syntax of basic specifications. The latter are

a78048ccbdb6256da15e6b0e7e95355e480c2301nd human-readable presentations of a signature together with some sentences.

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd with their types

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd or partially qualified

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd symbols of a signature as hidden.

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd presentations of signature morphisms.

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd record of Boolean flags, indicating whether some feature is

a78048ccbdb6256da15e6b0e7e95355e480c2301nd present in the sublogi of not.

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd * proof_tree: proof trees.

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd References:

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd J. A. Goguen and R. M. Burstall

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Institutions: Abstract Model Theory for Specification and

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Programming

a78048ccbdb6256da15e6b0e7e95355e480c2301nd JACM 39, p. 95-146, 1992

a78048ccbdb6256da15e6b0e7e95355e480c2301nd (general notion of logic - model theory only)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd J. Meseguer

a78048ccbdb6256da15e6b0e7e95355e480c2301nd General Logics

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd (general notion of logic - also proof theory;

a78048ccbdb6256da15e6b0e7e95355e480c2301nd notion of logic representation, called map there)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd T. Mossakowski:

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Specification in an arbitrary institution with symbols

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd (treatment of symbols and raw symbols, see also CASL semantics

a78048ccbdb6256da15e6b0e7e95355e480c2301nd in the CASL reference manual)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd T. Mossakowski, B. Klin:

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Institution Independent Static Analysis for CASL

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd (what is needed for static anaylsis)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd S. Autexier and T. Mossakowski

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Integrating HOLCASL into the Development Graph Manager MAYA

a78048ccbdb6256da15e6b0e7e95355e480c2301nd FroCoS 2002, LNCS 2309, p. 2-17, 2002.

a78048ccbdb6256da15e6b0e7e95355e480c2301nd (interface to provers)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd CoFI (ed.): CASL Reference Manual, LNCS 2960, Springer Verlag, 2004.

a78048ccbdb6256da15e6b0e7e95355e480c2301nd (static semantics of CASL structured and architectural specifications)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd T. Mossakowski

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Heterogeneous specification and the heterogeneous tool set

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Habilitation thesis, University of Bremen, 2005

a78048ccbdb6256da15e6b0e7e95355e480c2301nd (the general picture of heterogeneous specification)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-}

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndmodule Logic.Logic where

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Logic.Prover (Prover, ConsChecker, Theory (..))

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Logic.KnownIris

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Taxonomy.MMiSSOntology (MMiSSOntology)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport ATC.DefaultMorphism ()

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport qualified OMDoc.DataTypes as OMDoc

a78048ccbdb6256da15e6b0e7e95355e480c2301nd ( TCElement

a78048ccbdb6256da15e6b0e7e95355e480c2301nd , TCorOMElement

a78048ccbdb6256da15e6b0e7e95355e480c2301nd , NameMap

a78048ccbdb6256da15e6b0e7e95355e480c2301nd , SigMap

a78048ccbdb6256da15e6b0e7e95355e480c2301nd , SigMapI

a78048ccbdb6256da15e6b0e7e95355e480c2301nd , OMCD

a78048ccbdb6256da15e6b0e7e95355e480c2301nd , OmdADT)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport ATerm.Lib (ShATermConvertible)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.AS_Annotation

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.Amalgamate

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.AnnoState

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.Consistency

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.DefaultMorphism

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.Doc

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.DocUtils

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.ExtSign

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.GlobalAnnotations

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.Id

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.IRI

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.Item

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.Lib.Graph

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.LibName

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.Prec (PrecMap)

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.Result

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.Taxonomy

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport qualified Data.Set as Set

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport qualified Data.Map as Map

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Data.Monoid

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Data.Ord

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Data.Typeable

a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Control.Monad (unless)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- | Stability of logic implementations

a78048ccbdb6256da15e6b0e7e95355e480c2301nddata Stability = Stable | Testing | Unstable | Experimental

a78048ccbdb6256da15e6b0e7e95355e480c2301nd deriving (Eq, Show)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- | shortcut for class constraints

a78048ccbdb6256da15e6b0e7e95355e480c2301ndclass ShATermConvertible a => Convertible a

a78048ccbdb6256da15e6b0e7e95355e480c2301ndinstance ShATermConvertible a => Convertible a

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- | shortcut for class constraints

a78048ccbdb6256da15e6b0e7e95355e480c2301ndclass (Pretty a, Convertible a) => PrintTypeConv a

a78048ccbdb6256da15e6b0e7e95355e480c2301ndinstance (Pretty a, Convertible a) => PrintTypeConv a

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- | shortcut for class constraints with equality

a78048ccbdb6256da15e6b0e7e95355e480c2301ndclass (Eq a, PrintTypeConv a) => EqPrintTypeConv a

a78048ccbdb6256da15e6b0e7e95355e480c2301ndinstance (Eq a, PrintTypeConv a) => EqPrintTypeConv a

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- | maps from a to a

a78048ccbdb6256da15e6b0e7e95355e480c2301ndtype EndoMap a = Map.Map a a

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd{- | the name of a logic.

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Define instances like "data CASL = CASL deriving Show"

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-}

a78048ccbdb6256da15e6b0e7e95355e480c2301ndclass Show lid => Language lid where

a78048ccbdb6256da15e6b0e7e95355e480c2301nd language_name :: lid -> String

a78048ccbdb6256da15e6b0e7e95355e480c2301nd language_name = show

a78048ccbdb6256da15e6b0e7e95355e480c2301nd description :: lid -> String

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- default implementation

a78048ccbdb6256da15e6b0e7e95355e480c2301nd description _ = ""

4aa603e6448b99f9371397d439795c91a93637eand

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

4aa603e6448b99f9371397d439795c91a93637eand domain, codomain and composition. The type id is the name, or

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd of the type class, serving disambiguation among instances

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd The types for objects and morphisms may be restricted to

a78048ccbdb6256da15e6b0e7e95355e480c2301nd subtypes, using legal_obj and legal_mor. For example, for the

a78048ccbdb6256da15e6b0e7e95355e480c2301nd category of sets and injective maps, legal_mor would check

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

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Require Ord instances only for efficiency, i.e. in sets or maps.

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-}

a78048ccbdb6256da15e6b0e7e95355e480c2301ndclass (Ord object, Ord morphism)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd => Category object morphism | morphism -> object where

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- | identity morphisms

a78048ccbdb6256da15e6b0e7e95355e480c2301nd ide :: object -> morphism

a78048ccbdb6256da15e6b0e7e95355e480c2301nd {- | composition, in diagrammatic order,

a78048ccbdb6256da15e6b0e7e95355e480c2301nd if intermediate objects are equal (not checked!) -}

a78048ccbdb6256da15e6b0e7e95355e480c2301nd composeMorphisms :: morphism -> morphism -> Result morphism

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- | domain and codomain of morphisms

a78048ccbdb6256da15e6b0e7e95355e480c2301nd dom, cod :: morphism -> object

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- | the inverse of a morphism

a78048ccbdb6256da15e6b0e7e95355e480c2301nd inverse :: morphism -> Result morphism

a78048ccbdb6256da15e6b0e7e95355e480c2301nd inverse _ = fail "Logic.Logic.Category.inverse not implemented"

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- | test if the signature morphism an inclusion

a78048ccbdb6256da15e6b0e7e95355e480c2301nd isInclusion :: morphism -> Bool

a78048ccbdb6256da15e6b0e7e95355e480c2301nd isInclusion _ = False -- in general no inclusion

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd legal_mor :: morphism -> Result ()

a78048ccbdb6256da15e6b0e7e95355e480c2301nd legal_mor _ = return ()

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- | test if the signature morphism is the identity

a78048ccbdb6256da15e6b0e7e95355e480c2301ndisIdentity :: Category object morphism => morphism -> Bool

a78048ccbdb6256da15e6b0e7e95355e480c2301ndisIdentity m = isInclusion m && dom m == cod m

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndcomp :: Category object morphism => morphism -> morphism -> Result morphism

a78048ccbdb6256da15e6b0e7e95355e480c2301ndcomp m1 m2 = if cod m1 == dom m2 then composeMorphisms m1 m2 else

a78048ccbdb6256da15e6b0e7e95355e480c2301nd fail "target of first and source of second morphism are different"

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndinstance Ord sign => Category sign (DefaultMorphism sign) where

a78048ccbdb6256da15e6b0e7e95355e480c2301nd dom = domOfDefaultMorphism

a78048ccbdb6256da15e6b0e7e95355e480c2301nd cod = codOfDefaultMorphism

a78048ccbdb6256da15e6b0e7e95355e480c2301nd ide = ideOfDefaultMorphism

a78048ccbdb6256da15e6b0e7e95355e480c2301nd isInclusion = const True

a78048ccbdb6256da15e6b0e7e95355e480c2301nd composeMorphisms = compOfDefaultMorphism

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd{- | Abstract syntax, parsing and printing.

a78048ccbdb6256da15e6b0e7e95355e480c2301nd There are three types for abstract syntax:

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

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

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-}

a78048ccbdb6256da15e6b0e7e95355e480c2301ndclass (Language lid, PrintTypeConv basic_spec, GetRange basic_spec,

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Monoid basic_spec, -- for joining converted signatures and sentences

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Pretty symbol,

a78048ccbdb6256da15e6b0e7e95355e480c2301nd EqPrintTypeConv symb_items,

a78048ccbdb6256da15e6b0e7e95355e480c2301nd EqPrintTypeConv symb_map_items)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd => Syntax lid basic_spec symbol symb_items symb_map_items

a78048ccbdb6256da15e6b0e7e95355e480c2301nd | lid -> basic_spec symbol symb_items symb_map_items

a78048ccbdb6256da15e6b0e7e95355e480c2301nd where

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- | parsers and printers

a78048ccbdb6256da15e6b0e7e95355e480c2301nd parsersAndPrinters :: lid -> Map.Map String

a78048ccbdb6256da15e6b0e7e95355e480c2301nd (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd parsersAndPrinters li = case parse_basic_spec li of

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Nothing -> Map.empty

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Just p -> makeDefault (p, pretty)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- | parser for basic specifications

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- | parser for symbol lists

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- | parser for symbol maps

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd toItem :: lid -> basic_spec -> Item

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- default implementations

a78048ccbdb6256da15e6b0e7e95355e480c2301nd parse_basic_spec _ = Nothing

a78048ccbdb6256da15e6b0e7e95355e480c2301nd parse_symb_items _ = Nothing

a78048ccbdb6256da15e6b0e7e95355e480c2301nd parse_symb_map_items _ = Nothing

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndbasicSpecParser :: Syntax lid basic_spec symbol symb_items symb_map_items

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

a78048ccbdb6256da15e6b0e7e95355e480c2301ndbasicSpecParser sm = fmap fst . parserAndPrinter sm

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndbasicSpecPrinter :: Syntax lid basic_spec symbol symb_items symb_map_items

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

a78048ccbdb6256da15e6b0e7e95355e480c2301ndbasicSpecPrinter sm = fmap snd . parserAndPrinter sm

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndbasicSpecSyntaxes :: Syntax lid basic_spec symbol symb_items symb_map_items

a78048ccbdb6256da15e6b0e7e95355e480c2301nd => lid -> [String]

a78048ccbdb6256da15e6b0e7e95355e480c2301ndbasicSpecSyntaxes = Map.keys . serializations . language_name

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndparserAndPrinter :: Syntax lid basic_spec symbol symb_items symb_map_items

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd basic_spec -> Doc)

a78048ccbdb6256da15e6b0e7e95355e480c2301ndparserAndPrinter sm l = lookupDefault l sm (parsersAndPrinters l)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- | function to lookup parser or printer

a78048ccbdb6256da15e6b0e7e95355e480c2301ndlookupDefault :: Syntax lid basic_spec symbol symb_items symb_map_items

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

a78048ccbdb6256da15e6b0e7e95355e480c2301ndlookupDefault l im m = case im of

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Just i -> do

a78048ccbdb6256da15e6b0e7e95355e480c2301nd let s = iriToStringUnsecure i

a78048ccbdb6256da15e6b0e7e95355e480c2301nd ser <- if isSimple i then return s

a78048ccbdb6256da15e6b0e7e95355e480c2301nd else lookupSerialization (language_name l) s

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Map.lookup ser m

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd else Map.lookup "" m

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

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

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

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndmakeDefault :: b -> Map.Map String b

a78048ccbdb6256da15e6b0e7e95355e480c2301ndmakeDefault = Map.singleton ""

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301ndaddSyntax :: String -> b -> Map.Map String b -> Map.Map String b

a78048ccbdb6256da15e6b0e7e95355e480c2301ndaddSyntax = Map.insert

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd{- | Sentences, provers and symbols.

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Provers capture the entailment relation between sets of sentences

a78048ccbdb6256da15e6b0e7e95355e480c2301nd and sentences. They may return proof trees witnessing proofs.

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Signatures are equipped with underlying sets of symbols

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd see CASL RefMan p. 191ff.

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-}

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Ord symbol, -- for efficient lookup

a78048ccbdb6256da15e6b0e7e95355e480c2301nd PrintTypeConv sign, PrintTypeConv morphism,

a78048ccbdb6256da15e6b0e7e95355e480c2301nd GetRange sentence, GetRange symbol,

a78048ccbdb6256da15e6b0e7e95355e480c2301nd PrintTypeConv sentence, PrintTypeConv symbol)

a78048ccbdb6256da15e6b0e7e95355e480c2301nd => Sentences lid sentence sign morphism symbol

a78048ccbdb6256da15e6b0e7e95355e480c2301nd | lid -> sentence sign morphism symbol

a78048ccbdb6256da15e6b0e7e95355e480c2301nd where

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- | sentence translation along a signature morphism

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd map_sen l _ _ = statFail l "map_sen"

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- | simplification of sentences (leave out qualifications)

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

4aa603e6448b99f9371397d439795c91a93637eand simplify_sen _ _ = id

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- | negation of a sentence for disproving

a78048ccbdb6256da15e6b0e7e95355e480c2301nd negation :: lid -> sentence -> Maybe sentence

a78048ccbdb6256da15e6b0e7e95355e480c2301nd negation _ _ = Nothing

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- | modified signature printing when followed by sentences

a78048ccbdb6256da15e6b0e7e95355e480c2301nd print_sign :: lid -> sign -> Doc

a78048ccbdb6256da15e6b0e7e95355e480c2301nd print_sign _ = pretty

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- | print a sentence with comments

a78048ccbdb6256da15e6b0e7e95355e480c2301nd print_named :: lid -> Named sentence -> Doc

a78048ccbdb6256da15e6b0e7e95355e480c2301nd print_named _ = printAnnoted (addBullet . pretty) . fromLabelledSen

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- --------------------- symbols ---------------------------

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

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

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd sym_of _ _ = []

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd signature. This function contains more symbols than those being subject

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

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

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

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

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

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

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

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd mostSymsOf l = concatMap Set.toList . sym_of l

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- | symbol map for a signature morphism

a78048ccbdb6256da15e6b0e7e95355e480c2301nd symmap_of :: lid -> morphism -> EndoMap symbol

a78048ccbdb6256da15e6b0e7e95355e480c2301nd symmap_of _ _ = Map.empty

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd sym_name :: lid -> symbol -> Id

a78048ccbdb6256da15e6b0e7e95355e480c2301nd sym_name l _ = statError l "sym_name"

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- | a logic dependent kind of a symbol

a78048ccbdb6256da15e6b0e7e95355e480c2301nd symKind :: lid -> symbol -> String

a78048ccbdb6256da15e6b0e7e95355e480c2301nd symKind _ _ = ""

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

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd symsOfSen _ _ = []

a78048ccbdb6256da15e6b0e7e95355e480c2301nd -- | combine two symbols into another one

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd pair_symbols _ s1 _ = return s1

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- | makes a singleton list from the given value

a78048ccbdb6256da15e6b0e7e95355e480c2301ndsingletonList :: a -> [a]

a78048ccbdb6256da15e6b0e7e95355e480c2301ndsingletonList x = [x]

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- | set of symbols for a signature

a78048ccbdb6256da15e6b0e7e95355e480c2301ndsymset_of :: forall lid sentence sign morphism symbol .

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Sentences lid sentence sign morphism symbol =>

a78048ccbdb6256da15e6b0e7e95355e480c2301nd lid -> sign -> Set.Set symbol

a78048ccbdb6256da15e6b0e7e95355e480c2301ndsymset_of lid sig = Set.unions $ sym_of lid sig

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- | dependency ordered list of symbols for a signature

a78048ccbdb6256da15e6b0e7e95355e480c2301ndsymlist_of :: forall lid sentence sign morphism symbol .

a78048ccbdb6256da15e6b0e7e95355e480c2301nd Sentences lid sentence sign morphism symbol =>

a78048ccbdb6256da15e6b0e7e95355e480c2301nd lid -> sign -> [symbol]

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

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

a78048ccbdb6256da15e6b0e7e95355e480c2301ndinlineAxioms :: StaticAnalysis lid

a78048ccbdb6256da15e6b0e7e95355e480c2301nd basic_spec sentence symb_items symb_map_items

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

a78048ccbdb6256da15e6b0e7e95355e480c2301ndinlineAxioms _ _ = error "inlineAxioms"

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- | fail function for static analysis

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

a78048ccbdb6256da15e6b0e7e95355e480c2301ndstatFail lid = fail . statErrMsg lid

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

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

a78048ccbdb6256da15e6b0e7e95355e480c2301ndstatError lid = error . statErrMsg lid

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- | error message for static analysis

a78048ccbdb6256da15e6b0e7e95355e480c2301ndstatErrMsg :: Language lid => lid -> String -> String

a78048ccbdb6256da15e6b0e7e95355e480c2301ndstatErrMsg lid str =

a78048ccbdb6256da15e6b0e7e95355e480c2301nd "Logic." ++ str ++ " not implemented for: " ++ language_name lid

a78048ccbdb6256da15e6b0e7e95355e480c2301nd

a78048ccbdb6256da15e6b0e7e95355e480c2301nd{- static analysis

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd as explained in the structured specification semantics in the CASL

a78048ccbdb6256da15e6b0e7e95355e480c2301nd reference manual, chapter III.4.

a78048ccbdb6256da15e6b0e7e95355e480c2301nd The static analysis computes signatures from basic specifications,

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

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd unqualified symbols. Normal symbols are always fully qualified.

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

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

a78048ccbdb6256da15e6b0e7e95355e480c2301nd-}

a78048ccbdb6256da15e6b0e7e95355e480c2301ndclass ( Syntax lid basic_spec symbol symb_items symb_map_items

a78048ccbdb6256da15e6b0e7e95355e480c2301nd , Sentences lid sentence sign morphism symbol

a78048ccbdb6256da15e6b0e7e95355e480c2301nd , GetRange raw_symbol, Ord raw_symbol, Pretty raw_symbol

f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjung , Typeable raw_symbol)

727872d18412fc021f03969b8641810d8896820bhumbedooh => StaticAnalysis lid

0d0ba3a410038e179b695446bb149cce6264e0abnd basic_spec sentence symb_items symb_map_items

727872d18412fc021f03969b8641810d8896820bhumbedooh sign morphism symbol raw_symbol

cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedooh | lid -> basic_spec sentence symb_items symb_map_items

0d0ba3a410038e179b695446bb149cce6264e0abnd sign morphism symbol raw_symbol

cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedooh where

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

0d0ba3a410038e179b695446bb149cce6264e0abnd The resulting bspec has analyzed axioms in it.

0d0ba3a410038e179b695446bb149cce6264e0abnd The resulting sign is an extension of the input sign

0d0ba3a410038e179b695446bb149cce6264e0abnd plus newly declared or redeclared symbols.

ac082aefa89416cbdc9a1836eaf3bed9698201c8humbedooh See CASL RefMan p. 138 ff. -}

0d0ba3a410038e179b695446bb149cce6264e0abnd basic_analysis :: lid

0d0ba3a410038e179b695446bb149cce6264e0abnd -> Maybe ((basic_spec, sign, GlobalAnnos)

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

727872d18412fc021f03969b8641810d8896820bhumbedooh basic_analysis _ = Nothing

0d0ba3a410038e179b695446bb149cce6264e0abnd -- | Analysis of just sentences

0d0ba3a410038e179b695446bb149cce6264e0abnd sen_analysis :: lid

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

205f749042ed530040a4f0080dbcb47ceae8a374rjung sen_analysis _ = Nothing

af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowen -- | a basic analysis with additional arguments

0d0ba3a410038e179b695446bb149cce6264e0abnd extBasicAnalysis :: lid -> IRI -> LibName

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd -> basic_spec -> sign -> GlobalAnnos

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

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

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

-- | 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 "symbol(s) missing in target:"

, pretty $ Set.difference (symset_of l s1) $ 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

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

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

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

-}