7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu{- |

8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskiModule : $Header$

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescuCopyright : (c) Till Mossakowski, C.Maeder and Uni Bremen 2005

8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescuMaintainer : till@tzi.de

8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskiStability : provisional

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescuPortability : non-portable (various -fglasgow-exts extensions)

b74e9249a77f29b41d97ddcfdef9fdbdf357100cTill Mossakowski

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu-- for coercion used in Grothendieck.hs and Analysis modules

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu

b74e9249a77f29b41d97ddcfdef9fdbdf357100cTill Mossakowski-}

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowskimodule Logic.Coerce where

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowskiimport Logic.Logic

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescuimport Logic.Prover

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowskiimport Common.Id

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescuimport Common.Result

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowskiimport Common.AS_Annotation

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescuimport qualified Common.Lib.Set as Set

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowskiimport Data.Dynamic

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescuimport ATC.Prover()

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu-- coercion using the language name

8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskiprimCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Monad m) => lid1 -> lid2 -> String -> a -> m b

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescuprimCoerce i1 i2 err a =

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu if language_name i1 == language_name i2

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski then return $ fromDyn (toDyn a) $ error "mcoerce"

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu else fail (err1++"Logic "++ language_name i1 ++ " expected, but "

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski ++ language_name i2 ++ " found")

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu where err1 = if err=="" then "" else err++": "

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescuunsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2)

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski => lid1 -> lid2 -> a -> b

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescuunsafeCoerce i1 i2 a = maybe (error "unsafeCoerce") id $ primCoerce i1 i2 "" a

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescucoerceToResult :: (Typeable a, Typeable b, Language lid1, Language lid2) =>

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski lid1 -> lid2 -> Range -> a -> Result b

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescucoerceToResult i1 i2 pos a = adjustPos pos $ primCoerce i1 i2 "" a

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescucoerceSublogic ::

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2)

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski => lid1 -> lid2 -> sublogics1 -> sublogics2

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescucoerceSublogic l1 l2 s1 = unsafeCoerce l1 l2 s1

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescucoerceSign ::

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski Monad m) => lid1 -> lid2 -> String -> sign1 -> m sign2

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescucoerceSign l1 l2 msg s1 = primCoerce l1 l2 msg s1

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescucoerceBasicTheory ::

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Monad m) => lid1 -> lid2 -> String

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu -> (sign1, [Named sentence1]) -> m (sign2, [Named sentence2])

8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskicoerceBasicTheory l1 l2 msg t1 = primCoerce l1 l2 msg t1

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu

8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskicoerceMorphism ::

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Monad m) => lid1 -> lid2 -> String -> morphism1 -> m morphism2

8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskicoerceMorphism l1 l2 msg m1 = primCoerce l1 l2 msg m1

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu

8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskicoerceSymbol ::

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2)

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu => lid1 -> lid2 -> symbol1 -> symbol2

8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskicoerceSymbol l1 l2 s1 = unsafeCoerce l1 l2 s1

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu

8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskicoerceSymbItemsList ::

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Monad m) => lid1 -> lid2 -> String -> [symb_items1] -> m [symb_items2]

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescucoerceSymbItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescucoerceSymbMapItemsList ::

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Monad m) => lid1 -> lid2 -> String

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu -> [symb_map_items1] -> m [symb_map_items2]

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescucoerceSymbMapItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescucoerceBasicProof ::

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Monad m) => lid1 -> lid2 -> String

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu -> Proof_status proof_tree1 -> m (Proof_status proof_tree2)

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescucoerceBasicProof l1 l2 msg m1 = primCoerce l1 l2 msg m1

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescucoerceSymbolSet ::

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Monad m) => lid1 -> lid2 -> String -> Set.Set symbol1 -> m (Set.Set symbol2)

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescucoerceSymbolSet l1 l2 msg m1 = primCoerce l1 l2 msg m1

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescucoerceRawSymbolMap ::

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu Monad m) => lid1 -> lid2 -> String -> EndoMap raw_symbol1

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu -> m (EndoMap raw_symbol2)

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu ProdescucoerceRawSymbolMap l1 l2 msg m1 = primCoerce l1 l2 msg m1

7a8f957bfcc11b75a6a0aad027b8602f575687faCorneliu-Claudiu Prodescu