xref/hets/Logic.hs

	Logic.hs revision 4b479bc5f0136c43d7d7da9502556cb940818efb
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder-- needs ghc -fglasgow-exts
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder{- HetCATS/Logic.hs
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder   $Id$
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder   Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder   Provides data structures for logics (with symbols)
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder   and logic representations. Logics are
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder   a type class with an "identitiy" type (usually interpreted
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   by a singleton set) which serves to treat logics as
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   data. All the functions in the type class take the
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   identity as first argument in order to determine the logic.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   Logic representations are just collections of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   functions between (some of) the types of logics.
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder   References:
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   J. A. Goguen and R. M. Burstall
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   Institutions: Abstract Model Theory for Specification and
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski     Programming
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   JACM 39, p. 95--146, 1992
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   (general notion of logic - model theory only)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   J. Meseguer
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   General Logics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   Logic Colloquium 87, p. 275--329, North Holland, 1989
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   (general notion of logic - also proof theory;
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski    notion of logic representation, called map there)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   T. Mossakowski:
38f350357e92da312d2c344352180b3dc5c1fc8aTill Mossakowski   Specification in an arbitrary institution with symbols
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   14th WADT 1999, LNCS 1827, p. 252--270
425b287f28abf82702d46c176a38b668fb017ce4Felix Reckers   (treatment of symbols and raw symbols, see also CASL semantics)
425b287f28abf82702d46c176a38b668fb017ce4Felix Reckers
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   T. Mossakowski, B. Klin:
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   Institution Independent Static Analysis for CASL
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   15h WADT 2001, LNCS
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder   (what is needed for static anaylsis)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   S. Autexier and T. Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   Integrating HOLCASL into the Development Graph Manager MAYA
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   FroCoS 2002, to appear
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   (interface to provers)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   Todo:
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   Should annotations be globally fixed?
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   Sublanguages more abstractly (lattice)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   Weak amalgamability
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-}
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maedermodule Logic where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski-- maps and sets, just a quick thing
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowskitype Set a = [a]
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowskitype Map a = [(a,a)]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- diagrams, nodes are just integers
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
38f350357e92da312d2c344352180b3dc5c1fc8aTill Mossakowskitype Node = Int
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowskitype Edge morphism = (Node,morphism,Node)
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowskidata Diagram object morphism = Diagram [(Node,object)] [Edge morphism]
9a36df4f63e0214bc0b4aef9b388c8d4e48632bbTill Mossakowskiempty_diagram :: Diagram o m
9a36df4f63e0214bc0b4aef9b388c8d4e48632bbTill Mossakowskiempty_diagram = Diagram [] []
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowskiadd_node :: Diagram o m -> o -> (Node,Diagram o m)
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowskiadd_node (Diagram nodes edges) obj =
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski         (node,Diagram ((node,obj):nodes) edges) where
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski            node = maximum (map fst nodes)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiadd_edge :: Diagram o m -> Edge m -> Diagram o m
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiadd_edge (Diagram nodes edges) edge =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski         Diagram nodes (edge:edges)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiobject_at_node :: Node -> Diagram o m -> Maybe (Node,o)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiobject_at_node node (Diagram nodes edges) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski         case lookup node nodes of
425b287f28abf82702d46c176a38b668fb017ce4Felix Reckers           Just obj -> Just (node,obj)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder           Nothing -> Nothing
425b287f28abf82702d46c176a38b668fb017ce4Felix Reckersdiagram_nodes :: Diagram o m  -> [(Node,o)]
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederdiagram_nodes (Diagram nodes edges) = nodes
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidiagram_edges :: Diagram o m -> [Edge m]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidiagram_edges (Diagram nodes edges) = edges
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski-- identifiers, fixed for all logics
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowskidata ID = Simple_Id String
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder        | Compound_Id (String,[ID])
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- Categories are given by a quotient,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- i.e. we need equality
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- Should we allow arbitrary composition graphs and build paths?
230a51f3c282a3222d1cf40c2040fee19259964eTill Mossakowski
230a51f3c282a3222d1cf40c2040fee19259964eTill Mossakowskiclass (Eq object, Eq morphism) =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski      Category id object morphism | id ->, id -> morphism where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski         ide :: id -> object -> morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski         o :: id -> morphism -> morphism -> Maybe morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski         dom, cod :: id -> morphism -> object
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski         legal_obj :: id -> object -> Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski         legal_mor :: id -> morphism -> Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- abstract syntax, parsing and printing
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiclass (Read basic_spec, Read sentence, Read symb_items,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski       Read symb_map_items, Read anno,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski       Show basic_spec, Show sentence, Show symb_items,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski       Show symb_map_items, Show anno) =>
5e21bb46b24f477dafad6fdeff51aed7aaad0a47Till Mossakowski      Syntax basic_spec sentence symb_items symb_map_items anno
5e21bb46b24f477dafad6fdeff51aed7aaad0a47Till Mossakowski
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski-- sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Sublogic basic_spec sentence symb_items symb_map_items anno
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski              sign morphism symbol raw_symbol =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski     Sublogic {sublogic_name :: String,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski               is_in_basic_spec :: basic_spec -> Bool,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski               is_in_sentence :: sentence -> Bool,
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder               is_in_symb_items :: symb_items -> Bool,
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder               is_in_symb_map_items :: symb_map_items -> Bool,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski               is_in_anno :: anno -> Bool,
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski               is_in_sign :: sign -> Bool,
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder               is_in_morphism :: morphism -> Bool,
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder               is_in_symbol :: symbol -> Bool,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski               is_in_raw_symbol :: raw_symbol -> Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski              }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- theories and theory morphisms
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Theory sign sen =
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder     Theory {sign_of :: sign,
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder             ax_of :: [(String,sen)]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski            }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederdata TheoryMorphism sign sen mor =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski     TheoryMorphism {t_source, t_target :: Theory sign sen,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                     t_morphism :: mor
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                    }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- proofs and provers
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskitype Rule = String
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Proof_tree sen = Axiom sen
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                    | Branch (sen,Rule,[Proof_tree sen])  -- add substitutions here?
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maedertype Tactic_script = String  -- the file name
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Proof_status sen = Open sen
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder                      | Disproved sen
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                      | Proved(sen,[sen],Proof_tree sen,Tactic_script)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Prover sen symbol =
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder     Prover { prover_name :: String,
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski              prover_sublogic :: String,
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski              add_sym :: symbol -> IO(Bool),  -- returns True if succeeded
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski              remove_sym :: symbol -> IO(Bool), -- returns True if succeeded
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski              prove :: sen -> IO([Proof_status sen]) -- proof status for goal and lemmas
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski            }
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowskidata Cons_checker morphism =
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski     Cons_checker {cons_checker_name :: String,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                   cons_checker_sublogic :: String,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                   cons_check :: morphism -> IO(Bool, Tactic_script)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                  }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder-- logics
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiclass (Syntax basic_spec sentence symb_items symb_map_items anno,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski       Show sign, Show morphism, Show symbol, Show raw_symbol,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski       Ord symbol, --  needed for efficient symbol tables
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder       Category id sign morphism) =>
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder      Logic id
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder        basic_spec sentence symb_items symb_map_items anno
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski        sign morphism symbol raw_symbol
38f350357e92da312d2c344352180b3dc5c1fc8aTill Mossakowski        | id -> basic_spec, id -> sentence, id -> symb_items,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski          id -> symb_map_items, id -> anno,
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder          id -> sign, id -> morphism, id ->symbol, id -> raw_symbol
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder       where
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder         -- static analysis of basic specifications and symbol maps
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder         basic_analysis :: id ->
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder                           (basic_spec,sign,[anno]) ->
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder                           (sign,[(String,sentence)])
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder         stat_symb_map_items :: id -> [symb_map_items] -> Map raw_symbol
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder         stat_symb_items :: id -> [symb_items] -> [raw_symbol]
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski         -- architectural sharing analysis for one morphism
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder         ensures_amalgamability :: id ->
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder              (Diagram sign morphism, Node, sign, Edge morphism, morphism) ->
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder               Diagram sign morphism
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder         -- do we need it also for sinks consisting of two morphisms?
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
         -- symbols and symbol maps
         symbol_to_raw :: id -> symbol -> raw_symbol
         id_to_raw :: id -> ID -> raw_symbol
         sym_of :: id -> sign -> Set symbol
         symmap_of :: id -> morphism -> Map symbol
         matches :: id -> symbol -> raw_symbol -> Bool
         name :: id -> symbol -> ID

         -- operations on signatures and morphisms
         empty_signature :: id -> sign
         signature_union :: id -> sign -> sign -> sign
         final_union :: id -> sign -> sign -> sign
         is_subsig :: id -> sign -> sign -> Bool
         generated_sign, cogenerated_sign :: id -> [raw_symbol] -> sign -> morphism
         induced_from_morphism :: id -> Map raw_symbol -> sign -> morphism
         induced_from_to_morphism :: id -> Map raw_symbol -> sign -> sign -> morphism

         -- sublogics
         sublogics :: [Sublogic basic_spec sentence symb_items symb_map_items anno
                       sign morphism symbol raw_symbol]
         included_logic :: String -> String -> Bool

         -- provers
         provers :: [Prover sentence symbol]
         cons_checkers :: [Cons_checker (TheoryMorphism sign sentence morphism)]

         -- derived operations, need not to be given

         -- parsing, printing, accessible via logic identity
         read_basic_spec :: id -> String -> basic_spec
         read_sentence :: id -> String -> sentence
         read_symb_items :: id -> String -> symb_items
         read_symb_map_items :: id -> String -> symb_map_items
         read_anno :: id -> String -> anno

         read_basic_spec _ = read
         read_sentence _ = read
         read_symb_items _ = read
         read_symb_map_items _ = read
         read_anno _ = read

         show_basic_spec :: id -> basic_spec -> String
         show_sentence :: id -> sentence -> String
         show_symb_items :: id -> symb_items -> String
         show_symb_map_items :: id -> symb_map_items -> String
         show_anno :: id -> anno -> String
         show_sign :: id -> sign -> String
         show_morphism :: id -> morphism -> String
         show_symbol :: id -> symbol -> String
         show_raw_symbol :: id -> raw_symbol -> String

         show_basic_spec _ = show
         show_sentence _ = show
         show_symb_items _ = show
         show_symb_map_items _ = show
         show_anno _ = show
         show_sign _ = show
         show_morphism _ = show
         show_symbol _ = show
         show_raw_symbol _ = show


-- Simple logic representations (possibly also morphisms via adjointness)

data (Logic id1
        basic_spec1 sentence1 symb_items1 symb_map_items1 anno1
        sign1 morphism1 symbol1 raw_symbol1,
      Logic id2
        basic_spec2 sentence2 symb_items2 symb_map_items2 anno2
        sign2 morphism2 symbol2 raw_symbol2) =>
  LogicRepr id1 basic_spec1 sentence1 symb_items1 symb_map_items1 anno1 sign1 morphism1 symbol1 raw_symbol1
            id2 basic_spec2 sentence2 symb_items2 symb_map_items2 anno2 sign2 morphism2 symbol2 raw_symbol2
     =
     LogicRepr {source :: id1,
                target :: id2,
                map_basic_spec :: basic_spec1->basic_spec2,
                map_sentence :: sign1 -> sentence1 -> Maybe sentence2, -- also cover semi-representations
                map_anno :: anno1 -> anno2,
                map_sign :: sign1 -> sign2,
                project_sign :: Maybe (sign2 -> sign1,morphism2),  -- right adjoint and counit
                map_morphism :: morphism1 -> morphism2,
                map_symbol :: symbol1 -> symbol2
               }

-- Composition of representations is defined in LogicGraph