content: {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveDataTypeable
    , FlexibleInstances, UndecidableInstances, ExistentialQuantification #-}
  {- |
  Module      :  ./Logic/Comorphism.hs
  Description :  interface and class for logic translations
  Copyright   :  (c) Till Mossakowski, Uni Bremen 2002-2006
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  till@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  non-portable (via Logic)
  
  Central interface (type class) for logic translations (comorphisms) in Hets
     These are just collections of
     functions between (some of) the types of logics.
  
     References: see Logic.hs
  -}
  
  module Logic.Comorphism
      ( CompComorphism (..)
      , InclComorphism
      , inclusion_logic
      , inclusion_source_sublogic
      , inclusion_target_sublogic
      , mkInclComorphism
      , mkIdComorphism
      , Comorphism (..)
      , targetSublogic
      , map_sign
      , wrapMapTheory
      , wrapMapTheoryPossiblyLossy
      , mkTheoryMapping
      , AnyComorphism (..)
      , idComorphism
      , isIdComorphism
      , isModelTransportable
      , hasModelExpansion
      , isEps
      , isRps
      , isWeaklyAmalgamable
      , compComorphism
      ) where
  
  import Logic.Logic
  import Logic.Coerce
  
  import Common.AS_Annotation
  import Common.Doc
  import Common.DocUtils
  import Common.Id
  import Common.LibName
  import Common.ProofUtils
  import Common.Result
  import qualified Control.Monad.Fail as Fail
  
  import Data.Data
  import Data.Maybe
  import qualified Data.Set as Set
  
  class (Language cid,
         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) =>
    Comorphism cid
              lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                  sign1 morphism1 symbol1 raw_symbol1 proof_tree1
              lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                  sign2 morphism2 symbol2 raw_symbol2 proof_tree2
     | cid -> lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                  sign1 morphism1 symbol1 raw_symbol1 proof_tree1
              lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                  sign2 morphism2 symbol2 raw_symbol2 proof_tree2
    where
      {- source and target logic and sublogic
      the source sublogic is the maximal one for which the comorphism works -}
      sourceLogic :: cid -> lid1
      sourceSublogic :: cid -> sublogics1
      sourceSublogic cid = top_sublogic $ sourceLogic cid
      {- needed for lossy translations. Is stricter than sourceSublogic.
         Should be merged with sourceSublogic once #1706 has been fixed. -}
      sourceSublogicLossy :: cid -> sublogics1
      sourceSublogicLossy = sourceSublogic
      minSourceTheory :: cid -> Maybe (LibName, String)
      minSourceTheory _ = Nothing
      targetLogic :: cid -> lid2
      {- finer information of target sublogics corresponding to source sublogics
      this function must be partial because mapTheory is partial -}
      mapSublogic :: cid -> sublogics1 -> Maybe sublogics2
      mapSublogic cid _ = Just $ top_sublogic $ targetLogic cid
      {- the translation functions are partial
      because the target may be a sublanguage
      map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2
      cover theoroidal comorphisms as well -}
      map_theory :: cid -> (sign1, [Named sentence1])
                        -> Result (sign2, [Named sentence2])
      -- map_theory but also consider sentence marks
      mapMarkedTheory :: cid -> (sign1, [Named sentence1])
                        -> Result (sign2, [Named sentence2])
      mapMarkedTheory cid (sig, sens) = do
        (sig2, sens2) <- map_theory cid (sig, map unmark sens)
        return (sig2, map (markSen $ language_name cid) sens2)
      map_morphism :: cid -> morphism1 -> Result morphism2
      map_morphism = mapDefaultMorphism
      map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
            {- also covers semi-comorphisms
            with no sentence translation
            - but these are spans! -}
      map_sentence = failMapSentence
      map_symbol :: cid -> sign1 -> symbol1 -> Set.Set symbol2
      map_symbol = errMapSymbol
      extractModel :: cid -> sign1 -> proof_tree2
                   -> Result (sign1, [Named sentence1])
      extractModel cid _ _ = Fail.fail
        $ "extractModel not implemented for comorphism "
        ++ language_name cid
      -- properties of comorphisms
      is_model_transportable :: cid -> Bool
      {- a comorphism (\phi, \alpha, \beta) is model-transportable
      if for any signature \Sigma,
      any \Sigma-model M and any \phi(\Sigma)-model N
      for any isomorphism           h : \beta_\Sigma(N) -> M
      there exists an isomorphism   h': N -> M' such that \beta_\Sigma(h') = h -}
      is_model_transportable _ = False
      has_model_expansion :: cid -> Bool
      has_model_expansion _ = False
      is_weakly_amalgamable :: cid -> Bool
      is_weakly_amalgamable _ = False
      constituents :: cid -> [String]
      constituents cid = [language_name cid]
      isInclusionComorphism :: cid -> Bool
      isInclusionComorphism _ = False
      -- reduction preserves satisfaction
      rps :: cid -> Bool
      rps _ = True
      -- expansion preserves satisfaction
      eps :: cid -> Bool
      eps _ = True
      -- a comorphism is a generalized theoroidal comorphism (GTC)
      -- if the presence of an axiom in a theory
      -- impacts on the signature of the translated theory along the GTC
      isGTC :: cid -> Bool 
      isGTC _ = False
  
  targetSublogic :: Comorphism cid
              lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                  sign1 morphism1 symbol1 raw_symbol1 proof_tree1
              lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                  sign2 morphism2 symbol2 raw_symbol2 proof_tree2
           => cid -> sublogics2
  targetSublogic cid = fromMaybe (top_sublogic $ targetLogic cid)
                             $ mapSublogic cid $ sourceSublogic cid
  
  -- | this function is based on 'map_theory' using no sentences as input
  map_sign :: Comorphism cid
              lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                  sign1 morphism1 symbol1 raw_symbol1 proof_tree1
              lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                  sign2 morphism2 symbol2 raw_symbol2 proof_tree2
           => cid -> sign1 -> Result (sign2, [Named sentence2])
  map_sign cid sign = wrapMapTheory cid (sign, [])
  
  mapDefaultMorphism :: Comorphism cid
              lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                  sign1 morphism1 symbol1 raw_symbol1 proof_tree1
              lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                  sign2 morphism2 symbol2 raw_symbol2 proof_tree2
           => cid -> morphism1 -> Result morphism2
  mapDefaultMorphism cid mor = do
    (sig1, _) <- map_sign cid $ dom mor
    (sig2, _) <- map_sign cid $ cod mor
    inclusion (targetLogic cid) sig1 sig2
  
  failMapSentence :: Comorphism cid
              lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                  sign1 morphism1 symbol1 raw_symbol1 proof_tree1
              lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                  sign2 morphism2 symbol2 raw_symbol2 proof_tree2
           => cid -> sign1 -> sentence1 -> Result sentence2
  failMapSentence cid _ _ =
      Fail.fail $ "Unsupported sentence translation " ++ show cid
  
  errMapSymbol :: Comorphism cid
              lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                  sign1 morphism1 symbol1 raw_symbol1 proof_tree1
              lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                  sign2 morphism2 symbol2 raw_symbol2 proof_tree2
           => cid -> sign1 -> symbol1 -> Set.Set symbol2
  errMapSymbol cid _ _ = error $ "no symbol mapping for " ++ show cid
  
  -- | use this function instead of 'mapMarkedTheory'
  wrapMapTheoryPossiblyLossy :: Comorphism cid
              lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                  sign1 morphism1 symbol1 raw_symbol1 proof_tree1
              lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                  sign2 morphism2 symbol2 raw_symbol2 proof_tree2
              => Bool -> cid -> (sign1, [Named sentence1])
                     -> Result (sign2, [Named sentence2])
  wrapMapTheoryPossiblyLossy lossy cid (sign, sens) =
    let res = mapMarkedTheory cid (sign, sens)
        lid1 = sourceLogic cid
        thDoc = show (vcat $ pretty sign : map (print_named lid1) sens)
    in
    if isIdComorphism $ Comorphism cid
    then res
    else let sub = if lossy then sourceSublogicLossy cid else sourceSublogic cid
             sigLog = minSublogic sign
             senLog = foldl lub sigLog $ map (minSublogic . sentence) sens
             isInSub s = isSubElem (minSublogic $ sentence s) sub 
             sensLossy = filter isInSub sens
             resLossy = mapMarkedTheory cid (sign, sensLossy)
          in if isSubElem senLog sub
                   then res
                   else
                      if lossy && isSubElem sigLog sub
                      then resLossy 
                      else Result
                       [ Diag Hint thDoc nullRange
                       , Diag Error
                           ("for '" ++ language_name cid ++
                                "' expected sublogic '" ++
                                sublogicName sub ++
                                "'\n but found sublogic '" ++
                                sublogicName senLog ++
                                "' with signature sublogic '" ++
                                sublogicName sigLog ++ "'") nullRange] Nothing
  
  wrapMapTheory :: Comorphism cid
              lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                  sign1 morphism1 symbol1 raw_symbol1 proof_tree1
              lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                  sign2 morphism2 symbol2 raw_symbol2 proof_tree2
              => cid -> (sign1, [Named sentence1])
                     -> Result (sign2, [Named sentence2])
  wrapMapTheory = wrapMapTheoryPossiblyLossy False
  
  mkTheoryMapping :: Monad m => (sign1 -> m (sign2, [Named sentence2]))
                     -> (sign1 -> sentence1 -> m sentence2)
                     -> (sign1, [Named sentence1])
                     -> m (sign2, [Named sentence2])
  mkTheoryMapping mapSig mapSen (sign, sens) = do
         (sign', sens') <- mapSig sign
         sens'' <- mapM (mapNamedM (mapSen sign) . unmark) sens
         return (sign', nameAndDisambiguate
           $ map (markSen "SignatureProperty") sens' ++ sens'')
  
  data InclComorphism lid sublogics = InclComorphism
    { inclusion_logic :: lid
    , inclusion_source_sublogic :: sublogics
    , inclusion_target_sublogic :: sublogics }
    deriving (Show, Typeable, Data)
  
  -- | construction of an identity comorphism
  mkIdComorphism :: (Logic lid sublogics
                        basic_spec sentence symb_items symb_map_items
                        sign morphism symbol raw_symbol proof_tree) =>
                    lid -> sublogics -> InclComorphism lid sublogics
  mkIdComorphism lid sub = InclComorphism
    { inclusion_logic = lid
    , inclusion_source_sublogic = sub
    , inclusion_target_sublogic = sub }
  
  -- | construction of an inclusion comorphism
  mkInclComorphism :: (Logic lid sublogics
                             basic_spec sentence symb_items symb_map_items
                             sign morphism symbol raw_symbol proof_tree,
                       Fail.MonadFail m) =>
                      lid -> sublogics -> sublogics
                   -> m (InclComorphism lid sublogics)
  mkInclComorphism lid srcSub trgSub =
      if isSubElem srcSub trgSub
      then return InclComorphism
        { inclusion_logic = lid
        , inclusion_source_sublogic = srcSub
        , inclusion_target_sublogic = trgSub }
      else Fail.fail ("mkInclComorphism: first sublogic must be a " ++
                 "subElem of the second sublogic")
  
  instance (Language lid, Eq sublogics, Show sublogics, SublogicName sublogics)
      => Language (InclComorphism lid sublogics) where
          language_name (InclComorphism lid sub_src sub_trg) =
              let sblName = sublogicName sub_src
                  lname = language_name lid
              in if sub_src == sub_trg
                 then "id_" ++ lname ++
                      if null sblName then "" else '.' : sblName
                 else "incl_" ++ lname ++ ':'
                      : sblName ++ "->" ++ sublogicName sub_trg
  
  instance Logic lid sublogics
          basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree =>
           Comorphism (InclComorphism lid sublogics)
            lid sublogics
            basic_spec sentence symb_items symb_map_items
            sign morphism symbol raw_symbol proof_tree
            lid sublogics
            basic_spec sentence symb_items symb_map_items
            sign morphism symbol raw_symbol proof_tree
           where
             sourceLogic = inclusion_logic
             targetLogic = inclusion_logic
             sourceSublogic = inclusion_source_sublogic
             mapSublogic cid subl =
                 if isSubElem subl $ inclusion_source_sublogic cid
                 then Just subl
                 else Nothing
             map_theory _ = return
             map_morphism _ = return
             map_sentence _ _ = return
             map_symbol _ _ = Set.singleton
             constituents cid =
                 if inclusion_source_sublogic cid
                        == inclusion_target_sublogic cid
                 then []
                 else [language_name cid]
             is_model_transportable _ = True
             has_model_expansion _ = True
             is_weakly_amalgamable _ = True
             isInclusionComorphism _ = True
  
  data CompComorphism cid1 cid2 = CompComorphism cid1 cid2
    deriving (Show, Typeable, Data)
  
  instance (Language cid1, Language cid2)
            => Language (CompComorphism cid1 cid2) where
     language_name (CompComorphism cid1 cid2) =
       language_name cid1 ++ ";" ++ language_name cid2
  
  instance (Comorphism cid1
              lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                  sign1 morphism1 symbol1 raw_symbol1 proof_tree1
              lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                  sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
            Comorphism cid2
              lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
                  sign4 morphism4 symbol4 raw_symbol4 proof_tree4
              lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
                  sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
            => Comorphism (CompComorphism cid1 cid2)
                lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
                lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
                sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where
     sourceLogic (CompComorphism cid1 _) =
       sourceLogic cid1
     targetLogic (CompComorphism _ cid2) =
       targetLogic cid2
     sourceSublogic (CompComorphism cid1 _) =
       sourceSublogic cid1
     mapSublogic (CompComorphism cid1 cid2) sl =
           mapSublogic cid1 sl >>=
             mapSublogic cid2 .
              forceCoerceSublogic (targetLogic cid1) (sourceLogic cid2)
     map_sentence (CompComorphism cid1 cid2) si1 se1 =
           do (si2, _) <- map_sign cid1 si1
              se2 <- map_sentence cid1 si1 se1
              (si2', se2') <- coerceBasicTheory
                  (targetLogic cid1) (sourceLogic cid2)
                  "Mapping sentence along comorphism" (si2, [makeNamed "" se2])
              case se2' of
                  [x] -> map_sentence cid2 si2' $ sentence x
                  _ -> error "CompComorphism.map_sentence"
  
     map_theory (CompComorphism cid1 cid2) ti1 =
           do ti2 <- map_theory cid1 ti1
              ti2' <- coerceBasicTheory (targetLogic cid1) (sourceLogic cid2)
                          "Mapping theory along comorphism" ti2
              wrapMapTheory cid2 ti2'
  
     map_morphism (CompComorphism cid1 cid2) m1 =
         do m2 <- map_morphism cid1 m1
            m3 <- coerceMorphism (targetLogic cid1) (sourceLogic cid2)
                    "Mapping signature morphism along comorphism" m2
            map_morphism cid2 m3
  
     map_symbol (CompComorphism cid1 cid2) sig1 = let
       th = map_sign cid1 sig1 in
      case maybeResult th of
       Nothing -> error "failed translating signature"
       Just (sig2', _) -> let
         th2 = coerceBasicTheory
                  (targetLogic cid1) (sourceLogic cid2)
                  "Mapping symbol along comorphism" (sig2', [])
         in case maybeResult th2 of
             Nothing -> error "failed coercing"
             Just (sig2, _) ->
              \ s1 ->
                let mycast = coerceSymbol (targetLogic cid1) (sourceLogic cid2)
                in Set.unions
                  (map (map_symbol cid2 sig2 . mycast)
                   (Set.toList (map_symbol cid1 sig1 s1)))
  
     extractModel (CompComorphism cid1 cid2) sign pt3 =
       let lid1 = sourceLogic cid1
           lid3 = sourceLogic cid2
       in if language_name lid1 == language_name lid3 then do
           bTh1 <- map_sign cid1 sign
           (sign1, _) <-
             coerceBasicTheory (targetLogic cid1) lid3 "extractModel1" bTh1
           bTh2 <- extractModel cid2 sign1 pt3
           coerceBasicTheory lid3 lid1 "extractModel2" bTh2
       else Fail.fail $ "extractModel not implemented for comorphism composition with "
            ++ language_name cid1
     constituents (CompComorphism cid1 cid2) =
        constituents cid1 ++ constituents cid2
  
     is_model_transportable (CompComorphism cid1 cid2) =
         is_model_transportable cid1 && is_model_transportable cid2
  
     has_model_expansion (CompComorphism cid1 cid2) =
          has_model_expansion cid1 && has_model_expansion cid2
  
     is_weakly_amalgamable (CompComorphism cid1 cid2) =
          is_weakly_amalgamable cid1 && is_weakly_amalgamable cid2
     isInclusionComorphism (CompComorphism cid1 cid2) =
         isInclusionComorphism cid1 && isInclusionComorphism cid2
  
  -- * Comorphisms and existential types for the logic graph
  
  -- | Existential type for comorphisms
  data AnyComorphism = forall cid lid1 sublogics1
          basic_spec1 sentence1 symb_items1 symb_map_items1
          sign1 morphism1 symbol1 raw_symbol1 proof_tree1
          lid2 sublogics2
          basic_spec2 sentence2 symb_items2 symb_map_items2
          sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
        Comorphism cid
                   lid1 sublogics1 basic_spec1 sentence1
                   symb_items1 symb_map_items1
                   sign1 morphism1 symbol1 raw_symbol1 proof_tree1
                   lid2 sublogics2 basic_spec2 sentence2
                   symb_items2 symb_map_items2
                   sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
        Comorphism cid deriving Typeable -- used for GTheory
  
  instance Eq AnyComorphism where
      a == b = compare a b == EQ
  
  instance Ord AnyComorphism where
    compare (Comorphism cid1) (Comorphism cid2) = compare
       (language_name cid1, constituents cid1)
       (language_name cid2, constituents cid2)
    -- maybe needs to be refined, using comorphism translations?
  
  instance Show AnyComorphism where
    show (Comorphism cid) = language_name cid
      ++ " : " ++ language_name (sourceLogic cid)
      ++ " -> " ++ language_name (targetLogic cid)
  
  instance Pretty AnyComorphism where
    pretty = text . show
  
  -- | compute the identity comorphism for a logic
  idComorphism :: AnyLogic -> AnyComorphism
  idComorphism (Logic lid) = Comorphism (mkIdComorphism lid (top_sublogic lid))
  
  -- | Test whether a comporphism is the identity
  isIdComorphism :: AnyComorphism -> Bool
  isIdComorphism (Comorphism cid) = null $ constituents cid
  
  -- * Properties of comorphisms
  
  -- | Test whether a comorphism is model-transportable
  isModelTransportable :: AnyComorphism -> Bool
  isModelTransportable (Comorphism cid) = is_model_transportable cid
  
  -- | Test whether a comorphism has model expansion
  hasModelExpansion :: AnyComorphism -> Bool
  hasModelExpansion (Comorphism cid) = has_model_expansion cid
  
  -- | Test whether a comorphism is weakly amalgamable
  isWeaklyAmalgamable :: AnyComorphism -> Bool
  isWeaklyAmalgamable (Comorphism cid) = is_weakly_amalgamable cid
  
  -- | Tests whether a comorphism is rps or eps
  
  isEps :: AnyComorphism -> Bool
  isEps (Comorphism cid) = eps cid
  
  isRps :: AnyComorphism -> Bool
  isRps (Comorphism cid) = rps cid
  
  
  -- | Compose comorphisms
  compComorphism :: Fail.MonadFail m => AnyComorphism -> AnyComorphism -> m AnyComorphism
  compComorphism (Comorphism cid1) (Comorphism cid2) =
     let l1 = targetLogic cid1
         l2 = sourceLogic cid2
         msg = "ogic mismatch in composition of " ++ language_name cid1
                    ++ " and " ++ language_name cid2
     in
     if language_name l1 == language_name l2 then
        if isSubElem (forceCoerceSublogic l1 l2 $ targetSublogic cid1)
              $ sourceSublogic cid2
         then return $ Comorphism (CompComorphism cid1 cid2)
         else Fail.fail $ "Subl" ++ msg ++ " (Expected sublogic "
                            ++ sublogicName (sourceSublogic cid2)
                            ++ " but found sublogic "
                            ++ sublogicName (targetSublogic cid1) ++ ")"
      else Fail.fail $ 'L' : msg ++ " (Expected logic "
                            ++ language_name l2
                            ++ " but found logic "
                            ++ language_name l1 ++ ")"
  