{- |
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 :: lid1 -> lid2 -> String -> a -> m b
primCoerce i1 :: lid1
i1 i2 :: lid2
i2 err :: String
err a :: a
a =
  if lid1 -> String
forall lid. Language lid => lid -> String
language_name lid1
i1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== lid2 -> String
forall lid. Language lid => lid -> String
language_name lid2
i2
     then b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> m b) -> b -> m b
forall a b. (a -> b) -> a -> b
$ Dynamic -> b -> b
forall a. Typeable a => Dynamic -> a -> a
fromDyn (a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn a
a) (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ String -> b
forall a. HasCallStack => String -> a
error "primCoerce"
     else String -> m b
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m b) -> String -> m b
forall a b. (a -> b) -> a -> b
$ (if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
err then "" else String
err String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": ") String -> String -> String
forall a. [a] -> [a] -> [a]
++ "Logic "
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ lid2 -> String
forall lid. Language lid => lid -> String
language_name lid2
i2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " expected, but "
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ lid1 -> String
forall lid. Language lid => lid -> String
language_name lid1
i1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " found"

unsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2)
             => lid1 -> lid2 -> a -> b
unsafeCoerce :: lid1 -> lid2 -> a -> b
unsafeCoerce i1 :: lid1
i1 i2 :: lid2
i2 a :: a
a = b -> Maybe b -> b
forall a. a -> Maybe a -> a
fromMaybe (String -> b
forall a. HasCallStack => String -> a
error "unsafeCoerce") (lid1 -> lid2 -> String -> a -> Maybe b
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
primCoerce lid1
i1 lid2
i2 "" a
a)

coerceToResult :: (Typeable a, Typeable b, Language lid1, Language lid2) =>
                  lid1 -> lid2 -> Range -> a -> Result b
coerceToResult :: lid1 -> lid2 -> Range -> a -> Result b
coerceToResult i1 :: lid1
i1 i2 :: lid2
i2 pos :: Range
pos a :: a
a = Range -> Result b -> Result b
forall a. Range -> Result a -> Result a
adjustPos Range
pos (Result b -> Result b) -> Result b -> Result b
forall a b. (a -> b) -> a -> b
$ lid1 -> lid2 -> String -> a -> Result b
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
primCoerce lid1
i1 lid2
i2 "" a
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 :: lid1 -> lid2 -> String -> sublogics1 -> m sublogics2
coerceSublogic = lid1 -> lid2 -> String -> sublogics1 -> m sublogics2
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
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 :: lid1 -> lid2 -> sublogics1 -> sublogics2
forceCoerceSublogic = lid1 -> lid2 -> sublogics1 -> sublogics2
forall a b lid1 lid2.
(Typeable a, Typeable b, Language lid1, Language lid2) =>
lid1 -> lid2 -> a -> b
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 :: lid1 -> lid2 -> String -> sign1 -> m sign2
coercePlainSign = lid1 -> lid2 -> String -> sign1 -> m sign2
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
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 :: lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign = lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
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 :: lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory = lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
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 :: lid1
-> lid2
-> String
-> TheoryMorphism sign1 sentence1 morphism1 proof_tree1
-> m (TheoryMorphism sign2 sentence2 morphism2 proof_tree2)
coerceTheoryMorphism = lid1
-> lid2
-> String
-> TheoryMorphism sign1 sentence1 morphism1 proof_tree1
-> m (TheoryMorphism sign2 sentence2 morphism2 proof_tree2)
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
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 :: lid1 -> lid2 -> String -> [Named sentence1] -> m [Named sentence2]
coerceSens = lid1 -> lid2 -> String -> [Named sentence1] -> m [Named sentence2]
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
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 :: lid1 -> lid2 -> String -> morphism1 -> m morphism2
coerceMorphism = lid1 -> lid2 -> String -> morphism1 -> m morphism2
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
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 :: lid1 -> lid2 -> symbol1 -> symbol2
coerceSymbol = lid1 -> lid2 -> symbol1 -> symbol2
forall a b lid1 lid2.
(Typeable a, Typeable b, Language lid1, Language lid2) =>
lid1 -> lid2 -> a -> b
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 :: lid1 -> lid2 -> Map symbol1 a -> Map symbol2 a
coerceSymbolmap = lid1 -> lid2 -> Map symbol1 a -> Map symbol2 a
forall a b lid1 lid2.
(Typeable a, Typeable b, Language lid1, Language lid2) =>
lid1 -> lid2 -> a -> b
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 :: lid1 -> lid2 -> Map a symbol1 -> Map a symbol2
coerceMapofsymbol = lid1 -> lid2 -> Map a symbol1 -> Map a symbol2
forall a b lid1 lid2.
(Typeable a, Typeable b, Language lid1, Language lid2) =>
lid1 -> lid2 -> a -> b
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 :: lid1 -> lid2 -> String -> [symb_items1] -> m [symb_items2]
coerceSymbItemsList = lid1 -> lid2 -> String -> [symb_items1] -> m [symb_items2]
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
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 :: lid1 -> lid2 -> String -> [symb_map_items1] -> m [symb_map_items2]
coerceSymbMapItemsList = lid1 -> lid2 -> String -> [symb_map_items1] -> m [symb_map_items2]
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
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 :: lid1
-> lid2
-> String
-> ProofStatus proof_tree1
-> m (ProofStatus proof_tree2)
coerceProofStatus = lid1
-> lid2
-> String
-> ProofStatus proof_tree1
-> m (ProofStatus proof_tree2)
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
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 :: lid1 -> lid2 -> String -> Set symbol1 -> m (Set symbol2)
coerceSymbolSet = lid1 -> lid2 -> String -> Set symbol1 -> m (Set symbol2)
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
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 :: lid1
-> lid2 -> String -> EndoMap raw_symbol1 -> m (EndoMap raw_symbol2)
coerceRawSymbolMap = lid1
-> lid2 -> String -> EndoMap raw_symbol1 -> m (EndoMap raw_symbol2)
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
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 :: lid1
-> lid2
-> String
-> FreeDefMorphism sentence1 morphism1
-> m (FreeDefMorphism sentence2 morphism2)
coerceFreeDefMorphism = lid1
-> lid2
-> String
-> FreeDefMorphism sentence1 morphism1
-> m (FreeDefMorphism sentence2 morphism2)
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
primCoerce