f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich{-# OPTIONS -fallow-undecidable-instances #-}

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder{- |

c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2003

fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan PascanuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : till@tzi.de

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiStability : provisional

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiPortability : non-portable (various -fglasgow-exts extensions)

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederProvides data structures for logics (with symbols). Logics are

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder a type class with an /identity/ type (usually interpreted

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder by a singleton set) which serves to treat logics as

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder data. All the functions in the type class take the

da955132262baab309a50fdffe228c9efe68251dCui Jian identity as first argument in order to determine the logic.

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder For logic (co)morphisms see "Logic.Comorphism"

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder This module uses multiparameter type classes

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder (<http://haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#multi-param-type-classes>)

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder with functional dependencies (<http://haskell.org/hawiki/FunDeps>)

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder for defining an interface for the notion of logic. Multiparameter type

4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maeder classes are needed because a logic consists of a collection of types,

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder together with operations on these. Functional dependencies

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder are needed because no operation will involve all types of

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

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski the missing types. We chose an easy way: for each logic, we

c4451dc7da4a15726ba96179aecf046a5df5cae1Christian Maeder introduce a new singleton type that constitutes the identity

3c4e64e0b4361a24275ee8f308fa965ab1e52f2eHeng Jiang of the logic. All other types of the multiparameter type class

fa388aea9cef5f9734fec346159899a74432ce26Christian Maeder depend on this 'identy constituting' type, and all operations take

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder the 'identity constituting' type as first arguments. The value

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maeder of the argument of the 'identity constituting' type is irrelevant

59fddbdd745a05adeaf655b617ab8da947903832Christian Maeder (note that there is only one value of such a type anyway).

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maeder

cfaa17b0d2ed0a663f0a4f18b23f98ab876c2f40Christian Maeder References:

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder J. A. Goguen and R. M. Burstall

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder Institutions: Abstract Model Theory for Specification and

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder Programming

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder JACM 39, p. 95--146, 1992

da333ffa6336cf59a4071fcddad358c5eafd3e61Sonja Gröning (general notion of logic - model theory only)

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder

5b50a0fb9834540caf04471389df975fbd356ca3Razvan Pascanu J. Meseguer

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu General Logics

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

124c859ba4741d5e36d5d98634886b430b7af093Christian Maeder (general notion of logic - also proof theory;

66a774f13272fde036481edd2298081ab3d04678Razvan Pascanu notion of logic representation, called map there)

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maeder

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maeder T. Mossakowski:

923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl Specification in an arbitrary institution with symbols

923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl 14th WADT 1999, LNCS 1827, p. 252--270

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder (treatment of symbols and raw symbols, see also CASL semantics)

74885352ea11b26253d453af28dc904dadc4d530Christian Maeder

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maeder T. Mossakowski, B. Klin:

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maeder Institution Independent Static Analysis for CASL

44e2af9d1df92a39d25ac439c00c338e0ed5652bChristian Maeder 15h WADT 2001, LNCS 2267, p. 221-237, 2002.

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (what is needed for static anaylsis)

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder S. Autexier and T. Mossakowski

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Integrating HOLCASL into the Development Graph Manager MAYA

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder FroCoS 2002, to appear

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (interface to provers)

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Todo:

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ATerm, XML

8955ea64c61a6e8b96b7696021863afd1a75f6daRazvan Pascanu Weak amalgamability

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Metavars

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder raw symbols are now symbols, symbols are now signature symbols

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder provide both signature symbol set and symbol set of a signature

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder introduce coercion safer functions (separately for each type)

fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu-}

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maedermodule Logic.Logic where

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maeder

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maederimport Common.Id

fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanuimport Common.GlobalAnnotations

fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanuimport qualified Common.Lib.Set as Set

ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühlimport qualified Common.Lib.Map as Map

ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühlimport qualified Data.Graph.Inductive.Tree as Tree(Gr)

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport Data.Graph.Inductive.Graph(Node)

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport Common.Lib.Pretty

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport Common.AnnoState

c0c2380bced8159ff0297ece14eba948bd236471Christian Maederimport Common.Result

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport Common.AS_Annotation

c0c2380bced8159ff0297ece14eba948bd236471Christian Maederimport Common.Print_AS_Annotation

c4451dc7da4a15726ba96179aecf046a5df5cae1Christian Maederimport Logic.Prover -- for one half of class Sentences

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport Common.PrettyPrint

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

fa388aea9cef5f9734fec346159899a74432ce26Christian Maederimport Data.Dynamic

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maederimport Common.DynamicUtils

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maeder-- for Conversion to ATerms

63719301448519453f66383f4e583d9fd5b89ecbChristian Maederimport Common.ATerm.Lib -- (ShATermConvertible)

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- passed to ensures_amalgamability

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport Common.Amalgamate

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport Common.Taxonomy

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maederimport Taxonomy.MMiSSOntology (MMiSSOntology)

923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | shortcut for class constraints

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maederclass (Show a, PrettyPrint a, PrintLaTeX a, Typeable a, ShATermConvertible a)

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder => PrintTypeConv a

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | shortcut for class constraints with equality

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederclass (Eq a, PrintTypeConv a) => EqPrintTypeConv a

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maederinstance (Show a, PrettyPrint a, PrintLaTeX a, Typeable a,

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ShATermConvertible a) => PrintTypeConv a

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederinstance (Eq a, PrintTypeConv a) => EqPrintTypeConv a

f1dec6898638ba1131a9fadbc4d1544c93dfabb0Klaus Luettich

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maedertype EndoMap a = Map.Map a a

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- languages, define like "data CASL = CASL deriving Show"

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder

class Show lid => Language lid where

language_name :: lid -> String

language_name i = show i

description :: lid -> String

-- default implementation

description _ = "No description available"

-- Categories are given by a quotient,

-- i.e. we need equality

-- Should we allow arbitrary composition graphs and build paths?

class (Language lid, Eq sign, Eq morphism)

=> Category lid sign morphism | lid -> sign morphism where

ide :: lid -> sign -> morphism

comp :: lid -> morphism -> morphism -> Result morphism

-- diagrammatic order

dom, cod :: lid -> morphism -> sign

legal_obj :: lid -> sign -> Bool

legal_mor :: lid -> morphism -> Bool

-- abstract syntax, parsing and printing

class (Language lid, PrintTypeConv basic_spec,

EqPrintTypeConv symb_items,

EqPrintTypeConv symb_map_items)

=> Syntax lid basic_spec symb_items symb_map_items

| lid -> basic_spec symb_items symb_map_items

where

-- parsing

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

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

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

-- default implementations

parse_basic_spec _ = Nothing

parse_symb_items _ = Nothing

parse_symb_map_items _ = Nothing

-- sentences (plus prover stuff and "symbol" with "Ord" for efficient lookup)

class (Category lid sign morphism, Ord sentence,

Ord symbol,

PrintTypeConv sign, PrintTypeConv morphism,

PrintTypeConv sentence, PrintTypeConv symbol,

Eq proof_tree, Show proof_tree, ShATermConvertible proof_tree,

Typeable proof_tree)

=> Sentences lid sentence proof_tree sign morphism symbol

| lid -> sentence proof_tree sign morphism symbol

where

-- sentence translation

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

map_sen l _ _ = statErr l "map_sen"

-- simplification of sentences (leave out qualifications)

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

simplify_sen _ _ = id -- default implementation

-- parsing of sentences

parse_sentence :: lid -> Maybe (AParser st sentence)

parse_sentence _ = Nothing

-- print a sentence with comments

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

print_named _ = printLabelledSen

sym_of :: lid -> sign -> Set.Set symbol

symmap_of :: lid -> morphism -> EndoMap symbol

sym_name :: lid -> symbol -> Id

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

provers _ = []

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

cons_checkers _ = []

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

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

conservativityCheck l _ _ _ = statErr l "conservativityCheck"

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

inlineAxioms :: StaticAnalysis lid

basic_spec sentence proof_tree symb_items symb_map_items

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

inlineAxioms _ _ = error "inlineAxioms"

-- static analysis

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

statErr lid str = fail ("Logic." ++ str ++ " nyi for: " ++ language_name lid)

class ( Syntax lid basic_spec symb_items symb_map_items

, Sentences lid sentence proof_tree sign morphism symbol

, Ord raw_symbol, PrintLaTeX raw_symbol, Typeable raw_symbol)

=> StaticAnalysis lid

basic_spec sentence proof_tree symb_items symb_map_items

sign morphism symbol raw_symbol

| lid -> basic_spec sentence proof_tree symb_items symb_map_items

sign morphism symbol raw_symbol

where

-- static analysis of basic specifications and symbol maps

basic_analysis :: lid ->

Maybe((basic_spec, -- abstract syntax tree

sign, -- efficient table for env signature

GlobalAnnos) -> -- global annotations

Result (basic_spec,sign,sign,[Named sentence]))

-- the resulting bspec has analyzed axioms in it

-- sign's: sigma_local, sigma_complete, i.e.

-- the second output sign united with the input sign

-- should yield the first output sign

-- the second output sign is the accumulated sign

-- default implementation

basic_analysis _ = Nothing

-- Shouldn't the following deliver Maybes???

sign_to_basic_spec :: lid -> sign -> [Named sentence] -> basic_spec

stat_symb_map_items ::

lid -> [symb_map_items] -> Result (EndoMap raw_symbol)

stat_symb_map_items _ _ = fail "Logic.stat_symb_map_items"

stat_symb_items :: lid -> [symb_items] -> Result [raw_symbol]

stat_symb_items l _ = statErr l "stat_symb_items"

-- amalgamation

weaklyAmalgamableCocone :: lid -> Tree.Gr sign morphism

-> Result (sign, Map.Map Node morphism)

weaklyAmalgamableCocone l _ = statErr l "weaklyAmalgamableCocone"

-- architectural sharing analysis

ensures_amalgamability :: lid ->

([CASLAmalgOpt], -- the program options

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

[(Node, morphism)], -- the sink

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

-> Result Amalgamates

ensures_amalgamability l _ = statErr l "ensures_amalgamability"

-- symbols and symbol maps

symbol_to_raw :: lid -> symbol -> raw_symbol

id_to_raw :: lid -> Id -> raw_symbol

matches :: lid -> symbol -> raw_symbol -> Bool

-- operations on signatures and morphisms

empty_signature :: lid -> sign

signature_union :: lid -> sign -> sign -> Result sign

signature_union l _ _ = statErr l "signature_union"

morphism_union :: lid -> morphism -> morphism -> Result morphism

morphism_union l _ _ = statErr l "morphism_union"

final_union :: lid -> sign -> sign -> Result sign

final_union l _ _ = statErr l "final_union"

is_transportable :: lid -> morphism -> Bool

is_transportable l _ =

error ("Logic.is_transportable nyi for logic"++language_name l)

-- see CASL reference manual, III.4.1.2

is_subsig :: lid -> sign -> sign -> Bool

inclusion :: lid -> sign -> sign -> Result morphism

inclusion l _ _ = statErr l "inclusion"

generated_sign, cogenerated_sign ::

lid -> Set.Set symbol -> sign -> Result morphism

generated_sign l _ _ = statErr l "generated_sign"

cogenerated_sign l _ _ = statErr l "cogenerated_sign"

induced_from_morphism ::

lid -> EndoMap raw_symbol -> sign -> Result morphism

induced_from_morphism l _ _ = statErr l "induced_from_morphism"

induced_from_to_morphism ::

lid -> EndoMap raw_symbol -> sign -> sign -> Result morphism

induced_from_to_morphism l _ _ _ =

statErr l "induced_from_to_morphism"

-- generate taxonomy from theory

theory_to_taxonomy :: lid

-> TaxoGraphKind

-> MMiSSOntology

-> sign -> [Named sentence]

-> Result MMiSSOntology

theory_to_taxonomy l _ _ _ _ = statErr l "theory_to_taxonomy"

-- sublogics

class (Ord l, Show l) => LatticeWithTop l where

meet, join :: l -> l -> l

top :: l

-- a dummy instance

instance LatticeWithTop () where

meet _ _ = ()

join _ _ = ()

top = ()

-- logics

class (StaticAnalysis lid

basic_spec sentence proof_tree symb_items symb_map_items

sign morphism symbol raw_symbol,

LatticeWithTop sublogics, ShATermConvertible sublogics,

Typeable sublogics)

=> Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

| lid -> sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

where

-- for a process logic, return its data logic

data_logic :: lid -> Maybe AnyLogic

data_logic _ = Nothing

sublogic_names :: lid -> sublogics -> [String]

sublogic_names lid _ = [language_name lid]

-- the first name is the principal name

all_sublogics :: lid -> [sublogics]

all_sublogics _ = [top]

is_in_basic_spec :: lid -> sublogics -> basic_spec -> Bool

is_in_basic_spec _ _ _ = False

is_in_sentence :: lid -> sublogics -> sentence -> Bool

is_in_sentence _ _ _ = False

is_in_symb_items :: lid -> sublogics -> symb_items -> Bool

is_in_symb_items _ _ _ = False

is_in_symb_map_items :: lid -> sublogics -> symb_map_items -> Bool

is_in_symb_map_items _ _ _ = False

is_in_sign :: lid -> sublogics -> sign -> Bool

is_in_sign _ _ _ = False

is_in_morphism :: lid -> sublogics -> morphism -> Bool

is_in_morphism _ _ _ = False

is_in_symbol :: lid -> sublogics -> symbol -> Bool

is_in_symbol _ _ _ = False

min_sublogic_basic_spec :: lid -> basic_spec -> sublogics

min_sublogic_basic_spec _ _ = top

min_sublogic_sentence :: lid -> sentence -> sublogics

min_sublogic_sentence _ _ = top

min_sublogic_symb_items :: lid -> symb_items -> sublogics

min_sublogic_symb_items _ _ = top

min_sublogic_symb_map_items :: lid -> symb_map_items -> sublogics

min_sublogic_symb_map_items _ _ = top

min_sublogic_sign :: lid -> sign -> sublogics

min_sublogic_sign _ _ = top

min_sublogic_morphism :: lid -> morphism -> sublogics

min_sublogic_morphism _ _ = top

min_sublogic_symbol :: lid -> symbol -> sublogics

min_sublogic_symbol _ _ = top

proj_sublogic_basic_spec :: lid -> sublogics

-> basic_spec -> basic_spec

proj_sublogic_basic_spec _ _ b = b

proj_sublogic_symb_items :: lid -> sublogics

-> symb_items -> Maybe symb_items

proj_sublogic_symb_items _ _ _ = Nothing

proj_sublogic_symb_map_items :: lid -> sublogics

-> symb_map_items -> Maybe symb_map_items

proj_sublogic_symb_map_items _ _ _ = Nothing

proj_sublogic_sign :: lid -> sublogics -> sign -> sign

proj_sublogic_sign _ _ s = s

proj_sublogic_morphism :: lid -> sublogics -> morphism -> morphism

proj_sublogic_morphism _ _ m = m

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

proj_sublogic_epsilon li _ s = ide li s

proj_sublogic_symbol :: lid -> sublogics -> symbol -> Maybe symbol

proj_sublogic_symbol _ _ _ = Nothing

top_sublogic :: lid -> sublogics

top_sublogic _ = top

----------------------------------------------------------------

-- Derived functions

----------------------------------------------------------------

empty_theory :: StaticAnalysis lid

basic_spec sentence proof_tree symb_items symb_map_items

sign morphism symbol raw_symbol =>

lid -> Theory sign sentence

empty_theory lid = Theory (empty_signature lid) []

----------------------------------------------------------------

-- Existential type covering any logic

----------------------------------------------------------------

data AnyLogic = forall lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree .

Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

Logic lid

instance Show AnyLogic where

show (Logic lid) = language_name lid

instance Eq AnyLogic where

Logic lid1 == Logic lid2 = language_name lid1 == language_name lid2

tyconAnyLogic :: TyCon

tyconAnyLogic = mkTyCon "Logic.Logic.AnyLogic"

instance Typeable AnyLogic where

typeOf _ = mkTyConApp tyconAnyLogic []

----------------------------------------------------------------

-- Typeable instances

----------------------------------------------------------------

namedTc :: TyCon

namedTc = mkTyCon "Common.AS_Annotation.Named"

instance Typeable s => Typeable (Named s) where

typeOf s = mkTyConApp namedTc [typeOf ((undefined :: Named a -> a) s)]

setTc :: TyCon

setTc = mkTyCon "Common.Lib.Set.Set"

instance Typeable a => Typeable (Set.Set a) where

typeOf s = mkTyConApp setTc [typeOf ((undefined:: Set.Set a -> a) s)]

mapTc :: TyCon

mapTc = mkTyCon "Common.Lib.Map.Map"

instance (Typeable a, Typeable b) => Typeable (Map.Map a b) where

typeOf m = mkTyConApp mapTc [typeOf ((undefined :: Map.Map a b -> a) m),

typeOf ((undefined :: Map.Map a b -> b) m)]

{- class hierarchy:

Language

__________/

Category

| /

Sentences Syntax

\ /

StaticAnalysis (no sublogics)

\

\

Logic

-}