content: {- |
  Module      :  ./HasCASL/SymbolMapAnalysis.hs
  Description :  analysis of symbol mappings
  Copyright   :  (c) Till Mossakowski, Christian Maeder and Uni Bremen 2002-2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  symbol map analysis for the HasCASL logic
  
  -}
  module HasCASL.SymbolMapAnalysis
      ( inducedFromMorphism
      , inducedFromToMorphism
      , cogeneratedSign
      , generatedSign
      ) where
  
  import HasCASL.As
  import HasCASL.Le
  import HasCASL.PrintLe
  import HasCASL.AsToLe
  import HasCASL.Symbol
  import HasCASL.Merge
  import HasCASL.Morphism
  import HasCASL.VarDecl
  import HasCASL.TypeAna
  
  import Common.DocUtils
  import Common.Id
  import Common.ExtSign
  import Common.Result
  import Common.Lib.State
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  import Control.Monad
  
  inducedFromMorphism :: RawSymbolMap -> Env -> Result Morphism
  inducedFromMorphism rmap sigma = do
      let srcTypeMap = typeMap sigma
          srcClassMap = classMap sigma
          assMap = assumps sigma
      myClassIdMap <- foldr
                (\ (s, ti) m ->
                 do s' <- classFun sigma rmap s (rawKind ti)
                    m1 <- m
                    return $ if s == s' then m1 else Map.insert s s' m1)
                (return Map.empty) $ Map.toList srcClassMap
      tarClassMap0 <- foldM (\ m (i, k) ->
         let ni = Map.findWithDefault i i myClassIdMap
             nk = mapClassInfo myClassIdMap k
         in case Map.lookup ni m of
           Nothing -> return $ Map.insert ni nk m
           Just ok -> do
             mk <- mergeClassInfo ok nk
             return $ Map.insert ni mk m)
         Map.empty $ Map.toList srcClassMap
      let tarClassMap = minimizeClassMap tarClassMap0
    -- compute the type map (as a Map)
      myTypeIdMap <- foldr
                (\ (s, ti) m ->
                 do s' <- typeFun sigma rmap s (typeKind ti)
                    m1 <- m
                    return $ if s == s' then m1 else Map.insert s s' m1)
                (return Map.empty) $ Map.toList srcTypeMap
      tarTypeMap0 <- foldM (\ m (i, k) ->
         let ni = Map.findWithDefault i i myTypeIdMap
             nk = mapTypeInfo myClassIdMap myTypeIdMap k
         in case Map.lookup ni m of
           Nothing -> return $ Map.insert ni nk m
           Just ok -> do
             mk <- mergeTypeInfo tarClassMap ok nk
             return $ Map.insert ni mk m)
         Map.empty $ Map.toList srcTypeMap
      let tarTypeMap = addUnit (addCpoMap srcClassMap) tarTypeMap0
          tarAliases = filterAliases tarTypeMap
    -- compute the op map (as a Map)
      op_Map <- Map.foldrWithKey
        (opFun rmap sigma myClassIdMap tarAliases myTypeIdMap)
        (return Map.empty) assMap
    -- compute target signature
      let tarTypeMap2 = Map.map
            (mapRestTypeInfo myClassIdMap tarAliases myTypeIdMap op_Map)
                          tarTypeMap
          sigma' = Map.foldrWithKey
            (mapOps myClassIdMap tarAliases myTypeIdMap op_Map) sigma
                     { typeMap = tarTypeMap2
                     , classMap = tarClassMap
                     , assumps = Map.empty }
                     assMap
      disjointKeys tarTypeMap2 tarClassMap
    -- return assembled morphism
      Result (envDiags sigma') $ Just ()
      return $ (mkMorphism sigma $ cleanEnv sigma')
                   { typeIdMap = myTypeIdMap
                   , classIdMap = myClassIdMap
                   , funMap = op_Map }
  
  mapRestTypeInfo :: IdMap -> TypeMap -> IdMap -> FunMap -> TypeInfo -> TypeInfo
  mapRestTypeInfo jm tm im fm ti = ti
      { typeDefn = mapRestTypeDefn jm tm im fm $ typeDefn ti }
  
  mapRestTypeDefn :: IdMap -> TypeMap -> IdMap -> FunMap -> TypeDefn -> TypeDefn
  mapRestTypeDefn jm tm im fm td = case td of
      DatatypeDefn de -> DatatypeDefn $ mapDataEntry jm tm im fm de
      AliasTypeDefn t -> AliasTypeDefn $ mapTypeE jm tm im t
      _ -> td
  
  mapClassInfo :: IdMap -> ClassInfo -> ClassInfo
  mapClassInfo im ti =
      ti { classKinds = Set.map (mapKindI im) $ classKinds ti }
  
  mapTypeInfo :: IdMap -> IdMap -> TypeInfo -> TypeInfo
  mapTypeInfo jm im ti =
      ti { superTypes = Set.map ( \ i -> Map.findWithDefault i i im)
                        $ superTypes ti
         , otherTypeKinds = Set.map (mapKindI jm) $ otherTypeKinds ti
         , typeDefn = mapTypeDefn im $ typeDefn ti }
  
  mapTypeDefn :: IdMap -> TypeDefn -> TypeDefn
  mapTypeDefn im td = case td of
      DatatypeDefn (DataEntry dm i k args rk alts) ->
          DatatypeDefn $ DataEntry
             (Map.map (\ a -> Map.findWithDefault a a im) dm)
             i k args rk alts
      AliasTypeDefn sc -> AliasTypeDefn $ mapType im sc
      _ -> td
  
  -- | compute class mapping
  classFun :: Env -> RawSymbolMap -> Id -> RawKind -> Result Id
  classFun _e rmap s k = do
      let rsys = Set.unions $ map ( \ x -> case Map.lookup x rmap of
                   Nothing -> Set.empty
                   Just r -> Set.singleton r)
                 [ASymbol $ idToClassSymbol s k, AnID s, AKindedId SyKclass s]
      -- rsys contains the raw symbols to which s is mapped to
      if Set.null rsys then return s -- use default = identity mapping
         else if Set.null $ Set.deleteMin rsys then
              return $ rawSymName $ Set.findMin rsys
              else Result [mkDiag Error ("class: " ++ showDoc s
                         " mapped ambiguously") rsys] Nothing
  
  -- | compute type mapping
  typeFun :: Env -> RawSymbolMap -> Id -> RawKind -> Result Id
  typeFun _e rmap s k = do
      let rsys = Set.unions $ map ( \ x -> case Map.lookup x rmap of
                   Nothing -> Set.empty
                   Just r -> Set.singleton r)
                 [ASymbol $ idToTypeSymbol s k, AnID s, AKindedId SyKtype s]
      -- rsys contains the raw symbols to which s is mapped to
      if Set.null rsys then return s -- use default = identity mapping
         else if Set.null $ Set.deleteMin rsys then
              return $ rawSymName $ Set.findMin rsys
              else Result [mkDiag Error ("type: " ++ showDoc s
                         " mapped ambiguously") rsys] Nothing
  
  -- | compute mapping of functions
  opFun :: RawSymbolMap -> Env -> IdMap -> TypeMap -> IdMap -> Id
        -> Set.Set OpInfo -> Result FunMap -> Result FunMap
  opFun rmap e jm tm im i ots m =
      -- first consider all directly mapped profiles
      let (ots1, m1) = Set.fold (directOpMap rmap e jm tm im i)
                      (Set.empty, m) ots
      -- now try the remaining ones with (un)kinded raw symbol
      in case (Map.lookup (AKindedId SyKop i) rmap, Map.lookup (AnID i) rmap) of
         (Just rsy1, Just rsy2) ->
               Result [mkDiag Error ("Operation " ++ showId i " is mapped twice")
                       (rsy1, rsy2)] Nothing
         (Just rsy, Nothing) ->
            Set.fold (insertmapOpSym e jm tm im i rsy) m1 ots1
         (Nothing, Just rsy) ->
            Set.fold (insertmapOpSym e jm tm im i rsy) m1 ots1
         -- Anything not mapped explicitly is left unchanged
         (Nothing, Nothing) -> m1
  
      {- try to map an operation symbol directly and
      collect all opTypes that cannot be mapped directly -}
  directOpMap :: RawSymbolMap -> Env -> IdMap -> TypeMap -> IdMap -> Id -> OpInfo
              -> (Set.Set TypeScheme, Result FunMap)
              -> (Set.Set TypeScheme, Result FunMap)
  directOpMap rmap e jm tm im i oi (ots, m) = let ot = opType oi in
      case Map.lookup (ASymbol $ idToOpSymbol i ot) rmap of
          Just rsy -> (ots, insertmapOpSym e jm tm im i rsy ot m)
          Nothing -> (Set.insert ot ots, m)
  
      -- map op symbol (id,ot) to raw symbol rsy
  mapOpSym :: Env -> IdMap -> TypeMap -> IdMap -> Id -> TypeScheme -> RawSymbol
           -> Result (Id, TypeScheme)
  mapOpSym _e jm tm im i ot rsy =
      let sc = mapTypeScheme jm tm im ot
          err d = Result [mkDiag Error ("Operation symbol " ++
                               showDoc (idToOpSymbol i sc)
                               "\nis mapped to " ++ d) rsy] Nothing in
        case rsy of
        AnID id' -> return (id', sc)
        AKindedId k id' -> case k of
            SyKop -> return (id', sc)
            _ -> err "wrongly kinded raw symbol"
        ASymbol sy -> case symType sy of
            OpAsItemType ot2
              | ot2 == sc -> return (j, sc)
              | ots == scs -> hint (j, sc) msg rgn
              | otherwise ->
                  warning (j, sc) (msg ++ "\nversus: " ++ ots) rgn
              where
                j = symName sy
                ots = showDoc ot2 ""
                scs = showDoc sc ""
                msg = "ignoring different target symbol type for '"
                  ++ showDoc sy "'"
                rgn = getRange ot2
            _ -> err "wrongly kinded symbol"
  
      -- insert mapping of op symbol (id, ot) to raw symbol rsy into m
  insertmapOpSym :: Env -> IdMap -> TypeMap -> IdMap -> Id -> RawSymbol
                 -> TypeScheme -> Result FunMap -> Result FunMap
  insertmapOpSym e jm tm im i rsy ot m = do
        m1 <- m
        q <- mapOpSym e jm tm im i ot rsy
        let p = (i, mapTypeScheme jm tm im ot)
        return $ if p == q then m1 else Map.insert (i, ot) q m1
      -- insert mapping of op symbol (i, ot) into m
  
    -- map the ops in the source signature
  mapOps :: IdMap -> TypeMap -> IdMap -> FunMap -> Id -> Set.Set OpInfo -> Env
         -> Env
  mapOps jm tm im fm i ots e =
      Set.fold ( \ ot e' ->
          let osc = opType ot
              sc = mapTypeScheme jm tm im osc
              (id', sc') = Map.findWithDefault (i, sc)
                           (i, osc) fm
              in execState (addOpId id' sc' (Set.map (mapOpAttr jm tm im fm)
                                            $ opAttrs ot)
                            (mapOpDefn jm tm im fm $ opDefn ot)) e')
      e ots
  
  mapOpAttr :: IdMap -> TypeMap -> IdMap -> FunMap -> OpAttr -> OpAttr
  mapOpAttr jm tm im fm oa = case oa of
      UnitOpAttr t ps -> UnitOpAttr (mapSen jm tm im fm t) ps
      _ -> oa
  
  mapOpDefn :: IdMap -> TypeMap -> IdMap -> FunMap -> OpDefn -> OpDefn
  mapOpDefn jm tm im fm d = case d of
     ConstructData i -> ConstructData $ Map.findWithDefault i i im
     SelectData cs i -> SelectData (Set.map (mapConstrInfo jm tm im fm) cs)
                        $ Map.findWithDefault i i im
     Definition b t -> Definition b $ mapSen jm tm im fm t
     _ -> d
  
  mapConstrInfo :: IdMap -> TypeMap -> IdMap -> FunMap -> ConstrInfo
                -> ConstrInfo
  mapConstrInfo jm tm im fm (ConstrInfo i sc) =
      let (j, nSc) = mapFunSym jm tm im fm (i, sc) in ConstrInfo j nSc
  
  -- | basically test if the renamed source signature is in the target signature
  inducedFromToMorphism :: RawSymbolMap -> ExtSign Env Symbol
                        -> ExtSign Env Symbol -> Result Morphism
  inducedFromToMorphism rmap1 e1@(ExtSign sigma1 sy1) (ExtSign sigma2 sy2) = do
    mor1 <- inducedFromMorphism rmap1 sigma1
    if isSubEnv (mtarget mor1) sigma2
      -- yes => we are done
      then return mor1 { mtarget = sigma2 }
      -- no => OK, we've to take a harder way
      else do
          let ft = Set.filter ( \ (Symbol _ t) -> case t of
                          TypeAsItemType _ -> True
                          _ -> False)
              s1 = ft sy1
              s2 = ft sy2
              err mor = Result [Diag Error ("No symbol mapping found for:\n"
                   ++ shows (printMap1 rmap1) "\nOriginal Signature 1:\n"
                   ++ showDoc e1 "\nInduced "
                   ++ showEnvDiff (mtarget mor) sigma2
                   ++ "\nMor fun-Map\n" ++ shows (printMap1 $ funMap mor) "\n"
                   ++ "\ndeclared Symbols of Signature 2:\n"
                   ++ showDoc sy2 "") nullRange] Nothing
          if Set.size s1 == 1 && Set.size s2 == 1 then do
            let Symbol n1 _ = Set.findMin s1
                Symbol n2 _ = Set.findMin s2
            mor2 <- inducedFromMorphism (Map.insert (AKindedId SyKtype n1)
                                         (AKindedId SyKtype n2) rmap1) sigma1
            if isSubEnv (mtarget mor2) sigma2
              then return mor2 { mtarget = sigma2 }
              else err mor2
            else err mor1
  
  -- | reveal the symbols in the set
  generatedSign :: SymbolSet -> Env -> Result Morphism
  generatedSign syms sigma =
      let signSyms = Set.unions $ symOf sigma
          closedSyms = closeSymbSet syms
          subSigma = plainHide (signSyms Set.\\ closedSyms) sigma
      in checkSymbols closedSyms signSyms $
         return $ mkMorphism subSigma sigma
  
  -- | hide the symbols in the set
  cogeneratedSign :: SymbolSet -> Env -> Result Morphism
  cogeneratedSign syms sigma =
      let signSyms = Set.unions $ symOf sigma
          subSigma = Set.fold hideRelSymbol sigma syms
          in checkSymbols syms signSyms $
             return $ mkMorphism subSigma sigma
  