{- |

Module : $Header$

Description : Signatures for Maude

Copyright : (c) Martin Kuehl, Uni Bremen 2008

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

Maintainer : mkhl@informatik.uni-bremen.de

Stability : experimental

Portability : portable

Definition of signatures for Maude.

-}

{-

Ref.

...

-}

module Maude.Sign (

Sign(..),

fromMod,

symbols,

empty,

insertSort,

insertSubsort,

insertOpName,

insertOp,

isLegal,

includesSentence,

simplifySentence,

) where

import Maude.Meta

import Maude.Symbol

import Maude.Sentence

import Data.Map (Map)

import Data.Typeable (Typeable)

import qualified Data.Set as Set

import qualified Data.Map as Map

import qualified Data.Foldable as Fold

import Common.Lib.Rel (Rel)

import qualified Common.Lib.Rel as Rel

-- for ShATermConvertible

import Common.ATerm.Conversion (ShATermConvertible(..))

-- for Pretty

import Common.DocUtils (Pretty(..))

import qualified Common.Doc as Doc

type SubsortRel = Rel Sort

type OpMap = Map Symbol OpDeclSet

data Sign = Sign {

sorts :: SortSet,

subsorts :: SubsortRel,

ops :: OpMap

} deriving (Show, Eq, Ord, Typeable)

-- TODO: Add real pretty-printing for Maude Signatures.

instance Pretty Sign where

pretty _ = Doc.empty

-- TODO: Replace dummy implementation for ShATermConvertible Sign.

instance ShATermConvertible Sign where

toShATermAux table _ = return (table, 0)

fromShATermAux _ table = (table, empty)

instance HasSorts Sign where

getSorts = sorts

mapSorts mp sign = sign {

sorts = mapSorts mp (sorts sign),

subsorts = mapSorts mp (subsorts sign)

}

instance HasOps Sign where

getOps = Map.keysSet . ops

mapOps mp sign = sign {

ops = Map.foldWithKey (map'op mp) Map.empty (ops sign)

}

instance HasLabels Sign where

getLabels = getLabels . Map.elems . ops

mapLabels mp sign = sign {

ops = Map.map (mapLabels mp) (ops sign)

}

-- | extract the Signature of a Module

fromMod :: (Module a) => a -> Sign

fromMod modul = let

mk'subsorts = Rel.transClosure . Set.fold ins'subsort Rel.empty

mk'ops = Set.fold ins'op Map.empty

in Sign {

sorts = modSorts modul,

subsorts = mk'subsorts (modSubsorts modul),

ops = mk'ops (modOps modul)

}

-- | extract the Set of all Symbols from a Signature

symbols :: Sign -> SymbolSet

symbols sign = Set.unions [(getSorts sign), (getOps sign), (getLabels sign)]

-- | the empty Signature

empty :: Sign

empty = Sign { sorts = Set.empty, subsorts = Rel.empty, ops = Map.empty }

-- | insert a Sort into a Signature

insertSort :: Sort -> Sign -> Sign

insertSort sort sign = sign {sorts = ins'sort sort (sorts sign)}

-- | insert a Subsort declaration into a Signature

insertSubsort :: SubsortDecl -> Sign -> Sign

insertSubsort decl sign = sign {subsorts = ins'subsort decl (subsorts sign)}

-- | insert an Operator name into a Signature

insertOpName :: Symbol -> Sign -> Sign

insertOpName name sign = sign {ops = ins'opName name (ops sign)}

-- | insert an Operator declaration into a Signature

insertOp :: OpDecl -> Sign -> Sign

insertOp op sign = sign {ops = ins'op op (ops sign)}

-- | check that a Signature is legal

isLegal :: Sign -> Bool

isLegal sign = let

isLegalType typ = case typ of

Kind kind -> not $ null kind && all isLegalSort kind

-- TODO: Check that all sorts are in the same connected component.

Sort sort -> isLegalSort sort

isLegalSort sort = Set.member sort (sorts sign)

isLegalOp op = isLegalType (op'domain op) && all isLegalType (op'range op)

legal'subsorts = Fold.all isLegalSort $ Rel.nodes (subsorts sign)

legal'ops = Fold.all (Fold.all isLegalOp) (ops sign)

in all id [legal'subsorts, legal'ops]

-- | check that a Signature can include a Sentence

includesSentence :: Sign -> Sentence -> Bool

includesSentence sign sen = let

ops'subset = Set.isSubsetOf (getOps sen) (getOps sign)

sorts'subset = Set.isSubsetOf (getSorts sen) (getSorts sign)

labels'subset = Set.isSubsetOf (getLabels sen) (getLabels sign)

in all id [sorts'subset, ops'subset, labels'subset]

-- | simplification of sentences (leave out qualifications)

-- TODO: Add real implementation of simplification

simplifySentence :: Sign -> Sentence -> Sentence

simplifySentence _ = id

--- Helper functions for inserting Signature members into their respective collections.

-- insert a Sort into a Set of Sorts

ins'sort :: Sort -> SortSet -> SortSet

ins'sort = Set.insert

-- insert a Subsort declaration into a Subsort Relationship

ins'subsort :: SubsortDecl -> SubsortRel -> SubsortRel

ins'subsort sub = Rel.insert (subsort sub) (supersort sub)

-- insert an Operator name into an Operator Map

ins'opName :: Symbol -> OpMap -> OpMap

ins'opName name = Map.insert name Set.empty

-- insert an Operator declaration into an Operator Map

ins'op :: OpDecl -> OpMap -> OpMap

ins'op op opmap = let

name = op'name op

old'ops = Map.findWithDefault Set.empty name opmap

new'ops = Set.insert op old'ops

in Map.insert name new'ops opmap

-- map an OperatorMap key-value pair and insert it into the accumulator

map'op :: SymbolMap -> Symbol -> OpDeclSet -> OpMap -> OpMap

map'op mp op decls acc = let

key = mapToFunction mp op

val = mapOps mp decls

in Map.insert key val acc

mapToFunction :: (Ord a) => Map a a -> (a -> a)

mapToFunction mp name = Map.findWithDefault name name mp