{-# LANGUAGE DeriveDataTypeable #-}

{- |

Module : $Header$

Description : Maude Symbols

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 symbols for Maude.

-}

module Maude.Symbol (

{- * Types

The Symbol type -}

Symbol (..),

-- ** Auxiliary types

Symbols,

SymbolSet,

SymbolMap,

SymbolRel,

kindSym2sortSym,

-- * Conversion

toId,

qualify,

asSort,

asKind,

toType,

toOperator,

-- * Construction

mkOpTotal,

mkOpPartial,

-- * Testing

sameKind,

) where

import Maude.AS_Maude

import Maude.Meta.HasName

import Data.Data

import Data.Set (Set)

import Data.Map (Map)

import Common.Lib.Rel (Rel)

import qualified Data.Set as Set

import qualified Common.Lib.Rel as Rel

import Common.Id (Id, mkId, mkSimpleId, GetRange, getRange, nullRange)

import Common.Doc

import Common.DocUtils (Pretty (..))

import Data.Maybe (fromJust)

-- * Types

{- ** The Symbol type

A 'Sort', 'Kind', 'Label', or 'Operator'. -}

data Symbol = Sort Qid -- ^ A 'Sort' Symbol

| Kind Qid -- ^ A 'Kind' Symbol

| Labl Qid -- ^ A 'Label' Symbol

| Operator Qid Symbols Symbol -- ^ A qualified 'Operator' Symbol

| OpWildcard Qid -- ^ A wildcard 'Operator' Symbol

deriving (Show, Read, Ord, Eq, Typeable)

-- ** Auxiliary types

type Symbols = [Symbol]

type SymbolSet = Set Symbol

type SymbolMap = Map Symbol Symbol

type SymbolRel = Rel Symbol

-- ** Symbol instances

instance HasName Symbol where

getName symb = case symb of

Sort qid -> qid

Kind qid -> qid

Labl qid -> qid

OpWildcard qid -> qid

Operator qid _ _ -> qid

mapName mp symb = case symb of

Sort qid -> Sort $ mapName mp qid

Kind qid -> Kind $ mapName mp qid

Labl qid -> Labl $ mapName mp qid

OpWildcard qid -> OpWildcard $ mapName mp qid

Operator qid dom cod -> Operator (mapName mp qid) dom cod

instance Pretty Symbol where

pretty symb = case symb of

Sort qid -> pretty qid

Kind qid -> brackets $ pretty qid

Labl qid -> pretty qid

OpWildcard qid -> pretty qid

Operator qid dom cod -> hsep

[pretty qid, colon, hsep $ map pretty dom, funArrow, pretty cod]

instance GetRange Symbol where

getRange _ = nullRange

-- * Conversion

-- | Convert 'Symbol' to 'Id'.

toId :: Symbol -> Id

toId = mkId . return . getName

-- | Qualify the 'Symbol' name with a 'Qid'.

qualify :: Qid -> Symbol -> Symbol

qualify qid = let prepend sym = mkSimpleId $ concat [show qid, "$", show sym]

in mapName $ prepend . getName

-- | Convert 'Symbol' to 'Symbol', changing 'Kind's to 'Sort's.

asSort :: Symbol -> Symbol

asSort symb = case symb of

Kind qid -> Sort qid

_ -> symb

-- | Convert 'Symbol' to 'Symbol', changing 'Sort's to 'Kind's.

asKind :: Symbol -> Symbol

asKind symb = case symb of

Sort qid -> Kind qid

_ -> symb

-- | True iff the argument is a 'Sort' or 'Kind'.

isType :: Symbol -> Bool

isType symb = case symb of

Sort _ -> True

Kind _ -> True

_ -> False

toTypeMaybe :: Symbol -> Maybe Type

toTypeMaybe symb = case symb of

Sort qid -> Just . TypeSort . SortId $ qid

Kind qid -> Just . TypeKind . KindId $ qid

_ -> Nothing

-- | Convert 'Symbol' to 'Type', if possible.

toType :: Symbol -> Type

toType = fromJust . toTypeMaybe

-- | True iff the argument is a wildcard 'Operator'.

isOpWildcard :: Symbol -> Bool

isOpWildcard symb = case symb of

OpWildcard _ -> True

_ -> False

-- | True iff the argument is a qualified 'Operator'.

isOperator :: Symbol -> Bool

isOperator symb = case symb of

Operator {} -> True

_ -> False

toOperatorMaybe :: Symbol -> Maybe Operator

toOperatorMaybe symb = case symb of

Operator qid dom cod -> Just $

Op (OpId qid) (map toType dom) (toType cod) []

_ -> Nothing

-- | Convert 'Symbol' to 'Operator', if possible.

toOperator :: Symbol -> Operator

toOperator = fromJust . toOperatorMaybe

-- * Construction

-- | Create a total 'Operator' 'Symbol' with the given profile.

mkOpTotal :: Qid -> [Qid] -> Qid -> Symbol

mkOpTotal qid dom cod = Operator qid (map Sort dom) (Sort cod)

-- | Create a partial 'Operator' 'Symbol' with the given profile.

mkOpPartial :: Qid -> [Qid] -> Qid -> Symbol

mkOpPartial qid dom cod = Operator qid (map Sort dom) (Kind cod)

-- * Testing

{- | True iff both 'Symbol's are of the same 'Kind' in the given

'SymbolRel'. The 'isType' predicate is assumed to hold for both

'Symbol's; this precondition is /not/ checked. -}

typeSameKind :: SymbolRel -> Symbol -> Symbol -> Bool

typeSameKind rel s1 s2 = let

preds1 = Rel.predecessors rel s1

preds2 = Rel.predecessors rel s2

succs1 = Rel.succs rel s1

succs2 = Rel.succs rel s2

psect = Set.intersection preds1 preds2

ssect = Set.intersection succs1 succs2

in or [ s1 == s2

, Set.member s2 preds1

, Set.member s1 preds2

, Set.member s2 succs1

, Set.member s1 succs2

, not $ Set.null psect

, not $ Set.null ssect ]

{- | True iff the 'Symbol's of both lists are pairwise of the same

'Kind' in the given 'SymbolRel'. -}

zipSameKind :: SymbolRel -> Symbols -> Symbols -> Bool

zipSameKind rel s1 s2 = and $ zipWith (sameKind rel) s1 s2

-- | True iff both 'Symbol's are of the same 'Kind' in the given 'SymbolRel'.

sameKind :: SymbolRel -> Symbol -> Symbol -> Bool

sameKind rel s1 s2

| isOpWildcard s1 && isOperator s2 = True

| isOperator s1 && isOpWildcard s2 = True

| all isType [s1, s2] = typeSameKind rel (kindSym2sortSym s1) (kindSym2sortSym s2)

| all isOperator [s1, s2] = let

Operator _ dom1 _ = s1

Operator _ dom2 _ = s2

in zipSameKind rel dom1 dom2

| otherwise = False

kindSym2sortSym :: Symbol -> Symbol

kindSym2sortSym (Kind q) = Sort q

kindSym2sortSym s = s