Logic.hs revision 7ce50de323aa5255cf502c5aaa5cfe0286468613
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Header$
e47d29b522739fbf08aac80c6faa447dde113fbcChristian MaederCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2003
11d6ec73ee5550e00cb56b221bdbeb709142e779Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian MaederMaintainer : till@tzi.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability : non-portable (various -fglasgow-exts extensions)
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder Provides data structures for logics (with symbols). Logics are
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder a type class with an "identitiy" type (usually interpreted
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder by a singleton set) which serves to treat logics as
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder data. All the functions in the type class take the
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder identity as first argument in order to determine the logic.
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder For logic (co)morphisms see Comorphism.hs
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder
0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder References:
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder J. A. Goguen and R. M. Burstall
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder Institutions: Abstract Model Theory for Specification and
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder Programming
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder JACM 39, p. 95--146, 1992
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder (general notion of logic - model theory only)
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder J. Meseguer
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder General Logics
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder Logic Colloquium 87, p. 275--329, North Holland, 1989
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder (general notion of logic - also proof theory;
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder notion of logic representation, called map there)
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder T. Mossakowski:
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder Specification in an arbitrary institution with symbols
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder 14th WADT 1999, LNCS 1827, p. 252--270
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder (treatment of symbols and raw symbols, see also CASL semantics)
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder T. Mossakowski, B. Klin:
62925f4a144f45b5ed1e7c841f891d13f51e553dChristian Maeder Institution Independent Static Analysis for CASL
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder 15h WADT 2001, LNCS 2267, p. 221-237, 2002.
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder (what is needed for static anaylsis)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian Maeder S. Autexier and T. Mossakowski
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder Integrating HOLCASL into the Development Graph Manager MAYA
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder FroCoS 2002, to appear
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder (interface to provers)
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder Todo:
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder ATerm, XML
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder Weak amalgamability
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder Metavars
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder raw symbols are now symbols, symbols are now signature symbols
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder provide both signature symbol set and symbol set of a signature
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder-}
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maedermodule Logic.Logic where
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport Common.Id
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Common.GlobalAnnotations
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Common.Lib.Set
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Common.Lib.Map
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport Common.Lib.Graph
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Common.AnnoState
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Common.Result
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport Common.AS_Annotation
0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maederimport Logic.Prover -- for one half of class Sentences
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Common.PrettyPrint
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport Data.Dynamic
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- for coercion used in Grothendieck.hs and Analysis modules
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maederimport UnsafeCoerce
fa45d098e1c9d468f128be9505eb7e5b2705b304Christian Maeder
25612a7b3ce708909298d5426406592473880a20Christian Maeder-- for Conversion to ATerms
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maederimport Common.ATerm.Lib -- (ATermConvertible)
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maederimport ATC.Graph -- for Diagram
c1db3d36c29a6324745a86dbcba18b8e4cd9f338Christian Maederimport ATC.AS_Annotation -- for Named
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- diagrams are just graphs
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maedertype Diagram object morphism = Graph object morphism
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder-- | Amalgamability analysis might be undecidable, so we need
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- a special type for the result of ensures_amalgamability
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maederdata Amalgamates = Yes
18b709ce961d68328da768318dcc70067f066d86Christian Maeder | No String -- ^ failure description
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder | DontKnow
18b709ce961d68328da768318dcc70067f066d86Christian Maeder
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder-- languages, define like "data CASL = CASL deriving Show"
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder
908a6351595b57641353608c4449d5faa0d1adf8Christian Maederclass Show lid => Language lid where
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder language_name :: lid -> String
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder language_name i = show i
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder-- (a bit unsafe) coercion using the language name
0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maedercoerce :: (Typeable a, Typeable b, Language lid1, Language lid2) =>
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder lid1 -> lid2 -> a -> Maybe b
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maedercoerce i1 i2 a = if language_name i1 == language_name i2 then
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder --fromDynamic (toDyn (a)) else Nothing
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder (Just $ unsafeCoerce a) else Nothing
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maederrcoerce1 :: (Typeable a, Typeable b, Language lid1, Language lid2, Show a) =>
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder lid1 -> lid2 -> Pos-> a -> b -> Result b
908a6351595b57641353608c4449d5faa0d1adf8Christian Maederrcoerce1 i1 i2 pos a b =
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder maybeToResult pos
0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder (if language_name i1 == language_name i2 then
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder "Internal type error concerning types "++show (typeOf a)
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder ++" and "++show(typeOf b)
11d6ec73ee5550e00cb56b221bdbeb709142e779Christian Maeder else "Logic "++ language_name i1 ++ " expected, but "
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder ++ language_name i2++" found")
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder (coerce i1 i2 a)
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder
18b709ce961d68328da768318dcc70067f066d86Christian Maederrcoerce :: (Typeable a, Typeable b, Language lid1, Language lid2) =>
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski lid1 -> lid2 -> Pos-> a -> Result b
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maederrcoerce i1 i2 pos a = -- rcoerce1 i1 i2 pos a undefined
b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder maybeToResult pos
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder (if language_name i1 == language_name i2 then
18b709ce961d68328da768318dcc70067f066d86Christian Maeder "Internal type error concerning type "++show (typeOf a)
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder else "Logic "++ language_name i1 ++ " expected, but "
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder ++ language_name i2++" found")
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder (coerce i1 i2 a)
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder-- Categories are given by a quotient,
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder-- i.e. we need equality
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder-- Should we allow arbitrary composition graphs and build paths?
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederclass (Language lid, Eq sign, Show sign, Eq morphism, Show morphism) =>
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder Category lid sign morphism | lid -> sign, lid -> morphism where
d5c415f6373274fed04d83b9322891f3b82e9c26Christian Maeder ide :: lid -> sign -> morphism
22fc8a1bd14dc53c5c7f482d2e0c04eb5ee4beb4Christian Maeder comp :: lid -> morphism -> morphism -> Maybe morphism
22fc8a1bd14dc53c5c7f482d2e0c04eb5ee4beb4Christian Maeder -- diagrammatic order
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder dom, cod :: lid -> morphism -> sign
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder legal_obj :: lid -> sign -> Bool
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder legal_mor :: lid -> morphism -> Bool
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder-- abstract syntax, parsing and printing
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maederclass (Language lid, PrintLaTeX basic_spec,
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder PrintLaTeX symb_items, Eq symb_items,
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder PrintLaTeX symb_map_items, Eq symb_map_items ,
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder ATermConvertible basic_spec,
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder ATermConvertible symb_items,
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder ATermConvertible symb_map_items ) =>
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder Syntax lid basic_spec symb_items symb_map_items
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder | lid -> basic_spec, lid -> symb_items,
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder lid -> symb_map_items
e1fd2026bcd805296762eaa97090f7a29819d9f2Christian Maeder where
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder -- parsing
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder parse_basic_spec :: lid -> Maybe(AParser basic_spec)
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder parse_symb_items :: lid -> Maybe(AParser symb_items)
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder parse_symb_map_items :: lid -> Maybe(AParser symb_map_items)
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder fromShATerm_basic_spec :: lid -> ATermTable -> basic_spec
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder fromShATerm_basic_spec _ att = fromShATerm att
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder fromShATerm_symb_items :: lid -> ATermTable -> symb_items
11d6ec73ee5550e00cb56b221bdbeb709142e779Christian Maeder fromShATerm_symb_items _ att = fromShATerm att
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder fromShATerm_symb_map_items :: lid -> ATermTable -> symb_map_items
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder fromShATerm_symb_map_items _ att = fromShATerm att
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder fromShATerm_symb_items_list :: lid -> ATermTable -> [symb_items]
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder fromShATerm_symb_items_list _ att = fromShATerm att
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder fromShATerm_symb_map_items_list
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder :: lid -> ATermTable -> [symb_map_items]
b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder fromShATerm_symb_map_items_list _ att = fromShATerm att
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder-- sentences (plus prover stuff and "symbol" with "Ord" for efficient lookup)
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maederclass (Category lid sign morphism, Ord sentence,
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder PrettyPrint sentence, PrintLaTeX sign, PrintLaTeX morphism,
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder Ord symbol, Show symbol, PrintLaTeX symbol,
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder ATermConvertible sentence, ATermConvertible symbol,
b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder ATermConvertible sign, ATermConvertible morphism,
65835942d66905c377fa503e0d577df5aade58feChristian Maeder ATermConvertible proof_tree)
e1fd2026bcd805296762eaa97090f7a29819d9f2Christian Maeder => Sentences lid sentence proof_tree sign morphism symbol
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder | lid -> sentence, lid -> sign, lid -> morphism,
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder lid -> symbol, lid -> proof_tree
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder where
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -- sentence translation
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder map_sen :: lid -> morphism -> sentence -> Result sentence
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder -- parsing of sentences
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder parse_sentence :: lid -> Maybe (sign -> String -> Result sentence)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -- is a term parser needed as well?
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder sym_of :: lid -> sign -> Set symbol
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder symmap_of :: lid -> morphism -> EndoMap symbol
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder sym_name :: lid -> symbol -> Id
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder provers :: lid -> [Prover sign sentence proof_tree symbol]
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder cons_checkers :: lid -> [Cons_checker
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder (TheoryMorphism sign sentence morphism)]
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fromShATerm_sentence :: lid -> ATermTable -> sentence
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fromShATerm_sentence _ att = fromShATerm att
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fromShATerm_symbol :: lid -> ATermTable -> symbol
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fromShATerm_symbol _ att = fromShATerm att
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fromShATerm_sign :: lid -> ATermTable -> sign
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fromShATerm_sign _ att = fromShATerm att
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fromShATerm_sign_list :: lid -> ATermTable -> [sign]
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fromShATerm_sign_list _ att = fromShATerm att
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fromShATerm_morphism :: lid -> ATermTable -> morphism
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fromShATerm_morphism _ att = fromShATerm att
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fromShATerm_proof_tree :: lid -> ATermTable -> proof_tree
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fromShATerm_proof_tree _ att = fromShATerm att
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fromShATerm_l_sentence_list :: lid -> ATermTable -> [Named sentence]
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fromShATerm_l_sentence_list _ att = fromShATerm att
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fromShATerm_diagram :: lid -> ATermTable -> Diagram sign morphism
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fromShATerm_diagram _ att = fromShATerm att
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder-- static analysis
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maederclass ( Syntax lid basic_spec symb_items symb_map_items
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder , Sentences lid sentence proof_tree sign morphism symbol
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder , Ord raw_symbol, PrintLaTeX raw_symbol)
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder => StaticAnalysis lid
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder basic_spec sentence proof_tree symb_items symb_map_items
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder sign morphism symbol raw_symbol
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder | lid -> basic_spec, lid -> sentence, lid -> symb_items,
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder lid -> symb_map_items, lid -> proof_tree,
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder lid -> sign, lid -> morphism, lid -> symbol, lid -> raw_symbol
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder where
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder -- static analysis of basic specifications and symbol maps
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder basic_analysis :: lid ->
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder Maybe((basic_spec, -- abstract syntax tree
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder sign, -- efficient table for env signature
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder GlobalAnnos) -> -- global annotations
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder Result (basic_spec,sign,sign,[Named sentence]))
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder -- the resulting bspec has analyzed axioms in it
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder -- the first output sign united with the input sign
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder -- should yield the second output sign
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder -- the second output sign is the accumulated sign
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder -- Shouldn't the following deliver Maybes???
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder sign_to_basic_spec :: lid -> sign -> [Named sentence] -> basic_spec
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder stat_symb_map_items ::
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder lid -> [symb_map_items] -> Result (EndoMap raw_symbol)
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder stat_symb_items :: lid -> [symb_items] -> Result [raw_symbol]
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder -- architectural sharing analysis
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder ensures_amalgamability :: lid ->
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder (Diagram sign morphism, [LEdge morphism]) -> Result Amalgamates
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder -- 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
morphism_union :: lid -> morphism -> morphism -> Result morphism
final_union :: lid -> sign -> sign -> Result sign
-- see CASL reference manual, III.4.1.2
is_subsig :: lid -> sign -> sign -> Bool
inclusion :: lid -> sign -> sign -> Result morphism
generated_sign, cogenerated_sign ::
lid -> Set symbol -> sign -> Result morphism
induced_from_morphism ::
lid -> EndoMap raw_symbol -> sign -> Result morphism
induced_from_to_morphism ::
lid -> EndoMap raw_symbol -> sign -> sign -> Result morphism
-- sublogics
class (Eq l, Show l) => LatticeWithTop l where
meet, join :: l -> l -> l
top :: l
(<<=) :: LatticeWithTop l => l -> l -> Bool
a <<= b = meet a b == b
-- 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, ATermConvertible sublogics,
Typeable sublogics, Typeable basic_spec, Typeable sentence,
Typeable symb_items, Typeable symb_map_items, Typeable sign,
Typeable morphism, Typeable symbol, Typeable raw_symbol,
Typeable proof_tree) =>
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
data_logic :: lid -> Maybe AnyLogic
data_logic _ = Nothing
sublogic_names :: lid -> sublogics -> [String]
sublogic_names _ _ = []
-- the first name is the principal name
all_sublogics :: lid -> [sublogics]
all_sublogics _ = []
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_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_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
fromShATerm_sublogics :: lid -> ATermTable -> sublogics
fromShATerm_sublogics _ att = fromShATerm att
----------------------------------------------------------------
-- 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
----------------------------------------------------------------
-- Typeable instances
----------------------------------------------------------------
mkTyConApp :: TyCon -> [TypeRep] -> TypeRep
mkTyConApp = mkAppTy
proverTc :: TyCon
proverTc = mkTyCon "Logic.Prover.Prover"
instance Typeable (Prover sign sen proof_tree symbol) where
typeOf _ = mkTyConApp proverTc []
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 a) where
typeOf s = mkTyConApp setTc [typeOf ((undefined:: Set a -> a) s)]
mapTc :: TyCon
mapTc = mkTyCon "Common.Lib.Map.Map"
instance (Typeable a, Typeable b) => Typeable (Map a b) where
typeOf m = mkTyConApp mapTc [typeOf ((undefined :: Map a b -> a) m),
typeOf ((undefined :: Map a b -> b) m)]
{- class hierarchy:
Language
__________/
Category
| /
Sentences Syntax
\ /
StaticAnalysis (no sublogics)
\
\
Logic
-}