Logic.hs revision 05ca76b03b6d16bcfb3e7654c31e41a220e85663
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder{- |
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederModule : $Header$
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2003
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : till@tzi.de
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederStability : provisional
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederPortability : non-portable (various -fglasgow-exts extensions)
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder Provides data structures for logics (with symbols). Logics are
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder a type class with an "identitiy" type (usually interpreted
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder by a singleton set) which serves to treat logics as
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder data. All the functions in the type class take the
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder identity as first argument in order to determine the logic.
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder For logic (co)morphisms see Comorphism.hs
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder References:
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder J. A. Goguen and R. M. Burstall
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder Institutions: Abstract Model Theory for Specification and
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder Programming
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder JACM 39, p. 95--146, 1992
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder (general notion of logic - model theory only)
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder J. Meseguer
fc7df539e6d41b050161ed8f9ae6e444b1b5ab14Christian Maeder General Logics
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder Logic Colloquium 87, p. 275--329, North Holland, 1989
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder (general notion of logic - also proof theory;
2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maeder notion of logic representation, called map there)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
d3bca27d616c5741d0b18776c8a0848ec31c87f4Christian Maeder T. Mossakowski:
2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maeder Specification in an arbitrary institution with symbols
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder 14th WADT 1999, LNCS 1827, p. 252--270
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder (treatment of symbols and raw symbols, see also CASL semantics)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder T. Mossakowski, B. Klin:
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder Institution Independent Static Analysis for CASL
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder 15h WADT 2001, LNCS 2267, p. 221-237, 2002.
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder (what is needed for static anaylsis)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder S. Autexier and T. Mossakowski
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder Integrating HOLCASL into the Development Graph Manager MAYA
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder FroCoS 2002, to appear
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder (interface to provers)
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder Todo:
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder ATerm, XML
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder Weak amalgamability
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder Metavars
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder raw symbols are now symbols, symbols are now signature symbols
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder provide both signature symbol set and symbol set of a signature
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder-}
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maedermodule Logic.Logic where
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.Id
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederimport Common.GlobalAnnotations
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederimport Common.Lib.Set
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederimport Common.Lib.Map
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederimport Common.Lib.Graph
04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport Common.AnnoState
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maederimport Common.Result
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.AS_Annotation
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederimport Logic.Prover -- for one half of class Sentences
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maederimport Common.PrettyPrint
8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maederimport Data.Dynamic
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- for coercion used in Grothendieck.hs and Analysis modules
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederimport UnsafeCoerce
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- for Conversion to ATerms
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.ATerm.Lib -- (ATermConvertible)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski-- diagrams are just graphs
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maedertype Diagram object morphism = Graph object morphism
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder-- | Amalgamability analysis might be undecidable, so we need
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- a special type for the result of ensures_amalgamability
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederdata Amalgamates = Yes
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder | No String -- ^ failure description
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder | DontKnow
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- languages, define like "data CASL = CASL deriving Show"
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maederclass Show lid => Language lid where
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder language_name :: lid -> String
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder language_name i = show i
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder description :: lid -> String
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder -- default implementation
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder description _ = "No description available"
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder
0b14ccc700093e203914052bf6aceda3164af730Christian Maeder-- (a bit unsafe) coercion using the language name
0b14ccc700093e203914052bf6aceda3164af730Christian Maedercoerce :: (Typeable a, Typeable b, Language lid1, Language lid2) =>
0b14ccc700093e203914052bf6aceda3164af730Christian Maeder lid1 -> lid2 -> a -> Maybe b
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maedercoerce i1 i2 a = if language_name i1 == language_name i2 then
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder --fromDynamic (toDyn (a)) else Nothing
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder (Just $ unsafeCoerce a) else Nothing
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maederrcoerce1 :: (Typeable a, Typeable b, Language lid1, Language lid2, Show a) =>
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder lid1 -> lid2 -> Pos-> a -> b -> Result b
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederrcoerce1 i1 i2 pos a b =
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder maybeToResult pos
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder (if language_name i1 == language_name i2 then
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder "Internal type error concerning types "++show (typeOf a)
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder ++" and "++show(typeOf b)
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder else "Logic "++ language_name i1 ++ " expected, but "
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder ++ language_name i2++" found")
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder (coerce i1 i2 a)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
d48085f765fca838c1d972d2123601997174583dChristian Maederrcoerce :: (Typeable a, Typeable b, Language lid1, Language lid2) =>
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder lid1 -> lid2 -> Pos-> a -> Result b
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maederrcoerce i1 i2 pos a = -- rcoerce1 i1 i2 pos a undefined
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder maybeToResult pos
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder (if language_name i1 == language_name i2 then
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder "Internal type error concerning type "++show (typeOf a)
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder else "Logic "++ language_name i1 ++ " expected, but "
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder ++ language_name i2++" found")
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder (coerce i1 i2 a)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- Categories are given by a quotient,
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- i.e. we need equality
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder-- Should we allow arbitrary composition graphs and build paths?
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maederclass (PrintLaTeX a, Typeable a, ATermConvertible a) => PrintTypeConv a
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maederclass (Eq a, PrintTypeConv a) => EqPrintTypeConv a
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder
793945d4ac7c0f22760589c87af8e71427c76118Christian Maederinstance (PrintLaTeX a, Typeable a, ATermConvertible a) => PrintTypeConv a
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederinstance (Eq a, PrintTypeConv a) => EqPrintTypeConv a
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maederclass (Language lid, Eq sign, Eq morphism)
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder => Category lid sign morphism | lid -> sign, lid -> morphism where
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder ide :: lid -> sign -> morphism
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder comp :: lid -> morphism -> morphism -> Maybe morphism
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder -- diagrammatic order
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder dom, cod :: lid -> morphism -> sign
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder legal_obj :: lid -> sign -> Bool
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder legal_mor :: lid -> morphism -> Bool
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder-- abstract syntax, parsing and printing
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maederclass (Language lid, PrintTypeConv basic_spec,
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder EqPrintTypeConv symb_items,
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder EqPrintTypeConv symb_map_items)
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder => Syntax lid basic_spec symb_items symb_map_items
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder | lid -> basic_spec, lid -> symb_items,
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder lid -> symb_map_items
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder where
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder -- parsing
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder parse_basic_spec :: lid -> Maybe(AParser basic_spec)
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder parse_symb_items :: lid -> Maybe(AParser symb_items)
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder parse_symb_map_items :: lid -> Maybe(AParser symb_map_items)
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder-- sentences (plus prover stuff and "symbol" with "Ord" for efficient lookup)
0b14ccc700093e203914052bf6aceda3164af730Christian Maeder
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maederclass (Category lid sign morphism, Ord sentence,
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder Ord symbol,
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder PrintTypeConv sign, PrintTypeConv morphism,
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder PrintTypeConv sentence, PrintTypeConv symbol,
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder ATermConvertible proof_tree, Typeable proof_tree)
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder => Sentences lid sentence proof_tree sign morphism symbol
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder | lid -> sentence, lid -> sign, lid -> morphism,
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder lid -> symbol, lid -> proof_tree
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder where
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder -- sentence translation
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder map_sen :: lid -> morphism -> sentence -> Result sentence
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder -- parsing of sentences
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder parse_sentence :: lid -> Maybe (sign -> String -> Result sentence)
0b14ccc700093e203914052bf6aceda3164af730Christian Maeder -- is a term parser needed as well?
0b14ccc700093e203914052bf6aceda3164af730Christian Maeder sym_of :: lid -> sign -> Set symbol
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder symmap_of :: lid -> morphism -> EndoMap symbol
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder sym_name :: lid -> symbol -> Id
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder provers :: lid -> [Prover sign sentence proof_tree symbol]
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder cons_checkers :: lid -> [Cons_checker
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder (TheoryMorphism sign sentence morphism)]
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder-- static analysis
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederclass ( Syntax lid basic_spec symb_items symb_map_items
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder , Sentences lid sentence proof_tree sign morphism symbol
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder , Ord raw_symbol, PrintLaTeX raw_symbol, Typeable raw_symbol)
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder => StaticAnalysis lid
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder basic_spec sentence proof_tree symb_items symb_map_items
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder sign morphism symbol raw_symbol
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder | lid -> basic_spec, lid -> sentence, lid -> symb_items,
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder lid -> symb_map_items, lid -> proof_tree,
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder lid -> sign, lid -> morphism, lid -> symbol, lid -> raw_symbol
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder where
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -- static analysis of basic specifications and symbol maps
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder basic_analysis :: lid ->
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder Maybe((basic_spec, -- abstract syntax tree
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder sign, -- efficient table for env signature
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder GlobalAnnos) -> -- global annotations
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder Result (basic_spec,sign,sign,[Named sentence]))
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski -- the resulting bspec has analyzed axioms in it
20fe556546c9277cf017931a07d90add61f199d9Christian Maeder -- the first output sign united with the input sign
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder -- should yield the second output sign
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder -- the second output sign is the accumulated sign
20fe556546c9277cf017931a07d90add61f199d9Christian Maeder -- Shouldn't the following deliver Maybes???
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder sign_to_basic_spec :: lid -> sign -> [Named sentence] -> basic_spec
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder stat_symb_map_items ::
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder lid -> [symb_map_items] -> Result (EndoMap raw_symbol)
c9b711a46e5138b2742727817c8071960e673073Christian Maeder stat_symb_items :: lid -> [symb_items] -> Result [raw_symbol]
c9b711a46e5138b2742727817c8071960e673073Christian Maeder -- architectural sharing analysis
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder ensures_amalgamability :: lid ->
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder (Diagram sign morphism, [LEdge morphism]) -> Result Amalgamates
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder -- symbols and symbol maps
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder symbol_to_raw :: lid -> symbol -> raw_symbol
59c036af82aff7fbe074455dad50477b7878e2d8Christian Maeder id_to_raw :: lid -> Id -> raw_symbol
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder matches :: lid -> symbol -> raw_symbol -> Bool
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
59c036af82aff7fbe074455dad50477b7878e2d8Christian Maeder -- operations on signatures and morphisms
59c036af82aff7fbe074455dad50477b7878e2d8Christian Maeder empty_signature :: lid -> sign
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder 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)
=> 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
----------------------------------------------------------------
-- 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
----------------------------------------------------------------
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
-}