Coerce.hs revision ad69cb3627839ed3d33f13d71c81378b65a24b35
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : coerce logic entities dynamically
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) T. Mossakowski, C. Maeder, Uni Bremen 2005-2006
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : till@informatik.uni-bremen.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : non-portable (various -fglasgow-exts extensions)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederFunctions for coercion used in Grothendieck.hs and Analysis modules:
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski These tell the typechecker that things dynamically belong to the same logic
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport qualified Data.Set as Set
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang-- coercion using the language name
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaederprimCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2,
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder Monad m) => lid1 -> lid2 -> String -> a -> m b
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaederprimCoerce i1 i2 err a =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder if language_name i1 == language_name i2
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder then return $ fromDyn (toDyn a) $ error "mcoerce"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else fail (err1++"Logic "++ language_name i1 ++ " expected, but "
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ++ language_name i2 ++ " found")
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder where err1 = if err=="" then "" else err++": "
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian MaederunsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2)
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder => lid1 -> lid2 -> a -> b
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus LuettichunsafeCoerce i1 i2 a = maybe (error "unsafeCoerce") id $ primCoerce i1 i2 "" a
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus LuettichcoerceToResult :: (Typeable a, Typeable b, Language lid1, Language lid2) =>
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich lid1 -> lid2 -> Range -> a -> Result b
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedercoerceToResult i1 i2 pos a = adjustPos pos $ primCoerce i1 i2 "" a
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskicoerceSublogic ::
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder => lid1 -> lid2 -> String -> sublogics1 -> m sublogics2
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedercoerceSublogic l1 l2 msg s1 = primCoerce l1 l2 msg s1
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederforceCoerceSublogic ::
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder => lid1 -> lid2 -> sublogics1 -> sublogics2
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaederforceCoerceSublogic l1 l2 s1 = unsafeCoerce l1 l2 s1
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaedercoercePlainSign ::
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder Monad m) => lid1 -> lid2 -> String -> sign1 -> m sign2
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaedercoercePlainSign l1 l2 msg s1 = primCoerce l1 l2 msg s1
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Monad m) => lid1 -> lid2 -> String -> ExtSign sign1 symbol1
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder -> m (ExtSign sign2 symbol2)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedercoerceSign l1 l2 msg s1 = primCoerce l1 l2 msg s1
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedercoerceBasicTheory ::
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Monad m) => lid1 -> lid2 -> String
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -> (sign1, [Named sentence1]) -> m (sign2, [Named sentence2])
5e46b572ed576c0494768998b043d9d340594122Till MossakowskicoerceBasicTheory l1 l2 msg t1 = primCoerce l1 l2 msg t1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Monad m) => lid1 -> lid2 -> String
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -> [Named sentence1] -> m [Named sentence2]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedercoerceSens l1 l2 msg t1 = primCoerce l1 l2 msg t1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskicoerceMorphism ::
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Monad m) => lid1 -> lid2 -> String -> morphism1 -> m morphism2
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedercoerceMorphism l1 l2 msg m1 = primCoerce l1 l2 msg m1
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedercoerceSymbol ::
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder => lid1 -> lid2 -> symbol1 -> symbol2
26d11a256b1433604a3dbc69913b520fff7586acChristian MaedercoerceSymbol l1 l2 s1 = unsafeCoerce l1 l2 s1
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedercoerceSymbItemsList ::
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Monad m) => lid1 -> lid2 -> String -> [symb_items1] -> m [symb_items2]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedercoerceSymbItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedercoerceSymbMapItemsList ::
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Monad m) => lid1 -> lid2 -> String
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> [symb_map_items1] -> m [symb_map_items2]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedercoerceSymbMapItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedercoerceProofStatus ::
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Monad m) => lid1 -> lid2 -> String
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -> Proof_status proof_tree1 -> m (Proof_status proof_tree2)
74d9a385499bf903b24848dff450a153f525bda7Christian MaedercoerceProofStatus l1 l2 msg m1 = primCoerce l1 l2 msg m1
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedercoerceSymbolSet ::
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Monad m) => lid1 -> lid2 -> String -> Set.Set symbol1 -> m (Set.Set symbol2)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedercoerceSymbolSet l1 l2 msg m1 = primCoerce l1 l2 msg m1
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedercoerceRawSymbolMap ::
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder Monad m) => lid1 -> lid2 -> String -> EndoMap raw_symbol1
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder -> m (EndoMap raw_symbol2)
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaedercoerceRawSymbolMap l1 l2 msg m1 = primCoerce l1 l2 msg m1
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaedercoerceFreeDefMorphism ::
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder Monad m) => lid1 -> lid2 -> String
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder -> FreeDefMorphism sentence1 morphism1
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder -> m (FreeDefMorphism sentence2 morphism2)
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaedercoerceFreeDefMorphism l1 l2 msg freedef = primCoerce l1 l2 msg freedef