Logic.hs revision f586a20f0d391470365243cc1405af39c92c6372
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
44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowski data. All the functions in the type class take the
44fb55f639914f4f531641f32dd4904f15c510a4Till 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
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski JACM 39, p. 95--146, 1992
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (general notion of logic - model theory only)
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski
ae7058143db9e9993b5eff70bd6b7aede7cec658Till 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)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski T. Mossakowski:
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder Specification in an arbitrary institution with symbols
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski 14th WADT 1999, LNCS 1827, p. 252--270
9e2e744c6b967c3f5f581acf01c13769b6769285Till Mossakowski (treatment of symbols and raw symbols, see also CASL semantics)
38f350357e92da312d2c344352180b3dc5c1fc8aTill Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski T. Mossakowski, B. Klin:
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder Institution Independent Static Analysis for CASL
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski 15h WADT 2001, LNCS
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (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 ATerm, XML
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Sublanguages more abstractly (lattice), projs
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder Weak amalgamability
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder Metavars
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski extension of morphisms wrt. compound ids
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski-}
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskimodule Logic where
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowskiimport Id
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowskiimport Error
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski-- maps and sets, just a quick thing
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskitype Set a = [a]
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till 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 =
62867c8459918ce0a96960093eb43d758b97a603Till 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
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski Just obj -> Just (node,obj)
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski Nothing -> Nothing
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowskidiagram_nodes :: Diagram o m -> [(Node,o)]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidiagram_nodes (Diagram nodes edges) = nodes
586af0e9490a14dd3075095692b584c652584875Till Mossakowskidiagram_edges :: Diagram o m -> [Edge m]
586af0e9490a14dd3075095692b584c652584875Till Mossakowskidiagram_edges (Diagram nodes edges) = edges
933baca0720dae81434de384b32a93b47e754d09Christian Maeder
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski-- Categories are given by a quotient,
933baca0720dae81434de384b32a93b47e754d09Christian Maeder-- i.e. we need equality
586af0e9490a14dd3075095692b584c652584875Till Mossakowski-- Should we allow arbitrary composition graphs and build paths?
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till 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
586af0e9490a14dd3075095692b584c652584875Till Mossakowski dom, cod :: id -> morphism -> object
586af0e9490a14dd3075095692b584c652584875Till Mossakowski legal_obj :: id -> object -> Bool
933baca0720dae81434de384b32a93b47e754d09Christian Maeder legal_mor :: id -> morphism -> Bool
933baca0720dae81434de384b32a93b47e754d09Christian Maeder
933baca0720dae81434de384b32a93b47e754d09Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- abstract syntax, parsing and printing
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiclass (Show basic_spec, Show sentence, Show symb_items,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Show symb_map_items, Show anno) =>
586af0e9490a14dd3075095692b584c652584875Till Mossakowski Syntax basic_spec sentence symb_items symb_map_items anno
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- parsing
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski parse_basic_spec :: id -> String -> Result basic_spec
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski parse_sentence :: id -> String -> Result sentence
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski parse_symb_items :: id -> String -> Result symb_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski parse_symb_map_items :: id -> String -> Result symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski parse_anno :: id -> String -> Result anno
933baca0720dae81434de384b32a93b47e754d09Christian Maeder
933baca0720dae81434de384b32a93b47e754d09Christian Maeder
933baca0720dae81434de384b32a93b47e754d09Christian Maeder-- sublogics
933baca0720dae81434de384b32a93b47e754d09Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Sublogic basic_spec sentence symb_items symb_map_items anno
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign local_env morphism symbol raw_symbol =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Sublogic {sublogic_name :: String,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski is_in_basic_spec :: basic_spec -> Bool,
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski is_in_sentence :: sentence -> Bool,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski is_in_symb_items :: symb_items -> Bool,
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder is_in_symb_map_items :: symb_map_items -> Bool,
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder is_in_anno :: anno -> Bool,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski is_in_sign :: sign -> Bool,
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski is_in_morphism :: morphism -> Bool,
933baca0720dae81434de384b32a93b47e754d09Christian Maeder is_in_symbol :: symbol -> Bool,
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder is_in_raw_symbol :: raw_symbol -> Bool
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- theories and theory morphisms
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Theory sign sen =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Theory {sign_of :: sign,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ax_of :: [(String,sen)]
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder }
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata TheoryMorphism sign sen mor =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski TheoryMorphism {t_source, t_target :: Theory sign sen,
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder t_morphism :: mor
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- proofs and provers
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskitype Rule = String
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Proof_tree sen = Axiom sen
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | Branch (sen,Rule,[Proof_tree sen]) -- add substitutions here?
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskitype Tactic_script = String -- the file name
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederdata Proof_status sen = Open sen
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | Disproved sen
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | Proved(sen,[sen],Proof_tree sen,Tactic_script)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Prover sen symbol =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Prover { prover_name :: String,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski prover_sublogic :: String,
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder 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
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski }
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowskidata Cons_checker morphism =
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski Cons_checker {cons_checker_name :: String,
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski cons_checker_sublogic :: String,
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski cons_check :: morphism -> IO(Bool, Tactic_script)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- logics
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowskiclass (Syntax basic_spec sentence symb_items symb_map_items anno,
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder Show sign, Show morphism, Show symbol, Show raw_symbol,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Ord symbol, -- needed for efficient symbol tables
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Category id sign morphism) =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic id
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski basic_spec sentence symb_items symb_map_items anno
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski local_env sign morphism symbol raw_symbol
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder | id -> basic_spec, id -> sentence, id -> symb_items,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski id -> symb_map_items, id -> anno, id -> local_env,
38f350357e92da312d2c344352180b3dc5c1fc8aTill Mossakowski id -> sign, id -> morphism, id ->symbol, id -> raw_symbol
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski where
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder logic_name :: id -> String
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder has_parser :: id -> Bool
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder has_printer :: id -> Bool
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski has_analysis :: id -> Bool
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder -- sentence translation
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder map_sen :: id -> morphism -> sentence -> Result sentence
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder -- static analysis of basic specifications and symbol maps
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski basic_analysis :: id ->
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski (basic_spec, -- abstract syntax tree
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder local_env, -- efficient table for env signature
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski [anno]) -> -- global annotations
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder Result (sign,[(String,sentence)])
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski stat_symb_map_items :: id -> [symb_map_items] -> Result (Map raw_symbol)
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski stat_symb_items :: id -> [symb_items] -> Result [raw_symbol]
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder -- architectural sharing analysis for one morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ensures_amalgamability :: id ->
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski (Diagram sign morphism, Node, sign, Edge morphism, morphism) ->
933baca0720dae81434de384b32a93b47e754d09Christian Maeder Result (Diagram sign morphism)
-- do we need it also for sinks consisting of two morphisms?
-- 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
sym_name :: id -> symbol -> Id
-- operations on local envs, signatures and morphisms
empty_local_env :: local_env
add_sign :: sign -> local_env -> local_env
empty_signature :: id -> sign
signature_union :: id -> sign -> sign -> Result sign
final_union :: id -> sign -> sign -> Result sign
is_subsig :: id -> sign -> sign -> Bool
generated_sign, cogenerated_sign :: id -> [raw_symbol] -> sign -> Result morphism
induced_from_morphism :: id -> Map raw_symbol -> sign -> Result morphism
induced_from_to_morphism :: id -> Map raw_symbol -> sign -> sign -> Result morphism
-- sublogics
sublogics :: [Sublogic basic_spec sentence symb_items symb_map_items anno
local_env 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
-- printing, accessible via logic identity
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
local_env1 sign1 morphism1 symbol1 raw_symbol1,
Logic id2
basic_spec2 sentence2 symb_items2 symb_map_items2 anno2
local_env2 sign2 morphism2 symbol2 raw_symbol2) =>
LogicRepr id1 basic_spec1 sentence1 symb_items1 symb_map_items1 anno1
local_env1 sign1 morphism1 symbol1 raw_symbol1
id2 basic_spec2 sentence2 symb_items2 symb_map_items2 anno2
local_env2 sign2 morphism2 symbol2 raw_symbol2
=
LogicRepr {repr_name :: String,
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
}