content: {- |
  Module      :  ./Logic/Coerce.hs
  Description :  coerce logic entities dynamically
  Copyright   :  (c) T. Mossakowski, C. Maeder, Uni Bremen 2005-2006
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  till@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  non-portable (various -fglasgow-exts extensions)
  
  Functions for coercion used in Grothendieck.hs and Analysis modules:
    These tell the typechecker that things dynamically belong to the same logic
  -}
  
  module Logic.Coerce where
  
  import Logic.Logic
  import Logic.Prover
  import Common.ExtSign
  import Common.Id
  import Common.Result
  import Common.AS_Annotation
  import qualified Control.Monad.Fail as Fail
  import qualified Data.Set as Set
  import qualified Data.Map as Map
  import Data.Dynamic
  import ATC.LibName ()
  import ATC.Prover ()
  import ATC.ExtSign ()
  import Data.Maybe (fromMaybe)
  
  -- coercion using the language name
  primCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2,
                 Fail.MonadFail 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 "primCoerce"
       else Fail.fail $ (if null err then "" else err ++ ": ") ++ "Logic "
                ++ language_name i2 ++ " expected, but "
                ++ language_name i1 ++ " found"
  
  unsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2)
               => lid1 -> lid2 -> a -> b
  unsafeCoerce i1 i2 a = fromMaybe (error "unsafeCoerce") (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,
     Fail.MonadFail m)
     => lid1 -> lid2 -> String -> sublogics1 -> m sublogics2
  coerceSublogic = primCoerce
  
  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 = unsafeCoerce
  
  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,
     Fail.MonadFail m) => lid1 -> lid2 -> String -> sign1 -> m sign2
  coercePlainSign = primCoerce
  
  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,
     Fail.MonadFail m) => lid1 -> lid2 -> String -> ExtSign sign1 symbol1
      -> m (ExtSign sign2 symbol2)
  coerceSign = primCoerce
  
  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,
     Fail.MonadFail m) => lid1 -> lid2 -> String
              -> (sign1, [Named sentence1]) -> m (sign2, [Named sentence2])
  coerceBasicTheory = primCoerce
  
  coerceTheoryMorphism ::
     (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,
     Fail.MonadFail m) => lid1 -> lid2 -> String
              -> TheoryMorphism sign1 sentence1 morphism1 proof_tree1 -> m (TheoryMorphism sign2 sentence2 morphism2 proof_tree2)
  coerceTheoryMorphism = primCoerce
  
  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,
     Fail.MonadFail m) => lid1 -> lid2 -> String
              -> [Named sentence1] -> m [Named sentence2]
  coerceSens = primCoerce
  
  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,
     Fail.MonadFail m) => lid1 -> lid2 -> String -> morphism1 -> m morphism2
  coerceMorphism = primCoerce
  
  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 = unsafeCoerce
  
  coerceSymbolmap ::
     (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,
     Typeable a)
     => lid1 -> lid2 -> Map.Map symbol1 a
             -> Map.Map symbol2 a
  coerceSymbolmap = unsafeCoerce
  
  coerceMapofsymbol ::
     (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,
     Typeable a)
     => lid1 -> lid2 -> Map.Map a symbol1
             -> Map.Map a symbol2
  coerceMapofsymbol = unsafeCoerce
  
  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,
     Fail.MonadFail m) => lid1 -> lid2 -> String -> [symb_items1] -> m [symb_items2]
  coerceSymbItemsList = primCoerce
  
  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,
     Fail.MonadFail m) => lid1 -> lid2 -> String
        -> [symb_map_items1] -> m [symb_map_items2]
  coerceSymbMapItemsList = primCoerce
  
  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,
     Fail.MonadFail m) => lid1 -> lid2 -> String
        -> ProofStatus proof_tree1 -> m (ProofStatus proof_tree2)
  coerceProofStatus = primCoerce
  
  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,
     Fail.MonadFail m) => lid1 -> lid2 -> String -> Set.Set symbol1 -> m (Set.Set symbol2)
  coerceSymbolSet = primCoerce
  
  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,
     Fail.MonadFail m) => lid1 -> lid2 -> String -> EndoMap raw_symbol1
        -> m (EndoMap raw_symbol2)
  coerceRawSymbolMap = primCoerce
  
  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,
     Fail.MonadFail m) => lid1 -> lid2 -> String
                  -> FreeDefMorphism sentence1 morphism1
                  -> m (FreeDefMorphism sentence2 morphism2)
  coerceFreeDefMorphism = primCoerce
  