Logic.hs revision 7071dc65207d7e7ff42c7ac1561431068b99ca66
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-- needs ghc -fglasgow-exts
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder Till Mossakowski
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder Provides data structures for logics (with symbols)
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder and logic representations. 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.
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder Logic representations are just collections of
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder functions between (some of) the types of logics.
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
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 Sublanguages more abstractly (lattice), projs
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Weak amalgamability
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder extension of morphisms wrt. compound ids
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maedermodule Logic where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- error messages
df33a9af92444f63ad545da6bb326aac9284318eChristian Maederdata Diagnosis = Error String Pos
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder | Warning String Pos
df33a9af92444f63ad545da6bb326aac9284318eChristian Maedernewtype Result a = Result ([Diagnosis],Maybe a)
df33a9af92444f63ad545da6bb326aac9284318eChristian Maederinstance Monad Result where
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder return x = Result ([],Just x)
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder Result (errs, Nothing) >>= f = Result (errs,Nothing)
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder Result (errs1, Just x) >>= f = Result (errs1++errs2,y)
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder where Result (errs2,y) = f x
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder-- maps and sets, just a quick thing
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedertype Set a = [a]
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maedertype Map a = [(a,a)]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- diagrams, nodes are just integers
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maedertype Node = Int
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maedertype Edge morphism = (Node,morphism,Node)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maederdata Diagram object morphism = Diagram [(Node,object)] [Edge morphism]
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederempty_diagram :: Diagram o m
92aa1b88f02d2a413da60dba78acd34312e6f29aChristian Maederempty_diagram = Diagram [] []
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederadd_node :: Diagram o m -> o -> (Node,Diagram o m)
d92635f998347112e5d5803301c2abfe7832ab65Christian Maederadd_node (Diagram nodes edges) obj =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (node,Diagram ((node,obj):nodes) edges) where
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder node = maximum (map fst nodes)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederadd_edge :: Diagram o m -> Edge m -> Diagram o m
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederadd_edge (Diagram nodes edges) edge =
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder Diagram nodes (edge:edges)
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederobject_at_node :: Node -> Diagram o m -> Maybe (Node,o)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maederobject_at_node node (Diagram nodes edges) =
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder case lookup node nodes of
99f16a0f9ca757410960ff51a79b034503384fe2Christian Maeder Just obj -> Just (node,obj)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Nothing -> Nothing
d48085f765fca838c1d972d2123601997174583dChristian Maederdiagram_nodes :: Diagram o m -> [(Node,o)]
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maederdiagram_nodes (Diagram nodes edges) = nodes
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maederdiagram_edges :: Diagram o m -> [Edge m]
d48085f765fca838c1d972d2123601997174583dChristian Maederdiagram_edges (Diagram nodes edges) = edges
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder-- Categories are given by a quotient,
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder-- i.e. we need equality
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder-- Should we allow arbitrary composition graphs and build paths?
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maederclass (Eq object, Eq morphism) =>
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder Category id object morphism | id ->, id -> morphism where
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder ide :: id -> object -> morphism
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder o :: id -> morphism -> morphism -> Maybe morphism
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder dom, cod :: id -> morphism -> object
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder legal_obj :: id -> object -> Bool
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder legal_mor :: id -> morphism -> Bool
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder-- abstract syntax, parsing and printing
df33a9af92444f63ad545da6bb326aac9284318eChristian Maederclass (Show basic_spec, Show sentence, Show symb_items,
04a1ed0b360858b85de6f449b84df4eab81b3fc9Christian Maeder Show symb_map_items, Show anno) =>
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Syntax basic_spec sentence symb_items symb_map_items anno
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder parse_basic_spec :: id -> String -> Result basic_spec
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder parse_sentence :: id -> String -> Result sentence
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder parse_symb_items :: id -> String -> Result symb_items
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder parse_symb_map_items :: id -> String -> Result symb_map_items
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder parse_anno :: id -> String -> Result anno
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maederdata Sublogic basic_spec sentence symb_items symb_map_items anno
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder sign morphism symbol raw_symbol =
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder Sublogic {sublogic_name :: String,
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder is_in_basic_spec :: basic_spec -> Bool,
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder is_in_sentence :: sentence -> Bool,
99f16a0f9ca757410960ff51a79b034503384fe2Christian Maeder is_in_symb_items :: symb_items -> Bool,
99f16a0f9ca757410960ff51a79b034503384fe2Christian Maeder is_in_symb_map_items :: symb_map_items -> Bool,
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder is_in_anno :: anno -> Bool,
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder is_in_sign :: sign -> Bool,
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder is_in_morphism :: morphism -> Bool,
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder is_in_symbol :: symbol -> Bool,
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder is_in_raw_symbol :: raw_symbol -> Bool
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder-- theories and theory morphisms
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maederdata Theory sign sen =
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Theory {sign_of :: sign,
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder ax_of :: [(String,sen)]
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maederdata TheoryMorphism sign sen mor =
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder TheoryMorphism {t_source, t_target :: Theory sign sen,
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder t_morphism :: mor
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder-- proofs and provers
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maedertype Rule = String
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maederdata Proof_tree sen = Axiom sen
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder | Branch (sen,Rule,[Proof_tree sen]) -- add substitutions here?
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maedertype Tactic_script = String -- the file name
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata Proof_status sen = Open sen
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder | Disproved sen
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder | Proved(sen,[sen],Proof_tree sen,Tactic_script)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata Prover sen symbol =
37354e3ed68875fb527338105a610df481f98cb0Christian Maeder Prover { prover_name :: String,
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder prover_sublogic :: String,
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder add_sym :: symbol -> IO(Bool), -- returns True if succeeded
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder remove_sym :: symbol -> IO(Bool), -- returns True if succeeded
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder prove :: sen -> IO([Proof_status sen]) -- proof status for goal and lemmas
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata Cons_checker morphism =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Cons_checker {cons_checker_name :: String,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder cons_checker_sublogic :: String,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder cons_check :: morphism -> IO(Bool, Tactic_script)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederclass (Syntax basic_spec sentence symb_items symb_map_items anno,
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder Show sign, Show morphism, Show symbol, Show raw_symbol,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Ord symbol, -- needed for efficient symbol tables
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Category id sign morphism) =>
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder basic_spec sentence symb_items symb_map_items anno
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder sign morphism symbol raw_symbol
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder | id -> basic_spec, id -> sentence, id -> symb_items,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder id -> symb_map_items, id -> anno, id -> local_env,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder id -> sign, id -> morphism, id ->symbol, id -> raw_symbol
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder logic_name :: id -> String
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder has_parser :: id -> Bool
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder has_printer :: id -> Bool
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder has_analysis :: id -> Bool
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder -- sentence translation
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder map_sen :: id -> morphism -> sentence -> Result sentence
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder -- static analysis of basic specifications and symbol maps
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder basic_analysis :: id ->
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder (basic_spec, -- abstract syntax tree
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder local_env, -- efficient table for env signature
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder [anno]) -> -- global annotations
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder Result (sign,[(String,sentence)])
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder stat_symb_map_items :: id -> [symb_map_items] -> Result (Map raw_symbol)
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder stat_symb_items :: id -> [symb_items] -> Result [raw_symbol]
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder -- architectural sharing analysis for one morphism
79bf169bcae16ce390683c698bae248c1ed6ab13Christian Maeder ensures_amalgamability :: id ->
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder (Diagram sign morphism, Node, sign, Edge morphism, morphism) ->
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder Result (Diagram sign morphism)
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder -- do we need it also for sinks consisting of two morphisms?
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder -- symbols and symbol maps
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder symbol_to_raw :: id -> symbol -> raw_symbol
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder id_to_raw :: id -> Id -> raw_symbol
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder sym_of :: id -> sign -> Set symbol
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder symmap_of :: id -> morphism -> Map symbol
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder matches :: id -> symbol -> raw_symbol -> Bool
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder sym_name :: id -> symbol -> Id
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder -- operations on local envs, signatures and morphisms
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder empty_local_env :: local_env
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder add_sign :: sign -> local_env -> local_env
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder empty_signature :: id -> sign
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder signature_union :: id -> sign -> sign -> Result sign
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder final_union :: id -> sign -> sign -> Result sign
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder is_subsig :: id -> sign -> sign -> Bool
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder generated_sign, cogenerated_sign :: id -> [raw_symbol] -> sign -> Result morphism
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder induced_from_morphism :: id -> Map raw_symbol -> sign -> Result morphism
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder induced_from_to_morphism :: id -> Map raw_symbol -> sign -> sign -> Result morphism
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder sublogics :: [Sublogic basic_spec sentence symb_items symb_map_items anno
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder sign morphism symbol raw_symbol]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder included_logic :: String -> String -> Bool
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder provers :: [Prover sentence symbol]
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder cons_checkers :: [Cons_checker (TheoryMorphism sign sentence morphism)]
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder -- derived operations, need not to be given
b06572b54fcf9d6976cfff57da22672f996b4748Christian Maeder -- printing, accessible via logic identity
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder show_basic_spec :: id -> basic_spec -> String
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder show_sentence :: id -> sentence -> String
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder show_symb_items :: id -> symb_items -> String
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder show_symb_map_items :: id -> symb_map_items -> String
b06572b54fcf9d6976cfff57da22672f996b4748Christian Maeder show_anno :: id -> anno -> String
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder show_sign :: id -> sign -> String
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder show_morphism :: id -> morphism -> String
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder show_symbol :: id -> symbol -> String
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder show_raw_symbol :: id -> raw_symbol -> String
b06572b54fcf9d6976cfff57da22672f996b4748Christian Maeder show_basic_spec _ = show
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder show_sentence _ = show
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder show_symb_items _ = show
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder show_symb_map_items _ = show
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder show_anno _ = show
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder show_sign _ = show
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder show_morphism _ = show
84e7cfca5b97aef300acdaa8cf63a3572f9151c0Christian Maeder show_symbol _ = show
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder show_raw_symbol _ = show
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder-- Simple logic representations (possibly also morphisms via adjointness)
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maederdata (Logic id1
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1 anno1
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder sign1 morphism1 symbol1 raw_symbol1,
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2 anno2
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder sign2 morphism2 symbol2 raw_symbol2) =>
38d7048d3410a9c3d0883a00c6c589e7b84e470fChristian Maeder LogicRepr id1 basic_spec1 sentence1 symb_items1 symb_map_items1 anno1 sign1 morphism1 symbol1 raw_symbol1
30e50372105eacc129a413e390e06036735b69b2Christian Maeder id2 basic_spec2 sentence2 symb_items2 symb_map_items2 anno2 sign2 morphism2 symbol2 raw_symbol2
30e50372105eacc129a413e390e06036735b69b2Christian Maeder LogicRepr {repr_name :: String,
30e50372105eacc129a413e390e06036735b69b2Christian Maeder source :: id1,
30e50372105eacc129a413e390e06036735b69b2Christian Maeder target :: id2,
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder map_basic_spec :: basic_spec1->basic_spec2,
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder map_sentence :: sign1 -> sentence1 -> Maybe sentence2, -- also cover semi-representations
99edc5256de959957a8c27b05ae4ad4f0572233dChristian Maeder map_anno :: anno1 -> anno2,
f7663514e02f6095198371a64e574c50e6ec857aChristian Maeder map_sign :: sign1 -> sign2,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder project_sign :: Maybe (sign2 -> sign1,morphism2), -- right adjoint and counit
f7663514e02f6095198371a64e574c50e6ec857aChristian Maeder map_morphism :: morphism1 -> morphism2,
f7663514e02f6095198371a64e574c50e6ec857aChristian Maeder map_symbol :: symbol1 -> symbol2