ExtSign.hs revision 4033572ba385cee056cbeb07461382cf5a709295
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederModule : $Header$
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederDescription : signatures with symbol sets
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaederCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2006
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederMaintainer : till@informatik.uni-bremen.de
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiStability : provisional
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : non-portable (imports Logic.Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederThose functions that operate over signatures are extended to work over
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maedersignatures with symbol sets
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport qualified Data.Set as Set
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | signatures with symbol sets.
922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder-- (The Ord instance is needed for the ATC generation)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederdata Ord symbol => ExtSign sign symbol = ExtSign
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder { plainSign :: sign
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder , nonImportedSymbols :: (Set.Set symbol)
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder } deriving Show
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maederinstance (Ord symbol, Eq sign) => Eq (ExtSign sign symbol) where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ExtSign s1 _ == ExtSign s2 _ = s1 == s2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimkExtSign :: Ord symbol => sign -> ExtSign sign symbol
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimkExtSign s = ExtSign s Set.empty
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiext_sym_of :: Logic lid sublogics
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski => lid -> (ExtSign sign symbol) -> Set.Set symbol
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiext_sym_of l = sym_of l . plainSign
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiext_ide :: Logic lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder sign morphism symbol raw_symbol proof_tree
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski => lid -> (ExtSign sign symbol) -> morphism
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskiext_ide l = ide l . plainSign
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowskiext_empty_signature :: Logic lid sublogics
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski basic_spec sentence symb_items symb_map_items
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski sign morphism symbol raw_symbol proof_tree
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski => lid -> (ExtSign sign symbol)
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskiext_empty_signature l = mkExtSign (empty_signature l)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiext_signature_union :: Logic lid sublogics
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski => lid -> (ExtSign sign symbol) -> (ExtSign sign symbol)
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder -> Result (ExtSign sign symbol)
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maederext_signature_union l (ExtSign s1 sy1) (ExtSign s2 sy2) = do
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder s <- signature_union l s1 s2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski return $ ExtSign s $ Set.union sy1 sy2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiext_signature_difference :: Logic lid sublogics
0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder basic_spec sentence symb_items symb_map_items
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu sign morphism symbol raw_symbol proof_tree
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu => lid -> (ExtSign sign symbol) -> (ExtSign sign symbol)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu -> Result (ExtSign sign symbol)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescuext_signature_difference l (ExtSign s1 sy1) (ExtSign s2 sy2) = do
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu s <- signature_difference l s1 s2
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu return $ ExtSign s $ Set.difference sy1 sy2
f2c050360525df494e6115073b0edc4c443a847cMihai Codescuext_is_subsig :: Logic lid sublogics
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu basic_spec sentence symb_items symb_map_items
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu sign morphism symbol raw_symbol proof_tree
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu => lid -> (ExtSign sign symbol) -> (ExtSign sign symbol) -> Bool
f2c050360525df494e6115073b0edc4c443a847cMihai Codescuext_is_subsig l (ExtSign sig1 _) (ExtSign sig2 _) =
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu is_subsig l sig1 sig2
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowskiext_final_union :: Logic lid sublogics
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder => lid -> (ExtSign sign symbol) -> (ExtSign sign symbol)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -> Result (ExtSign sign symbol)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederext_final_union l (ExtSign s1 sy1) (ExtSign s2 sy2) = do
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder s <- final_union l s1 s2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder return $ ExtSign s $ Set.union sy1 sy2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederext_inclusion :: Logic lid sublogics
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder basic_spec sentence symb_items symb_map_items
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder sign morphism symbol raw_symbol proof_tree
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder => lid -> (ExtSign sign symbol) -> (ExtSign sign symbol)
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -> Result morphism
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maederext_inclusion l (ExtSign s1 _) (ExtSign s2 _) =
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder inclusion l s1 s2
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maederext_generated_sign :: Logic lid sublogics
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder basic_spec sentence symb_items symb_map_items
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sign morphism symbol raw_symbol proof_tree
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder => lid -> Set.Set symbol -> (ExtSign sign symbol) -> Result morphism
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederext_generated_sign l s (ExtSign sig _) =
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder generated_sign l s sig
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederext_cogenerated_sign :: Logic lid sublogics
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder basic_spec sentence symb_items symb_map_items
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign morphism symbol raw_symbol proof_tree
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder => lid -> Set.Set symbol -> (ExtSign sign symbol) -> Result morphism
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederext_cogenerated_sign l s (ExtSign sig _) =
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder cogenerated_sign l s sig
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederext_induced_from_morphism :: Logic lid sublogics
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder basic_spec sentence symb_items symb_map_items
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign morphism symbol raw_symbol proof_tree
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder => lid -> EndoMap raw_symbol -> (ExtSign sign symbol)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -> Result morphism
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederext_induced_from_morphism l r (ExtSign s _) =
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder induced_from_morphism l r s
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederext_induced_from_to_morphism :: Logic lid sublogics
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder basic_spec sentence symb_items symb_map_items
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign morphism symbol raw_symbol proof_tree
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder => lid -> EndoMap raw_symbol -> (ExtSign sign symbol)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -> (ExtSign sign symbol) -> Result morphism
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederext_induced_from_to_morphism l r (ExtSign s1 _) (ExtSign s2 _) =
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder induced_from_to_morphism l r s1 s2