Coerce.hs revision 0095c7efbddd0ffeed6aaf8ec015346be161d819
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederModule : $Header$
73dfcef93ee2ba07fedf4f3c74bace31853d1b9fChristian MaederCopyright : (c) T. Mossakowski, C. Maeder, Uni Bremen 2005-2006
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederMaintainer : till@tzi.de
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederStability : provisional
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederPortability : non-portable (various -fglasgow-exts extensions)
0095c7efbddd0ffeed6aaf8ec015346be161d819Till MossakowskiDescription : tell the typechecker that things dynamically belong to the same logic
0095c7efbddd0ffeed6aaf8ec015346be161d819Till Mossakowski for coercion used in Grothendieck.hs and Analysis modules
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport qualified Common.Lib.Set as Set
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- coercion using the language name
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederprimCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2,
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Monad m) => lid1 -> lid2 -> String -> a -> m b
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaederprimCoerce i1 i2 err a =
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder if language_name i1 == language_name i2
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder then return $ fromDyn (toDyn a) $ error "mcoerce"
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder else fail (err1++"Logic "++ language_name i1 ++ " expected, but "
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder ++ language_name i2 ++ " found")
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder where err1 = if err=="" then "" else err++": "
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederunsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder => lid1 -> lid2 -> a -> b
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaederunsafeCoerce i1 i2 a = maybe (error "unsafeCoerce") id $ primCoerce i1 i2 "" a
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceToResult :: (Typeable a, Typeable b, Language lid1, Language lid2) =>
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder lid1 -> lid2 -> Range -> a -> Result b
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercoerceToResult i1 i2 pos a = adjustPos pos $ primCoerce i1 i2 "" a
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceSublogic ::
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski => lid1 -> lid2 -> String -> sublogics1 -> m sublogics2
6abfd7000f15635fd29746bd841b4c36819e552bTill MossakowskicoerceSublogic l1 l2 msg s1 = primCoerce l1 l2 msg s1
6abfd7000f15635fd29746bd841b4c36819e552bTill MossakowskiforceCoerceSublogic ::
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder => lid1 -> lid2 -> sublogics1 -> sublogics2
6abfd7000f15635fd29746bd841b4c36819e552bTill MossakowskiforceCoerceSublogic l1 l2 s1 = unsafeCoerce l1 l2 s1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Monad m) => lid1 -> lid2 -> String -> sign1 -> m sign2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercoerceSign l1 l2 msg s1 = primCoerce l1 l2 msg s1
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceBasicTheory ::
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder Monad m) => lid1 -> lid2 -> String
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -> (sign1, [Named sentence1]) -> m (sign2, [Named sentence2])
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercoerceBasicTheory l1 l2 msg t1 = primCoerce l1 l2 msg t1
b20cc520e698253354303b7bf3bc17f84240b213Klaus LuettichcoerceTheory ::
b20cc520e698253354303b7bf3bc17f84240b213Klaus Luettich (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
b20cc520e698253354303b7bf3bc17f84240b213Klaus Luettich sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
b20cc520e698253354303b7bf3bc17f84240b213Klaus Luettich Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
b20cc520e698253354303b7bf3bc17f84240b213Klaus Luettich sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
b20cc520e698253354303b7bf3bc17f84240b213Klaus Luettich Monad m) => lid1 -> lid2 -> String
b20cc520e698253354303b7bf3bc17f84240b213Klaus Luettich -> Theory sign1 sentence1 proof_tree1
b20cc520e698253354303b7bf3bc17f84240b213Klaus Luettich -> m (Theory sign2 sentence2 proof_tree2)
b20cc520e698253354303b7bf3bc17f84240b213Klaus LuettichcoerceTheory l1 l2 msg t1 = primCoerce l1 l2 msg t1
b20cc520e698253354303b7bf3bc17f84240b213Klaus LuettichcoerceMorphism ::
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Monad m) => lid1 -> lid2 -> String -> morphism1 -> m morphism2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercoerceMorphism l1 l2 msg m1 = primCoerce l1 l2 msg m1
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceSymbol ::
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder => lid1 -> lid2 -> symbol1 -> symbol2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercoerceSymbol l1 l2 s1 = unsafeCoerce l1 l2 s1
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceSymbItemsList ::
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Monad m) => lid1 -> lid2 -> String -> [symb_items1] -> m [symb_items2]
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercoerceSymbItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceSymbMapItemsList ::
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder Monad m) => lid1 -> lid2 -> String
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -> [symb_map_items1] -> m [symb_map_items2]
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercoerceSymbMapItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceBasicProof ::
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder Monad m) => lid1 -> lid2 -> String
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -> Proof_status proof_tree1 -> m (Proof_status proof_tree2)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercoerceBasicProof l1 l2 msg m1 = primCoerce l1 l2 msg m1
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceSymbolSet ::
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Monad m) => lid1 -> lid2 -> String -> Set.Set symbol1 -> m (Set.Set symbol2)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercoerceSymbolSet l1 l2 msg m1 = primCoerce l1 l2 msg m1
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceRawSymbolMap ::
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder Monad m) => lid1 -> lid2 -> String -> EndoMap raw_symbol1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -> m (EndoMap raw_symbol2)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercoerceRawSymbolMap l1 l2 msg m1 = primCoerce l1 l2 msg m1