7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

81d182b21020b815887e9057959228546cf61b6bChristian MaederCopyright : (c) T. Mossakowski, C. Maeder, Uni Bremen 2005-2006

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederMaintainer : till@tzi.de

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederPortability : non-portable (various -fglasgow-exts extensions)

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder-- for coercion used in Grothendieck.hs and Analysis modules

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-}

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maedermodule Logic.Coerce where

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport Logic.Logic

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Logic.Prover

950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maederimport Common.Id

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.Result

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.AS_Annotation

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport qualified Common.Lib.Set as Set

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederimport Common.DynamicUtils

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport ATC.Prover()

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder-- coercion using the language name

8197d0be8b81692f311ad5ca34e125e2cf9eecb8Christian MaederprimCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2,

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder Monad m) => lid1 -> lid2 -> String -> a -> m b

a6f84880cea4485fba85b521d122eba73b0df70bChristian MaederprimCoerce i1 i2 err a =

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder if language_name i1 == language_name i2

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder then return $ fromDyn (toDyn a) $ error "mcoerce"

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder else fail (err1++"Logic "++ language_name i1 ++ " expected, but "

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder ++ language_name i2 ++ " found")

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder where err1 = if err=="" then "" else err++": "

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaederunsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2)

878ac75d7acbbb06412e82a4c95356ce60f942deChristian Maeder => lid1 -> lid2 -> a -> b

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaederunsafeCoerce i1 i2 a = maybe (error "unsafeCoerce") id $ primCoerce i1 i2 "" a

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedercoerceToResult :: (Typeable a, Typeable b, Language lid1, Language lid2) =>

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder lid1 -> lid2 -> Range -> a -> Result b

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedercoerceToResult i1 i2 pos a = adjustPos pos $ primCoerce i1 i2 "" a

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedercoerceSublogic ::

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder => lid1 -> lid2 -> sublogics1 -> sublogics2

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedercoerceSublogic l1 l2 s1 = unsafeCoerce l1 l2 s1

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedercoerceSign ::

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Monad m) => lid1 -> lid2 -> String -> sign1 -> m sign2

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedercoerceSign l1 l2 msg s1 = primCoerce l1 l2 msg s1

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedercoerceBasicTheory ::

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Monad m) => lid1 -> lid2 -> String

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -> (sign1, [Named sentence1]) -> m (sign2, [Named sentence2])

2ac1742771a267119f1d839054b5e45d0a468085Christian MaedercoerceBasicTheory l1 l2 msg t1 = primCoerce l1 l2 msg t1

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian MaedercoerceTheory ::

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

522913d1d69be804c9579bbc77868ec6b501b608Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder Monad m) => lid1 -> lid2 -> String

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder -> Theory sign1 sentence1 proof_tree1

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder -> m (Theory sign2 sentence2 proof_tree2)

b1bd8688a1ce545444792a307412711c2c61df5fChristian MaedercoerceTheory l1 l2 msg t1 = primCoerce l1 l2 msg t1

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder

b1bd8688a1ce545444792a307412711c2c61df5fChristian MaedercoerceMorphism ::

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder Monad m) => lid1 -> lid2 -> String -> morphism1 -> m morphism2

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian MaedercoerceMorphism l1 l2 msg m1 = primCoerce l1 l2 msg m1

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian MaedercoerceSymbol ::

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder => lid1 -> lid2 -> symbol1 -> symbol2

b1bd8688a1ce545444792a307412711c2c61df5fChristian MaedercoerceSymbol l1 l2 s1 = unsafeCoerce l1 l2 s1

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedercoerceSymbItemsList ::

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder Monad m) => lid1 -> lid2 -> String -> [symb_items1] -> m [symb_items2]

2ac1742771a267119f1d839054b5e45d0a468085Christian MaedercoerceSymbItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaedercoerceSymbMapItemsList ::

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder Monad m) => lid1 -> lid2 -> String

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -> [symb_map_items1] -> m [symb_map_items2]

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedercoerceSymbMapItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedercoerceBasicProof ::

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder Monad m) => lid1 -> lid2 -> String

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -> Proof_status proof_tree1 -> m (Proof_status proof_tree2)

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedercoerceBasicProof l1 l2 msg m1 = primCoerce l1 l2 msg m1

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder

5ba383b1607c20c57e14324e72cee2c789436d5fChristian MaedercoerceSymbolSet ::

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Monad m) => lid1 -> lid2 -> String -> Set.Set symbol1 -> m (Set.Set symbol2)

72909c6c1cfe9702f5910d0a135c8b55729c7917Christian MaedercoerceSymbolSet l1 l2 msg m1 = primCoerce l1 l2 msg m1

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian MaedercoerceRawSymbolMap ::

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

2118d66b6aa3c90458925019c9b2fb986e2b2aabChristian Maeder Monad m) => lid1 -> lid2 -> String -> EndoMap raw_symbol1

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder -> m (EndoMap raw_symbol2)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedercoerceRawSymbolMap l1 l2 msg m1 = primCoerce l1 l2 msg m1

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder