d657c51f14601d0235434ffb78cf6ac0f27cc83cLennart Poettering{-# OPTIONS -fallow-undecidable-instances #-}

220a21d38f675eb835f5758e3d23e896573aa5eaLennart Poettering{- |

4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay SieversModule : $Header$

4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay SieversDescription : central interface (type class) for logics in Hets

4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay SieversCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2006

4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay SieversLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay SieversMaintainer : till@tzi.de

4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay SieversStability : provisional

4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay SieversPortability : non-portable (various -fglasgow-exts extensions)

4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay Sievers

4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay SieversCentral interface (type class) for logics in Hets

4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay Sievers

4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay SieversProvides data structures for logics (with symbols). Logics are

71449cafa1f3aecad6fc755ae5e571eddf0bbd02Kay Sievers a type class with an /identity/ type (usually interpreted

4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay Sievers by a singleton set) which serves to treat logics as

4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay Sievers data. All the functions in the type class take the

4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay Sievers identity as first argument in order to determine the logic.

4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay Sievers

4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay Sievers For logic (co)morphisms see "Logic.Comorphism"

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering This module uses multiparameter type classes

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering (<http://haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#multi-param-type-classes>)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering with functional dependencies (<http://haskell.org/hawiki/FunDeps>)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering for defining an interface for the notion of logic. Multiparameter type

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering classes are needed because a logic consists of a collection of types,

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering together with operations on these. Functional dependencies

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering are needed because no operation will involve all types of

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering the multiparameter type class; hence we need a method to derive

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering the missing types. We chose an easy way: for each logic, we

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering introduce a new singleton type that constitutes the identity

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering of the logic. All other types of the multiparameter type class

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering depend on this 'identy constituting' type, and all operations take

71449cafa1f3aecad6fc755ae5e571eddf0bbd02Kay Sievers the 'identity constituting' type as first arguments. The value

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering of the argument of the 'identity constituting' type is irrelevant

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering (note that there is only one value of such a type anyway).

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering References:

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering J. A. Goguen and R. M. Burstall

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering Institutions: Abstract Model Theory for Specification and

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering Programming

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering JACM 39, p. 95--146, 1992

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering (general notion of logic - model theory only)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering J. Meseguer

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering General Logics

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering Logic Colloquium 87, p. 275--329, North Holland, 1989

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering (general notion of logic - also entailment\/proof theory;

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering notion of logic representation, called map there)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering T. Mossakowski:

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering Specification in an arbitrary institution with symbols

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering 14th WADT 1999, LNCS 1827, p. 252--270

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering (treatment of symbols and raw symbols, see also CASL semantics

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering in the CASL reference manual)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

cd14eda3212f9109c98a77cd5fee4168010d80daLennart Poettering T. Mossakowski, B. Klin:

cd14eda3212f9109c98a77cd5fee4168010d80daLennart Poettering Institution Independent Static Analysis for CASL

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

cd14eda3212f9109c98a77cd5fee4168010d80daLennart Poettering (what is needed for static anaylsis)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering S. Autexier and T. Mossakowski

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering Integrating HOLCASL into the Development Graph Manager MAYA

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering FroCoS 2002, LNCS 2309, p. 2-17, 2002.

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering (interface to provers)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering CoFI (ed.): CASL Reference Manual, LNCS 2960, Springer Verlag, 2004.

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering (static semantics of CASL structured and architectural specifications)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering T. Mossakowski

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering Heterogeneous specification and the heterogeneous tool set

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering Habilitation thesis, University of Bremen, 2005

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering (the general picture of heterogeneous specification)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering-}

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringmodule Logic.Logic where

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringimport Common.Id

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringimport Common.GlobalAnnotations

71449cafa1f3aecad6fc755ae5e571eddf0bbd02Kay Sieversimport qualified Common.Lib.Set as Set

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringimport qualified Common.Lib.Map as Map

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringimport Common.Lib.Graph as Tree

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringimport Common.AnnoState

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringimport Common.Result

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringimport Common.AS_Annotation

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringimport Common.Doc

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringimport Common.DocUtils

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringimport Logic.Prover -- for one half of class Sentences

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringimport Common.DynamicUtils

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringimport Common.ATerm.Lib -- (ShATermConvertible)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringimport ATC.DefaultMorphism()

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringimport Common.Amalgamate -- passed to ensures_amalgamability

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringimport Common.Taxonomy

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringimport Taxonomy.MMiSSOntology (MMiSSOntology)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering-- | Stability of logic implementations

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringdata Stability = Stable | Testing | Unstable | Experimental

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering deriving (Eq, Show)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering-- | shortcut for class constraints

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringclass (Show a, Pretty a, Typeable a, ShATermConvertible a)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering => PrintTypeConv a

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering-- | shortcut for class constraints with equality

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringclass (Eq a, PrintTypeConv a) => EqPrintTypeConv a

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringinstance (Show a, Pretty a, Typeable a,

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering ShATermConvertible a) => PrintTypeConv a

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringinstance (Eq a, PrintTypeConv a) => EqPrintTypeConv a

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering-- | maps from a to a

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringtype EndoMap a = Map.Map a a

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering{- | the name of a logic.

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering Define instances like "data CASL = CASL deriving Show"

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering-}

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringclass Show lid => Language lid where

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering language_name :: lid -> String

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering language_name i = show i

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering description :: lid -> String

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering -- default implementation

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering description _ = "No description available"

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering{- | Categories are given as usual: objects, morphisms, identities,

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering domain, codomain and composition. The type id is the name, or

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering the identity of the category. It is an argument to all functions

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering of the type class, serving disambiguation among instances

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering (via the functional dependency lid -> sign morphism).

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering The types for objects and morphisms may be restricted to

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering subtypes, using legal_obj and legal_mor. For example, for the

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering category of sets and injective maps, legal_mor would check

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering injectivity. Since Eq is a subclass of Category, it is also

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering possible to impose a quotient on the types for objects and morphisms.

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering-}

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringclass (Language lid, Eq sign, Eq morphism)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering => Category lid sign morphism | lid -> sign morphism where

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering -- | identity morphisms

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering ide :: lid -> sign -> morphism

71449cafa1f3aecad6fc755ae5e571eddf0bbd02Kay Sievers -- | composition, in diagrammatic order

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering comp :: lid -> morphism -> morphism -> Result morphism

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering -- | domain and codomain of morphisms

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering dom, cod :: lid -> morphism -> sign

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering -- | is a value of type sign denoting a legal signature?

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering legal_obj :: lid -> sign -> Bool

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering -- | is a value of type morphism denoting a legal signature morphism?

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering legal_mor :: lid -> morphism -> Bool

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering{- | Abstract syntax, parsing and printing.

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering There are three types for abstract syntax:

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering basic_spec is for basic specifications (see CASL RefMan p. 5ff.),

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering symb_items is for symbol lists (see CASL RefMan p. 35ff.),

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering symb_map_items is for symbol maps (see CASL RefMan p. 35ff.).

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering-}

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringclass (Language lid, PrintTypeConv basic_spec,

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering EqPrintTypeConv symb_items,

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering EqPrintTypeConv symb_map_items)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering => Syntax lid basic_spec symb_items symb_map_items

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering | lid -> basic_spec symb_items symb_map_items

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering where

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering -- | parser for basic specifications

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering parse_basic_spec :: lid -> Maybe(AParser st basic_spec)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering -- | parser for symbol lists

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering parse_symb_items :: lid -> Maybe(AParser st symb_items)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering -- | parser for symbol maps

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering parse_symb_map_items :: lid -> Maybe(AParser st symb_map_items)

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering -- default implementations

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering parse_basic_spec _ = Nothing

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering parse_symb_items _ = Nothing

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering parse_symb_map_items _ = Nothing

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering{- | Sentences, provers and symbols.

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering Provers capture the entailment relation between sets of sentences

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering and sentences. They may return proof trees witnessing proofs.

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering Signatures are equipped with underlying sets of symbols

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering (such that the category of signatures becomes a concrete category),

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering see CASL RefMan p. 191ff.

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering-}

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringclass (Category lid sign morphism, Ord sentence,

04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering Ord symbol, -- for efficient lookup

dc1d6c02fcf55bb7dac918d0ed3bd3e2a3d67525Lennart Poettering PrintTypeConv sign, PrintTypeConv morphism,

dc1d6c02fcf55bb7dac918d0ed3bd3e2a3d67525Lennart Poettering PrintTypeConv sentence, PrintTypeConv symbol,

dc1d6c02fcf55bb7dac918d0ed3bd3e2a3d67525Lennart Poettering Eq proof_tree, Show proof_tree, ShATermConvertible proof_tree,

dc1d6c02fcf55bb7dac918d0ed3bd3e2a3d67525Lennart Poettering Ord proof_tree, Typeable proof_tree)

dc1d6c02fcf55bb7dac918d0ed3bd3e2a3d67525Lennart Poettering => Sentences lid sentence proof_tree sign morphism symbol

dc1d6c02fcf55bb7dac918d0ed3bd3e2a3d67525Lennart Poettering | lid -> sentence proof_tree sign morphism symbol

dc1d6c02fcf55bb7dac918d0ed3bd3e2a3d67525Lennart Poettering where

dc1d6c02fcf55bb7dac918d0ed3bd3e2a3d67525Lennart Poettering

dc1d6c02fcf55bb7dac918d0ed3bd3e2a3d67525Lennart Poettering ----------------------- sentences ---------------------------

dc1d6c02fcf55bb7dac918d0ed3bd3e2a3d67525Lennart Poettering -- | sentence translation along a signature morphism

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering map_sen :: lid -> morphism -> sentence -> Result sentence

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering map_sen l _ _ = statErr l "map_sen"

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering -- | simplification of sentences (leave out qualifications)

69beda1f75070b36d0562e4050cd567bf2da5a87Kay Sievers simplify_sen :: lid -> sign -> sentence -> sentence

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering simplify_sen _ _ = id -- default implementation

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering -- | parsing of sentences

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering parse_sentence :: lid -> Maybe (AParser st sentence)

c9679c652b3c31f2510e8805d81630680ebc7e95Lennart Poettering parse_sentence _ = Nothing

c9679c652b3c31f2510e8805d81630680ebc7e95Lennart Poettering -- | print a sentence with comments

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering print_named :: lid -> Named sentence -> Doc

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering print_named _ = printAnnoted (addBullet . pretty) . fromLabelledSen

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering ----------------------- symbols ---------------------------

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering -- | set of symbols for a signature

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering sym_of :: lid -> sign -> Set.Set symbol

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering -- | symbol map for a signature morphism

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering symmap_of :: lid -> morphism -> EndoMap symbol

69beda1f75070b36d0562e4050cd567bf2da5a87Kay Sievers -- | symbols have a name, see CASL RefMan p. 192

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering sym_name :: lid -> symbol -> Id

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering

c9679c652b3c31f2510e8805d81630680ebc7e95Lennart Poettering ----------------------- provers ---------------------------

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

c9679c652b3c31f2510e8805d81630680ebc7e95Lennart Poettering provers :: lid -> [Prover sign sentence proof_tree]

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering provers _ = [] -- default implementation

69beda1f75070b36d0562e4050cd567bf2da5a87Kay Sievers -- | consistency checkers

69beda1f75070b36d0562e4050cd567bf2da5a87Kay Sievers cons_checkers :: lid -> [ConsChecker sign sentence morphism proof_tree]

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering cons_checkers _ = [] -- default implementation

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering -- | conservativity checkers

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering conservativityCheck :: lid -> (sign, [Named sentence]) ->

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering morphism -> [Named sentence] -> Result (Maybe Bool)

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering conservativityCheck l _ _ _ = statErr l "conservativityCheck"

499b604b21c02ee64c8590a76d7900d64d7a5cb7Zbigniew Jędrzejewski-Szmek -- | the empty proof tree

499b604b21c02ee64c8590a76d7900d64d7a5cb7Zbigniew Jędrzejewski-Szmek empty_proof_tree :: proof_tree

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering

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

6936cd8926b6935364874b3701e86fe823e8c4ceLennart PoetteringinlineAxioms :: StaticAnalysis lid

499b604b21c02ee64c8590a76d7900d64d7a5cb7Zbigniew Jędrzejewski-Szmek basic_spec sentence proof_tree symb_items symb_map_items

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering sign morphism symbol raw_symbol => lid -> String -> [Named sentence]

6936cd8926b6935364874b3701e86fe823e8c4ceLennart PoetteringinlineAxioms _ _ = error "inlineAxioms"

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering

499b604b21c02ee64c8590a76d7900d64d7a5cb7Zbigniew Jędrzejewski-Szmek-- error function for static analysis

6936cd8926b6935364874b3701e86fe823e8c4ceLennart PoetteringstatErr :: (Language lid, Monad m) => lid -> String -> m a

6936cd8926b6935364874b3701e86fe823e8c4ceLennart PoetteringstatErr lid str = fail ("Logic." ++ str ++ " nyi for: " ++ language_name lid)

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering{- static analysis

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering This type class provides the data needed for an institution with symbols,

499b604b21c02ee64c8590a76d7900d64d7a5cb7Zbigniew Jędrzejewski-Szmek as explained in the structured specification semantics in the CASL

499b604b21c02ee64c8590a76d7900d64d7a5cb7Zbigniew Jędrzejewski-Szmek reference manual, chapter III.4.

499b604b21c02ee64c8590a76d7900d64d7a5cb7Zbigniew Jędrzejewski-Szmek The static analysis computes signatures from basic specifications,

499b604b21c02ee64c8590a76d7900d64d7a5cb7Zbigniew Jędrzejewski-Szmek and signature morphisms from symbol lists and symbol maps. The latter

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering needs an intermediate stage, so-called raw symbols, which are possibly

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering unqualified symbols. Normal symbols are always fully qualified.

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering In the CASL reference manual, our symbols are called "signature symbols",

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering and our raw symbols are called "symbols". (Terminology should be adapted.)

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering-}

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poetteringclass ( Syntax lid basic_spec symb_items symb_map_items

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering , Sentences lid sentence proof_tree sign morphism symbol

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering , Ord raw_symbol, Pretty raw_symbol, Typeable raw_symbol)

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering => StaticAnalysis lid

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering basic_spec sentence proof_tree symb_items symb_map_items

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering sign morphism symbol raw_symbol

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering | lid -> basic_spec sentence proof_tree symb_items symb_map_items

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering sign morphism symbol raw_symbol

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering where

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering ----------------------- static analysis ---------------------------

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering {- | static analysis of basic specifications and symbol maps.

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering The resulting bspec has analyzed axioms in it.

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering The resulting sign is an extension of the input sign.

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering See CASL RefMan p. 138 ff. -}

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering basic_analysis :: lid ->

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering Maybe((basic_spec, -- abstract syntax tree

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering sign, -- input signature, for the local

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering -- environment, carrying the previously

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering -- declared symbols

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering GlobalAnnos) -> -- global annotations

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering Result (basic_spec, sign, [Named sentence]))

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering -- default implementation

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering basic_analysis _ = Nothing

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering -- | one-sided inverse for static analysis

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering sign_to_basic_spec :: lid -> sign -> [Named sentence] -> basic_spec

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

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering stat_symb_map_items ::

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering lid -> [symb_map_items] -> Result (EndoMap raw_symbol)

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering stat_symb_map_items l _ = statErr l "stat_symb_map_items"

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

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering stat_symb_items :: lid -> [symb_items] -> Result [raw_symbol]

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering stat_symb_items l _ = statErr l "stat_symb_items"

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering ------------------------- amalgamation ---------------------------

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering {- | Computation of colimits of signature diagram.

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering Indeed, it suffices to compute a coconce that is weakly amalgamable

68dd0956ef9d607e6ff9aea15883a2c290a33c2aTom Gundersen see Till Mossakowski,

68dd0956ef9d607e6ff9aea15883a2c290a33c2aTom Gundersen Heterogeneous specification and the heterogeneous tool set

68dd0956ef9d607e6ff9aea15883a2c290a33c2aTom Gundersen p. 25ff. -}

68dd0956ef9d607e6ff9aea15883a2c290a33c2aTom Gundersen weaklyAmalgamableCocone :: lid -> Tree.Gr sign morphism

68dd0956ef9d607e6ff9aea15883a2c290a33c2aTom Gundersen -> Result (sign, Map.Map Int morphism)

68dd0956ef9d607e6ff9aea15883a2c290a33c2aTom Gundersen weaklyAmalgamableCocone l _ = statErr l "weaklyAmalgamableCocone"

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering -- | architectural sharing analysis, see CASL RefMan p. 247ff.

499b604b21c02ee64c8590a76d7900d64d7a5cb7Zbigniew Jędrzejewski-Szmek ensures_amalgamability :: lid ->

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering ([CASLAmalgOpt], -- the program options

69beda1f75070b36d0562e4050cd567bf2da5a87Kay Sievers Tree.Gr sign morphism, -- the diagram to be analyzed

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering [(Int, morphism)], -- the sink

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering Tree.Gr String String) -- the descriptions of nodes and edges

8e7acf67b278e47cff0f849780365f8b1a824189Lennart Poettering -> Result Amalgamates

8e7acf67b278e47cff0f849780365f8b1a824189Lennart Poettering ensures_amalgamability l _ = statErr l "ensures_amalgamability"

8e7acf67b278e47cff0f849780365f8b1a824189Lennart Poettering

8e7acf67b278e47cff0f849780365f8b1a824189Lennart Poettering -------------------- symbols and raw symbols ---------------------

8e7acf67b278e47cff0f849780365f8b1a824189Lennart Poettering {- | Construe a symbol, like f:->t, as a raw symbol.

8e7acf67b278e47cff0f849780365f8b1a824189Lennart Poettering This is a one-sided inverse to the function SymSySigSym

8e7acf67b278e47cff0f849780365f8b1a824189Lennart Poettering in the CASL RefMan p. 192. -}

8e7acf67b278e47cff0f849780365f8b1a824189Lennart Poettering symbol_to_raw :: lid -> symbol -> raw_symbol

8e7acf67b278e47cff0f849780365f8b1a824189Lennart Poettering {- | Construe an identifier, like f, as a raw symbol.

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering See CASL RefMan p. 192, function IDAsSym -}

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering id_to_raw :: lid -> Id -> raw_symbol

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering {- | Check wether a symbol matches a raw symbol, for

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering example, f:s->t matches f. See CASL RefMan p. 192 -}

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering matches :: lid -> symbol -> raw_symbol -> Bool

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering --------------- operations on signatures and morphisms -----------

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

8e7acf67b278e47cff0f849780365f8b1a824189Lennart Poettering empty_signature :: lid -> sign

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

8e7acf67b278e47cff0f849780365f8b1a824189Lennart Poettering signature_union :: lid -> sign -> sign -> Result sign

8e7acf67b278e47cff0f849780365f8b1a824189Lennart Poettering signature_union l _ _ = statErr l "signature_union"

8e7acf67b278e47cff0f849780365f8b1a824189Lennart Poettering {- | Compute the difference of signatures. The first

8e7acf67b278e47cff0f849780365f8b1a824189Lennart Poettering signature must be an inclusion of the second. The resulting

8e7acf67b278e47cff0f849780365f8b1a824189Lennart Poettering signature might be an unclosed signature that should only be

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering used with care, though the following property should hold:

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering is_subsig s1 s2 => union s1 (difference s2 s1) = s2

8e7acf67b278e47cff0f849780365f8b1a824189Lennart Poettering (Unions are supposed to be symmetric and associative.) -}

6936cd8926b6935364874b3701e86fe823e8c4ceLennart Poettering signature_difference :: lid -> sign -> sign -> Result sign

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering signature_difference l _ _ = statErr l "signature_difference"

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering -- | subsignatures, see CASL RefMan p. 194

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering is_subsig :: lid -> sign -> sign -> Bool

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

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering final_union :: lid -> sign -> sign -> Result sign

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering final_union l _ _ = statErr l "final_union"

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

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering morphism_union :: lid -> morphism -> morphism -> Result morphism

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering morphism_union l _ _ = statErr l "morphism_union"

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering {- | construct the inclusion morphisms between subsignatures,

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering see CASL RefMan p. 194 -}

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering inclusion :: lid -> sign -> sign -> Result morphism

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering inclusion l _ _ = statErr l "inclusion"

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering {- | the signature (co)generated by a set of symbols in another

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering signature is the smallest (largest) signature containing

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering (excluding) the set of symbols. Needed for revealing and

499b604b21c02ee64c8590a76d7900d64d7a5cb7Zbigniew Jędrzejewski-Szmek hiding, see CASL RefMan p. 197ff. -}

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering generated_sign, cogenerated_sign ::

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering lid -> Set.Set symbol -> sign -> Result morphism

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering generated_sign l _ _ = statErr l "generated_sign"

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering cogenerated_sign l _ _ = statErr l "cogenerated_sign"

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering {- | Induce a signature morphism from a source signature and

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering a raw symbol map. Needed for translation (SP with SM).

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering See CASL RefMan p. 198 -}

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering induced_from_morphism ::

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering lid -> EndoMap raw_symbol -> sign -> Result morphism

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering induced_from_morphism l _ _ = statErr l "induced_from_morphism"

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering {- | Induce a signature morphism between two signatures by a

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering raw symbol map. Needed for instantiation and views.

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering See CASL RefMan p. 198f. -}

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering induced_from_to_morphism ::

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering lid -> EndoMap raw_symbol -> sign -> sign -> Result morphism

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering induced_from_to_morphism l _ _ _ =

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering statErr l "induced_from_to_morphism"

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering {- | Check whether a signature morphism is transportable.

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering See CASL RefMan p. 304f. -}

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering is_transportable :: lid -> morphism -> Bool

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering is_transportable _ _ = False -- safe default

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

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering is injective -}

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering is_injective :: lid -> morphism -> Bool

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering is_injective _ _ = False -- safe default

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering ------------------- generate taxonomy from theory ----------------

70a44afee385c4afadaab9a002b3f9dd44aedf4aJan Engelhardt -- | generate an ontological taxonomy, if this makes sense

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering theory_to_taxonomy :: lid

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering -> TaxoGraphKind

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering -> MMiSSOntology

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering -> sign -> [Named sentence]

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering -> Result MMiSSOntology

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering theory_to_taxonomy l _ _ _ _ = statErr l "theory_to_taxonomy"

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering-- | semi lattices with top (needed for sublogics)

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poetteringclass (Eq l, Show l) => SemiLatticeWithTop l where

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering join :: l -> l -> l

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering top :: l

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poetteringinstance SemiLatticeWithTop () where

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering join _ _ = ()

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering top = ()

b8bde11658366290521e3d03316378b482600323Jan Engelhardt

b8bde11658366290521e3d03316378b482600323Jan Engelhardt-- | less or equal for semi lattices

b8bde11658366290521e3d03316378b482600323Jan EngelhardtisSubElem :: SemiLatticeWithTop l => l -> l -> Bool

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart PoetteringisSubElem a b = join a b == b

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering-- | class providing the minimal sublogic of an item

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poetteringclass MinSublogic sublogic item where

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering minSublogic :: item -> sublogic

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering-- | a default instance for no sublogics

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poetteringinstance MinSublogic () a where

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering minSublogic _ = ()

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering{-

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poetteringinstance SemiLatticeWithTop s => MinSublogic s a where

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering minSublogic _ = top

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering-}

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering-- | class providing also the projection of an item to a sublogic

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poetteringclass MinSublogic sublogic item => ProjectSublogic sublogic item where

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering projectSublogic :: sublogic -> item -> item

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering-- | a default instance for no sublogics

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poetteringinstance ProjectSublogic () b where

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering projectSublogic _ = id

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering{-

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poetteringinstance MinSublogic a b => ProjectSublogic a b where

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering projectSublogic _ = id

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering-}

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering-- | like ProjectSublogic, but providing a partial projection

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poetteringclass MinSublogic sublogic item => ProjectSublogicM sublogic item where

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering projectSublogicM :: sublogic -> item -> Maybe item

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering

b8bde11658366290521e3d03316378b482600323Jan Engelhardt-- | a default instance for no sublogics

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poetteringinstance ProjectSublogicM () b where

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering projectSublogicM _ = Just

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering{-

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poetteringinstance (SemiLatticeWithTop a, MinSublogic a b) => ProjectSublogicM a b where

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering projectSublogicM l i = if isSubElem (minSublogic i) l

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering then Just i else Nothing

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering-}

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering-- | class for providing a list of sublogic names

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poetteringclass Sublogics l where

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering sublogic_names :: l -> [String]

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poetteringinstance Sublogics () where

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering sublogic_names () = [""]

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering{- Type class logic. The central type class of Hets, providing the

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering interface for logics. This type class is instantiated for many logics,

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering and it is used for the logic independent parts of Hets.

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering It hence provides an sbatraction barrier between logic specific and

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering logic indepdendent code.

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering This type class extends the class StaticAnalysis by a sublogic mechanism.

b8bde11658366290521e3d03316378b482600323Jan Engelhardt Sublogics are important since they avoid the need to provide an own

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering instance of the class logic for each sublogic. Instead, the sublogic

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering can use the datastructures and operations of the main logic, and

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering functions are provided to test whether a given item lies within the

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering sublogic. Also, projection functions from a super-logic to a sublogic

b8bde11658366290521e3d03316378b482600323Jan Engelhardt are provided.

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering-}

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poetteringclass (StaticAnalysis lid

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering basic_spec sentence proof_tree symb_items symb_map_items

d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan Engelhardt sign morphism symbol raw_symbol,

d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan Engelhardt SemiLatticeWithTop sublogics,

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering MinSublogic sublogics sentence,

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering ProjectSublogic sublogics basic_spec,

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering ProjectSublogicM sublogics symb_items,

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering ProjectSublogicM sublogics symb_map_items,

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering ProjectSublogic sublogics sign,

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering ProjectSublogic sublogics morphism,

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering ProjectSublogicM sublogics symbol,

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering Typeable sublogics,

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering ShATermConvertible sublogics,

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering Sublogics sublogics)

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering => Logic lid sublogics

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering basic_spec sentence symb_items symb_map_items

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering sign morphism symbol raw_symbol proof_tree

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering | lid -> sublogics

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering basic_spec sentence symb_items symb_map_items

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering sign morphism symbol raw_symbol proof_tree

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering where

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering -- | stability of the implementation

51c61cda1a542c9e999bfdc6aab4a029c0ae7f5aLennart Poettering stability :: lid -> Stability

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering -- default

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering stability _ = Experimental

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering -- | for a process logic, return its data logic

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering data_logic :: lid -> Maybe AnyLogic

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering data_logic _ = Nothing

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering -- | the top sublogic, corresponding to the whole logic

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering top_sublogic :: lid -> sublogics

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering top_sublogic _ = top

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering -- | list all the sublogics of the current logic

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering all_sublogics :: lid -> [sublogics]

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering all_sublogics li = [top_sublogic li]

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering {- | provide the embedding of a projected signature into the

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering original signature -}

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

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering proj_sublogic_epsilon li _ s = ide li s

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering----------------------------------------------------------------

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering-- Derived functions

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering----------------------------------------------------------------

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering-- | the empty theory

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poetteringempty_theory :: StaticAnalysis lid

22e7062d749c69d7edfcd52ef7cc6ec005e862d5David Herrmann basic_spec sentence proof_tree symb_items symb_map_items

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering sign morphism symbol raw_symbol =>

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering lid -> Theory sign sentence proof_tree

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poetteringempty_theory lid = Theory (empty_signature lid) Map.empty

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering----------------------------------------------------------------

b8bde11658366290521e3d03316378b482600323Jan Engelhardt-- Existential type covering any logic

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering----------------------------------------------------------------

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering-- | the disjoint union of all logics

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poetteringdata AnyLogic = forall lid sublogics

b8bde11658366290521e3d03316378b482600323Jan Engelhardt basic_spec sentence symb_items symb_map_items

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering sign morphism symbol raw_symbol proof_tree .

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering Logic lid sublogics

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering basic_spec sentence symb_items symb_map_items

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering sign morphism symbol raw_symbol proof_tree =>

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering Logic lid

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poetteringinstance Show AnyLogic where

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering show (Logic lid) = language_name lid

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poetteringinstance Eq AnyLogic where

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering Logic lid1 == Logic lid2 = language_name lid1 == language_name lid2

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering

699b6b3491dc265ead79602404ad67ccdacae302Lennart PoetteringtyconAnyLogic :: TyCon

499b604b21c02ee64c8590a76d7900d64d7a5cb7Zbigniew Jędrzejewski-SzmektyconAnyLogic = mkTyCon "Logic.Logic.AnyLogic"

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poetteringinstance Typeable AnyLogic where

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering typeOf _ = mkTyConApp tyconAnyLogic []

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering{- class hierarchy:

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering Language

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering __________/

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering Category

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering | /

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering Sentences Syntax

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering \ /

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering StaticAnalysis (no sublogics)

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering \

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering \

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering Logic

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering-}

699b6b3491dc265ead79602404ad67ccdacae302Lennart Poettering