Logic.hs revision e1542391fc8fe6f74f75e0f83366ec254ae909f8
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose{-# OPTIONS -fallow-undecidable-instances #-}
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseModule : $Header$
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseDescription : central interface (type class) for logics in Hets
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2006
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseMaintainer : till@informatik.uni-bremen.de
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseStability : provisional
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BosePortability : non-portable (various -fglasgow-exts extensions)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseCentral interface (type class) for logics in Hets
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseProvides data structures for logics (with symbols). Logics are
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose a type class with an /identity type/ (usually interpreted
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose by a singleton set) which serves to treat logics as
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose data. All the functions in the type class take the
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose identity as first argument in order to determine the logic.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose For logic (co)morphisms see "Logic.Comorphism"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose This module uses multiparameter type classes
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose (<http://haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#multi-param-type-classes>)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose with functional dependencies (<http://haskell.org/hawiki/FunDeps>)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose for defining an interface for the notion of logic. Multiparameter type
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose classes are needed because a logic consists of a collection of types,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose together with operations on these. Functional dependencies
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose are needed because no operation will involve all types of
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose the multiparameter type class; hence we need a method to derive
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose the missing types. We chose an easy way: for each logic, we
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose introduce a new singleton type that is the name, or constitutes the identity
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose of the logic. All other types of the multiparameter type class
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose depend on this /identity constituting/ type, and all operations take
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose the 'identity constituting' type as first arguments. The value
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose of the argument of the /identity constituting/ type is irrelevant
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose (note that there is only one value of such a type anyway).
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Note that we tend to use @lid@ both for the /identity type/
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose of a logic, as well as for its unique inhabitant, i.e. @lid :: lid@.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose The other types involved in the definition of logic are as follows:
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose * sign: signatures, that is, contexts, or non-logical vocabularies,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose typically consisting of a set of declared sorts, predicates,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose function symbols, propositional letters etc., together with their
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose * sentence: logical formulas.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose * basic_spec: abstract syntax of basic specifications. The latter are
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose human-readable presentations of a signature together with some sentences.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose * symbol: symbols that may occur in a signature, fully qualified
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose with their types
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose * raw_symbol: symbols that may occur in a signature, possibly not
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose or partially qualified
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose * morphism: maps between signatures (typically preserving the structure).
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose * symb_items: abstract syntax of symbol lists, used for declaring some
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose symbols of a signature as hidden.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose * symb_map_items: abstract syntax of symbol maps, i.e. human-readable
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose presentations of signature morphisms.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose * sublogics: sublogics of the given logic. This type might be a
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose record of Boolean flags, indicating whether some feature is
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose present in the sublogi of not.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose * proof_tree: proof trees.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose J. A. Goguen and R. M. Burstall
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Institutions: Abstract Model Theory for Specification and
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose JACM 39, p. 95-146, 1992
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose (general notion of logic - model theory only)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose General Logics
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Logic Colloquium 87, p. 275-329, North Holland, 1989
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose (general notion of logic - also proof theory;
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose notion of logic representation, called map there)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose T. Mossakowski:
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Specification in an arbitrary institution with symbols
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose 14th WADT 1999, LNCS 1827, p. 252-270
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose (treatment of symbols and raw symbols, see also CASL semantics
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose in the CASL reference manual)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose T. Mossakowski, B. Klin:
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Institution Independent Static Analysis for CASL
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose 15h WADT 2001, LNCS 2267, p. 221-237, 2002.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose (what is needed for static anaylsis)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose S. Autexier and T. Mossakowski
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Integrating HOLCASL into the Development Graph Manager MAYA
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose FroCoS 2002, LNCS 2309, p. 2-17, 2002.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose (interface to provers)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose CoFI (ed.): CASL Reference Manual, LNCS 2960, Springer Verlag, 2004.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose (static semantics of CASL structured and architectural specifications)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose T. Mossakowski
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Heterogeneous specification and the heterogeneous tool set
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Habilitation thesis, University of Bremen, 2005
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose (the general picture of heterogeneous specification)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseimport qualified Data.Set as Set
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseimport qualified Data.Map as Map
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseimport qualified Data.Graph.Inductive.Graph as Graph
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseimport Logic.Prover (Prover, ConsChecker, Theory(..))
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseimport Common.ATerm.Lib (ShATermConvertible)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseimport Taxonomy.MMiSSOntology (MMiSSOntology)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-- | Stability of logic implementations
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bosedata Stability = Stable | Testing | Unstable | Experimental
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose deriving (Eq, Show)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-- | shortcut for class constraints
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseclass (Show a, Pretty a, Typeable a, ShATermConvertible a)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose => PrintTypeConv a
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-- | shortcut for class constraints with equality
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseclass (Eq a, PrintTypeConv a) => EqPrintTypeConv a
42604cc8d11743febf5aa892cb3a7d3c32bfed48Lukas Slebodnikinstance (Show a, Pretty a, Typeable a,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ShATermConvertible a) => PrintTypeConv a
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseinstance (Eq a, PrintTypeConv a) => EqPrintTypeConv a
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-- | maps from a to a
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bosetype EndoMap a = Map.Map a a
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose{- | the name of a logic.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Define instances like "data CASL = CASL deriving Show"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseclass Show lid => Language lid where
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose language_name :: lid -> String
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose language_name i = show i
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose description :: lid -> String
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- default implementation
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose description _ = "No description available"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose{- | Categories are given as usual: objects, morphisms, identities,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose domain, codomain and composition. The type id is the name, or
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose the identity of the category. It is an argument to all functions
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose of the type class, serving disambiguation among instances
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose (via the functional dependency lid -> object morphism).
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose The types for objects and morphisms may be restricted to
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose subtypes, using legal_obj and legal_mor. For example, for the
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose category of sets and injective maps, legal_mor would check
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose injectivity. Since Eq is a subclass of Category, it is also
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose possible to impose a quotient on the types for objects and morphisms.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseclass (Eq object, Eq morphism)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose => Category object morphism | morphism -> object where
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | identity morphisms
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ide :: object -> morphism
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | composition, in diagrammatic order
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose comp :: morphism -> morphism -> Result morphism
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | domain and codomain of morphisms
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose dom, cod :: morphism -> object
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | test if the signature morphism an inclusion
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose isInclusion :: morphism -> Bool
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose isInclusion _ = False -- in general no inclusion
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | is a value of type morphism denoting a legal morphism?
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose legal_mor :: morphism -> Bool
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseinstance Eq sign => Category sign (DefaultMorphism sign) where
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose dom = domOfDefaultMorphism
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose cod = codOfDefaultMorphism
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ide = ideOfDefaultMorphism
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose isInclusion = isInclusionDefaultMorphism
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose comp = compOfDefaultMorphism
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose legal_mor = legalDefaultMorphism (const True)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose{- | Abstract syntax, parsing and printing.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose There are three types for abstract syntax:
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose basic_spec is for basic specifications (see CASL RefMan p. 5ff.),
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose symb_items is for symbol lists (see CASL RefMan p. 35ff.),
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose symb_map_items is for symbol maps (see CASL RefMan p. 35ff.).
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseclass (Language lid, PrintTypeConv basic_spec,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose EqPrintTypeConv symb_items,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose EqPrintTypeConv symb_map_items)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose => Syntax lid basic_spec symb_items symb_map_items
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose | lid -> basic_spec symb_items symb_map_items
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | parser for basic specifications
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose parse_basic_spec :: lid -> Maybe(AParser st basic_spec)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | parser for symbol lists
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose parse_symb_items :: lid -> Maybe(AParser st symb_items)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | parser for symbol maps
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose parse_symb_map_items :: lid -> Maybe(AParser st symb_map_items)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- default implementations
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose parse_basic_spec _ = Nothing
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose parse_symb_items _ = Nothing
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose parse_symb_map_items _ = Nothing
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose{- | Sentences, provers and symbols.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Provers capture the entailment relation between sets of sentences
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek and sentences. They may return proof trees witnessing proofs.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Signatures are equipped with underlying sets of symbols
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose (such that the category of signatures becomes a concrete category),
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose see CASL RefMan p. 191ff.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseclass (Language lid, Category sign morphism, Ord sentence,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Ord symbol, -- for efficient lookup
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose PrintTypeConv sign, PrintTypeConv morphism,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose PrintTypeConv sentence, PrintTypeConv symbol)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose => Sentences lid sentence sign morphism symbol
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose | lid -> sentence sign morphism symbol
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ----------------------- sentences ---------------------------
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | check whether a sentence belongs to a signature
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose is_of_sign :: lid -> sentence -> signature -> Bool
544a20de7667f05c1a406c4dea0706b0ab507430Sumit Bose is_of_sign l _ _ = error $ statErrMsg l "is_of_sign"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | sentence translation along a signature morphism
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose map_sen :: lid -> morphism -> sentence -> Result sentence
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose map_sen l _ _ = statErr l "map_sen"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | simplification of sentences (leave out qualifications)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose simplify_sen :: lid -> sign -> sentence -> sentence
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose simplify_sen _ _ = id -- default implementation
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | parsing of sentences
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose parse_sentence :: lid -> Maybe (AParser st sentence)
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek parse_sentence _ = Nothing
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek -- | print a sentence with comments
544a20de7667f05c1a406c4dea0706b0ab507430Sumit Bose print_named :: lid -> Named sentence -> Doc
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose print_named _ = printAnnoted (addBullet . pretty) . fromLabelledSen
544a20de7667f05c1a406c4dea0706b0ab507430Sumit Bose ----------------------- symbols ---------------------------
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | set of symbols for a signature
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sym_of :: lid -> sign -> Set.Set symbol
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | symbol map for a signature morphism
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose symmap_of :: lid -> morphism -> EndoMap symbol
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose symmap_of _ _ = Map.empty
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | symbols have a name, see CASL RefMan p. 192
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sym_name :: lid -> symbol -> Id
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sym_name l _ = error $ statErrMsg l "sym_name"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-- | a dummy static analysis function to allow type checking *.inline.hs files
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseinlineAxioms :: StaticAnalysis lid
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose basic_spec sentence symb_items symb_map_items
544a20de7667f05c1a406c4dea0706b0ab507430Sumit Bose sign morphism symbol raw_symbol => lid -> String -> [Named sentence]
544a20de7667f05c1a406c4dea0706b0ab507430Sumit BoseinlineAxioms _ _ = error "inlineAxioms"
544a20de7667f05c1a406c4dea0706b0ab507430Sumit Bose-- | fail function for static analysis
544a20de7667f05c1a406c4dea0706b0ab507430Sumit BosestatErr :: (Language lid, Monad m) => lid -> String -> m a
544a20de7667f05c1a406c4dea0706b0ab507430Sumit BosestatErr lid = fail . statErrMsg lid
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-- | error message for static analysis
544a20de7667f05c1a406c4dea0706b0ab507430Sumit BosestatErrMsg :: (Language lid) => lid -> String -> String
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BosestatErrMsg lid str = "Logic." ++ str ++ " nyi for: " ++ language_name lid
544a20de7667f05c1a406c4dea0706b0ab507430Sumit Bose{- static analysis
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose This type class provides the data needed for an institution with symbols,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose as explained in the structured specification semantics in the CASL
544a20de7667f05c1a406c4dea0706b0ab507430Sumit Bose reference manual, chapter III.4.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose The static analysis computes signatures from basic specifications,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose and signature morphisms from symbol lists and symbol maps. The latter
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose needs an intermediate stage, so-called raw symbols, which are possibly
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose unqualified symbols. Normal symbols are always fully qualified.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose In the CASL reference manual, our symbols are called "signature symbols",
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose and our raw symbols are called "symbols". (Terminology should be adapted.)
544a20de7667f05c1a406c4dea0706b0ab507430Sumit Boseclass ( Syntax lid basic_spec symb_items symb_map_items
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose , Sentences lid sentence sign morphism symbol
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose , Ord raw_symbol, Pretty raw_symbol, Typeable raw_symbol)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose => StaticAnalysis lid
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose basic_spec sentence symb_items symb_map_items
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sign morphism symbol raw_symbol
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose | lid -> basic_spec sentence symb_items symb_map_items
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sign morphism symbol raw_symbol
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ----------------------- static analysis ---------------------------
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose {- | static analysis of basic specifications and symbol maps.
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek The resulting bspec has analyzed axioms in it.
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek The resulting sign is an extension of the input sign
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek plus newly declared or redeclared symbols.
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek See CASL RefMan p. 138 ff. -}
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek basic_analysis :: lid ->
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek Maybe((basic_spec, -- abstract syntax tree
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek sign, -- input signature, for the local
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek -- environment, carrying the previously
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek -- declared symbols
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose GlobalAnnos) -> -- global annotations
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Result (basic_spec, ExtSign sign symbol
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose , [Named sentence]))
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- default implementation
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose basic_analysis _ = Nothing
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | one-sided inverse for static analysis
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sign_to_basic_spec :: lid -> sign -> [Named sentence] -> basic_spec
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sign_to_basic_spec l _ _ = error $ statErrMsg l "sign_to_basic_spec"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | static analysis of symbol maps, see CASL RefMan p. 222f.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose stat_symb_map_items ::
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose lid -> [symb_map_items] -> Result (EndoMap raw_symbol)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose stat_symb_map_items l _ = statErr l "stat_symb_map_items"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | static analysis of symbol lists, see CASL RefMan p. 221f.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose stat_symb_items :: lid -> [symb_items] -> Result [raw_symbol]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose stat_symb_items l _ = statErr l "stat_symb_items"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ------------------------- amalgamation ---------------------------
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose {- | Computation of colimits of signature diagram.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Indeed, it suffices to compute a coconce that is weakly amalgamable
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose see Till Mossakowski,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Heterogeneous specification and the heterogeneous tool set
de8815aba87d08b6b7ac5d502dcb1755787e0857Jakub Hrozek weakly_amalgamable_colimit :: lid -> Tree.Gr sign (Int, morphism)
de8815aba87d08b6b7ac5d502dcb1755787e0857Jakub Hrozek -> Result (sign, Map.Map Int morphism)
de8815aba87d08b6b7ac5d502dcb1755787e0857Jakub Hrozek weakly_amalgamable_colimit l diag = do
de8815aba87d08b6b7ac5d502dcb1755787e0857Jakub Hrozek (sig, sink) <- signature_colimit l diag
de8815aba87d08b6b7ac5d502dcb1755787e0857Jakub Hrozek amalgCheck <- ensures_amalgamability l
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ([Cell, ColimitThinness], diag, Map.toList sink, Graph.empty)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose case amalgCheck of
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek NoAmalgamation s -> fail $ "failed amalgamability test " ++ s
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek DontKnow s -> fail $ "amalgamability test returns DontKnow: "++ s
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek _ -> return (sig, sink)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | architectural sharing analysis, see CASL RefMan p. 247ff.
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek ensures_amalgamability :: lid ->
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek ([CASLAmalgOpt], -- the program options
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek Tree.Gr sign (Int,morphism), -- the diagram to be analyzed
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose [(Int, morphism)], -- the sink
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Tree.Gr String String) -- the descriptions of nodes and edges
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -> Result Amalgamates
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ensures_amalgamability l _ = warning Amalgamates
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ("amalgamability test not implemented for logic " ++ show l)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | signature colimits
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose signature_colimit :: lid -> Tree.Gr sign (Int, morphism)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -> Result (sign, Map.Map Int morphism)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose signature_colimit l _ = fail
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ("signature colimits not implemented for logic " ++ show l)
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -------------------- symbols and raw symbols ---------------------
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose {- | Construe a symbol, like f:->t, as a raw symbol.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose This is a one-sided inverse to the function SymSySigSym
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose in the CASL RefMan p. 192. -}
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose symbol_to_raw :: lid -> symbol -> raw_symbol
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose symbol_to_raw l _ = error $ statErrMsg l "symbol_to_raw"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose {- | Construe an identifier, like f, as a raw symbol.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose See CASL RefMan p. 192, function IDAsSym -}
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose id_to_raw :: lid -> Id -> raw_symbol
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose id_to_raw l _ = error $ statErrMsg l "id_to_raw"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose {- | Check wether a symbol matches a raw symbol, for
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose example, f:s->t matches f. See CASL RefMan p. 192 -}
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose matches :: lid -> symbol -> raw_symbol -> Bool
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose matches l _ _ = error $ statErrMsg l "matches"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose --------------- operations on signatures and morphisms -----------
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | the empty (initial) signature, see CASL RefMan p. 193
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose empty_signature :: lid -> sign
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | union of signatures, see CASL RefMan p. 193
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek signature_union :: lid -> sign -> sign -> Result sign
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose signature_union l _ _ = statErr l "signature_union"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | intersection of signatures
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose intersection :: lid -> sign -> sign -> Result sign
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose intersection l _ _ = statErr l "intersection"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | final union of signatures, see CASL RefMan p. 194
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose final_union :: lid -> sign -> sign -> Result sign
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose final_union l _ _ = statErr l "final_union"
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek -- | union of signature morphims, see CASL RefMan p. 196
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose morphism_union :: lid -> morphism -> morphism -> Result morphism
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose morphism_union l _ _ = statErr l "morphism_union"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose {- | construct the inclusion morphisms between subsignatures,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose see CASL RefMan p. 194 -}
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose inclusion :: lid -> sign -> sign -> Result morphism
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose inclusion l _ _ = statErr l "inclusion"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose {- | the signature (co)generated by a set of symbols in another
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose signature is the smallest (largest) signature containing
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose (excluding) the set of symbols. Needed for revealing and
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose hiding, see CASL RefMan p. 197ff. -}
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose generated_sign, cogenerated_sign ::
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose lid -> Set.Set symbol -> sign -> Result morphism
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose generated_sign l _ _ = statErr l "generated_sign"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose cogenerated_sign l _ _ = statErr l "cogenerated_sign"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose {- | Induce a signature morphism from a source signature and
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose a raw symbol map. Needed for translation (SP with SM).
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose See CASL RefMan p. 198 -}
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose induced_from_morphism ::
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose lid -> EndoMap raw_symbol -> sign -> Result morphism
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose induced_from_morphism l _ _ = statErr l "induced_from_morphism"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose {- | Induce a signature morphism between two signatures by a
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose raw symbol map. Needed for instantiation and views.
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek See CASL RefMan p. 198f. -}
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozek induced_from_to_morphism ::
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose lid -> EndoMap raw_symbol -> ExtSign sign symbol
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -> ExtSign sign symbol -> Result morphism
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose induced_from_to_morphism l _ _ _ =
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose statErr l "induced_from_to_morphism"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose {- | Check whether a signature morphism is transportable.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose See CASL RefMan p. 304f. -}
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose is_transportable :: lid -> morphism -> Bool
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose is_transportable _ _ = False -- safe default
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose {- | Check whether the underlying symbol map of a signature morphism
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose is injective -}
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose is_injective :: lid -> morphism -> Bool
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose is_injective _ _ = False -- safe default
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ------------------- generate taxonomy from theory ----------------
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | generate an ontological taxonomy, if this makes sense
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose theory_to_taxonomy :: lid
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -> TaxoGraphKind
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -> MMiSSOntology
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -> sign -> [Named sentence]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -> Result MMiSSOntology
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose theory_to_taxonomy l _ _ _ _ = statErr l "theory_to_taxonomy"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-- | subsignatures, see CASL RefMan p. 194
45e11be651dbd3855a35de4abd2922e5b9d4b963Jakub Hrozekis_subsig :: StaticAnalysis lid
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose basic_spec sentence symb_items symb_map_items
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sign morphism symbol raw_symbol => lid -> sign -> sign -> Bool
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseis_subsig lid s = maybe False (const True) . maybeResult . inclusion lid s
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose{- | semi lattices with top (needed for sublogics). Note that `Ord` is
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseonly used for efficiency and is not related to the /partial/ order given
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseby the lattice. Only `Eq` is used to define `isSubElem` -}
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseclass (Ord l, Show l) => SemiLatticeWithTop l where
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose join :: l -> l -> l
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseinstance SemiLatticeWithTop () where
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose join _ _ = ()
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-- | less or equal for semi lattices
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseisSubElem :: SemiLatticeWithTop l => l -> l -> Bool
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseisSubElem a b = join a b == b
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-- | class providing the minimal sublogic of an item
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseclass MinSublogic sublogic item where
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose minSublogic :: item -> sublogic
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-- | a default instance for no sublogics
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseinstance MinSublogic () a where
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose minSublogic _ = ()
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-- | class providing also the projection of an item to a sublogic
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseclass MinSublogic sublogic item => ProjectSublogic sublogic item where
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose projectSublogic :: sublogic -> item -> item
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-- | a default instance for no sublogics
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseinstance ProjectSublogic () b where
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose projectSublogic _ = id
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-- | like ProjectSublogic, but providing a partial projection
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseclass MinSublogic sublogic item => ProjectSublogicM sublogic item where
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose projectSublogicM :: sublogic -> item -> Maybe item
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-- | a default instance for no sublogics
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseinstance ProjectSublogicM () b where
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose projectSublogicM _ = Just
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-- | class for providing a list of sublogic names
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseclass Sublogics l where
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sublogic_names :: l -> [String]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseinstance Sublogics () where
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sublogic_names () = [""]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose{- Type class logic. The central type class of Hets, providing the
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose interface for logics. This type class is instantiated for many logics,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose and it is used for the logic independent parts of Hets.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose It hence provides an sbatraction barrier between logic specific and
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose logic indepdendent code.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose This type class extends the class StaticAnalysis by a sublogic mechanism.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose Sublogics are important since they avoid the need to provide an own
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose instance of the class logic for each sublogic. Instead, the sublogic
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose can use the datastructures and operations of the main logic, and
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose functions are provided to test whether a given item lies within the
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sublogic. Also, projection functions from a super-logic to a sublogic
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose are provided.
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseclass (StaticAnalysis lid
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose basic_spec sentence symb_items symb_map_items
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sign morphism symbol raw_symbol,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose SemiLatticeWithTop sublogics,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose MinSublogic sublogics sentence,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ProjectSublogic sublogics basic_spec,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ProjectSublogicM sublogics symb_items,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ProjectSublogicM sublogics symb_map_items,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ProjectSublogic sublogics sign,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ProjectSublogic sublogics morphism,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ProjectSublogicM sublogics symbol,
d86224608ff60ec5cc7e7cbf9e53d8a04e083530Sumit Bose Typeable sublogics,
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Bose ShATermConvertible sublogics,
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Bose Sublogics sublogics,
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Bose Eq proof_tree, Show proof_tree, ShATermConvertible proof_tree,
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Bose Ord proof_tree, Typeable proof_tree)
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Bose => Logic lid sublogics
d86224608ff60ec5cc7e7cbf9e53d8a04e083530Sumit Bose basic_spec sentence symb_items symb_map_items
d86224608ff60ec5cc7e7cbf9e53d8a04e083530Sumit Bose sign morphism symbol raw_symbol proof_tree
2b62d5a414b8b7dba4f714dc5033e28dc4b1f4feJakub Hrozek | lid -> sublogics
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose basic_spec sentence symb_items symb_map_items
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sign morphism symbol raw_symbol proof_tree
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | stability of the implementation
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose stability :: lid -> Stability
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose stability _ = Experimental
2b62d5a414b8b7dba4f714dc5033e28dc4b1f4feJakub Hrozek -- | for a process logic, return its data logic
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose data_logic :: lid -> Maybe AnyLogic
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose data_logic _ = Nothing
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | the top sublogic, corresponding to the whole logic
3649b959709f1ab187092f054d4aace0798c98faSumit Bose top_sublogic :: lid -> sublogics
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose top_sublogic _ = top
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | list all the sublogics of the current logic
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose all_sublogics :: lid -> [sublogics]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose all_sublogics li = [top_sublogic li]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose {- | provide the embedding of a projected signature into the
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose original signature -}
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose proj_sublogic_epsilon :: lid -> sublogics -> sign -> morphism
3649b959709f1ab187092f054d4aace0798c98faSumit Bose proj_sublogic_epsilon _ _ s = ide s
3649b959709f1ab187092f054d4aace0798c98faSumit Bose ----------------------- provers ---------------------------
3649b959709f1ab187092f054d4aace0798c98faSumit Bose -- | several provers can be provided. See module "Logic.Prover"
3649b959709f1ab187092f054d4aace0798c98faSumit Bose provers :: lid -> [Prover sign sentence sublogics proof_tree]
3649b959709f1ab187092f054d4aace0798c98faSumit Bose provers _ = [] -- default implementation
3649b959709f1ab187092f054d4aace0798c98faSumit Bose -- | consistency checkers
3649b959709f1ab187092f054d4aace0798c98faSumit Bose cons_checkers :: lid
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -> [ConsChecker sign sentence
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sublogics morphism proof_tree]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose cons_checkers _ = [] -- default implementation
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- | conservativity checkers
d86224608ff60ec5cc7e7cbf9e53d8a04e083530Sumit Bose conservativityCheck :: lid -> (sign, [Named sentence]) ->
d86224608ff60ec5cc7e7cbf9e53d8a04e083530Sumit Bose morphism -> [Named sentence]
d86224608ff60ec5cc7e7cbf9e53d8a04e083530Sumit Bose -> Result (Maybe ConsistencyStatus)
d86224608ff60ec5cc7e7cbf9e53d8a04e083530Sumit Bose -- -> Result (Maybe Bool)
d86224608ff60ec5cc7e7cbf9e53d8a04e083530Sumit Bose conservativityCheck l _ _ _ = statErr l "conservativityCheck"
d86224608ff60ec5cc7e7cbf9e53d8a04e083530Sumit Bose -- | the empty proof tree
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Bose empty_proof_tree :: lid -> proof_tree
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Bose empty_proof_tree l = error $ statErrMsg l "empty_proof_tree"
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Bose----------------------------------------------------------------
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Bose-- Derived functions
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Bose----------------------------------------------------------------
d86224608ff60ec5cc7e7cbf9e53d8a04e083530Sumit Bose-- | the empty theory
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Boseempty_theory :: StaticAnalysis lid
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Bose basic_spec sentence symb_items symb_map_items
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Bose sign morphism symbol raw_symbol =>
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Bose lid -> Theory sign sentence proof_tree
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Boseempty_theory lid = Theory (empty_signature lid) Map.empty
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Bose----------------------------------------------------------------
71cd9f98150577224559bdc12c53c01ce6f2c3d9Sumit Bose-- Existential type covering any logic
d86224608ff60ec5cc7e7cbf9e53d8a04e083530Sumit Bose----------------------------------------------------------------
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-- | the disjoint union of all logics
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bosedata AnyLogic = forall lid sublogics