Logic.hs revision 90d4b4667d5b25e067ac262aaf49efc0b175b74c
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveDataTypeable
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , FlexibleInstances, UndecidableInstances, ExistentialQuantification #-}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederModule : $Header$
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederDescription : central interface (type class) for logics in Hets
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2006
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederMaintainer : till@informatik.uni-bremen.de
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederStability : provisional
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederPortability : non-portable (various -fglasgow-exts extensions)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederCentral interface (type class) for logics in Hets
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederProvides data structures for logics (with symbols). Logics are
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder a type class with an /identity type/ (usually interpreted
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder by a singleton set) which serves to treat logics as
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder data. All the functions in the type class take the
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder identity as first argument in order to determine the logic.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder For logic (co)morphisms see "Logic.Comorphism"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder This module uses multiparameter type classes with functional dependencies
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (<http://www.haskell.org/haskellwiki/Functional_dependencies>)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder for defining an interface for the notion of logic. Multiparameter type
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder classes are needed because a logic consists of a collection of types,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder together with operations on these. Functional dependencies
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder are needed because no operation will involve all types of
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder the multiparameter type class; hence we need a method to derive
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder the missing types. We chose an easy way: for each logic, we
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder introduce a new singleton type that is the name, or constitutes the identity
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder of the logic. All other types of the multiparameter type class
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder depend on this /identity constituting/ type, and all operations take
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder the 'identity constituting' type as first arguments. The value
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder of the argument of the /identity constituting/ type is irrelevant
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (note that there is only one value of such a type anyway).
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Note that we tend to use @lid@ both for the /identity type/
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder of a logic, as well as for its unique inhabitant, i.e. @lid :: lid@.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder The other types involved in the definition of logic are as follows:
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder * sign: signatures, that is, contexts, or non-logical vocabularies,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder typically consisting of a set of declared sorts, predicates,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder function symbols, propositional letters etc., together with their
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder * sentence: logical formulas.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder * basic_spec: abstract syntax of basic specifications. The latter are
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder human-readable presentations of a signature together with some sentences.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder * symbol: symbols that may occur in a signature, fully qualified
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder with their types
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder * raw_symbol: symbols that may occur in a signature, possibly not
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder or partially qualified
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder * morphism: maps between signatures (typically preserving the structure).
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder * symb_items: abstract syntax of symbol lists, used for declaring some
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder symbols of a signature as hidden.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder * symb_map_items: abstract syntax of symbol maps, i.e. human-readable
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder presentations of signature morphisms.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder * sublogics: sublogics of the given logic. This type might be a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder record of Boolean flags, indicating whether some feature is
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder present in the sublogi of not.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder * proof_tree: proof trees.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder J. A. Goguen and R. M. Burstall
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Institutions: Abstract Model Theory for Specification and
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder JACM 39, p. 95-146, 1992
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (general notion of logic - model theory only)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder General Logics
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Logic Colloquium 87, p. 275-329, North Holland, 1989
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (general notion of logic - also proof theory;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder notion of logic representation, called map there)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder T. Mossakowski:
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Specification in an arbitrary institution with symbols
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 14th WADT 1999, LNCS 1827, p. 252-270
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (treatment of symbols and raw symbols, see also CASL semantics
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder in the CASL reference manual)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder T. Mossakowski, B. Klin:
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Institution Independent Static Analysis for CASL
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 15h WADT 2001, LNCS 2267, p. 221-237, 2002.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (what is needed for static anaylsis)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder S. Autexier and T. Mossakowski
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Integrating HOLCASL into the Development Graph Manager MAYA
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder FroCoS 2002, LNCS 2309, p. 2-17, 2002.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (interface to provers)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder CoFI (ed.): CASL Reference Manual, LNCS 2960, Springer Verlag, 2004.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (static semantics of CASL structured and architectural specifications)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder T. Mossakowski
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Heterogeneous specification and the heterogeneous tool set
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Habilitation thesis, University of Bremen, 2005
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (the general picture of heterogeneous specification)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Logic.Prover (Prover, ConsChecker, Theory (..))
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Taxonomy.MMiSSOntology (MMiSSOntology)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport qualified OMDoc.DataTypes as OMDoc
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , TCorOMElement
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport ATerm.Lib (ShATermConvertible)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Common.Prec (PrecMap)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport qualified Data.Set as Set
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport qualified Data.Map as Map
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | Stability of logic implementations
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederdata Stability = Stable | Testing | Unstable | Experimental
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder deriving (Eq, Show)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | shortcut for class constraints
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass ShATermConvertible a => Convertible a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance ShATermConvertible a => Convertible a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | shortcut for class constraints
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass (Pretty a, Convertible a) => PrintTypeConv a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance (Pretty a, Convertible a) => PrintTypeConv a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | shortcut for class constraints with equality
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass (Eq a, PrintTypeConv a) => EqPrintTypeConv a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance (Eq a, PrintTypeConv a) => EqPrintTypeConv a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | maps from a to a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedertype EndoMap a = Map.Map a a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- | the name of a logic.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Define instances like "data CASL = CASL deriving Show"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass Show lid => Language lid where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder language_name :: lid -> String
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder language_name = show
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder description :: lid -> String
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- default implementation
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder description _ = "No description available"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- | Categories are given as usual: objects, morphisms, identities,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder domain, codomain and composition. The type id is the name, or
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder the identity of the category. It is an argument to all functions
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder of the type class, serving disambiguation among instances
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (via the functional dependency lid -> object morphism).
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder The types for objects and morphisms may be restricted to
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder subtypes, using legal_obj and legal_mor. For example, for the
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder category of sets and injective maps, legal_mor would check
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder injectivity. Since Eq is a subclass of Category, it is also
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder possible to impose a quotient on the types for objects and morphisms.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Require Ord instances only for efficiency, i.e. in sets or maps.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass (Ord object, Ord morphism)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder => Category object morphism | morphism -> object where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | identity morphisms
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ide :: object -> morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | composition, in diagrammatic order,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder if intermediate objects are equal (not checked!) -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder composeMorphisms :: morphism -> morphism -> Result morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | domain and codomain of morphisms
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder dom, cod :: morphism -> object
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | the inverse of a morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder inverse :: morphism -> Result morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder inverse _ = fail "Logic.Logic.Category.inverse not implemented"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | test if the signature morphism an inclusion
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder isInclusion :: morphism -> Bool
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder isInclusion _ = False -- in general no inclusion
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | is a value of type morphism denoting a legal morphism?
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder legal_mor :: morphism -> Result ()
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder legal_mor _ = return ()
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | test if the signature morphism is the identity
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederisIdentity :: Category object morphism => morphism -> Bool
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederisIdentity m = isInclusion m && dom m == cod m
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedercomp :: Category object morphism => morphism -> morphism -> Result morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedercomp m1 m2 = if cod m1 == dom m2 then composeMorphisms m1 m2 else
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder fail "target of first and source of second morphism are different"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance Ord sign => Category sign (DefaultMorphism sign) where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder dom = domOfDefaultMorphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder cod = codOfDefaultMorphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ide = ideOfDefaultMorphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder isInclusion = const True
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder composeMorphisms = compOfDefaultMorphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- | Abstract syntax, parsing and printing.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder There are three types for abstract syntax:
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder basic_spec is for basic specifications (see CASL RefMan p. 5ff.),
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder symb_items is for symbol lists (see CASL RefMan p. 35ff.),
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder symb_map_items is for symbol maps (see CASL RefMan p. 35ff.).
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass (Language lid, PrintTypeConv basic_spec, GetRange basic_spec,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder EqPrintTypeConv symb_items,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder EqPrintTypeConv symb_map_items)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder => Syntax lid basic_spec symb_items symb_map_items
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder | lid -> basic_spec symb_items symb_map_items
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | parsers and printers
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder parsersAndPrinters :: lid -> Map.Map String
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (AParser st basic_spec, basic_spec -> Doc)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder parsersAndPrinters _ = Map.empty
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | parser for basic specifications
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder parse_basic_spec :: lid -> Maybe (AParser st basic_spec)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | parser for symbol lists
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder parse_symb_items :: lid -> Maybe (AParser st symb_items)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | parser for symbol maps
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder parse_symb_map_items :: lid -> Maybe (AParser st symb_map_items)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder toItem :: lid -> basic_spec -> Item
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- default implementations
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder parse_basic_spec _ = Nothing
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder parse_symb_items _ = Nothing
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder parse_symb_map_items _ = Nothing
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder toItem _ bs = mkFlatItem ("Basicspec", pretty bs) $ getRangeSpan bs
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- | Sentences, provers and symbols.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Provers capture the entailment relation between sets of sentences
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder and sentences. They may return proof trees witnessing proofs.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Signatures are equipped with underlying sets of symbols
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (such that the category of signatures becomes a concrete category),
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder see CASL RefMan p. 191ff.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass (Language lid, Category sign morphism, Ord sentence,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Ord symbol, -- for efficient lookup
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder PrintTypeConv sign, PrintTypeConv morphism,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder GetRange sentence, GetRange symbol,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder PrintTypeConv sentence, PrintTypeConv symbol)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder => Sentences lid sentence sign morphism symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder | lid -> sentence sign morphism symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | sentence translation along a signature morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder map_sen :: lid -> morphism -> sentence -> Result sentence
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder map_sen l _ _ = statFail l "map_sen"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | simplification of sentences (leave out qualifications)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder simplify_sen :: lid -> sign -> sentence -> sentence
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder simplify_sen _ _ = id
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | negation of a sentence for disproving
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder negation :: lid -> sentence -> Maybe sentence
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder negation _ _ = Nothing
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | modified signature printing when followed by sentences
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder print_sign :: lid -> sign -> Doc
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder print_sign _ = pretty
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | print a sentence with comments
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder print_named :: lid -> Named sentence -> Doc
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder print_named _ = printAnnoted (addBullet . pretty) . fromLabelledSen
4c4a3329080becd4b81d56396586b740487924cbChristian Maeder -- --------------------- symbols ---------------------------
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | dependency ordered list of symbol sets for a signature
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sym_of :: lid -> sign -> [Set.Set symbol]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sym_of _ _ = []
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | Dependency ordered list of a bigger symbol set for a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder signature. This function contains more symbols than those being subject
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder to hiding and renaming (given by 'sym_of') to better represent a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder signature as a set of symbols given within xml files. At least for CASL
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder additional symbols for (direct) subsorts will be created, but note, that
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder no symbol for a partial function will be created, if the signature
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder contains this function as total, although a signature with just that
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder partial function would be a subsignature. This function is supposed to
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder work over partial signatures created by 'signatureDiff'. -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder mostSymsOf :: lid -> sign -> [symbol]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder mostSymsOf l = concatMap Set.toList . sym_of l
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | symbol map for a signature morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder symmap_of :: lid -> morphism -> EndoMap symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder symmap_of _ _ = Map.empty
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | symbols have a name, see CASL RefMan p. 192
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sym_name :: lid -> symbol -> Id
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sym_name l _ = statError l "sym_name"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | a logic dependent kind of a symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder symKind :: lid -> symbol -> String
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder symKind _ _ = ""
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | the symbols occuring in a sentence (any order)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder symsOfSen :: lid -> sentence -> [symbol]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder symsOfSen _ _ = []
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | makes a singleton list from the given value
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedersingletonList :: a -> [a]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedersingletonList x = [x]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | set of symbols for a signature
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedersymset_of :: forall lid sentence sign morphism symbol .
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Sentences lid sentence sign morphism symbol =>
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder lid -> sign -> Set.Set symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedersymset_of lid sig = Set.unions $ sym_of lid sig
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | dependency ordered list of symbols for a signature
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedersymlist_of :: forall lid sentence sign morphism symbol .
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Sentences lid sentence sign morphism symbol =>
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder lid -> sign -> [symbol]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedersymlist_of lid sig = concatMap Set.toList $ sym_of lid sig
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | a dummy static analysis function to allow type checking *.inline.hs files
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederinlineAxioms :: StaticAnalysis lid
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder basic_spec sentence symb_items symb_map_items
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sign morphism symbol raw_symbol => lid -> String -> [Named sentence]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederinlineAxioms _ _ = error "inlineAxioms"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | fail function for static analysis
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederstatFail :: (Language lid, Monad m) => lid -> String -> m a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederstatFail lid = fail . statErrMsg lid
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederstatError :: Language lid => lid -> String -> a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederstatError lid = error . statErrMsg lid
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | error message for static analysis
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederstatErrMsg :: Language lid => lid -> String -> String
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederstatErrMsg lid str =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder "Logic." ++ str ++ " not implemented for: " ++ language_name lid
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- static analysis
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder This type class provides the data needed for an institution with symbols,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder as explained in the structured specification semantics in the CASL
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder reference manual, chapter III.4.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder The static analysis computes signatures from basic specifications,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder and signature morphisms from symbol lists and symbol maps. The latter
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder needs an intermediate stage, so-called raw symbols, which are possibly
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder unqualified symbols. Normal symbols are always fully qualified.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder In the CASL reference manual, our symbols are called "signature symbols",
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder and our raw symbols are called "symbols". (Terminology should be adapted.)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass ( Syntax lid basic_spec symb_items symb_map_items
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , Sentences lid sentence sign morphism symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , GetRange raw_symbol, Ord raw_symbol, Pretty raw_symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , Typeable raw_symbol)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder => StaticAnalysis lid
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder basic_spec sentence symb_items symb_map_items
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sign morphism symbol raw_symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder | lid -> basic_spec sentence symb_items symb_map_items
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sign morphism symbol raw_symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | static analysis of basic specifications and symbol maps.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder The resulting bspec has analyzed axioms in it.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder The resulting sign is an extension of the input sign
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder plus newly declared or redeclared symbols.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder See CASL RefMan p. 138 ff. -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder basic_analysis :: lid
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> Maybe ((basic_spec, sign, GlobalAnnos)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder basic_analysis _ = Nothing
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | a basic analysis with additional arguments
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder extBasicAnalysis :: lid -> IRI -> LibId
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> basic_spec -> sign -> GlobalAnnos
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> Result (basic_spec, ExtSign sign symbol, [Named sentence])
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder extBasicAnalysis l _ _ b s g = case basic_analysis l of
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Nothing -> statFail l "basic_analysis"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Just ba -> ba (b, s, g)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | static analysis of symbol maps, see CASL RefMan p. 222f.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder stat_symb_map_items :: lid -> sign -> Maybe sign -> [symb_map_items]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> Result (EndoMap raw_symbol)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder stat_symb_map_items l _ _ _ = statFail l "stat_symb_map_items"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | static analysis of symbol lists, see CASL RefMan p. 221f.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder stat_symb_items :: lid -> sign -> [symb_items] -> Result [raw_symbol]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder stat_symb_items l _ _ = statFail l "stat_symb_items"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- ----------------------- amalgamation ---------------------------
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Computation of colimits of signature diagram.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Indeed, it suffices to compute a cocone that is weakly amalgamable
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder see Till Mossakowski,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Heterogeneous specification and the heterogeneous tool set
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | architectural sharing analysis, see CASL RefMan p. 247ff.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ensures_amalgamability :: lid ->
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ([CASLAmalgOpt], -- the program options
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Gr sign (Int, morphism), -- the diagram to be analyzed
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder [(Int, morphism)], -- the sink
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Gr String String) -- the descriptions of nodes and edges
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> Result Amalgamates
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ensures_amalgamability l _ = warning Amalgamates
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ("amalgamability test not implemented for logic " ++ show l)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | quotient term algebra for normalization of freeness
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder quotient_term_algebra :: lid -- the logic
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> morphism -- sigma : Sigma -> SigmaM
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> [Named sentence] -- Th(M)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (sign, -- SigmaK
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder [Named sentence] -- Ax(K)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder quotient_term_algebra l _ _ = statFail l "quotient_term_algebra"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | signature colimits
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder signature_colimit :: lid -> Gr sign (Int, morphism)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> Result (sign, Map.Map Int morphism)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder signature_colimit l _ = statFail l "signature_colimit"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | rename and qualify the symbols considering a united incoming
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder morphisms, code out overloading and
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder create sentences for the overloading relation -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder qualify :: lid -> SIMPLE_ID -> LibId -> morphism -> sign
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> Result (morphism, [Named sentence])
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder qualify l _ _ _ _ = statFail l "qualify"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- ------------------ symbols and raw symbols ---------------------
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | Construe a symbol, like f:->t, as a raw symbol.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder This is a one-sided inverse to the function SymSySigSym
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder in the CASL RefMan p. 192. -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder symbol_to_raw :: lid -> symbol -> raw_symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder symbol_to_raw l _ = statError l "symbol_to_raw"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | Construe an identifier, like f, as a raw symbol.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder See CASL RefMan p. 192, function IDAsSym -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder id_to_raw :: lid -> Id -> raw_symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder id_to_raw l _ = statError l "id_to_raw"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | Check wether a symbol matches a raw symbol, for
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder example, f:s->t matches f. See CASL RefMan p. 192 -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder matches :: lid -> symbol -> raw_symbol -> Bool
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder matches _ _ _ = True
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- ------------- operations on signatures and morphisms -----------
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | the empty (initial) signature, see CASL RefMan p. 193
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder empty_signature :: lid -> sign
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | adds a symbol to a given signature
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder add_symb_to_sign :: lid -> sign -> symbol -> Result sign
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder add_symb_to_sign l _ _ = statFail l "add_symb_to_sign"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | union of signatures, see CASL RefMan p. 193
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder signature_union :: lid -> sign -> sign -> Result sign
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder signature_union l _ _ = statFail l "signature_union"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | difference of signatures resulting in unclosed pre-signatures
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder signatureDiff :: lid -> sign -> sign -> Result sign
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder signatureDiff l _ _ = statFail l "signatureDiff"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | intersection of signatures
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder intersection :: lid -> sign -> sign -> Result sign
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder intersection l _ _ = statFail l "intersection"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | final union of signatures, see CASL RefMan p. 194
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder final_union :: lid -> sign -> sign -> Result sign
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder final_union l _ _ = statFail l "final_union"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | union of signature morphims, see CASL RefMan p. 196
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder morphism_union :: lid -> morphism -> morphism -> Result morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder morphism_union l _ _ = statFail l "morphism_union"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | subsignatures, see CASL RefMan p. 194
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder is_subsig :: lid -> sign -> sign -> Bool
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder is_subsig _ _ _ = False
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | construct the inclusion morphisms between subsignatures,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder see CASL RefMan p. 194 -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder subsig_inclusion :: lid -> sign -> sign -> Result morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder subsig_inclusion l _ _ = statFail l "subsig_inclusion"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | the signature (co)generated by a set of symbols in another
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder signature is the smallest (largest) signature containing
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (excluding) the set of symbols. Needed for revealing and
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder hiding, see CASL RefMan p. 197ff. -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder generated_sign, cogenerated_sign ::
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder lid -> Set.Set symbol -> sign -> Result morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder generated_sign l _ _ = statFail l "generated_sign"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder cogenerated_sign l _ _ = statFail l "cogenerated_sign"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | Induce a signature morphism from a source signature and
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder a raw symbol map. Needed for translation (SP with SM).
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder See CASL RefMan p. 198 -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder induced_from_morphism ::
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder lid -> EndoMap raw_symbol -> sign -> Result morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder induced_from_morphism l _ _ = statFail l "induced_from_morphism"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | Induce a signature morphism between two signatures by a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder raw symbol map. Needed for instantiation and views.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder See CASL RefMan p. 198f. -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder induced_from_to_morphism ::
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder lid -> EndoMap raw_symbol -> ExtSign sign symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> ExtSign sign symbol -> Result morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder induced_from_to_morphism l rm (ExtSign sig _) (ExtSign tar _) = do
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder mor <- induced_from_morphism l rm sig
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder inclusion l (cod mor) tar >>= composeMorphisms mor
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | Check whether a signature morphism is transportable.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder See CASL RefMan p. 304f. -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder is_transportable :: lid -> morphism -> Bool
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder is_transportable _ _ = False
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | Check whether the underlying symbol map of a signature morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder is injective -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder is_injective :: lid -> morphism -> Bool
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder is_injective _ _ = False
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | generate an ontological taxonomy, if this makes sense
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder theory_to_taxonomy :: lid
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> TaxoGraphKind
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> MMiSSOntology
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> sign -> [Named sentence]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> Result MMiSSOntology
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder theory_to_taxonomy l _ _ _ _ = statFail l "theory_to_taxonomy"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | guarded inclusion
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinclusion :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sign morphism symbol raw_symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder => lid -> sign -> sign -> Result morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinclusion l s1 s2 = if is_subsig l s1 s2 then subsig_inclusion l s1 s2
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder else fail $ show $ fsep
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder [ text (language_name l)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , text "symbol(s) missing in target:"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , pretty $ Set.difference (symset_of l s1) $ symset_of l s2 ]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- | semi lattices with top (needed for sublogics). Note that `Ord` is
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederonly used for efficiency and is not related to the /partial/ order given
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederby the lattice. Only `Eq` is used to define `isSubElem` -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass (Ord l, Show l) => SemiLatticeWithTop l where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder join :: l -> l -> l
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance SemiLatticeWithTop () where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder join _ _ = ()
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | less or equal for semi lattices
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederisSubElem :: SemiLatticeWithTop l => l -> l -> Bool
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederisSubElem a b = join a b == b
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | class providing the minimal sublogic of an item
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass MinSublogic sublogic item where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder minSublogic :: item -> sublogic
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | a default instance for no sublogics
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance MinSublogic () a where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder minSublogic _ = ()
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | class providing also the projection of an item to a sublogic
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass MinSublogic sublogic item => ProjectSublogic sublogic item where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder projectSublogic :: sublogic -> item -> item
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | a default instance for no sublogics
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance ProjectSublogic () b where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder projectSublogic _ = id
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | like ProjectSublogic, but providing a partial projection
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass MinSublogic sublogic item => ProjectSublogicM sublogic item where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder projectSublogicM :: sublogic -> item -> Maybe item
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | a default instance for no sublogics
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance ProjectSublogicM () b where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder projectSublogicM _ = Just
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | a class for providing a sublogi name
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass SublogicName l where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sublogicName :: l -> String
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance SublogicName () where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sublogicName () = ""
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | a type for syntax information eventually stored in the signature
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedertype SyntaxTable = (PrecMap, AssocMap)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- Type class logic. The central type class of Hets, providing the
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder interface for logics. This type class is instantiated for many logics,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder and it is used for the logic independent parts of Hets.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder It hence provides an abstraction barrier between logic specific and
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder logic indepdendent code.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder This type class extends the class StaticAnalysis by a sublogic mechanism.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Sublogics are important since they avoid the need to provide an own
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder instance of the class logic for each sublogic. Instead, the sublogic
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder can use the datastructures and operations of the main logic, and
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder functions are provided to test whether a given item lies within the
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sublogic. Also, projection functions from a super-logic to a sublogic
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder are provided.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass (StaticAnalysis lid
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder basic_spec sentence symb_items symb_map_items
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sign morphism symbol raw_symbol,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder SemiLatticeWithTop sublogics,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder MinSublogic sublogics sentence,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ProjectSublogic sublogics basic_spec,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ProjectSublogicM sublogics symb_items,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ProjectSublogicM sublogics symb_map_items,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ProjectSublogic sublogics sign,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ProjectSublogic sublogics morphism,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ProjectSublogicM sublogics symbol,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Convertible sublogics,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder SublogicName sublogics,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Ord proof_tree, Show proof_tree,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Convertible proof_tree)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder => Logic lid sublogics
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder basic_spec sentence symb_items symb_map_items
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sign morphism symbol raw_symbol proof_tree
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder | lid -> sublogics
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder basic_spec sentence symb_items symb_map_items
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sign morphism symbol raw_symbol proof_tree
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | stability of the implementation
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder stability :: lid -> Stability
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder stability _ = Experimental
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | for a process logic, return its data logic
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder data_logic :: lid -> Maybe AnyLogic
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder data_logic _ = Nothing
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | the top sublogic, corresponding to the whole logic
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder top_sublogic :: lid -> sublogics
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder top_sublogic _ = top
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | list all the sublogics of the current logic
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder all_sublogics :: lid -> [sublogics]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder all_sublogics li = [top_sublogic li]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | provide the embedding of a projected signature into the
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder original signature -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder proj_sublogic_epsilon :: lid -> sublogics -> sign -> morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder proj_sublogic_epsilon _ _ = ide
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- --------------------- provers ---------------------------
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | several provers can be provided. See module "Logic.Prover"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder provers :: lid -> [Prover sign sentence morphism sublogics proof_tree]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder provers _ = []
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | consistency checkers
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder cons_checkers :: lid
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> [ConsChecker sign sentence
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sublogics morphism proof_tree]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder cons_checkers _ = []
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | conservativity checkers
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder conservativityCheck :: lid
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> [ConservativityChecker sign sentence morphism]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder conservativityCheck _ = []
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | the empty proof tree
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder empty_proof_tree :: lid -> proof_tree
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder empty_proof_tree l = statError l "empty_proof_tree"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- --------------------- OMDoc ---------------------------
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder syntaxTable :: lid -> sign -> Maybe SyntaxTable
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder syntaxTable _ _ = Nothing
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder omdoc_metatheory :: lid -> Maybe OMDoc.OMCD
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- default implementation, no logic should throw an error here
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder and the base of omcd should be a parseable URI -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder omdoc_metatheory _ = Nothing
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder export_symToOmdoc :: lid -> OMDoc.NameMap symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> symbol -> String -> Result OMDoc.TCElement
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder export_symToOmdoc l _ _ = statFail l "export_symToOmdoc"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder export_senToOmdoc :: lid -> OMDoc.NameMap symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> sentence -> Result OMDoc.TCorOMElement
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder export_senToOmdoc l _ _ = statFail l "export_senToOmdoc"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | additional information which has to be exported can be
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder exported by this function -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder export_theoryToOmdoc :: lid -> OMDoc.SigMap symbol -> sign
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> [Named sentence] -> Result [OMDoc.TCElement]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- default implementation does no extra export
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , sufficient in some cases -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder export_theoryToOmdoc _ _ _ _ = return []
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder omdocToSym :: lid -> OMDoc.SigMapI symbol -> OMDoc.TCElement
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> String -> Result symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder omdocToSym l _ _ _ = statFail l "omdocToSym"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder omdocToSen :: lid -> OMDoc.SigMapI symbol -> OMDoc.TCElement
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> String -> Result (Maybe (Named sentence))
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder omdocToSen l _ _ _ = statFail l "omdocToSen"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | Algebraic Data Types are imported with this function.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder By default the input is returned without changes. -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder addOMadtToTheory :: lid -> OMDoc.SigMapI symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> (sign, [Named sentence]) -> [[OMDoc.OmdADT]]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> Result (sign, [Named sentence])
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- no logic should throw an error here
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder addOMadtToTheory l _ t adts = do
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder unless (null adts) $ warning ()
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (concat [ "ADT handling not implemented for logic "
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , show l, " but some adts have to be handled" ])
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | additional information which has to be imported can be
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder imported by this function. By default the input is returned
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder without changes. -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder addOmdocToTheory :: lid -> OMDoc.SigMapI symbol
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> (sign, [Named sentence]) -> [OMDoc.TCElement]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> Result (sign, [Named sentence])
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- no logic should throw an error here
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder addOmdocToTheory _ _ t _ = return t
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- The class of logics which can be used as logical frameworks, in which object
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder logics can be specified by the user. Currently the only logics implementing
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder this class are LF, Maude, and Isabelle, with the latter two only having
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder dummy implementations.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder The function "base_sig" returns the base signature of the framework -
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder for details see Integrating Logical Frameworks in Hets by M. Codescu et al
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder The function "write_logic" constructs the contents of the Logic_L
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder file, where L is the name of the object logic passed as an argument.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Typically, this file will declare the lid of the object logic L and
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder instances of the classes Language, Syntax, Sentences, Logic, and
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder StaticAnalysis. The instance of Category is usually inherited from
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder the framework itself as the object logic reuses the signatures and
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder morphisms of the framework.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder The function "write_syntax" constructs the contents of the file declaring
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder the Ltruth morphism (see the reference given above). If proofs and models
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder are later integrated into Hets, there should be analogous functions
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder "write_proofs" and "write_models" added, declaring the Lpf and
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Lmod morphisms respectively. -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass Logic lid sublogics basic_spec sentence
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder symb_items symb_map_items sign
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder morphism symbol raw_symbol proof_tree
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder => LogicFram lid sublogics basic_spec sentence
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder symb_items symb_map_items sign
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder morphism symbol raw_symbol proof_tree
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder | lid -> sublogics basic_spec sentence symb_items symb_map_items
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sign morphism symbol raw_symbol proof_tree
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- | the base signature
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder base_sig :: lid -> sign
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder base_sig l = error $ "Function base_sig nyi for logic " ++ shows l "."
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | generation of the object logic instances
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder second argument is object logic name -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder write_logic :: lid -> String -> String
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder write_logic l = error
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder $ "Function write_logic nyi for logic " ++ shows l "."
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {- | generation of the Ltruth morphism declaration
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder second argument is the object logic name
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder third argument is the Ltruth morphism -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder write_syntax :: lid -> String -> morphism -> String
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder write_syntax l = error $
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder "Function write_syntax nyi for logic " ++ shows l "."
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder write_proof :: lid -> String -> morphism -> String
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder write_proof l = error $
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder "Function write_proof nyi for logic " ++ shows l "."
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder write_model :: lid -> String -> morphism -> String
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder write_model l = error $
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder "Function write_model nyi for logic " ++ shows l "."
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder read_morphism :: lid -> FilePath -> morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder read_morphism l _ = error $
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder "Function read_morphism nyi for logic " ++ shows l "."
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder write_comorphism :: lid -> String -> String -> String
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> morphism -> morphism -> morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder write_comorphism l = error $
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder "Function write_comorphism nyi for logic " ++ shows l "."
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- --------------------------------------------------------------
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederDerived functions
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-------------------------------------------------------------- -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | the empty theory
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederemptyTheory :: StaticAnalysis lid
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder basic_spec sentence symb_items symb_map_items
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sign morphism symbol raw_symbol =>
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder lid -> Theory sign sentence proof_tree
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederemptyTheory lid = Theory (empty_signature lid) Map.empty
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- --------------------------------------------------------------
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederExistential type covering any logic
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-------------------------------------------------------------- -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | the disjoint union of all logics
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederdata AnyLogic = forall lid sublogics
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder basic_spec sentence symb_items symb_map_items
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sign morphism symbol raw_symbol proof_tree .
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Logic lid sublogics
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder basic_spec sentence symb_items symb_map_items
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sign morphism symbol raw_symbol proof_tree =>
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder deriving Typeable
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance GetRange AnyLogic
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance Show AnyLogic where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder show (Logic lid) = language_name lid
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance Eq AnyLogic where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder a == b = compare a b == EQ
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance Ord AnyLogic where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder compare = comparing show
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- class hierarchy:
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Sentences Syntax
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder StaticAnalysis (no sublogics)