f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederDescription : derived functions for signatures with symbol sets
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederMaintainer : till@informatik.uni-bremen.de
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederStability : provisional
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederPortability : non-portable (imports Logic.Logic)
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederFunctions from the class Logic that operate over signatures are
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maederextended to work over signatures with symbol sets.
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Data.Set as Set
64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport qualified Data.Map as Map
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederext_sym_of :: Logic lid sublogics
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder basic_spec sentence symb_items symb_map_items
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign morphism symbol raw_symbol proof_tree
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder => lid -> ExtSign sign symbol -> Set.Set symbol
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulzext_sym_of l = symset_of l . plainSign
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder-- | simply put all symbols into the symbol set
64e1905404e5135e98a26d2ab4150b6764956576Christian MaedermakeExtSign :: Logic lid sublogics
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder basic_spec sentence symb_items symb_map_items
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder sign morphism symbol raw_symbol proof_tree
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder => lid -> sign -> ExtSign sign symbol
d5a225e7c58f6a8ab7b5acda22841784a19e261fmcodescumakeExtSign l s = ExtSign s $ symset_of l s
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maederext_ide :: (Ord symbol, Category sign morphism)
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder => ExtSign sign symbol -> morphism
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maederext_ide = ide . plainSign
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederext_empty_signature :: Logic lid sublogics
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder basic_spec sentence symb_items symb_map_items
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign morphism symbol raw_symbol proof_tree
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder => lid -> ExtSign sign symbol
083a5256468076d5a9bfeb22a6e97076c224252eChristian Maederext_empty_signature = mkExtSign . empty_signature
64e1905404e5135e98a26d2ab4150b6764956576Christian MaedercheckExtSign :: Logic lid sublogics
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder basic_spec sentence symb_items symb_map_items
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder sign morphism symbol raw_symbol proof_tree
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder => lid -> String -> ExtSign sign symbol -> Result ()
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzcheckExtSign l msg e@(ExtSign s sy) = let sys = symset_of l s in
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder unless (Set.isSubsetOf sy sys) $
65dce48b81f69e11a36bf1051314a845299446e1Christian Maeder error $ "inconsistent symbol set in extended signature: " ++ msg ++ "\n"
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder ++ showDoc e "\rwith unknown symbols\n"
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder ++ showDoc (Set.difference sy sys) ""
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederext_signature_union :: Logic lid sublogics
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder basic_spec sentence symb_items symb_map_items
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign morphism symbol raw_symbol proof_tree
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder => lid -> ExtSign sign symbol -> ExtSign sign symbol
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -> Result (ExtSign sign symbol)
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maederext_signature_union l e1@(ExtSign s1 _) e2@(ExtSign s2 _) = do
431eff6083370269f3a37767bcde001f389ac927mcodescu checkExtSign l "ext_signature_union_1" e1
431eff6083370269f3a37767bcde001f389ac927mcodescu checkExtSign l "ext_signature_union_2" e2
62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder s <- signature_union l s1 s2
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder return $ makeExtSign l s
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuext_signature_intersect :: Logic lid sublogics
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu basic_spec sentence symb_items symb_map_items
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu sign morphism symbol raw_symbol proof_tree
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu => lid -> ExtSign sign symbol -> ExtSign sign symbol
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu -> Result (ExtSign sign symbol)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuext_signature_intersect l e1@(ExtSign s1 _) e2@(ExtSign s2 _) = do
431eff6083370269f3a37767bcde001f389ac927mcodescu checkExtSign l "ext_signature_intersect_1" e1
431eff6083370269f3a37767bcde001f389ac927mcodescu checkExtSign l "ext_signature_intersect_2" e2
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu s <- intersection l s1 s2
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu return $ makeExtSign l s
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederext_is_subsig :: Logic lid sublogics
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder basic_spec sentence symb_items symb_map_items
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign morphism symbol raw_symbol proof_tree
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder => lid -> ExtSign sign symbol -> ExtSign sign symbol -> Bool
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederext_is_subsig l (ExtSign sig1 _) (ExtSign sig2 _) =
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder is_subsig l sig1 sig2
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederext_final_union :: Logic lid sublogics
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder basic_spec sentence symb_items symb_map_items
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign morphism symbol raw_symbol proof_tree
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder => lid -> ExtSign sign symbol -> ExtSign sign symbol
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -> Result (ExtSign sign symbol)
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maederext_final_union l e1@(ExtSign s1 _) e2@(ExtSign s2 _) = do
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder checkExtSign l "f1" e1
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder checkExtSign l "f2" e2
62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder s <- final_union l s1 s2
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder return $ makeExtSign l s
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederext_inclusion :: Logic lid sublogics
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder basic_spec sentence symb_items symb_map_items
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign morphism symbol raw_symbol proof_tree
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder => lid -> ExtSign sign symbol -> ExtSign sign symbol -> Result morphism
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederext_inclusion l (ExtSign s1 _) (ExtSign s2 _) =
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder inclusion l s1 s2
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederext_generated_sign :: Logic lid sublogics
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder basic_spec sentence symb_items symb_map_items
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign morphism symbol raw_symbol proof_tree
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder => lid -> Set.Set symbol -> ExtSign sign symbol -> Result morphism
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederext_generated_sign l s (ExtSign sig _) =
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder generated_sign l s sig
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederext_cogenerated_sign :: Logic lid sublogics
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder basic_spec sentence symb_items symb_map_items
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign morphism symbol raw_symbol proof_tree
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder => lid -> Set.Set symbol -> ExtSign sign symbol -> Result morphism
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederext_cogenerated_sign l s (ExtSign sig _) =
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder cogenerated_sign l s sig
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederext_induced_from_morphism :: Logic lid sublogics
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder basic_spec sentence symb_items symb_map_items
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign morphism symbol raw_symbol proof_tree
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder => lid -> EndoMap raw_symbol -> ExtSign sign symbol
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -> Result morphism
ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maederext_induced_from_morphism l rmap (ExtSign sigma _) = do
ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder -- first check: do all source raw symbols match with source signature?
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder checkRawMap l rmap sigma
935613eb8e67d724f1c4a4d4a37be3324ef6708dChristian Maeder mor <- induced_from_morphism l rmap sigma
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder legal_mor mor
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian MaedercheckRawMap :: Logic lid sublogics
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder basic_spec sentence symb_items symb_map_items
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder sign morphism symbol raw_symbol proof_tree
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder => lid -> EndoMap raw_symbol -> sign -> Result ()
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzcheckRawMap l rmap = checkRawSyms l (Map.keys rmap) . symset_of l
083a5256468076d5a9bfeb22a6e97076c224252eChristian MaedercheckRawSyms :: Logic lid sublogics
083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder basic_spec sentence symb_items symb_map_items
083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder sign morphism symbol raw_symbol proof_tree
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder => lid -> [raw_symbol] -> Set.Set symbol -> Result ()
083a5256468076d5a9bfeb22a6e97076c224252eChristian MaedercheckRawSyms l rsyms syms = do
083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder let unknownSyms = filter
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder ( \ rsy -> Set.null $ Set.filter (flip (matches l) rsy) syms)
083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder unless (null unknownSyms)
392b67dbb9414475750ac2a977348de77354c600Christian Maeder $ Result [mkDiag Error "unknown symbols" unknownSyms] $ Just ()
de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maederext_induced_from_to_morphism :: Logic lid sublogics
de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder basic_spec sentence symb_items symb_map_items
de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder sign morphism symbol raw_symbol proof_tree
de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder => lid -> EndoMap raw_symbol -> ExtSign sign symbol
de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder -> ExtSign sign symbol -> Result morphism
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maederext_induced_from_to_morphism l r s@(ExtSign p sy) t = do
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder checkExtSign l "from" s
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder checkExtSign l "to" t
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder checkRawMap l r p
083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder checkRawSyms l (Map.elems r) $ nonImportedSymbols t
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder mor <- induced_from_to_morphism l r s t
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz let sysI = Set.toList $ Set.difference (symset_of l p) sy
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder morM = symmap_of l mor
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder msysI = map (\ sym -> Map.findWithDefault sym sym morM) sysI
6d4d212092e2edb139e0907a14e87c4df74ff06aChristian Maeder unless (sysI == msysI)
6d4d212092e2edb139e0907a14e87c4df74ff06aChristian Maeder $ fail $ "imported symbols are mapped differently.\n"
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder ++ showDoc (filter (uncurry (/=)) $ zip sysI msysI) ""
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder legal_mor mor