Coerce.hs revision 10b1417752a7cd79344892ad4dbb14831851c638
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettModule : $Header$
e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiDescription : coerce logic entities dynamically
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachCopyright : (c) T. Mossakowski, C. Maeder, Uni Bremen 2005-2006
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachMaintainer : till@informatik.uni-bremen.de
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiStability : provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : non-portable (various -fglasgow-exts extensions)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachFunctions for coercion used in Grothendieck.hs and Analysis modules:
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder These tell the typechecker that things dynamically belong to the same logic
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyimport qualified Data.Set as Set
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reillyimport qualified Data.Map as Map
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- coercion using the language name
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyprimCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2,
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Monad m) => lid1 -> lid2 -> String -> a -> m b
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyprimCoerce i1 i2 err a =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly if language_name i1 == language_name i2
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett then return $ fromDyn (toDyn a) $ error "primCoerce"
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett else fail $ (if null err then "" else err ++ ": ") ++ "Logic "
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder ++ language_name i2 ++ " expected, but "
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder ++ language_name i1 ++ " found"
e771539425f4a0abef9f94cf4b63690f3603f682Andy GimblettunsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett => lid1 -> lid2 -> a -> b
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy GimblettunsafeCoerce i1 i2 a = maybe (error "unsafeCoerce") id $ primCoerce i1 i2 "" a
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettcoerceToResult :: (Typeable a, Typeable b, Language lid1, Language lid2) =>
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett lid1 -> lid2 -> Range -> a -> Result b
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettcoerceToResult i1 i2 pos a = adjustPos pos $ primCoerce i1 i2 "" a
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillycoerceSublogic ::
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett => lid1 -> lid2 -> String -> sublogics1 -> m sublogics2
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettcoerceSublogic l1 l2 msg s1 = primCoerce l1 l2 msg s1
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaederforceCoerceSublogic ::
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly => lid1 -> lid2 -> sublogics1 -> sublogics2
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyforceCoerceSublogic l1 l2 s1 = unsafeCoerce l1 l2 s1
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycoercePlainSign ::
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett Monad m) => lid1 -> lid2 -> String -> sign1 -> m sign2
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaedercoercePlainSign l1 l2 msg s1 = primCoerce l1 l2 msg s1
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder Monad m) => lid1 -> lid2 -> String -> ExtSign sign1 symbol1
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett -> m (ExtSign sign2 symbol2)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettcoerceSign l1 l2 msg s1 = primCoerce l1 l2 msg s1
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettcoerceBasicTheory ::
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder Monad m) => lid1 -> lid2 -> String
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett -> (sign1, [Named sentence1]) -> m (sign2, [Named sentence2])
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaedercoerceBasicTheory l1 l2 msg t1 = primCoerce l1 l2 msg t1
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett Monad m) => lid1 -> lid2 -> String
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -> [Named sentence1] -> m [Named sentence2]
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettcoerceSens l1 l2 msg t1 = primCoerce l1 l2 msg t1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillycoerceMorphism ::
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett Monad m) => lid1 -> lid2 -> String -> morphism1 -> m morphism2
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettcoerceMorphism l1 l2 msg m1 = primCoerce l1 l2 msg m1
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillycoerceSymbol ::
cdf1545bdcd39a9d53c00761ffa42e7b1174b91eLiam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
cdf1545bdcd39a9d53c00761ffa42e7b1174b91eLiam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly => lid1 -> lid2 -> symbol1 -> symbol2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillycoerceSymbol l1 l2 s1 = unsafeCoerce l1 l2 s1
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettcoerceSymbolplmap ::
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett => lid1 -> lid2 -> Map.Map symbol1 [LinkPath symbol1]
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett -> Map.Map symbol2 [LinkPath symbol2]
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettcoerceSymbolplmap l1 l2 sm1 = unsafeCoerce l1 l2 sm1
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettcoerceSymbItemsList ::
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett Monad m) => lid1 -> lid2 -> String -> [symb_items1] -> m [symb_items2]
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettcoerceSymbItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1
1df33829303cbf924aa018ac5ce9a28e69c17d22Till MossakowskicoerceSymbMapItemsList ::
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly Monad m) => lid1 -> lid2 -> String
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly -> [symb_map_items1] -> m [symb_map_items2]
f08f7774e4c47012f3c349205310750198cdc434Liam O'ReillycoerceSymbMapItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettcoerceProofStatus ::
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
eaf34cf96fbfcdcce7f3bdb322c4ea7ebd1fd220Liam O'Reilly Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Monad m) => lid1 -> lid2 -> String
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly -> ProofStatus proof_tree1 -> m (ProofStatus proof_tree2)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillycoerceProofStatus l1 l2 msg m1 = primCoerce l1 l2 msg m1
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillycoerceSymbolSet ::
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Monad m) => lid1 -> lid2 -> String -> Set.Set symbol1 -> m (Set.Set symbol2)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillycoerceSymbolSet l1 l2 msg m1 = primCoerce l1 l2 msg m1
eaf34cf96fbfcdcce7f3bdb322c4ea7ebd1fd220Liam O'ReillycoerceRawSymbolMap ::
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Monad m) => lid1 -> lid2 -> String -> EndoMap raw_symbol1
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly -> m (EndoMap raw_symbol2)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillycoerceRawSymbolMap l1 l2 msg m1 = primCoerce l1 l2 msg m1
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillycoerceFreeDefMorphism ::
eaf34cf96fbfcdcce7f3bdb322c4ea7ebd1fd220Liam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Monad m) => lid1 -> lid2 -> String
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly -> FreeDefMorphism sentence1 morphism1
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly -> m (FreeDefMorphism sentence2 morphism2)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillycoerceFreeDefMorphism l1 l2 msg freedef = primCoerce l1 l2 msg freedef