Coerce.hs revision 3a6c7a7ff823616f56cd3d205fc44664a683effd
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederModule : $Header$
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederDescription : coerce logic entities dynamically
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) T. Mossakowski, C. Maeder, Uni Bremen 2005-2006
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : till@informatik.uni-bremen.de
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederStability : provisional
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederPortability : non-portable (various -fglasgow-exts extensions)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederFunctions for coercion used in Grothendieck.hs and Analysis modules:
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder These tell the typechecker that things dynamically belong to the same logic
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederimport qualified Data.Set as Set
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder-- coercion using the language name
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian MaederprimCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2,
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder Monad m) => lid1 -> lid2 -> String -> a -> m b
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederprimCoerce i1 i2 err a =
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder if language_name i1 == language_name i2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder then return $ fromDyn (toDyn a) $ error "mcoerce"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else fail (err1++"Logic "++ language_name i1 ++ " expected, but "
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ++ language_name i2 ++ " found")
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder where err1 = if err=="" then "" else err++": "
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaederunsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder => lid1 -> lid2 -> a -> b
ce3928e71520030ad0275b72050a8f4377f9313cChristian MaederunsafeCoerce i1 i2 a = maybe (error "unsafeCoerce") id $ primCoerce i1 i2 "" a
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercoerceToResult :: (Typeable a, Typeable b, Language lid1, Language lid2) =>
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder lid1 -> lid2 -> Range -> a -> Result b
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercoerceToResult i1 i2 pos a = adjustPos pos $ primCoerce i1 i2 "" a
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaedercoerceSublogic ::
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder => lid1 -> lid2 -> String -> sublogics1 -> m sublogics2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercoerceSublogic l1 l2 msg s1 = primCoerce l1 l2 msg s1
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaederforceCoerceSublogic ::
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder => lid1 -> lid2 -> sublogics1 -> sublogics2
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederforceCoerceSublogic l1 l2 s1 = unsafeCoerce l1 l2 s1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercoercePlainSign ::
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder Monad m) => lid1 -> lid2 -> String -> sign1 -> m sign2
92aa1b88f02d2a413da60dba78acd34312e6f29aChristian MaedercoercePlainSign l1 l2 msg s1 = primCoerce l1 l2 msg s1
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder Monad m) => lid1 -> lid2 -> String -> ExtSign sign1 symbol1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -> m (ExtSign sign2 symbol2)
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaedercoerceSign l1 l2 msg s1 = primCoerce l1 l2 msg s1
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedercoerceBasicTheory ::
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
d48085f765fca838c1d972d2123601997174583dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
d48085f765fca838c1d972d2123601997174583dChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder Monad m) => lid1 -> lid2 -> String
d48085f765fca838c1d972d2123601997174583dChristian Maeder -> (sign1, [Named sentence1]) -> m (sign2, [Named sentence2])
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaedercoerceBasicTheory l1 l2 msg t1 = primCoerce l1 l2 msg t1
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaedercoerceTheory ::
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder Monad m) => lid1 -> lid2 -> String
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder -> Theory sign1 sentence1 proof_tree1
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder -> m (Theory sign2 sentence2 proof_tree2)
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaedercoerceTheory l1 l2 msg t1 = primCoerce l1 l2 msg t1
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
d48085f765fca838c1d972d2123601997174583dChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
ae8052003e1ec7247597f034069db0939a7387e1Christian Maeder Monad m) => lid1 -> lid2 -> String
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder -> [Named sentence1] -> m [Named sentence2]
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian MaedercoerceSens l1 l2 msg t1 = primCoerce l1 l2 msg t1
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaedercoerceMorphism ::
d48085f765fca838c1d972d2123601997174583dChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder Monad m) => lid1 -> lid2 -> String -> morphism1 -> m morphism2
d48085f765fca838c1d972d2123601997174583dChristian MaedercoerceMorphism l1 l2 msg m1 = primCoerce l1 l2 msg m1
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaedercoerceSymbol ::
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
d48085f765fca838c1d972d2123601997174583dChristian Maeder => lid1 -> lid2 -> symbol1 -> symbol2
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaedercoerceSymbol l1 l2 s1 = unsafeCoerce l1 l2 s1
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaedercoerceSymbItemsList ::
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d48085f765fca838c1d972d2123601997174583dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder Monad m) => lid1 -> lid2 -> String -> [symb_items1] -> m [symb_items2]
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaedercoerceSymbItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaedercoerceSymbMapItemsList ::
d48085f765fca838c1d972d2123601997174583dChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d48085f765fca838c1d972d2123601997174583dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder Monad m) => lid1 -> lid2 -> String
d48085f765fca838c1d972d2123601997174583dChristian Maeder -> [symb_map_items1] -> m [symb_map_items2]
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaedercoerceSymbMapItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1
d48085f765fca838c1d972d2123601997174583dChristian MaedercoerceBasicProof ::
d48085f765fca838c1d972d2123601997174583dChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder Monad m) => lid1 -> lid2 -> String
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder -> Proof_status proof_tree1 -> m (Proof_status proof_tree2)
eab576044505ba1fbc64610323053490fbd9e82cChristian MaedercoerceBasicProof l1 l2 msg m1 = primCoerce l1 l2 msg m1
ae8052003e1ec7247597f034069db0939a7387e1Christian MaedercoerceSymbolSet ::
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
d48085f765fca838c1d972d2123601997174583dChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder Monad m) => lid1 -> lid2 -> String -> Set.Set symbol1 -> m (Set.Set symbol2)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedercoerceSymbolSet l1 l2 msg m1 = primCoerce l1 l2 msg m1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercoerceRawSymbolMap ::
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Monad m) => lid1 -> lid2 -> String -> EndoMap raw_symbol1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -> m (EndoMap raw_symbol2)
37354e3ed68875fb527338105a610df481f98cb0Christian MaedercoerceRawSymbolMap l1 l2 msg m1 = primCoerce l1 l2 msg m1