Coerce.hs revision 04857331be117d4e2215d866c309a17bd9a7e15c
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettModule : $Header$
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettDescription : coerce logic entities dynamically
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyCopyright : (c) T. Mossakowski, C. Maeder, Uni Bremen 2005-2006
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyLicense : GPLv2 or higher, see LICENSE.txt
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederMaintainer : till@informatik.uni-bremen.de
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettPortability : non-portable (various -fglasgow-exts extensions)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachFunctions for coercion used in Grothendieck.hs and Analysis modules:
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach These tell the typechecker that things dynamically belong to the same logic
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyimport qualified Data.Set as Set
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblettimport qualified Data.Map as Map
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-- coercion using the language name
ae930b77ed60580110b52a09456d651f9b841883Andy GimblettprimCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2,
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett Monad m) => lid1 -> lid2 -> String -> a -> m b
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachprimCoerce i1 i2 err a =
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach if language_name i1 == language_name i2
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder then return $ fromDyn (toDyn a) $ error "primCoerce"
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett else fail $ (if null err then "" else err ++ ": ") ++ "Logic "
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly ++ language_name i2 ++ " expected, but "
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach ++ language_name i1 ++ " found"
0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy GimblettunsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2)
04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett => lid1 -> lid2 -> a -> b
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy GimblettunsafeCoerce i1 i2 a = maybe (error "unsafeCoerce") id $ primCoerce i1 i2 "" a
06dd4e7c29f33f6122a910719e3bd9062256e397Andy GimblettcoerceToResult :: (Typeable a, Typeable b, Language lid1, Language lid2) =>
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett lid1 -> lid2 -> Range -> a -> Result b
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'ReillycoerceToResult i1 i2 pos a = adjustPos pos $ primCoerce i1 i2 "" a
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillycoerceSublogic ::
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,
765e55b764e0fd32c09d33709d6e2770c4766799Christian Maeder => lid1 -> lid2 -> String -> sublogics1 -> m sublogics2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillycoerceSublogic l1 l2 msg s1 = primCoerce l1 l2 msg s1
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian MaederforceCoerceSublogic ::
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly => lid1 -> lid2 -> sublogics1 -> sublogics2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyforceCoerceSublogic l1 l2 s1 = unsafeCoerce l1 l2 s1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillycoercePlainSign ::
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett Monad m) => lid1 -> lid2 -> String -> sign1 -> m sign2
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettcoercePlainSign l1 l2 msg s1 = primCoerce l1 l2 msg s1
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Monad m) => lid1 -> lid2 -> String -> ExtSign sign1 symbol1
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett -> m (ExtSign sign2 symbol2)
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettcoerceSign l1 l2 msg s1 = primCoerce l1 l2 msg s1
e771539425f4a0abef9f94cf4b63690f3603f682Andy GimblettcoerceBasicTheory ::
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett Monad m) => lid1 -> lid2 -> String
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett -> (sign1, [Named sentence1]) -> m (sign2, [Named sentence2])
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettcoerceBasicTheory l1 l2 msg t1 = primCoerce l1 l2 msg t1
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy GimblettcoerceTheoryMorphism ::
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Monad m) => lid1 -> lid2 -> String
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -> TheoryMorphism sign1 sentence1 morphism1 proof_tree1-> m (TheoryMorphism sign2 sentence2 morphism2 proof_tree2)
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettcoerceTheoryMorphism l1 l2 msg t1 = primCoerce l1 l2 msg t1
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Monad m) => lid1 -> lid2 -> String
820947bd01ca952c3909eaa0366c6914c87cc1cbTill Mossakowski -> [Named sentence1] -> m [Named sentence2]
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettcoerceSens l1 l2 msg t1 = primCoerce l1 l2 msg t1
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettcoerceMorphism ::
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett Monad m) => lid1 -> lid2 -> String -> morphism1 -> m morphism2
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettcoerceMorphism l1 l2 msg m1 = primCoerce l1 l2 msg m1
31f039ffdb33d78cb31d24b71d3155b11a323975Andy GimblettcoerceSymbol ::
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly => lid1 -> lid2 -> symbol1 -> symbol2
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'ReillycoerceSymbol l1 l2 s1 = unsafeCoerce l1 l2 s1
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'ReillycoerceSymbolmap ::
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett => lid1 -> lid2 -> Map.Map symbol1 a
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettcoerceSymbolmap l1 l2 sm1 = unsafeCoerce l1 l2 sm1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettcoerceMapofsymbol ::
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett => lid1 -> lid2 -> Map.Map a symbol1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettcoerceMapofsymbol l1 l2 sm1 = unsafeCoerce l1 l2 sm1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettcoerceSymbItemsList ::
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett Monad m) => lid1 -> lid2 -> String -> [symb_items1] -> m [symb_items2]
31f039ffdb33d78cb31d24b71d3155b11a323975Andy GimblettcoerceSymbItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettcoerceSymbMapItemsList ::
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Monad m) => lid1 -> lid2 -> String
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -> [symb_map_items1] -> m [symb_map_items2]
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettcoerceSymbMapItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1
31f039ffdb33d78cb31d24b71d3155b11a323975Andy GimblettcoerceProofStatus ::
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Monad m) => lid1 -> lid2 -> String
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -> ProofStatus proof_tree1 -> m (ProofStatus proof_tree2)
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'ReillycoerceProofStatus l1 l2 msg m1 = primCoerce l1 l2 msg m1
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'ReillycoerceSymbolSet ::
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett Monad m) => lid1 -> lid2 -> String -> Set.Set symbol1 -> m (Set.Set symbol2)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettcoerceSymbolSet l1 l2 msg m1 = primCoerce l1 l2 msg m1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettcoerceRawSymbolMap ::
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Monad m) => lid1 -> lid2 -> String -> EndoMap raw_symbol1
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett -> m (EndoMap raw_symbol2)
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy GimblettcoerceRawSymbolMap l1 l2 msg m1 = primCoerce l1 l2 msg m1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettcoerceFreeDefMorphism ::
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Monad m) => lid1 -> lid2 -> String
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly -> FreeDefMorphism sentence1 morphism1
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly -> m (FreeDefMorphism sentence2 morphism2)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillycoerceFreeDefMorphism l1 l2 msg freedef = primCoerce l1 l2 msg freedef