449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken Stubbings{- |

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterModule : $Header$

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterCopyright : (c) T. Mossakowski, C. Maeder, Uni Bremen 2005-2006

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterMaintainer : till@tzi.de

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterStability : provisional

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterPortability : non-portable (various -fglasgow-exts extensions)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster-- for coercion used in Grothendieck.hs and Analysis modules

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster-}

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fostermodule Logic.Coerce where

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterimport Logic.Logic

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterimport Logic.Prover

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterimport Common.Id

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterimport Common.Result

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterimport Common.AS_Annotation

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterimport qualified Common.Lib.Set as Set

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterimport Common.DynamicUtils

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterimport ATC.Prover()

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster-- coercion using the language name

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterprimCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Monad m) => lid1 -> lid2 -> String -> a -> m b

449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken StubbingsprimCoerce i1 i2 err a =

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster if language_name i1 == language_name i2

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster then return $ fromDyn (toDyn a) $ error "mcoerce"

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster else fail (err1++"Logic "++ language_name i1 ++ " expected, but "

449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken Stubbings ++ language_name i2 ++ " found")

449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken Stubbings where err1 = if err=="" then "" else err++": "

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterunsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster => lid1 -> lid2 -> a -> b

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterunsafeCoerce i1 i2 a = maybe (error "unsafeCoerce") id $ primCoerce i1 i2 "" a

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceToResult :: (Typeable a, Typeable b, Language lid1, Language lid2) =>

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster lid1 -> lid2 -> Range -> a -> Result b

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceToResult i1 i2 pos a = adjustPos pos $ primCoerce i1 i2 "" a

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceSublogic ::

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Monad m)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster => lid1 -> lid2 -> String -> sublogics1 -> m sublogics2

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceSublogic l1 l2 msg s1 = primCoerce l1 l2 msg s1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterforceCoerceSublogic ::

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign2 morphism2 symbol2 raw_symbol2 proof_tree2)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster => lid1 -> lid2 -> sublogics1 -> sublogics2

449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken StubbingsforceCoerceSublogic l1 l2 s1 = unsafeCoerce l1 l2 s1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceSign ::

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Monad m) => lid1 -> lid2 -> String -> sign1 -> m sign2

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceSign l1 l2 msg s1 = primCoerce l1 l2 msg s1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceBasicTheory ::

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Monad m) => lid1 -> lid2 -> String

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -> (sign1, [Named sentence1]) -> m (sign2, [Named sentence2])

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceBasicTheory l1 l2 msg t1 = primCoerce l1 l2 msg t1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceTheory ::

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Monad m) => lid1 -> lid2 -> String

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -> Theory sign1 sentence1 proof_tree1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -> m (Theory sign2 sentence2 proof_tree2)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceTheory l1 l2 msg t1 = primCoerce l1 l2 msg t1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceMorphism ::

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Monad m) => lid1 -> lid2 -> String -> morphism1 -> m morphism2

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceMorphism l1 l2 msg m1 = primCoerce l1 l2 msg m1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceSymbol ::

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign2 morphism2 symbol2 raw_symbol2 proof_tree2)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster => lid1 -> lid2 -> symbol1 -> symbol2

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceSymbol l1 l2 s1 = unsafeCoerce l1 l2 s1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceSymbItemsList ::

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Monad m) => lid1 -> lid2 -> String -> [symb_items1] -> m [symb_items2]

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceSymbItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceSymbMapItemsList ::

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Monad m) => lid1 -> lid2 -> String

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -> [symb_map_items1] -> m [symb_map_items2]

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceSymbMapItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceBasicProof ::

449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken Stubbings (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken Stubbings sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken Stubbings Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

5bdd6bf9211505ff52afc7e32bdc49cdfacf4879Charles Sparey sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

5bdd6bf9211505ff52afc7e32bdc49cdfacf4879Charles Sparey Monad m) => lid1 -> lid2 -> String

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -> Proof_status proof_tree1 -> m (Proof_status proof_tree2)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostercoerceBasicProof l1 l2 msg m1 = primCoerce l1 l2 msg m1

coerceSymbolSet ::

(Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

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

coerceSymbolSet l1 l2 msg m1 = primCoerce l1 l2 msg m1

coerceRawSymbolMap ::

(Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

Monad m) => lid1 -> lid2 -> String -> EndoMap raw_symbol1

-> m (EndoMap raw_symbol2)

coerceRawSymbolMap l1 l2 msg m1 = primCoerce l1 l2 msg m1