c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder-- needs ghc -fglasgow-exts -fallow-overlapping-instances -package data

81d182b21020b815887e9057959228546cf61b6bChristian Maeder

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder{- HetCATS/Logic.hs

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder $Id$

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder Till Mossakowski, Christian Maeder

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder Provides data structures for logics (with symbols). Logics are

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder a type class with an "identitiy" type (usually interpreted

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

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

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder identity as first argument in order to determine the logic.

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder For logic representations see LogicRepr.hs

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder References:

23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder J. A. Goguen and R. M. Burstall

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Institutions: Abstract Model Theory for Specification and

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder Programming

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder JACM 39, p. 95--146, 1992

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder (general notion of logic - model theory only)

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder J. Meseguer

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder General Logics

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

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (general notion of logic - also proof theory;

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder notion of logic representation, called map there)

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder T. Mossakowski:

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder Specification in an arbitrary institution with symbols

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder 14th WADT 1999, LNCS 1827, p. 252--270

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

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder T. Mossakowski, B. Klin:

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Institution Independent Static Analysis for CASL

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder 15h WADT 2001, LNCS 2267, p. 221-237, 2002.

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder (what is needed for static anaylsis)

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder S. Autexier and T. Mossakowski

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder Integrating HOLCASL into the Development Graph Manager MAYA

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder FroCoS 2002, to appear

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder (interface to provers)

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski Todo:

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder ATerm, XML

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder Weak amalgamability

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Metavars

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder-}

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maedermodule Logic where

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maederimport Id

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederimport GlobalAnnotations

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maederimport FiniteSet

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maederimport FiniteMap

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederimport Graph

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederimport Result

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder--import Parsec

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Prover -- for one half of class Sentences

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder-- import IOExts(trace)

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maederimport PrettyPrint

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder-- for coercion used in Grothendieck.hs and Analysis modules

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederimport UnsafeCoerce

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder-- maps

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maedertype EndoMap a = FiniteMap a a

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- diagrams are just graphs

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederdata Diagram object morphism = Graph object morphism

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

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

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederclass Show lid => Language lid where

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder language_name :: lid -> String

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder language_name i = show i

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder-- (a bit unsafe) coercion using the language name

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maedercoerce :: (Language lid1, Language lid2, Show a) => lid1 -> lid2 -> a -> Maybe b

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maedercoerce i1 i2 a = if language_name i1 == language_name i2 then

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder (Just $ unsafeCoerce a) else Nothing

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederrcoerce :: (Language lid1, Language lid2, Show a) => lid1 -> lid2 -> Pos-> a -> Result b

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederrcoerce i1 i2 pos a =

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder maybeToResult pos

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder ("Logic "++ language_name i1 ++ " expected, but "

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder ++ language_name i2++" found")

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder (coerce i1 i2 a)

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder-- Categories are given by a quotient,

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder-- i.e. we need equality

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

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederclass (Language lid, Eq sign, Show sign, Eq morphism, Show morphism) =>

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder Category lid sign morphism | lid -> sign, lid -> morphism where

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder ide :: lid -> sign -> morphism

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder comp :: lid -> morphism -> morphism -> Maybe morphism

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder -- diagrammatic order

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder dom, cod :: lid -> morphism -> sign

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder legal_obj :: lid -> sign -> Bool

15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder legal_mor :: lid -> morphism -> Bool

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder-- abstract syntax, parsing and printing

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maedertype ParseFun a = FilePath -> Int -> Int -> String -> (a,String,Int,Int)

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder -- args: filename, line, column, input text

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder -- result: value, remaining text, line, column

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maederclass (Language lid, PrettyPrint basic_spec, Eq basic_spec,

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder PrettyPrint symb_items, Eq symb_items,

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder PrettyPrint symb_map_items, Eq symb_map_items) =>

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Syntax lid basic_spec symb_items symb_map_items

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder | lid -> basic_spec, lid -> symb_items,

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder lid -> symb_map_items

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder where

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder -- parsing

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder parse_basic_spec :: lid -> Maybe(ParseFun basic_spec)

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder parse_symb_items :: lid -> Maybe(ParseFun symb_items)

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder parse_symb_map_items :: lid -> Maybe(ParseFun symb_map_items)

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

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

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maederclass (Category lid sign morphism, Show sentence,

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Ord symbol, Show symbol)

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder => Sentences lid sentence proof_tree sign morphism symbol

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder | lid -> sentence, lid -> sign, lid -> morphism,

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder lid -> symbol, lid -> proof_tree

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder where

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder -- sentence translation

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

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder -- parsing of sentences

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder parse_sentence :: lid -> sign -> String -> Result sentence

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder -- is a term parser needed as well?

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder provers :: lid -> [Prover sentence proof_tree symbol]

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder cons_checkers :: lid -> [Cons_checker

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder (TheoryMorphism sign sentence morphism)]

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder-- static analysis

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederclass ( Syntax lid basic_spec symb_items symb_map_items

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , Sentences lid sentence proof_tree sign morphism symbol

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder , Show raw_symbol, Eq raw_symbol)

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder => StaticAnalysis lid

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder basic_spec sentence proof_tree symb_items symb_map_items

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder sign morphism symbol raw_symbol

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder | lid -> basic_spec, lid -> sentence, lid -> symb_items,

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder lid -> symb_map_items, lid -> proof_tree,

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder lid -> sign, lid -> morphism, lid -> symbol, lid -> raw_symbol

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder where

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder -- static analysis of basic specifications and symbol maps

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder basic_analysis :: lid ->

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Maybe((basic_spec, -- abstract syntax tree

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder sign, -- efficient table for env signature

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder GlobalAnnos) -> -- global annotations

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder Result (sign,sign,[(String,sentence)]))

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder -- the first output sign is the accumulated sign

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder -- the second output sign united with the input sing

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder -- should yield the first output sign

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder sign_to_basic_spec :: lid -> sign -> [(String,sentence)] -> basic_spec

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder stat_symb_map_items ::

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

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

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder -- architectural sharing analysis for one morphism

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder ensures_amalgamability :: lid ->

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder (Diagram sign morphism, Node, sign, LEdge morphism, morphism) ->

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder Result (Diagram sign morphism)

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder -- do we need it also for sinks consisting of two morphisms?

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder -- symbols and symbol maps

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder symbol_to_raw :: lid -> symbol -> raw_symbol

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder id_to_raw :: lid -> Id -> raw_symbol

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder sym_of :: lid -> sign -> Set symbol

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder symmap_of :: lid -> morphism -> EndoMap symbol

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder matches :: lid -> symbol -> raw_symbol -> Bool

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder sym_name :: lid -> symbol -> Id

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder -- operations on signatures and morphisms

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder add_sign :: lid -> sign -> sign -> sign

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder empty_signature :: lid -> sign

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder signature_union :: lid -> sign -> sign -> Result sign

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder morphism_union :: lid -> morphism -> morphism -> Result morphism

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder final_union :: lid -> sign -> sign -> Result sign

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder is_subsig :: lid -> sign -> sign -> Bool

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder generated_sign, cogenerated_sign ::

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder lid -> [symbol] -> sign -> Result morphism

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder induced_from_morphism ::

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder lid -> EndoMap raw_symbol -> sign -> Result morphism

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder induced_from_to_morphism ::

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder lid -> EndoMap raw_symbol -> sign -> sign -> Result morphism

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder extend_morphism ::

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder lid -> sign -> morphism -> sign -> sign -> Result morphism

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder-- sublogics

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maederclass (Ord l, Show l) => LatticeWithTop l where

15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder meet, join :: l -> l -> l

15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder top :: l

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski

-- logics

class (StaticAnalysis lid

basic_spec sentence proof_tree symb_items symb_map_items

sign morphism symbol raw_symbol,

LatticeWithTop sublogics) =>

Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

| lid -> sublogics, lid -> basic_spec, lid -> sentence, lid -> symb_items,

lid -> symb_map_items, lid -> proof_tree,

lid -> sign, lid -> morphism, lid ->symbol, lid -> raw_symbol

where

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

-- the first name is the principal name

all_sublogics :: lid -> [sublogics]

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

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

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

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

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

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

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

min_sublogic_basic_spec :: lid -> basic_spec -> sublogics

min_sublogic_sentence :: lid -> sentence -> sublogics

min_sublogic_symb_items :: lid -> symb_items -> sublogics

min_sublogic_symb_map_items :: lid -> symb_map_items -> sublogics

min_sublogic_sign :: lid -> sign -> sublogics

min_sublogic_morphism :: lid -> morphism -> sublogics

min_sublogic_symbol :: lid -> symbol -> sublogics

proj_sublogic_basic_spec :: lid -> sublogics -> basic_spec -> basic_spec

proj_sublogic_symb_items :: lid -> sublogics -> symb_items -> Maybe symb_items

proj_sublogic_symb_map_items :: lid -> sublogics -> symb_map_items -> Maybe symb_map_items

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

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

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

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

{- class hierarchy:

Language

__________/

Category

| /

Sentences Syntax

\ /

StaticAnalysis (no sublogics)

\

\

Logic

-}