Coerce.hs revision acabd9ab36e1870f6f02c513bcfbfd10ffd118e0
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
c3efd4f435e954846981cf46bca64e0485266634Liam O'ReillyCopyright : (c) Till Mossakowski, C.Maeder and Uni Bremen 2005
c3efd4f435e954846981cf46bca64e0485266634Liam O'ReillyLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : till@tzi.de
c3efd4f435e954846981cf46bca64e0485266634Liam O'ReillyStability : provisional
c3efd4f435e954846981cf46bca64e0485266634Liam O'ReillyPortability : non-portable (various -fglasgow-exts extensions)
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly-- for coercion used in Grothendieck.hs and Analysis modules
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reillyimport qualified Common.Lib.Set as Set
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly-- coercion using the language name
9738b4e358f960105062839c835bb9eff3e44588Liam O'ReillyprimCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Monad m) => lid1 -> lid2 -> String -> a -> m b
abc67c4b359c4a5bb953c6d55fb0f9133369d707Liam O'ReillyprimCoerce i1 i2 err a =
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly if language_name i1 == language_name i2
0e51f08fb6ced8e6a9e69eb5976fcc20dbf07019Liam O'Reilly then return $ fromDyn (toDyn a) $ error "mcoerce"
0e51f08fb6ced8e6a9e69eb5976fcc20dbf07019Liam O'Reilly else fail (err1++"Logic "++ language_name i1 ++ " expected, but "
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly ++ language_name i2 ++ " found")
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly where err1 = if err=="" then "" else err++": "
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian MaederunsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2)
9738b4e358f960105062839c835bb9eff3e44588Liam O'Reilly => lid1 -> lid2 -> a -> b
842ae753ab848a8508c4832ab64296b929167a97Christian MaederunsafeCoerce i1 i2 a = maybe (error "unsafeCoerce") id $ primCoerce i1 i2 "" a
c3efd4f435e954846981cf46bca64e0485266634Liam O'ReillycoerceToResult :: (Typeable a, Typeable b, Language lid1, Language lid2) =>
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly lid1 -> lid2 -> Range -> a -> Result b
c3efd4f435e954846981cf46bca64e0485266634Liam O'ReillycoerceToResult i1 i2 pos a = adjustPos pos $ primCoerce i1 i2 "" a
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillycoerceSublogic ::
0e51f08fb6ced8e6a9e69eb5976fcc20dbf07019Liam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly => lid1 -> lid2 -> sublogics1 -> sublogics2
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillycoerceSublogic l1 l2 s1 = unsafeCoerce l1 l2 s1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Monad m) => lid1 -> lid2 -> String -> sign1 -> m sign2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceSign l1 l2 msg s1 = primCoerce l1 l2 msg s1
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillycoerceBasicTheory ::
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly Monad m) => lid1 -> lid2 -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> (sign1, [Named sentence1]) -> m (sign2, [Named sentence2])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceBasicTheory l1 l2 msg t1 = primCoerce l1 l2 msg t1
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillycoerceMorphism ::
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Monad m) => lid1 -> lid2 -> String -> morphism1 -> m morphism2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceMorphism l1 l2 msg m1 = primCoerce l1 l2 msg m1
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillycoerceSymbol ::
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder => lid1 -> lid2 -> symbol1 -> symbol2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceSymbol l1 l2 s1 = unsafeCoerce l1 l2 s1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceSymbItemsList ::
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
0e51f08fb6ced8e6a9e69eb5976fcc20dbf07019Liam O'Reilly Monad m) => lid1 -> lid2 -> String -> [symb_items1] -> m [symb_items2]
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillycoerceSymbItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillycoerceSymbMapItemsList ::
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Monad m) => lid1 -> lid2 -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> [symb_map_items1] -> m [symb_map_items2]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceSymbMapItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1
0e51f08fb6ced8e6a9e69eb5976fcc20dbf07019Liam O'ReillycoerceBasicProof ::
0e51f08fb6ced8e6a9e69eb5976fcc20dbf07019Liam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
0e51f08fb6ced8e6a9e69eb5976fcc20dbf07019Liam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
0e51f08fb6ced8e6a9e69eb5976fcc20dbf07019Liam O'Reilly Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
7db74d99f2d2705558510202067b91aca1912f6fLiam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly Monad m) => lid1 -> lid2 -> String
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly -> Proof_status proof_tree1 -> m (Proof_status proof_tree2)
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillycoerceBasicProof l1 l2 msg m1 = primCoerce l1 l2 msg m1
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'ReillycoerceSymbolSet ::
0e51f08fb6ced8e6a9e69eb5976fcc20dbf07019Liam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Monad m) => lid1 -> lid2 -> String -> Set.Set symbol1 -> m (Set.Set symbol2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceSymbolSet l1 l2 msg m1 = primCoerce l1 l2 msg m1
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillycoerceRawSymbolMap ::
abc67c4b359c4a5bb953c6d55fb0f9133369d707Liam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Monad m) => lid1 -> lid2 -> String -> EndoMap raw_symbol1
abc67c4b359c4a5bb953c6d55fb0f9133369d707Liam O'Reilly -> m (EndoMap raw_symbol2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoerceRawSymbolMap l1 l2 msg m1 = primCoerce l1 l2 msg m1