Logic.hs revision b3a6e8022e4a38976980d1264682eae6df92978d
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-- needs ghc -fglasgow-exts -fallow-overlapping-instances -package data
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder Till Mossakowski, Christian Maeder
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder Provides data structures for logics (with symbols). Logics are
413db961f13e112716509b6d61d7a7bbf50c98b2Christian 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
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder identity as first argument in order to determine the logic.
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder For logic representations see LogicRepr.hs
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder J. A. Goguen and R. M. Burstall
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Institutions: Abstract Model Theory for Specification and
d48085f765fca838c1d972d2123601997174583dChristian Maeder JACM 39, p. 95--146, 1992
47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder (general notion of logic - model theory only)
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder General Logics
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder Logic Colloquium 87, p. 275--329, North Holland, 1989
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (general notion of logic - also proof theory;
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder notion of logic representation, called map there)
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder T. Mossakowski:
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder Specification in an arbitrary institution with symbols
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder 14th WADT 1999, LNCS 1827, p. 252--270
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder (treatment of symbols and raw symbols, see also CASL semantics)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder T. Mossakowski, B. Klin:
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Institution Independent Static Analysis for CASL
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder 15h WADT 2001, LNCS 2267, p. 221-237, 2002.
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (what is needed for static anaylsis)
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder S. Autexier and T. Mossakowski
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Integrating HOLCASL into the Development Graph Manager MAYA
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder FroCoS 2002, to appear
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (interface to provers)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Weak amalgamability
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedermodule Logic where
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maederimport AS_Annotation
df33a9af92444f63ad545da6bb326aac9284318eChristian Maederimport FiniteMap
df33a9af92444f63ad545da6bb326aac9284318eChristian Maederimport Prover -- for one half of class Sentences
df33a9af92444f63ad545da6bb326aac9284318eChristian Maederimport PrettyPrint
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder-- for coercion used in LogicGraph.hs and Grothendieck.hs
df33a9af92444f63ad545da6bb326aac9284318eChristian Maederimport GlaExts(unsafeCoerce#)
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maedertype EndoMap a = FiniteMap a a
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- diagrams are just graphs
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederdata Diagram object morphism = Graph object morphism
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- languages, define like "data CASL = CASL deriving Show"
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maederclass Show id => Language id where
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder language_name :: id -> String
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder language_name i = show i
92aa1b88f02d2a413da60dba78acd34312e6f29aChristian Maeder-- (a bit unsafe) coercion using the language name
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedercoerce :: (Language id1, Language id2) => id1 -> id2 -> a -> Maybe b
d92635f998347112e5d5803301c2abfe7832ab65Christian Maedercoerce i1 i2 a = if language_name i1 == language_name i2 then
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (Just $ unsafeCoerce# a) else Nothing
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- Categories are given by a quotient,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- i.e. we need equality
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder-- Should we allow arbitrary composition graphs and build paths?
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maederclass (Language id, Eq sign, Show sign, Eq morphism) =>
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder Category id sign morphism | id -> sign, id -> morphism where
99f16a0f9ca757410960ff51a79b034503384fe2Christian Maeder ide :: id -> sign -> morphism
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder o :: id -> morphism -> morphism -> Maybe morphism
d48085f765fca838c1d972d2123601997174583dChristian Maeder dom, cod :: id -> morphism -> sign
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder legal_obj :: id -> sign -> Bool
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder legal_mor :: id -> morphism -> Bool
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder-- abstract syntax, parsing and printing
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maederclass (Language id, PrettyPrint basic_spec, Eq basic_spec,
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder PrettyPrint symb_items, Eq symb_items,
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder PrettyPrint symb_map_items, Eq symb_map_items) =>
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder Syntax id basic_spec symb_items symb_map_items
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder | id -> basic_spec, id -> symb_items,
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder id -> symb_map_items
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder parse_basic_spec :: id -> Maybe(GenParser Char st basic_spec)
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder parse_symb_items :: id -> GenParser Char st symb_items
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder parse_symb_map_items :: id -> GenParser Char st symb_map_items
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder-- sentences (plus prover stuff and "symbol" with "Ord" for efficient lookup)
df33a9af92444f63ad545da6bb326aac9284318eChristian Maederclass (Category id sign morphism, Show sentence,
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder Show local_env, Ord symbol, Show symbol)
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder => Sentences id sentence local_env sign morphism symbol
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder | id -> sentence, id -> local_env, id -> sign, id -> morphism,
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder -- sentence translation
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder map_sen :: id -> morphism -> sentence -> Result sentence
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder -- parsing of sentences
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder parse_sentence :: id -> local_env -> String -> Result sentence
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder -- is a term parser needed as well?
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder provers :: id -> [Prover sentence symbol]
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder cons_checkers :: id -> [Cons_checker
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder (TheoryMorphism sign sentence morphism)]
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder-- static analysis
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maederclass ( Syntax id basic_spec symb_items symb_map_items
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder , Sentences id sentence local_env sign morphism symbol
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder , Show raw_symbol, Eq raw_symbol)
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder => StaticAnalysis id
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder basic_spec sentence symb_items symb_map_items
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder local_env sign morphism symbol raw_symbol
99f16a0f9ca757410960ff51a79b034503384fe2Christian Maeder | id -> basic_spec, id -> sentence, id -> symb_items,
99f16a0f9ca757410960ff51a79b034503384fe2Christian Maeder id -> symb_map_items, id -> local_env,
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder id -> sign, id -> morphism, id -> symbol, id -> raw_symbol
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder -- static analysis of basic specifications and symbol maps
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder basic_analysis :: id ->
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Maybe((basic_spec, -- abstract syntax tree
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder local_env, -- efficient table for env signature
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [Annotation]) -> -- global annotations
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Result (local_env,sign,[(String,sentence)]))
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder -- the output local env is expected to be
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder -- just the input local env, united with the sign.
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder -- We have both just for efficiency reasons.
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder -- These include any new annotations
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder stat_symb_map_items ::
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder id -> symb_map_items -> Result (EndoMap raw_symbol)
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder stat_symb_items :: id -> symb_items -> Result [raw_symbol]
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder -- architectural sharing analysis for one morphism
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder ensures_amalgamability :: id ->
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder (Diagram sign morphism, Node, sign, LEdge morphism, morphism) ->
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder Result (Diagram sign morphism)
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder -- do we need it also for sinks consisting of two morphisms?
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder -- symbols and symbol maps
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder symbol_to_raw :: id -> symbol -> raw_symbol
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder id_to_raw :: id -> Id -> raw_symbol
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder sym_of :: id -> sign -> Set symbol
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder symmap_of :: id -> morphism -> EndoMap symbol
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder matches :: id -> symbol -> raw_symbol -> Bool
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder sym_name :: id -> symbol -> Id
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder -- operations on local envs, signatures and morphisms
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder empty_local_env :: id -> local_env
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder add_sign :: id -> sign -> local_env -> local_env
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder empty_signature :: id -> sign
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder signature_union :: id -> sign -> sign -> Result sign
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder final_union :: id -> sign -> sign -> Result sign
37354e3ed68875fb527338105a610df481f98cb0Christian Maeder is_subsig :: id -> sign -> sign -> Bool
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder generated_sign, cogenerated_sign ::
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder id -> [raw_symbol] -> sign -> Result morphism
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder induced_from_morphism ::
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder id -> EndoMap raw_symbol -> sign -> Result morphism
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder induced_from_to_morphism ::
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder id -> EndoMap raw_symbol -> sign -> sign -> Result morphism
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder extend_morphism ::
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder id -> sign -> morphism -> sign -> sign -> Result morphism
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederclass Ord l => LatticeWithTop l where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder meet, join :: l -> l -> l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederclass (StaticAnalysis id
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder basic_spec sentence symb_items symb_map_items
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder local_env sign morphism symbol raw_symbol,
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder LatticeWithTop sublogics) =>
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder Logic id sublogics
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder basic_spec sentence symb_items symb_map_items
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder local_env sign morphism symbol raw_symbol
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | id -> sublogics, id -> basic_spec, id -> sentence, id -> symb_items,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder id -> symb_map_items, id -> local_env,
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder id -> sign, id -> morphism, id ->symbol, id -> raw_symbol
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder sublogic_names :: id -> sublogics -> [String]
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder -- the first name is the principal name
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder all_sublogics :: id -> [sublogics]
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder is_in_basic_spec :: id -> sublogics -> basic_spec -> Bool
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder is_in_sentence :: id -> sublogics -> sentence -> Bool
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder is_in_symb_items :: id -> sublogics -> symb_items -> Bool
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder is_in_symb_map_items :: id -> sublogics -> symb_map_items -> Bool
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder is_in_sign :: id -> sublogics -> sign -> Bool
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder is_in_morphism :: id -> sublogics -> morphism -> Bool
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder is_in_symbol :: id -> sublogics -> symbol -> Bool
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder min_sublogic_basic_spec :: id -> basic_spec -> sublogics
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder min_sublogic_sentence :: id -> sentence -> sublogics
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder min_sublogic_symb_items :: id -> symb_items -> sublogics
79bf169bcae16ce390683c698bae248c1ed6ab13Christian Maeder min_sublogic_symb_map_items :: id -> symb_map_items -> sublogics
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder min_sublogic_sign :: id -> sign -> sublogics
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder min_sublogic_morphism :: id -> morphism -> sublogics
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder min_sublogic_symbol :: id -> symbol -> sublogics
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder proj_sublogic_basic_spec :: id -> sublogics -> basic_spec -> basic_spec
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder proj_sublogic_symb_items :: id -> sublogics -> symb_items -> Maybe symb_items
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder proj_sublogic_symb_map_items :: id -> sublogics -> symb_map_items -> Maybe symb_map_items
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder proj_sublogic_sign :: id -> sublogics -> sign -> sign
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder proj_sublogic_morphism :: id -> sublogics -> morphism -> morphism
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder proj_sublogic_epsilon :: id -> sublogics -> sign -> morphism
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder proj_sublogic_symbol :: id -> sublogics -> symbol -> Maybe symbol
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder{- class hierarchy:
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder Sentences Syntax
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder StaticAnalysis (no sublogics)