Logic.hs revision d21f1db14625cb0a536fc06b46fcc115d48a25bb
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian Maeder-- needs ghc -fglasgow-exts -fallow-overlapping-instances -package data
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Till Mossakowski, Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Provides data structures for logics (with symbols). Logics are
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder a type class with an "identitiy" type (usually interpreted
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder by a singleton set) which serves to treat logics as
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder data. All the functions in the type class take the
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder identity as first argument in order to determine the logic.
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder For logic representations see LogicRepr.hs
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder J. A. Goguen and R. M. Burstall
a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maeder Institutions: Abstract Model Theory for Specification and
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich JACM 39, p. 95--146, 1992
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder (general notion of logic - model theory only)
4cb215739e9ab13447fa21162482ebe485b47455Christian Maeder General Logics
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maeder Logic Colloquium 87, p. 275--329, North Holland, 1989
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich (general notion of logic - also proof theory;
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder notion of logic representation, called map there)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder T. Mossakowski:
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder Specification in an arbitrary institution with symbols
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maeder 14th WADT 1999, LNCS 1827, p. 252--270
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maeder (treatment of symbols and raw symbols, see also CASL semantics)
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maeder T. Mossakowski, B. Klin:
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Institution Independent Static Analysis for CASL
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder 15h WADT 2001, LNCS 2267, p. 221-237, 2002.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (what is needed for static anaylsis)
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maeder S. Autexier and T. Mossakowski
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder Integrating HOLCASL into the Development Graph Manager MAYA
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder FroCoS 2002, to appear
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder (interface to provers)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder Weak amalgamability
6a2dad705deefd1b7a7e09b84fd2d75f2213be47Christian Maederimport Logic.Prover -- for one half of class Sentences
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maeder-- for coercion used in Grothendieck.hs and Analysis modules
feca1d35123d8c31aee238c9ce79947b0bf65494Christian Maederimport UnsafeCoerce
db675e8302ddb0d6528088ce68f5e98a00e890e3Christian Maedertype EndoMap a = Map a a
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder-- diagrams are just graphs
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederdata Diagram object morphism = Graph object morphism
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- languages, define like "data CASL = CASL deriving Show"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederclass Show lid => Language lid where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder language_name :: lid -> String
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder language_name i = show i
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- (a bit unsafe) coercion using the language name
9e748851c150e1022fb952bab3315e869aaf0214Christian Maedercoerce :: (Typeable a, Typeable b, Language lid1, Language lid2, Show a) =>
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder lid1 -> lid2 -> a -> Maybe b
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maedercoerce i1 i2 a = if language_name i1 == language_name i2 then
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder --fromDynamic (toDyn (a)) else Nothing
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (Just $ unsafeCoerce a) else Nothing
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederrcoerce1 :: (Typeable a, Typeable b, Language lid1, Language lid2, Show a) =>
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder lid1 -> lid2 -> Pos-> a -> b -> Result b
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maederrcoerce1 i1 i2 pos a b =
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder maybeToResult pos
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder (if language_name i1 == language_name i2 then
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder "Internal type error concerning types "++show (typeOf a)
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder ++" and "++show(typeOf b)
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder else "Logic "++ language_name i1 ++ " expected, but "
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian Maeder ++ language_name i2++" found")
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian Maeder (coerce i1 i2 a)
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian Maederrcoerce :: (Typeable a, Typeable b, Language lid1, Language lid2, Show a) =>
1cd4f6541984962658add5cfaa9f28a93879881bChristian Maeder lid1 -> lid2 -> Pos-> a -> Result b
1cd4f6541984962658add5cfaa9f28a93879881bChristian Maederrcoerce i1 i2 pos a = -- rcoerce1 i1 i2 pos a undefined
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder maybeToResult pos
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (if language_name i1 == language_name i2 then
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder "Internal type error concerning type "++show (typeOf a)
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder else "Logic "++ language_name i1 ++ " expected, but "
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder ++ language_name i2++" found")
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (coerce i1 i2 a)
a9b59eb2ce961014974276cdae0e9df4419bd212Christian Maeder-- Categories are given by a quotient,
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- i.e. we need equality
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- Should we allow arbitrary composition graphs and build paths?
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederclass (Language lid, Eq sign, Show sign, Eq morphism, Show morphism) =>
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Category lid sign morphism | lid -> sign, lid -> morphism where
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder ide :: lid -> sign -> morphism
dc679edd4ca027663212afdf00926ae2ce19b555Christian Maeder comp :: lid -> morphism -> morphism -> Maybe morphism
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- diagrammatic order
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder dom, cod :: lid -> morphism -> sign
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder legal_obj :: lid -> sign -> Bool
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder legal_mor :: lid -> morphism -> Bool
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- abstract syntax, parsing and printing
b568982efd0997d877286faa592d81b03c8c67b8Christian Maedertype ParseFun a = FilePath -> Int -> Int -> String -> (a,String,Int,Int)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder -- args: filename, line, column, input text
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich -- result: value, remaining text, line, column
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederclass (Language lid, PrettyPrint basic_spec, Eq basic_spec,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder PrettyPrint symb_items, Eq symb_items,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder PrettyPrint symb_map_items, Eq symb_map_items) =>
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder Syntax lid basic_spec symb_items symb_map_items
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder | lid -> basic_spec, lid -> symb_items,
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder lid -> symb_map_items
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder parse_basic_spec :: lid -> Maybe(ParseFun basic_spec)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder parse_symb_items :: lid -> Maybe(ParseFun symb_items)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder parse_symb_map_items :: lid -> Maybe(ParseFun symb_map_items)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- sentences (plus prover stuff and "symbol" with "Ord" for efficient lookup)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederclass (Category lid sign morphism, Show sentence,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Ord symbol, Show symbol)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder => Sentences lid sentence proof_tree sign morphism symbol
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder | lid -> sentence, lid -> sign, lid -> morphism,
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder lid -> symbol, lid -> proof_tree
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder -- sentence translation
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder map_sen :: lid -> morphism -> sentence -> Result sentence
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder -- parsing of sentences
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder parse_sentence :: lid -> sign -> String -> Result sentence
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian Maeder -- is a term parser needed as well?
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder provers :: lid -> [Prover sentence proof_tree symbol]
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder cons_checkers :: lid -> [Cons_checker
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maeder (TheoryMorphism sign sentence morphism)]
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maeder-- static analysis
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederclass ( Syntax lid basic_spec symb_items symb_map_items
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder , Sentences lid sentence proof_tree sign morphism symbol
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder , Show raw_symbol, Eq raw_symbol)
8d178ae08a52d61379e6b8074f61646499bc88bbChristian Maeder => StaticAnalysis lid
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder basic_spec sentence proof_tree symb_items symb_map_items
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder sign morphism symbol raw_symbol
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder | lid -> basic_spec, lid -> sentence, lid -> symb_items,
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder lid -> symb_map_items, lid -> proof_tree,
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder lid -> sign, lid -> morphism, lid -> symbol, lid -> raw_symbol
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder -- static analysis of basic specifications and symbol maps
59138b404f12352d103eeffbeaeb3957b90e75fdChristian Maeder basic_analysis :: lid ->
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder Maybe((basic_spec, -- abstract syntax tree
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder sign, -- efficient table for env signature
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder GlobalAnnos) -> -- global annotations
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Result (sign,sign,[(String,sentence)]))
10883d13973c46cac98964b66ace7a52b2d059abChristian Maeder -- the first output sign is the accumulated sign
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder -- the second output sign united with the input sing
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder -- should yield the first output sign
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder sign_to_basic_spec :: lid -> sign -> [(String,sentence)] -> basic_spec
0e5b095a19790411e5352fa7cf57cb0388e70472Christian Maeder stat_symb_map_items ::
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder lid -> [symb_map_items] -> Result (EndoMap raw_symbol)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder stat_symb_items :: lid -> [symb_items] -> Result [raw_symbol]
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder -- architectural sharing analysis for one morphism
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder ensures_amalgamability :: lid ->
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder (Diagram sign morphism, Node, sign, LEdge morphism, morphism) ->
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder Result (Diagram sign morphism)
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder -- do we need it also for sinks consisting of two morphisms?
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder -- symbols and symbol maps
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder symbol_to_raw :: lid -> symbol -> raw_symbol
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder id_to_raw :: lid -> Id -> raw_symbol
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder sym_of :: lid -> sign -> Set symbol
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder symmap_of :: lid -> morphism -> EndoMap symbol
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder matches :: lid -> symbol -> raw_symbol -> Bool
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder sym_name :: lid -> symbol -> Id
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder -- operations on signatures and morphisms
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblett add_sign :: lid -> sign -> sign -> sign
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder empty_signature :: lid -> sign
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder signature_union :: lid -> sign -> sign -> Result sign
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder morphism_union :: lid -> morphism -> morphism -> Result morphism
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder final_union :: lid -> sign -> sign -> Result sign
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers is_subsig :: lid -> sign -> sign -> Bool
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder generated_sign, cogenerated_sign ::
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder lid -> [symbol] -> sign -> Result morphism
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder induced_from_morphism ::
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder lid -> EndoMap raw_symbol -> sign -> Result morphism
140287998aa8592c9c403bd9e308e447ba92ae11Christian Maeder induced_from_to_morphism ::
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder lid -> EndoMap raw_symbol -> sign -> sign -> Result morphism
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder extend_morphism ::
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder lid -> sign -> morphism -> sign -> sign -> Result morphism
9e748851c150e1022fb952bab3315e869aaf0214Christian Maederclass (Ord l, Show l) => LatticeWithTop l where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder meet, join :: l -> l -> l
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maederclass (StaticAnalysis lid
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder basic_spec sentence proof_tree symb_items symb_map_items
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder sign morphism symbol raw_symbol,
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder LatticeWithTop sublogics,
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder Typeable sublogics, Typeable basic_spec, Typeable sentence,
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder Typeable symb_items, Typeable symb_map_items, Typeable sign,
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder Typeable morphism, Typeable symbol, Typeable raw_symbol,
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder Typeable proof_tree) =>
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder Logic lid sublogics
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder basic_spec sentence symb_items symb_map_items
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder sign morphism symbol raw_symbol proof_tree
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder | lid -> sublogics, lid -> basic_spec, lid -> sentence, lid -> symb_items,
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder lid -> symb_map_items, lid -> proof_tree,
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder lid -> sign, lid -> morphism, lid ->symbol, lid -> raw_symbol
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder sublogic_names :: lid -> sublogics -> [String]
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder -- the first name is the principal name
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder all_sublogics :: lid -> [sublogics]
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder is_in_basic_spec :: lid -> sublogics -> basic_spec -> Bool
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder is_in_sentence :: lid -> sublogics -> sentence -> Bool
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder is_in_symb_items :: lid -> sublogics -> symb_items -> Bool
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder is_in_symb_map_items :: lid -> sublogics -> symb_map_items -> Bool
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder is_in_sign :: lid -> sublogics -> sign -> Bool
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder is_in_morphism :: lid -> sublogics -> morphism -> Bool
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder is_in_symbol :: lid -> sublogics -> symbol -> Bool
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder min_sublogic_basic_spec :: lid -> basic_spec -> sublogics
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder min_sublogic_sentence :: lid -> sentence -> sublogics
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder min_sublogic_symb_items :: lid -> symb_items -> sublogics
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder min_sublogic_symb_map_items :: lid -> symb_map_items -> sublogics
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder min_sublogic_sign :: lid -> sign -> sublogics
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder min_sublogic_morphism :: lid -> morphism -> sublogics
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder min_sublogic_symbol :: lid -> symbol -> sublogics
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder proj_sublogic_basic_spec :: lid -> sublogics -> basic_spec -> basic_spec
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder proj_sublogic_symb_items :: lid -> sublogics -> symb_items -> Maybe symb_items
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder proj_sublogic_symb_map_items :: lid -> sublogics -> symb_map_items -> Maybe symb_map_items
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder proj_sublogic_sign :: lid -> sublogics -> sign -> sign
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder proj_sublogic_morphism :: lid -> sublogics -> morphism -> morphism
ac34194a668399bb8ef238da77c3a09e93fb253bChristian Maeder proj_sublogic_epsilon :: lid -> sublogics -> sign -> morphism
4fc9de0da898448f1d3597ebbd8c04a066464c21Christian Maeder proj_sublogic_symbol :: lid -> sublogics -> symbol -> Maybe symbol
c208973c890b8f993297720fd0247bc7481d4304Christian MaedersetTc :: TyCon
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maederinstance Typeable a => Typeable (Set a) where
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder typeOf s = mkAppTy setTc [typeOf ((undefined:: Set a -> a) s)]
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedermapTc :: TyCon
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederinstance (Typeable a, Typeable b) => Typeable (Map a b) where
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder typeOf m = mkAppTy mapTc [typeOf ((undefined :: Map a b -> a) m),
01e278bdd7dce13b9303ed3d79683d83c89d09f9Liam O'Reilly typeOf ((undefined :: Map a b -> b) m)]
5ad5dffe06818a13e1632b1119fbca7881085fc1Dominik Luecke{- class hierarchy:
31d6d9286988dc31639d105841296759aeb743e0Jonathan von Schroeder Sentences Syntax
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder StaticAnalysis (no sublogics)