f39d7216a61322865a5b3424ad1343d8317170f3Kristina Sojakova{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

f39d7216a61322865a5b3424ad1343d8317170f3Kristina SojakovaDescription : coerce logic entities dynamically

f39d7216a61322865a5b3424ad1343d8317170f3Kristina SojakovaCopyright : (c) T. Mossakowski, C. Maeder, Uni Bremen 2005-2006

f39d7216a61322865a5b3424ad1343d8317170f3Kristina SojakovaLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : till@informatik.uni-bremen.de

f39d7216a61322865a5b3424ad1343d8317170f3Kristina SojakovaStability : provisional

f39d7216a61322865a5b3424ad1343d8317170f3Kristina SojakovaPortability : non-portable (various -fglasgow-exts extensions)

f39d7216a61322865a5b3424ad1343d8317170f3Kristina Sojakova

f39d7216a61322865a5b3424ad1343d8317170f3Kristina SojakovaFunctions for coercion used in Grothendieck.hs and Analysis modules:

f39d7216a61322865a5b3424ad1343d8317170f3Kristina Sojakova These tell the typechecker that things dynamically belong to the same logic

f39d7216a61322865a5b3424ad1343d8317170f3Kristina Sojakova-}

f39d7216a61322865a5b3424ad1343d8317170f3Kristina Sojakova

f39d7216a61322865a5b3424ad1343d8317170f3Kristina Sojakovamodule Logic.Coerce where

f39d7216a61322865a5b3424ad1343d8317170f3Kristina Sojakova

f39d7216a61322865a5b3424ad1343d8317170f3Kristina Sojakovaimport Logic.Logic

ebe9c5fc2d714f0e549c2d571e7f59bca021cd09Iulia Ignatovimport Logic.Prover

import Common.ExtSign

import Common.Id

import Common.Result

import Common.AS_Annotation

import qualified Data.Set as Set

import Data.Dynamic

import ATC.Prover ()

import ATC.ExtSign ()

-- coercion using the language name

primCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2,

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

primCoerce i1 i2 err a =

if language_name i1 == language_name i2

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

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

++ language_name i2 ++ " found")

where err1 = if err=="" then "" else err++": "

unsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2)

=> lid1 -> lid2 -> a -> b

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

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

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

coerceToResult i1 i2 pos a = adjustPos pos $ primCoerce i1 i2 "" a

coerceSublogic ::

(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 -> sublogics1 -> m sublogics2

coerceSublogic l1 l2 msg s1 = primCoerce l1 l2 msg s1

forceCoerceSublogic ::

(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)

=> lid1 -> lid2 -> sublogics1 -> sublogics2

forceCoerceSublogic l1 l2 s1 = unsafeCoerce l1 l2 s1

coercePlainSign ::

(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 -> sign1 -> m sign2

coercePlainSign l1 l2 msg s1 = primCoerce l1 l2 msg s1

coerceSign ::

(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 -> ExtSign sign1 symbol1

-> m (ExtSign sign2 symbol2)

coerceSign l1 l2 msg s1 = primCoerce l1 l2 msg s1

coerceBasicTheory ::

(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

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

coerceBasicTheory l1 l2 msg t1 = primCoerce l1 l2 msg t1

coerceSens ::

(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

-> [Named sentence1] -> m [Named sentence2]

coerceSens l1 l2 msg t1 = primCoerce l1 l2 msg t1

coerceMorphism ::

(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 -> morphism1 -> m morphism2

coerceMorphism l1 l2 msg m1 = primCoerce l1 l2 msg m1

coerceSymbol ::

(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)

=> lid1 -> lid2 -> symbol1 -> symbol2

coerceSymbol l1 l2 s1 = unsafeCoerce l1 l2 s1

coerceSymbItemsList ::

(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 -> [symb_items1] -> m [symb_items2]

coerceSymbItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1

coerceSymbMapItemsList ::

(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

-> [symb_map_items1] -> m [symb_map_items2]

coerceSymbMapItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1

coerceProofStatus ::

(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

-> Proof_status proof_tree1 -> m (Proof_status proof_tree2)

coerceProofStatus 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

coerceFreeDefMorphism ::

(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

-> FreeDefMorphism sentence1 morphism1

-> m (FreeDefMorphism sentence2 morphism2)

coerceFreeDefMorphism l1 l2 msg freedef = primCoerce l1 l2 msg freedef