Coerce.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
3a6c7a7ff823616f56cd3d205fc44664a683effdChristian MaederDescription : coerce logic entities dynamically
73dfcef93ee2ba07fedf4f3c74bace31853d1b9fChristian MaederCopyright : (c) T. Mossakowski, C. Maeder, Uni Bremen 2005-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : till@informatik.uni-bremen.de
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederStability : provisional
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederPortability : non-portable (various -fglasgow-exts extensions)
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiFunctions for coercion used in Grothendieck.hs and Analysis modules:
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski These tell the typechecker that things dynamically belong to the same logic
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulzimport qualified Data.Map as Map
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Data.Maybe (fromMaybe)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- coercion using the language name
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederprimCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2,
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder Monad m) => lid1 -> lid2 -> String -> a -> m b
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaederprimCoerce i1 i2 err a =
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder if language_name i1 == language_name i2
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder then return $ fromDyn (toDyn a) $ error "primCoerce"
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder else fail $ (if null err then "" else err ++ ": ") ++ "Logic "
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder ++ language_name i2 ++ " expected, but "
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder ++ language_name i1 ++ " found"
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederunsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2)
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder => lid1 -> lid2 -> a -> b
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederunsafeCoerce i1 i2 a = fromMaybe (error "unsafeCoerce") (primCoerce i1 i2 "" a)
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceToResult :: (Typeable a, Typeable b, Language lid1, Language lid2) =>
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder lid1 -> lid2 -> Range -> a -> Result b
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercoerceToResult i1 i2 pos a = adjustPos pos $ primCoerce i1 i2 "" a
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceSublogic ::
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceSublogic = primCoerce
6abfd7000f15635fd29746bd841b4c36819e552bTill MossakowskiforceCoerceSublogic ::
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederforceCoerceSublogic = unsafeCoerce
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedercoercePlainSign ::
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoercePlainSign = primCoerce
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Monad m) => lid1 -> lid2 -> String -> ExtSign sign1 symbol1
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -> m (ExtSign sign2 symbol2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceSign = primCoerce
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceBasicTheory ::
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceBasicTheory = primCoerce
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceTheoryMorphism ::
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
04857331be117d4e2215d866c309a17bd9a7e15cLoredana Mihaela Diaconu sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
04857331be117d4e2215d866c309a17bd9a7e15cLoredana Mihaela Diaconu sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
04857331be117d4e2215d866c309a17bd9a7e15cLoredana Mihaela Diaconu Monad m) => lid1 -> lid2 -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> TheoryMorphism sign1 sentence1 morphism1 proof_tree1 -> m (TheoryMorphism sign2 sentence2 morphism2 proof_tree2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceTheoryMorphism = primCoerce
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski Monad m) => lid1 -> lid2 -> String
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski -> [Named sentence1] -> m [Named sentence2]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceSens = primCoerce
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceMorphism ::
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceMorphism = primCoerce
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceSymbol ::
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceSymbol = unsafeCoerce
295566c1778f463b624caf1be714b70d808e2a51Ewaryst SchulzcoerceSymbolmap ::
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst Schulz sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz => lid1 -> lid2 -> Map.Map symbol1 a
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceSymbolmap = unsafeCoerce
295566c1778f463b624caf1be714b70d808e2a51Ewaryst SchulzcoerceMapofsymbol ::
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz => lid1 -> lid2 -> Map.Map a symbol1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceMapofsymbol = unsafeCoerce
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceSymbItemsList ::
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceSymbItemsList = primCoerce
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceSymbMapItemsList ::
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceSymbMapItemsList = primCoerce
07baaf27fc0029203075ed916999006dcc619ef0Christian MaedercoerceProofStatus ::
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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
3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian Maeder -> ProofStatus proof_tree1 -> m (ProofStatus proof_tree2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceProofStatus = primCoerce
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceSymbolSet ::
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceSymbolSet = primCoerce
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercoerceRawSymbolMap ::
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceRawSymbolMap = primCoerce
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian MaedercoerceFreeDefMorphism ::
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder Monad m) => lid1 -> lid2 -> String
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder -> FreeDefMorphism sentence1 morphism1
ad69cb3627839ed3d33f13d71c81378b65a24b35Till Mossakowski -> m (FreeDefMorphism sentence2 morphism2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceFreeDefMorphism = primCoerce