Coerce.hs revision 999f839e42d594e4ae288208fec398626837c41c
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederModule : $Header$
3a6c7a7ff823616f56cd3d205fc44664a683effdChristian MaederDescription : coerce logic entities dynamically
73dfcef93ee2ba07fedf4f3c74bace31853d1b9fChristian MaederCopyright : (c) T. Mossakowski, C. Maeder, Uni Bremen 2005-2006
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.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
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
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedercoercePlainSign ::
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
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedercoercePlainSign l1 l2 msg s1 = primCoerce l1 l2 msg s1
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder 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)
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
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski 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]
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till MossakowskicoerceSens l1 l2 msg t1 = primCoerce l1 l2 msg t1
da955132262baab309a50fdffe228c9efe68251dCui JiancoerceMorphism ::
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
07baaf27fc0029203075ed916999006dcc619ef0Christian MaedercoerceProofStatus ::
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)
07baaf27fc0029203075ed916999006dcc619ef0Christian MaedercoerceProofStatus 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
999f839e42d594e4ae288208fec398626837c41cTill MossakowskicoerceFreeDefMorphism ::
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski Monad m) => lid1 -> lid2 -> String
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski -> FreeDefMorphism morphism1
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski -> m (FreeDefMorphism morphism2)
999f839e42d594e4ae288208fec398626837c41cTill MossakowskicoerceFreeDefMorphism l1 l2 msg freedef = do
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski f <- coerceMorphism l1 l2 msg $ freeDefMorphism freedef
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski p <- coerceMorphism l1 l2 msg $ pathFromFreeDef freedef
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski let c = isCofree freedef
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski return FreeDefMorphism { freeDefMorphism = f,
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski pathFromFreeDef = p,
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski isCofree = c }