content: {- |
  Module      :  ./HasCASL/Morphism.hs
  Description :  morphisms implementation
  Copyright   :  (c) Christian Maeder and Uni Bremen 2002-2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  mapping entities of morphisms
  
  -}
  
  module HasCASL.Morphism where
  
  import HasCASL.As
  import HasCASL.AsToLe
  import HasCASL.AsUtils
  import HasCASL.FoldType
  import HasCASL.Le
  import HasCASL.MapTerm
  import HasCASL.Merge
  import HasCASL.PrintLe
  import HasCASL.TypeAna
  
  import Common.DocUtils
  import Common.Doc
  import Common.Id
  import Common.Result
  import Common.Utils (composeMap)
  import Common.Lib.MapSet (setToMap)
  
  import Control.Monad
  import qualified Control.Monad.Fail as Fail
  
  import qualified Data.Set as Set
  import qualified Data.Map as Map
  
  disjointKeys :: (Ord a, Pretty a, Fail.MonadFail m) => Map.Map a b -> Map.Map a c
               -> m ()
  disjointKeys m1 m2 = let d = Map.keysSet $ Map.intersection m1 m2 in
    unless (Set.null d) $ Fail.fail $ show
           (sep [ text "overlapping identifiers for types and classes:"
                , pretty d])
  
  -- | map a kind along an identifier map
  mapKindI :: IdMap -> Kind -> Kind
  mapKindI jm = mapKind (\ a -> Map.findWithDefault a a jm)
  
  -- | map a kind along a signature morphism (variance is preserved)
  mapKinds :: Morphism -> Kind -> Kind
  mapKinds = mapKindI . classIdMap
  
  -- | only rename the kinds in a type
  mapKindsOfType :: IdMap -> TypeMap -> IdMap -> Type -> Type
  mapKindsOfType jm tm im = foldType mapTypeRec
      { foldTypeAbs = \ _ -> TypeAbs . mapTypeArg jm tm im
      , foldKindedType = \ _ t -> KindedType t . Set.map (mapKindI jm) }
  
  -- | map type, expand it, and also adjust the kinds
  mapTypeE :: IdMap -> TypeMap -> IdMap -> Type -> Type
  mapTypeE jm tm im =
    mapKindsOfType jm tm im . expandAliases tm . mapType im
  
  -- | map a kind along a signature morphism (variance is preserved)
  mapVarKind :: IdMap -> TypeMap -> IdMap -> VarKind -> VarKind
  mapVarKind jm tm im vk = case vk of
    VarKind k -> VarKind $ mapKindI jm k
    Downset ty -> Downset $ mapTypeE jm tm im ty
    _ -> vk
  
  mapTypeArg :: IdMap -> TypeMap -> IdMap -> TypeArg -> TypeArg
  mapTypeArg jm tm im (TypeArg i v vk rk c s r) =
    TypeArg i v (mapVarKind jm tm im vk) rk c s r
  
  mapTypeScheme :: IdMap -> TypeMap -> IdMap -> TypeScheme -> TypeScheme
  mapTypeScheme jm tm im (TypeScheme args ty ps) =
      TypeScheme (map (mapTypeArg jm tm im) args) (mapTypeE jm tm im ty) ps
  
  mapSen :: IdMap -> TypeMap -> IdMap -> FunMap -> Term -> Term
  mapSen jm tm im fm = mapTerm (mapFunSym jm tm im fm, mapTypeE jm tm im)
  
  getDatatypeIds :: DataEntry -> Set.Set Id
  getDatatypeIds (DataEntry _ i _ _ _ alts) =
      let getAltIds (Construct _ tys _ sels) = Set.union
              (Set.unions $ map getTypeIds tys)
              $ Set.unions $ concatMap (map getSelIds) sels
          getSelIds (Select _ ty _) = getTypeIds ty
          getTypeIds = idsOf (== 0)
      in Set.insert i $ Set.unions $ map getAltIds $ Set.toList alts
  
  mapDataEntry :: IdMap -> TypeMap -> IdMap -> FunMap -> DataEntry -> DataEntry
  mapDataEntry jm tm im fm (DataEntry dm i k args rk alts) =
      let nDm = Map.map (\ a -> Map.findWithDefault a a im) dm
          newargs = map (mapTypeArg jm tm im) args
          nIm = Map.difference im dm
      in DataEntry nDm i k newargs rk $ Set.map
             (mapAlt jm tm im fm nIm newargs
             $ patToType (Map.findWithDefault i i dm) newargs rk) alts
  
  mapAlt :: IdMap -> TypeMap -> IdMap -> FunMap -> IdMap -> [TypeArg] -> Type
    -> AltDefn -> AltDefn
  mapAlt jm tm im fm nIm args dt (Construct mi ts p sels) =
    let newTs = map (mapTypeE jm tm nIm) ts
        newSels = map (map (mapSel jm tm im fm nIm args dt)) sels
    in case mi of
      Just i -> let
          sc = TypeScheme args (getFunType dt p ts) nullRange
          (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
          in Construct (Just j) newTs (getPartiality newTs ty) newSels
      Nothing -> Construct mi newTs p newSels
  
  mapSel :: IdMap -> TypeMap -> IdMap -> FunMap -> IdMap -> [TypeArg] -> Type
    -> Selector -> Selector
  mapSel jm tm im fm nIm args dt (Select mid t p) =
    let newT = mapTypeE jm tm nIm t
    in case mid of
      Nothing -> Select mid newT p
      Just i -> let
          sc = TypeScheme args (getSelType dt p t) nullRange
          (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
          in Select (Just j) newT $ getPartiality [dt] ty
  
  {- | get the partiality from a constructor type
  with a given number of curried arguments. -}
  getPartiality :: [a] -> Type -> Partiality
  getPartiality args t = case getTypeAppl t of
     (TypeName i _ _, [_, res]) | isArrow i -> case args of
       [] -> Total
       [_] -> if isPartialArrow i then Partial else Total
       _ : rs -> getPartiality rs res
     (TypeName i _ _, [_]) | i == lazyTypeId ->
          if null args then Partial else error "getPartiality"
     _ -> Total
  
  mapSentence :: Morphism -> Sentence -> Result Sentence
  mapSentence m s = let
      tm = filterAliases . typeMap $ mtarget m
      im = typeIdMap m
      jm = classIdMap m
      fm = funMap m
      f = mapFunSym jm tm im fm
      in return $ case s of
        Formula t -> Formula $ mapSen jm tm im fm t
        DatatypeSen td -> DatatypeSen $ map (mapDataEntry jm tm im fm) td
        ProgEqSen i sc pe ->
          let (ni, nsc) = f (i, sc)
          in ProgEqSen ni nsc $ mapEq (f, mapTypeE jm tm im) pe
  
  mapFunSym :: IdMap -> TypeMap -> IdMap -> FunMap -> (Id, TypeScheme)
            -> (Id, TypeScheme)
  mapFunSym jm tm im fm (i, sc) =
      let msc = mapTypeScheme jm tm im sc
      in Map.findWithDefault (i, msc) (i, sc) fm
  
  ideMor :: Env -> Morphism
  ideMor e = mkMorphism e e
  
  compMor :: Morphism -> Morphism -> Result Morphism
  compMor m1 m2 = let
            tm1 = typeIdMap m1
            tm2 = typeIdMap m2
            ctm = composeMap (typeMap src) tm1 tm2
            cm1 = classIdMap m1
            cm2 = classIdMap m2
            ccm = composeMap (classMap src) cm1 cm2
            fm2 = funMap m2
            fm1 = funMap m1
            tar = mtarget m2
            src = msource m1
            tm = filterAliases $ typeMap tar
            emb = mkMorphism src tar
       in if isInclMor m1 && isInclMor m2 then return emb else do
       disjointKeys ctm ccm
       return emb
        { typeIdMap = ctm
        , classIdMap = ccm
        , funMap = Map.intersection
            (Map.foldrWithKey ( \ p1@(i, sc) p2 ->
                         let p3 = mapFunSym ccm tm tm2 fm2 p2
                             nSc = mapTypeScheme ccm tm ctm sc
                         in if (i, nSc) == p3 then Map.delete p1 else
                                Map.insert p1 p3)
                   fm2 fm1) $ Map.fromList $
                      concatMap ( \ (k, os) ->
                            map ( \ o -> ((k, opType o), ())) $ Set.toList os)
                       $ Map.toList $ assumps src }
  
  showEnvDiff :: Env -> Env -> String
  showEnvDiff e1 e2 =
      "Signature 1:\n" ++ showDoc e1 "\nSignature 2:\n"
             ++ showDoc e2 "\nDifference\n" ++ showDoc
                (diffEnv e1 e2) ""
  
  legalMor :: Morphism -> Result ()
  legalMor m = let
      s = msource m
      t = mtarget m
      ts = typeIdMap m
      cs = classIdMap m
      fs = funMap m in
      unless (all (`elem` Map.keys (typeMap s)) (Map.keys ts)
      && all (`elem` Map.keys (typeMap t)) (Map.elems ts)
      && all (`elem` Map.keys (classMap s)) (Map.keys cs)
      && all (`elem` Map.keys (classMap t)) (Map.elems cs)
      && all ((`elem` Map.keys (assumps s)) . fst) (Map.keys fs)
      && all ((`elem` Map.keys (assumps t)) . fst) (Map.elems fs))
       (Fail.fail "illegal HasCASL morphism")
  
  morphismUnion :: Morphism -> Morphism -> Result Morphism
  morphismUnion m1 m2 = do
    let s1 = msource m1
        s2 = msource m2
    s <- merge s1 s2
    t <- merge (mtarget m1) $ mtarget m2
    let tm1 = typeMap s1
        tm2 = typeMap s2
        im1 = typeIdMap m1
        im2 = typeIdMap m2
        -- unchanged types
        ut1 = Map.keysSet tm1 Set.\\ Map.keysSet im1
        ut2 = Map.keysSet tm2 Set.\\ Map.keysSet im2
        ima1 = Map.union im1 $ setToMap ut1
        ima2 = Map.union im2 $ setToMap ut2
        sAs = filterAliases $ typeMap s
        tAs = filterAliases $ typeMap t
        cm1 = classMap s1
        cm2 = classMap s2
        jm1 = classIdMap m1
        jm2 = classIdMap m2
        -- unchanged classes
        cut1 = Map.keysSet cm1 Set.\\ Map.keysSet jm1
        cut2 = Map.keysSet cm2 Set.\\ Map.keysSet jm2
        cima1 = Map.union jm1 $ setToMap cut1
        cima2 = Map.union jm2 $ setToMap cut2
        expP = Map.fromList . map ( \ ((i, o), (j, p)) ->
                              ((i, expand tAs o), (j, expand tAs p)))
                    . Map.toList
        fm1 = expP $ funMap m1
        fm2 = expP $ funMap m2
        af jm im = Set.unions . map ( \ (i, os) ->
                     Set.map ( \ o -> (i, mapTypeScheme jm tAs im
                                      $ expand sAs $ opType o)) os)
                        . Map.toList
                   -- unchanged functions
        uf1 = af jm1 im1 (assumps s1) Set.\\ Map.keysSet fm1
        uf2 = af jm2 im2 (assumps s2) Set.\\ Map.keysSet fm2
        fma1 = Map.union fm1 $ setToMap uf1
        fma2 = Map.union fm2 $ setToMap uf2
        showFun (i, ty) = showId i . (" : " ++) . showDoc ty
    tma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
                        Fail.fail $ "incompatible type mapping to `"
                           ++ showId t1 "' and '" ++ showId t2 "'") ima1 ima2
    cma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
                        Fail.fail $ "incompatible class mapping to `"
                           ++ showId t1 "' and '" ++ showId t2 "'") cima1 cima2
    fma <- mergeMap ( \ o1 o2 -> if o1 == o2 then return o1 else
                        Fail.fail $ "incompatible mapping to '"
                           ++ showFun o1 "' and '" ++ showFun o2 "'") fma1 fma2
    disjointKeys tma cma
    return (mkMorphism s t)
      { typeIdMap = tma
      , classIdMap = cma
      , funMap = fma }
  
  morphismToSymbMap :: Morphism -> SymbolMap
  morphismToSymbMap mor = let
      src = msource mor
      tar = mtarget mor
      im = typeIdMap mor
      jm = classIdMap mor
      tm = filterAliases $ typeMap tar
      classSymMap = Map.foldrWithKey ( \ i ti ->
         let j = Map.findWithDefault i i jm
             k = rawKind ti
             in Map.insert (idToClassSymbol i k)
                 $ idToClassSymbol j k) Map.empty $ classMap src
      typeSymMap = Map.foldrWithKey ( \ i ti ->
         let j = Map.findWithDefault i i im
             k = typeKind ti
             in Map.insert (idToTypeSymbol i k)
                 $ idToTypeSymbol j k) classSymMap $ typeMap src
     in Map.foldrWithKey
           ( \ i s m ->
               Set.fold ( \ oi ->
               let ty = opType oi
                   (j, t2) = mapFunSym jm tm im (funMap mor) (i, ty)
               in Map.insert (idToOpSymbol i ty)
                          (idToOpSymbol j t2)) m s)
           typeSymMap $ assumps src
  