ExtSign.hs revision 42e78fd3454812d4f98b06154fdabc5ec3488718
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
a8f3e7d86a5088f48b23249a932a1d0259ed3cd1Felix Gabriel ManceDescription : derived functions for signatures with symbol sets
a8f3e7d86a5088f48b23249a932a1d0259ed3cd1Felix Gabriel ManceCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2006
a8f3e7d86a5088f48b23249a932a1d0259ed3cd1Felix Gabriel ManceLicense : GPLv2 or higher, see LICENSE.txt
a8f3e7d86a5088f48b23249a932a1d0259ed3cd1Felix Gabriel ManceMaintainer : till@informatik.uni-bremen.de
a8f3e7d86a5088f48b23249a932a1d0259ed3cd1Felix Gabriel ManceStability : provisional
a8f3e7d86a5088f48b23249a932a1d0259ed3cd1Felix Gabriel MancePortability : non-portable (imports Logic.Logic)
eeac8845adce2ed666f019575596a647876b8771Felix Gabriel ManceFunctions from the class Logic that operate over signatures are
a8f3e7d86a5088f48b23249a932a1d0259ed3cd1Felix Gabriel Manceextended to work over signatures with symbol sets.
fb59be47d4ce4feb5398be4f6e77cad3c37c673bChristian Maederimport qualified Data.Set as Set
fb59be47d4ce4feb5398be4f6e77cad3c37c673bChristian Maederimport qualified Data.Map as Map
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceext_sym_of :: Logic lid sublogics
0971dd6c0389ce5219e4cfa6dcb8d6e5db502917Felix Gabriel Mance basic_spec sentence symb_items symb_map_items
0971dd6c0389ce5219e4cfa6dcb8d6e5db502917Felix Gabriel Mance sign morphism symbol raw_symbol proof_tree
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance => lid -> ExtSign sign symbol -> Set.Set symbol
c7b3ce5a2a1f81bfa99845d00c33f75252329f74Felix Gabriel Manceext_sym_of l = symset_of l . plainSign
a0f0d960eb205b61206643ff75ec170802e3fa00Felix Gabriel Mance-- | simply put all symbols into the symbol set
25ad27f18cf93dc1980b27fe6e9285c5f221f750Felix Gabriel MancemakeExtSign :: Logic lid sublogics
25ad27f18cf93dc1980b27fe6e9285c5f221f750Felix Gabriel Mance basic_spec sentence symb_items symb_map_items
74a7d4dbf06c32e346a79f9e6f39dae2b7c33939Christian Maeder sign morphism symbol raw_symbol proof_tree
74a7d4dbf06c32e346a79f9e6f39dae2b7c33939Christian Maeder => lid -> sign -> ExtSign sign symbol
76db6b749bcfc39d72fbc6fb4d2f9e41e7fe15c4Felix Gabriel MancemakeExtSign l s = -- trace ("symset:" ++ show (symset_of l s)) $
76db6b749bcfc39d72fbc6fb4d2f9e41e7fe15c4Felix Gabriel Mance ExtSign s $ symset_of l s
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceext_ide :: (Ord symbol, Category sign morphism)
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance => ExtSign sign symbol -> morphism
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceext_ide = ide . plainSign
d4ec1718f8dafa9743d3e60c0715644c15bcd834Felix Gabriel Manceext_empty_signature :: Logic lid sublogics
d4ec1718f8dafa9743d3e60c0715644c15bcd834Felix Gabriel Mance basic_spec sentence symb_items symb_map_items
22a0bc45b22397199459c4b56e0e770f44a0f34aFelix Gabriel Mance sign morphism symbol raw_symbol proof_tree
d4ec1718f8dafa9743d3e60c0715644c15bcd834Felix Gabriel Mance => lid -> ExtSign sign symbol
d4ec1718f8dafa9743d3e60c0715644c15bcd834Felix Gabriel Manceext_empty_signature = mkExtSign . empty_signature
d4ec1718f8dafa9743d3e60c0715644c15bcd834Felix Gabriel MancecheckExtSign :: Logic lid sublogics
962477e877e546f2073cc6fbd1bc18a12eb0589bFelix Gabriel Mance basic_spec sentence symb_items symb_map_items
ac132ecf49c479a92236d0bfdfdb7ae59e75c992Felix Gabriel Mance sign morphism symbol raw_symbol proof_tree
962477e877e546f2073cc6fbd1bc18a12eb0589bFelix Gabriel Mance => lid -> String -> ExtSign sign symbol -> Result ()
962477e877e546f2073cc6fbd1bc18a12eb0589bFelix Gabriel MancecheckExtSign l msg e@(ExtSign s sy) = let sys = symset_of l s in
ac132ecf49c479a92236d0bfdfdb7ae59e75c992Felix Gabriel Mance unless (Set.isSubsetOf sy sys) $
962477e877e546f2073cc6fbd1bc18a12eb0589bFelix Gabriel Mance error $ "inconsistent symbol set in extended signature: " ++ msg ++ "\n"
25ad27f18cf93dc1980b27fe6e9285c5f221f750Felix Gabriel Mance ++ showDoc e "\rwith unknown symbols\n"
1ea1794fe8bebbd2d807240f9ea9a7217f5fb75fChristian Maeder ++ showDoc (Set.difference sy sys) ""
25ad27f18cf93dc1980b27fe6e9285c5f221f750Felix Gabriel Manceext_signature_union :: Logic lid sublogics
5e8db9d910a9fa441c3d4701899841fc8889e011Felix Gabriel Mance basic_spec sentence symb_items symb_map_items
962477e877e546f2073cc6fbd1bc18a12eb0589bFelix Gabriel Mance sign morphism symbol raw_symbol proof_tree
962477e877e546f2073cc6fbd1bc18a12eb0589bFelix Gabriel Mance => lid -> ExtSign sign symbol -> ExtSign sign symbol
962477e877e546f2073cc6fbd1bc18a12eb0589bFelix Gabriel Mance -> Result (ExtSign sign symbol)
5e8db9d910a9fa441c3d4701899841fc8889e011Felix Gabriel Manceext_signature_union l e1@(ExtSign s1 _) e2@(ExtSign s2 _) = do
962477e877e546f2073cc6fbd1bc18a12eb0589bFelix Gabriel Mance checkExtSign l "u1" e1
962477e877e546f2073cc6fbd1bc18a12eb0589bFelix Gabriel Mance checkExtSign l "u2" e2
962477e877e546f2073cc6fbd1bc18a12eb0589bFelix Gabriel Mance s <- signature_union l s1 s2
5e8db9d910a9fa441c3d4701899841fc8889e011Felix Gabriel Mance return $ makeExtSign l s
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceext_signature_intersect :: Logic lid sublogics
f008d37d7fd3b2394a717ac3561f5f1982bb0b28Felix Gabriel Mance basic_spec sentence symb_items symb_map_items
a0f0d960eb205b61206643ff75ec170802e3fa00Felix Gabriel Mance sign morphism symbol raw_symbol proof_tree
5e8db9d910a9fa441c3d4701899841fc8889e011Felix Gabriel Mance => lid -> ExtSign sign symbol -> ExtSign sign symbol
a0f0d960eb205b61206643ff75ec170802e3fa00Felix Gabriel Mance -> Result (ExtSign sign symbol)
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceext_signature_intersect l e1@(ExtSign s1 _) e2@(ExtSign s2 _) = do
f008d37d7fd3b2394a717ac3561f5f1982bb0b28Felix Gabriel Mance checkExtSign l "u1" e1
a0f0d960eb205b61206643ff75ec170802e3fa00Felix Gabriel Mance checkExtSign l "u2" e2
5e8db9d910a9fa441c3d4701899841fc8889e011Felix Gabriel Mance s <- intersection l s1 s2
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance -- trace ("ext_intersect:" ++ show s) $
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance return $ makeExtSign l s
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiext_is_subsig :: Logic lid sublogics
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski basic_spec sentence symb_items symb_map_items
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski sign morphism symbol raw_symbol proof_tree
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski => lid -> ExtSign sign symbol -> ExtSign sign symbol -> Bool
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiext_is_subsig l (ExtSign sig1 _) (ExtSign sig2 _) =
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski is_subsig l sig1 sig2
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiext_final_union :: Logic lid sublogics
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski basic_spec sentence symb_items symb_map_items
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski sign morphism symbol raw_symbol proof_tree
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance => lid -> ExtSign sign symbol -> ExtSign sign symbol
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance -> Result (ExtSign sign symbol)
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceext_final_union l e1@(ExtSign s1 _) e2@(ExtSign s2 _) = do
68e123352da63f918c8ba230b04533de3d796699Felix Gabriel Mance checkExtSign l "f1" e1
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance checkExtSign l "f2" e2
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski s <- final_union l s1 s2
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski return $ makeExtSign l s
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiext_inclusion :: Logic lid sublogics
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski basic_spec sentence symb_items symb_map_items
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance sign morphism symbol raw_symbol proof_tree
5e8db9d910a9fa441c3d4701899841fc8889e011Felix Gabriel Mance => lid -> ExtSign sign symbol -> ExtSign sign symbol -> Result morphism
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceext_inclusion l (ExtSign s1 _) (ExtSign s2 _) =
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski inclusion l s1 s2
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiext_generated_sign :: Logic lid sublogics
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski basic_spec sentence symb_items symb_map_items
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski sign morphism symbol raw_symbol proof_tree
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski => lid -> Set.Set symbol -> ExtSign sign symbol -> Result morphism
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiext_generated_sign l s (ExtSign sig _) =
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski generated_sign l s sig
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiext_cogenerated_sign :: Logic lid sublogics
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski basic_spec sentence symb_items symb_map_items
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance sign morphism symbol raw_symbol proof_tree
5e8db9d910a9fa441c3d4701899841fc8889e011Felix Gabriel Mance => lid -> Set.Set symbol -> ExtSign sign symbol -> Result morphism
771c32080c77497c6c023a3b1c422f7daf3773f7Felix Gabriel Manceext_cogenerated_sign l s (ExtSign sig _) =
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski cogenerated_sign l s sig
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceext_induced_from_morphism :: Logic lid sublogics
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski basic_spec sentence symb_items symb_map_items
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski sign morphism symbol raw_symbol proof_tree
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski => lid -> EndoMap raw_symbol -> ExtSign sign symbol
68e123352da63f918c8ba230b04533de3d796699Felix Gabriel Mance -> Result morphism
b9a7827caf331ae5b7eb491455d7e647c83f1345Christian Maederext_induced_from_morphism l rmap (ExtSign sigma _) = do
b9a7827caf331ae5b7eb491455d7e647c83f1345Christian Maeder -- first check: do all source raw symbols match with source signature?
b9a7827caf331ae5b7eb491455d7e647c83f1345Christian Maeder checkRawMap l rmap sigma
b9a7827caf331ae5b7eb491455d7e647c83f1345Christian Maeder mor <- induced_from_morphism l rmap sigma
b9a7827caf331ae5b7eb491455d7e647c83f1345Christian Maeder legal_mor mor
b9a7827caf331ae5b7eb491455d7e647c83f1345Christian MaedercheckRawMap :: Logic lid sublogics
5e8db9d910a9fa441c3d4701899841fc8889e011Felix Gabriel Mance basic_spec sentence symb_items symb_map_items
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance sign morphism symbol raw_symbol proof_tree
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance => lid -> EndoMap raw_symbol -> sign -> Result ()
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel MancecheckRawMap l rmap = checkRawSyms l (Map.keys rmap) . symset_of l
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel MancecheckRawSyms :: Logic lid sublogics
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski basic_spec sentence symb_items symb_map_items
f008d37d7fd3b2394a717ac3561f5f1982bb0b28Felix Gabriel Mance sign morphism symbol raw_symbol proof_tree
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski => lid -> [raw_symbol] -> Set.Set symbol -> Result ()
80875f917d741946a39d0ec0b5721e46ba609823Till MossakowskicheckRawSyms l rsyms syms = do
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski let unknownSyms = filter
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance ( \ rsy -> Set.null $ Set.filter (flip (matches l) rsy) syms)
5e8db9d910a9fa441c3d4701899841fc8889e011Felix Gabriel Mance unless (null unknownSyms)
68e123352da63f918c8ba230b04533de3d796699Felix Gabriel Mance $ Result [mkDiag Error "unknown symbols" unknownSyms] $ Just ()
8a4f6f9f7eeaa5ed86a77ea1676c10ecd2bc9442Christian Maederext_induced_from_to_morphism :: Logic lid sublogics
8a4f6f9f7eeaa5ed86a77ea1676c10ecd2bc9442Christian Maeder basic_spec sentence symb_items symb_map_items
8a4f6f9f7eeaa5ed86a77ea1676c10ecd2bc9442Christian Maeder sign morphism symbol raw_symbol proof_tree
8a4f6f9f7eeaa5ed86a77ea1676c10ecd2bc9442Christian Maeder => lid -> EndoMap raw_symbol -> ExtSign sign symbol
68e123352da63f918c8ba230b04533de3d796699Felix Gabriel Mance -> ExtSign sign symbol -> Result morphism
68e123352da63f918c8ba230b04533de3d796699Felix Gabriel Manceext_induced_from_to_morphism l r s@(ExtSign p sy) t = do
8a4f6f9f7eeaa5ed86a77ea1676c10ecd2bc9442Christian Maeder checkExtSign l "from" s
68e123352da63f918c8ba230b04533de3d796699Felix Gabriel Mance checkExtSign l "to" t
5e8db9d910a9fa441c3d4701899841fc8889e011Felix Gabriel Mance checkRawMap l r p
68e123352da63f918c8ba230b04533de3d796699Felix Gabriel Mance checkRawSyms l (Map.elems r) $ nonImportedSymbols t
68e123352da63f918c8ba230b04533de3d796699Felix Gabriel Mance mor <- induced_from_to_morphism l r s t
68e123352da63f918c8ba230b04533de3d796699Felix Gabriel Mance let sysI = Set.toList $ Set.difference (symset_of l p) sy
0b4abe255a45398b8451bf5df821277c3cbbfc01Felix Gabriel Mance morM = symmap_of l mor
1ea1794fe8bebbd2d807240f9ea9a7217f5fb75fChristian Maeder msysI = map (\ sym -> Map.findWithDefault sym sym morM) sysI
1ea1794fe8bebbd2d807240f9ea9a7217f5fb75fChristian Maeder unless (sysI == msysI)
0b4abe255a45398b8451bf5df821277c3cbbfc01Felix Gabriel Mance $ fail $ "imported symbols are mapped differently.\n"
771c32080c77497c6c023a3b1c422f7daf3773f7Felix Gabriel Mance ++ showDoc (filter (uncurry (/=)) $ zip sysI msysI) ""
7852de3551fc797566ee71165bafe05b6d81728cnotanartist legal_mor mor