fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz{- |

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzModule : $Header$

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzDescription : Morphisms for Maude

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzCopyright : (c) Martin Kuehl, Uni Bremen 2008

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzMaintainer : mkhl@informatik.uni-bremen.de

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzStability : experimental

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzPortability : portable

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzDefinition of morphisms for Maude.

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz-}

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz{-

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz Ref.

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz ...

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz-}

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzmodule Maude.Morphism (

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz Morphism(..),

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz fromRenamingSet,

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz symbolMap,

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz identity,

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz compose,

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz isLegal,

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz mapSentence,

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz) where

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Maude.Meta

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Maude.Symbol

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuimport Maude.Sentence

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Maude.Sign hiding (empty, isLegal)

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport qualified Maude.Sign as Sign (empty, isLegal)

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Data.Typeable (Typeable)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuimport qualified Data.Map as Map

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuimport qualified Data.Set as Set

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuimport qualified Common.Result as Result

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- for ShATermConvertible

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuimport Common.ATerm.Conversion

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- for Pretty

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuimport Common.DocUtils (Pretty, pretty)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuimport qualified Common.Doc as Doc

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savutype SortMap = Map.Map Symbol Symbol

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savutype OpMap = Map.Map Symbol Symbol

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savutype LabelMap = Map.Map Symbol Symbol

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savudata Morphism = Morphism {

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu source :: Sign,

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu target :: Sign,

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu sortMap :: SortMap,

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu opMap :: OpMap,

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu labelMap :: LabelMap

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu } deriving (Show, Eq, Typeable)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- TODO: Add real pretty-printing for Maude Morphisms.

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuinstance Pretty Morphism where

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu pretty _ = Doc.empty

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- TODO: Replace dummy implementation for ShATermConvertible Morphism.

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuinstance ShATermConvertible Morphism where

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu toShATermAux table _ = return (table, 0)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu fromShATermAux _ table = (table, empty)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- | extract a Morphism from a RenamingSet

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavufromRenamingSet :: RenamingSet -> Morphism

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavufromRenamingSet = Set.fold insertRenaming empty

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- | extract a Symbol Map from a Morphism

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavusymbolMap :: Morphism -> SymbolMap

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavusymbolMap mor = Map.unions [(sortMap mor), (opMap mor), (labelMap mor)]

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- | insert a Renaming into a Morphism

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuinsertRenaming :: Renaming -> Morphism -> Morphism

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuinsertRenaming rename mor = let

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu src = source mor

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu tgt = target mor

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu smap = sortMap mor

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu omap = opMap mor

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu lmap = labelMap mor

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu op nam as cod dom = Op { op'name = nam, op'range = cod, op'domain = dom, op'attrs = as }

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu in case rename of

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu Sort'To {from = a, to = b} -> mor {

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu source = insertSort a src,

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu target = insertSort b tgt,

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu sortMap = Map.insert a b smap

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu }

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu Op'To {from = a, to = b} -> mor {

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu source = insertOpName a src,

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu target = insertOpName b tgt,

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu opMap = Map.insert a b omap

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu }

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu Op'Type'To {from = a, range = cod, domain = dom, to = b, attrs = as} -> mor {

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu source = insertOp (op a as cod dom) src,

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu target = insertOp (op b as cod dom) tgt,

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu opMap = Map.insert a b omap

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu }

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu Label'To {from = a, to = b} -> mor {

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu labelMap = Map.insert a b lmap

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu }

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- | the empty Morphism

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuempty :: Morphism

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuempty = identity Sign.empty

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- | the identity Morphism

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuidentity :: Sign -> Morphism

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuidentity sign = Morphism {

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu source = sign,

target = sign,

sortMap = Map.empty,

opMap = Map.empty,

labelMap = Map.empty

}

-- | the composition of two Morphisms

compose :: Morphism -> Morphism -> Result.Result Morphism

compose f g

| (target f) /= (source g) = fail "target of the first and source of the second morphism are different"

| otherwise = let

apply mp nam = Map.findWithDefault nam nam mp

map'map mp = apply (mp g) . apply (mp f)

insert mp x = let y = map'map mp x

in if x == y then id else Map.insert x y

compose'map mp items = if Map.null (mp g)

then mp f

else Set.fold (insert mp) Map.empty $ items (source f)

in return Morphism {

source = (source f),

target = (target g),

sortMap = compose'map sortMap getSorts,

opMap = compose'map opMap getOps,

labelMap = compose'map labelMap getLabels

}

-- | check that a Morphism is legal

isLegal :: Morphism -> Bool

isLegal mor = let

src = source mor

tgt = target mor

smap = sortMap mor

omap = opMap mor

lmap = labelMap mor

apply mp nam = Map.findWithDefault nam nam mp

subset mp items = Set.isSubsetOf (Set.map (apply mp) $ items src) (items tgt)

legal'source = Sign.isLegal src

legal'sortMap = subset smap getSorts

legal'opMap = subset omap getOps

legal'labelMap = subset lmap getLabels

legal'target = Sign.isLegal tgt

in all id [legal'source, legal'sortMap, legal'opMap, legal'labelMap, legal'target]

-- | translate a Sentence along a Morphism

mapSentence :: Morphism -> Sentence -> Result.Result Sentence

mapSentence mor = let

smap = mapSorts (sortMap mor)

omap = mapOps (opMap mor)

lmap = mapLabels (labelMap mor)

in return . lmap . omap . smap