4865N/A{- |

4865N/AModule : $Header$

4865N/ADescription : coerce logic entities dynamically

4865N/ACopyright : (c) T. Mossakowski, C. Maeder, Uni Bremen 2005-2006

4865N/ALicense : GPLv2 or higher, see LICENSE.txt

4865N/AMaintainer : till@informatik.uni-bremen.de

4865N/AStability : provisional

4865N/APortability : non-portable (various -fglasgow-exts extensions)

4865N/A

4865N/AFunctions for coercion used in Grothendieck.hs and Analysis modules:

4865N/A These tell the typechecker that things dynamically belong to the same logic

4865N/A-}

4865N/A

4865N/Amodule Logic.Coerce where

4865N/A

4865N/Aimport Logic.Logic

4865N/Aimport Logic.Prover

4865N/Aimport Common.ExtSign

4865N/Aimport Common.Id

4865N/Aimport Common.Result

4865N/Aimport Common.AS_Annotation

4865N/Aimport qualified Data.Set as Set

4865N/Aimport qualified Data.Map as Map

4865N/Aimport Data.Dynamic

4865N/Aimport ATC.LibName ()

4865N/Aimport ATC.Prover ()

4865N/Aimport ATC.ExtSign ()

4865N/Aimport Data.Maybe (fromMaybe)

4865N/A

4865N/A-- coercion using the language name

4865N/AprimCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2,

4865N/A Monad m) => lid1 -> lid2 -> String -> a -> m b

4865N/AprimCoerce i1 i2 err a =

4865N/A if language_name i1 == language_name i2

4865N/A then return $ fromDyn (toDyn a) $ error "primCoerce"

4865N/A else fail $ (if null err then "" else err ++ ": ") ++ "Logic "

4865N/A ++ language_name i2 ++ " expected, but "

4865N/A ++ language_name i1 ++ " found"

4865N/A

4865N/AunsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2)

4865N/A => lid1 -> lid2 -> a -> b

4865N/AunsafeCoerce i1 i2 a = fromMaybe (error "unsafeCoerce") (primCoerce i1 i2 "" a)

4865N/A

4865N/AcoerceToResult :: (Typeable a, Typeable b, Language lid1, Language lid2) =>

4865N/A lid1 -> lid2 -> Range -> a -> Result b

4865N/AcoerceToResult i1 i2 pos a = adjustPos pos $ primCoerce i1 i2 "" a

4865N/A

4865N/AcoerceSublogic ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

4865N/A Monad m)

4865N/A => lid1 -> lid2 -> String -> sublogics1 -> m sublogics2

4865N/AcoerceSublogic = primCoerce

4865N/A

4865N/AforceCoerceSublogic ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2)

4865N/A => lid1 -> lid2 -> sublogics1 -> sublogics2

4865N/AforceCoerceSublogic = unsafeCoerce

4865N/A

4865N/AcoercePlainSign ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

4865N/A Monad m) => lid1 -> lid2 -> String -> sign1 -> m sign2

4865N/AcoercePlainSign = primCoerce

4865N/A

4865N/AcoerceSign ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

4865N/A Monad m) => lid1 -> lid2 -> String -> ExtSign sign1 symbol1

4865N/A -> m (ExtSign sign2 symbol2)

4865N/AcoerceSign = primCoerce

4865N/A

4865N/AcoerceBasicTheory ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

4865N/A Monad m) => lid1 -> lid2 -> String

4865N/A -> (sign1, [Named sentence1]) -> m (sign2, [Named sentence2])

4865N/AcoerceBasicTheory = primCoerce

4865N/A

4865N/AcoerceTheoryMorphism ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

4865N/A Monad m) => lid1 -> lid2 -> String

4865N/A -> TheoryMorphism sign1 sentence1 morphism1 proof_tree1 -> m (TheoryMorphism sign2 sentence2 morphism2 proof_tree2)

4865N/AcoerceTheoryMorphism = primCoerce

4865N/A

4865N/AcoerceSens ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

4865N/A Monad m) => lid1 -> lid2 -> String

4865N/A -> [Named sentence1] -> m [Named sentence2]

4865N/AcoerceSens = primCoerce

4865N/A

4865N/AcoerceMorphism ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

4865N/A Monad m) => lid1 -> lid2 -> String -> morphism1 -> m morphism2

4865N/AcoerceMorphism = primCoerce

4865N/A

4865N/AcoerceSymbol ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2)

4865N/A => lid1 -> lid2 -> symbol1 -> symbol2

4865N/AcoerceSymbol = unsafeCoerce

4865N/A

4865N/AcoerceSymbolmap ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

4865N/A Typeable a)

4865N/A => lid1 -> lid2 -> Map.Map symbol1 a

4865N/A -> Map.Map symbol2 a

4865N/AcoerceSymbolmap = unsafeCoerce

4865N/A

4865N/AcoerceMapofsymbol ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

4865N/A Typeable a)

4865N/A => lid1 -> lid2 -> Map.Map a symbol1

4865N/A -> Map.Map a symbol2

4865N/AcoerceMapofsymbol = unsafeCoerce

4865N/A

4865N/AcoerceSymbItemsList ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

4865N/A Monad m) => lid1 -> lid2 -> String -> [symb_items1] -> m [symb_items2]

4865N/AcoerceSymbItemsList = primCoerce

4865N/A

4865N/AcoerceSymbMapItemsList ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

4865N/A Monad m) => lid1 -> lid2 -> String

4865N/A -> [symb_map_items1] -> m [symb_map_items2]

4865N/AcoerceSymbMapItemsList = primCoerce

4865N/A

4865N/AcoerceProofStatus ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

4865N/A Monad m) => lid1 -> lid2 -> String

4865N/A -> ProofStatus proof_tree1 -> m (ProofStatus proof_tree2)

4865N/AcoerceProofStatus = primCoerce

4865N/A

4865N/AcoerceSymbolSet ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

4865N/A Monad m) => lid1 -> lid2 -> String -> Set.Set symbol1 -> m (Set.Set symbol2)

4865N/AcoerceSymbolSet = primCoerce

4865N/A

4865N/AcoerceRawSymbolMap ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

4865N/A Monad m) => lid1 -> lid2 -> String -> EndoMap raw_symbol1

4865N/A -> m (EndoMap raw_symbol2)

4865N/AcoerceRawSymbolMap = primCoerce

4865N/A

4865N/AcoerceFreeDefMorphism ::

4865N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4865N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

4865N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4865N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

4865N/A Monad m) => lid1 -> lid2 -> String

4865N/A -> FreeDefMorphism sentence1 morphism1

4865N/A -> m (FreeDefMorphism sentence2 morphism2)

4865N/AcoerceFreeDefMorphism = primCoerce

4865N/A