{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Maude/Morphism.hs
Description :  Maude Morphisms
Copyright   :  (c) Martin Kuehl, Uni Bremen 2008-2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  mkhl@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

Definition of morphisms for Maude.
-}

module Maude.Morphism (
    -- * Types

    -- ** The Morphism type
    Morphism (..),
    -- ** Auxiliary type
    SortMap,
    KindMap,
    OpMap,
    -- * Construction
    fromSignRenamings,
    fromSignsRenamings,
    empty,
    identity,
    inclusion,
    -- * Combination
    inverse,
    union,
    compose,
    -- * Testing
    isInclusion,
    isLegal,
    -- * Conversion
    symbolMap,
    -- * Modification
    setTarget,
    qualifySorts,
    applyRenamings,
    extendWithSortRenaming,
    -- * Application
    translateSentence,
    translateSorts,
) where

import Maude.AS_Maude
import Maude.Symbol
import Maude.Meta
import Maude.Util
import Maude.Printing ()

import Maude.Sign (Sign, kindRel, KindRel)
import Maude.Sentence (Sentence)
import qualified Maude.Sign as Sign

import Data.Data
import Data.List (partition)
import Data.Maybe (fromJust)
import qualified Data.Set as Set
import qualified Data.Map as Map

import Common.Result (Result)

import Common.Doc hiding (empty)
import Common.DocUtils (Pretty (..))

import Control.Monad (unless)

-- * Types

-- ** Auxiliary types

type SortMap = SymbolMap
type KindMap = SymbolMap
type OpMap = SymbolMap
type LabelMap = SymbolMap

-- ** The Morphism type

data Morphism = Morphism {
        source :: Sign,
        target :: Sign,
        sortMap :: SortMap,
        kindMap :: KindMap,
        opMap :: OpMap,
        labelMap :: LabelMap
    } deriving (Show, Ord, Eq, Typeable)

-- ** 'Morphism' instances

instance Pretty Morphism where
    pretty mor = let
        pr'pair txt left right = hsep
            [txt, pretty left, text "to", pretty right]
        pr'ops src tgt = pr'pair (text "op") src (getName tgt)
        pr'map fun = vcat . map (uncurry fun) . Map.toList
        smap = pr'map (pr'pair $ text "sort") $ sortMap mor
        kmap = pr'map (pr'pair $ text "kind") $ kindMap mor
        omap = pr'map pr'ops $ opMap mor
        lmap = pr'map (pr'pair $ text "label") $ labelMap mor
        s = pretty $ source mor
        t = pretty $ target mor
        in vcat [ smap, kmap, omap, lmap, pretty "\nSource:\n", s
                , pretty "\nTarget\n", t ]

-- * Helper functions

-- ** to modify Morphisms

mapTarget :: (Sign -> Sign) -> Morphism -> Morphism
mapTarget func mor = mor { target = func $ target mor }

mapSortMap :: (SortMap -> SortMap) -> Morphism -> Morphism
mapSortMap func mor = mor { sortMap = func $ sortMap mor }
mapOpMap :: (OpMap -> OpMap) -> Morphism -> Morphism
mapOpMap func mor = mor { opMap = func $ opMap mor }
mapLabelMap :: (LabelMap -> LabelMap) -> Morphism -> Morphism
mapLabelMap func mor = mor { labelMap = func $ labelMap mor }

-- ** to handle Renamings

-- TODO: Handle Attrs in Op Renamings.
renamingSymbolsMaybe :: Renaming -> Maybe (Symbol, Symbol)
renamingSymbolsMaybe rename = case rename of
    SortRenaming src tgt -> Just (asSymbol src, asSymbol tgt)
    LabelRenaming src tgt -> Just (asSymbol src, asSymbol tgt)
    OpRenaming1 src (To tgt _) -> Just (asSymbol src, asSymbol tgt)
    OpRenaming2 src dom cod (To tgt _) -> let
        src' = Op src dom cod []
        tgt' = Op tgt dom cod []
        in Just (asSymbol src', asSymbol tgt')
    TermMap _ _ -> Nothing

-- | Extract the 'Symbol's from a 'Renaming', if possible.
renamingSymbols :: Renaming -> (Symbol, Symbol)
renamingSymbols = fromJust . renamingSymbolsMaybe

-- | Separate Operator and other Renamings.
partitionRenamings :: [Renaming] -> ([Renaming], [Renaming])
partitionRenamings = let
    is'op renaming = case renaming of
        OpRenaming1 _ _ -> True
        OpRenaming2 {} -> True
        _ -> False
    in partition is'op

-- ** to apply Renamings to Morphisms

{- | Insert an 'Operator' 'Renaming' into a 'Morphism'.
Iff apply is True, apply the Renaming to the Morphism's target Signature. -}
insertOpRenaming :: Bool -> Renaming -> Morphism -> Morphism
insertOpRenaming apply rename = let
    syms = renamingSymbols rename
    add'op = mapOpMap $ uncurry Map.insert syms
    use'op attrs = if apply
        then mapTarget $ uncurry Sign.renameOp syms attrs
        else id
    in case rename of
        OpRenaming1 _ (To _ attrs) -> use'op attrs . add'op
        OpRenaming2 _ _ _ (To _ attrs) -> use'op attrs . add'op
        _ -> id

{- | Insert a non-Operator 'Renaming' into a 'Morphism'.
iff True, apply the Renaming to the target Sign -}
insertRenaming :: Bool -> Renaming -> Morphism -> Morphism
insertRenaming apply rename = let
    syms = renamingSymbols rename
    add'sort = mapSortMap $ uncurry Map.insert syms
    use'sort = if apply
        then mapTarget $ uncurry Sign.renameSort syms
        else id
    ren'sort = mapOpMap $ uncurry renameSortOpMap syms
    add'labl = mapLabelMap $ uncurry Map.insert syms
    use'labl = if apply
        then mapTarget $ uncurry Sign.renameLabel syms
        else id
    in case rename of
        SortRenaming _ _ -> ren'sort . use'sort . add'sort
        LabelRenaming _ _ -> use'labl . add'labl
        _ -> id

-- | Rename sorts in the profiles of an operator map.
renameSortOpMap :: Symbol -> Symbol -> OpMap -> OpMap
renameSortOpMap from to = Map.map $ mapSorts $ Map.singleton from to

-- | Insert 'Renaming's into a 'Morphism'.
insertRenamings :: Bool -> Morphism -> [Renaming] -> Morphism
insertRenamings apply mor rens = let
    (ops, rest) = partitionRenamings rens
    add'ops = flip (foldr $ insertOpRenaming apply) ops
    add'rest = flip (foldr $ insertRenaming apply) rest
    in add'rest . add'ops $ mor

-- * Construction

-- | Create a 'Morphism' from an initial 'Sign'ature and a list of 'Renaming's.
fromSignRenamings :: Sign -> [Renaming] -> Morphism
fromSignRenamings s rs = kindMorph $ insertRenamings True (identity s) rs

-- | Create a 'Morphism' from a pair of 'Sign'atures and a list of 'Renaming's.
fromSignsRenamings :: Sign -> Sign -> [Renaming] -> Morphism
fromSignsRenamings sign1 sign2 rs =
  kindMorph $ insertRenamings False (inclusion sign1 sign2) rs

-- | the empty 'Morphism'
empty :: Morphism
empty = identity Sign.empty

-- | the identity 'Morphism'
identity :: Sign -> Morphism
identity sign = inclusion sign sign

-- | the inclusion 'Morphism'
inclusion :: Sign -> Sign -> Morphism
inclusion src tgt = Morphism {
        source = src,
        target = tgt,
        sortMap = Map.empty,
        kindMap = Map.empty,
        opMap = Map.empty,
        labelMap = Map.empty
    }

-- * Combination

-- | the inverse 'Morphism'
inverse :: Morphism -> Result Morphism
inverse mor = let
    invertMap = Map.foldWithKey (flip Map.insert) Map.empty
    in return $ kindMorph Morphism {
        source = target mor,
        target = source mor,
        sortMap = invertMap $ sortMap mor,
        kindMap = invertMap $ kindMap mor,
        opMap = invertMap $ opMap mor,
        labelMap = invertMap $ labelMap mor
    }

-- | the union of two 'Morphism's
union :: Morphism -> Morphism -> Morphism
union mor1 mor2 = let
    apply func items = func (items mor1) (items mor2)
    in kindMorph Morphism {
        source = apply Sign.union source,
        target = apply Sign.union target,
        sortMap = apply Map.union sortMap,
        kindMap = apply Map.union kindMap,
        opMap = apply Map.union opMap,
        labelMap = apply Map.union labelMap
    }

-- Just a shorthand for types inside compose.
type Extraction = Morphism -> SymbolMap

-- | the composition of two 'Morphism's
compose :: Morphism -> Morphism -> Result Morphism
compose f g
    | target f /= source g = fail
        "target of the first and source of the second morphism are different"
    | otherwise = let
        {- Take SymbolMap |mp| of each Morphism.
        Convert each SymbolMap to a function.
        Compose those functions. -}
        map'map :: Extraction -> Symbol -> Symbol
        map'map mp = mapAsFunction (mp g) . mapAsFunction (mp f)
        {- Map |x| via the composed SymbolMaps |mp| of both Morphisms.
        Insert the renaming mapping into a SymbolMap. -}
        insert :: Extraction -> Symbol -> SymbolMap -> SymbolMap
        insert mp x = let y = map'map mp x
            in if x == y then id else Map.insert x y
        -- Map each symbol in |items| via the combined SymbolMaps |mp|.
        compose'map :: Extraction -> (Sign -> SymbolSet) -> SymbolMap
        compose'map mp items = if Map.null (mp g)
            -- if the SymbolMap of |g| is empty, we use the one from |f|
            then mp f
            {- otherwise we start with the SymbolSet from |source f|
            and construct a combined SymbolMap by applying both
            SymbolMaps (from |f| and |g|) to each item in |insert| -}
            else Set.fold (insert mp) Map.empty $ items (source f)
        -- We want a morphism from |source f| to |target g|.
        mor = inclusion (source f) (target g)
        in return $ kindMorph mor {
            sortMap = compose'map sortMap getSorts,
            opMap = compose'map opMap getOps,
            labelMap = compose'map labelMap getLabels
        }

-- * Testing

-- | True iff the 'Morphism' is an inclusion
isInclusion :: Morphism -> Bool
isInclusion mor = let
    null'sortMap = Map.null (sortMap mor)
    null'opMap = Map.null (opMap mor)
    null'labelMap = Map.null (labelMap mor)
    in null'sortMap && null'opMap && null'labelMap

-- | True iff the 'Morphism' is legal
isLegal :: Morphism -> Result ()
isLegal mor = let
    src = source mor
    tgt = target mor
    smap = sortMap mor
    omap = opMap mor
    lmap = labelMap mor
    subset mp items = let mapped = Set.map $ mapAsFunction mp
        in Set.isSubsetOf (mapped $ items src) $ items tgt
    lg'source = Sign.isLegal src
    lg'sortMap = subset smap getSorts
    lg'opMap = subset omap getOps
    lg'labelMap = subset lmap getLabels
    lg'target = Sign.isLegal tgt
    in unless (and [lg'source, lg'sortMap, lg'opMap, lg'labelMap, lg'target]) $
       fail "illegal Maude morphism"

-- * Conversion

-- | extract the complete 'SymbolMap' of a 'Morphism'
symbolMap :: Morphism -> SymbolMap
symbolMap mor = Map.unions [sortMap mor, opMap mor, labelMap mor]

-- * Modification

-- | set a new target for a 'Morphism'
setTarget :: Sign -> Morphism -> Morphism
setTarget sg m = kindMorph $ mapTarget (const sg) m

-- | qualify a list of 'Symbol's inside a 'Morphism'
qualifySorts :: Morphism -> Qid -> Symbols -> Morphism
qualifySorts mor qid syms = let
    insert symb = Map.insert symb $ qualify qid symb
    smap = foldr insert Map.empty syms
    q'tgt = mapTarget $ mapSorts smap
    q'smap = mapSortMap $ mapSorts smap
    x'smap = mapSortMap $ Map.union smap
    in kindMorph $ q'tgt . x'smap . q'smap $ mor

-- | apply a list of 'Renaming's to a 'Morphism'
applyRenamings :: Morphism -> [Renaming] -> Morphism
applyRenamings m rs = kindMorph $ insertRenamings True m rs

-- | apply a 'Sort' 'Renaming' to a 'Morphism'
extendWithSortRenaming :: Symbol -> Symbol -> Morphism -> Morphism
extendWithSortRenaming src tgt m = let
    add'sort = mapSortMap $ Map.insert src tgt
    use'sort = mapTarget $ Sign.renameSort src tgt
    ren'sort = mapOpMap $ renameSortOpMap src tgt
    in kindMorph $ ren'sort . use'sort $ add'sort m

-- * Application

-- | translate a 'Sentence' along a 'Morphism'
translateSentence :: Morphism -> Sentence -> Result Sentence
translateSentence mor = let
    smap = mapSorts (sortMap mor)
    omap = mapOps (opMap mor)
    lmap = mapLabels (labelMap mor)
    in return . lmap . smap . omap

-- | translate 'Sort's along a 'Morphism'
translateSorts :: (HasSorts a) => Morphism -> a -> a
translateSorts = mapSorts . sortMap

-- * Auxiliary functions
kindMorph :: Morphism -> Morphism
kindMorph morph = morph { kindMap = kindMorphAux kr1 sm kr2}
     where kr1 = kindRel $ source morph
           kr2 = kindRel $ target morph
           sm = Map.toList $ sortMap morph

kindMorphAux :: KindRel -> [(Symbol, Symbol)] -> KindRel -> KindMap
kindMorphAux _ [] _ = Map.empty
kindMorphAux kr1 ((s1, s2) : ls) kr2 = Map.union m m'
     where m = kindMorphAux kr1 ls kr2
           (k1, k2) = case (Map.lookup s1 kr1, Map.lookup s2 kr2) of
              (Just r1, Just r2) -> (r1, r2)
              _ -> (s1, s1)
           m' = if k1 == k2
                then Map.empty
                else Map.singleton k1 k2
