Logic.hs revision d058429727dd696a0327cdc28cadd268c34c36ba
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu{-# OPTIONS -fallow-undecidable-instances #-}
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuModule : $Header$
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuDescription : central interface (type class) for logics in Hets
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2006
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuMaintainer : till@informatik.uni-bremen.de
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuStability : provisional
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuPortability : non-portable (various -fglasgow-exts extensions)
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuCentral interface (type class) for logics in Hets
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuProvides data structures for logics (with symbols). Logics are
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu a type class with an /identity type/ (usually interpreted
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu by a singleton set) which serves to treat logics as
239330cd665aac95fcf9cf95449594c96667cbc2Robert Savu data. All the functions in the type class take the
69b1e90bbb27ce2dd365628c07c0f03a3ae97b26Robert Savu identity as first argument in order to determine the logic.
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz For logic (co)morphisms see "Logic.Comorphism"
239330cd665aac95fcf9cf95449594c96667cbc2Robert Savu This module uses multiparameter type classes with functional dependencies
239330cd665aac95fcf9cf95449594c96667cbc2Robert Savu (<http://www.haskell.org/haskellwiki/Functional_dependencies>)
37dd4c99dbe470cce3fe0d89a011186f080e8910Robert Savu for defining an interface for the notion of logic. Multiparameter type
37dd4c99dbe470cce3fe0d89a011186f080e8910Robert Savu classes are needed because a logic consists of a collection of types,
37dd4c99dbe470cce3fe0d89a011186f080e8910Robert Savu together with operations on these. Functional dependencies
37dd4c99dbe470cce3fe0d89a011186f080e8910Robert Savu are needed because no operation will involve all types of
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz the multiparameter type class; hence we need a method to derive
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu the missing types. We chose an easy way: for each logic, we
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu introduce a new singleton type that is the name, or constitutes the identity
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz of the logic. All other types of the multiparameter type class
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu depend on this /identity constituting/ type, and all operations take
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu the 'identity constituting' type as first arguments. The value
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu of the argument of the /identity constituting/ type is irrelevant
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz (note that there is only one value of such a type anyway).
ad2e68e571352b6759441733df697e075ceed341Robert Savu Note that we tend to use @lid@ both for the /identity type/
239330cd665aac95fcf9cf95449594c96667cbc2Robert Savu of a logic, as well as for its unique inhabitant, i.e. @lid :: lid@.
ad2e68e571352b6759441733df697e075ceed341Robert Savu The other types involved in the definition of logic are as follows:
ad2e68e571352b6759441733df697e075ceed341Robert Savu * sign: signatures, that is, contexts, or non-logical vocabularies,
ad2e68e571352b6759441733df697e075ceed341Robert Savu typically consisting of a set of declared sorts, predicates,
ad2e68e571352b6759441733df697e075ceed341Robert Savu function symbols, propositional letters etc., together with their
239330cd665aac95fcf9cf95449594c96667cbc2Robert Savu * sentence: logical formulas.
ad2e68e571352b6759441733df697e075ceed341Robert Savu * basic_spec: abstract syntax of basic specifications. The latter are
ad2e68e571352b6759441733df697e075ceed341Robert Savu human-readable presentations of a signature together with some sentences.
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu * symbol: symbols that may occur in a signature, fully qualified
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu with their types
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu * raw_symbol: symbols that may occur in a signature, possibly not
ad2e68e571352b6759441733df697e075ceed341Robert Savu or partially qualified
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz * morphism: maps between signatures (typically preserving the structure).
ad2e68e571352b6759441733df697e075ceed341Robert Savu * symb_items: abstract syntax of symbol lists, used for declaring some
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu symbols of a signature as hidden.
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu * symb_map_items: abstract syntax of symbol maps, i.e. human-readable
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu presentations of signature morphisms.
ec95eebae395ed8858ba5b51d992d6b4c50cec86Robert Savu * sublogics: sublogics of the given logic. This type might be a
ec95eebae395ed8858ba5b51d992d6b4c50cec86Robert Savu record of Boolean flags, indicating whether some feature is
ec95eebae395ed8858ba5b51d992d6b4c50cec86Robert Savu present in the sublogi of not.
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu * proof_tree: proof trees.
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu J. A. Goguen and R. M. Burstall
ec95eebae395ed8858ba5b51d992d6b4c50cec86Robert Savu Institutions: Abstract Model Theory for Specification and
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz JACM 39, p. 95-146, 1992
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu (general notion of logic - model theory only)
ad2e68e571352b6759441733df697e075ceed341Robert Savu General Logics
ad2e68e571352b6759441733df697e075ceed341Robert Savu Logic Colloquium 87, p. 275-329, North Holland, 1989
e09066e7b76cea97557974b825bb057455b24ab0Robert Savu (general notion of logic - also proof theory;
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu notion of logic representation, called map there)
ad2e68e571352b6759441733df697e075ceed341Robert Savu T. Mossakowski:
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu Specification in an arbitrary institution with symbols
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu 14th WADT 1999, LNCS 1827, p. 252-270
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu (treatment of symbols and raw symbols, see also CASL semantics
ad2e68e571352b6759441733df697e075ceed341Robert Savu in the CASL reference manual)
ad2e68e571352b6759441733df697e075ceed341Robert Savu T. Mossakowski, B. Klin:
ad2e68e571352b6759441733df697e075ceed341Robert Savu Institution Independent Static Analysis for CASL
a9c461443a740732a62d58c1c465b88cba3c606bRobert Savu 15h WADT 2001, LNCS 2267, p. 221-237, 2002.
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz (what is needed for static anaylsis)
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz S. Autexier and T. Mossakowski
239330cd665aac95fcf9cf95449594c96667cbc2Robert Savu Integrating HOLCASL into the Development Graph Manager MAYA
module Logic.Logic where
import Logic.Prover (Prover, ConsChecker, Theory(..))
import Taxonomy.MMiSSOntology (MMiSSOntology)
import ATC.DefaultMorphism ()
import Common.AS_Annotation
import Common.ATerm.Lib (ShATermConvertible)
import Common.Amalgamate
import Common.AnnoState
import Common.Consistency
import Common.DefaultMorphism
import Common.Doc
import Common.DocUtils
import Common.ExtSign
import Common.GlobalAnnotations
import Common.Id
import Common.Lib.Graph
import Common.LibName
import Common.Result
import Common.Taxonomy
import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.Typeable
type EndoMap a = Map.Map a a
inverse _ = fail "Logic.Logic.Category.inverse not implemented"
sym_of :: lid -> sign -> Set.Set symbol
sym_of _ _ = Set.empty
symmap_of _ _ = Map.empty
-- | a dummy static analysis function to allow type checking *.inline.hs files
-> Result (sign, Map.Map Int morphism)
lid -> Set.Set symbol -> sign -> Result morphism
-- | several provers can be provided. See module "Logic.Prover"
empty_theory lid = Theory (empty_signature lid) Map.empty