{-# LANGUAGE DeriveDataTypeable #-} {- | Module : ./CSL/Symbol.hs Description : symbols for CSL Copyright : (c) Dominik Dietrich, DFKI Bremen 2010 License : GPLv2 or higher, see LICENSE.txt Maintainer : dominik.dietrich@dfki.de Stability : experimental Portability : portable -} module CSL.Symbol where import Common.Id import Common.Doc import Common.DocUtils import Data.Data import qualified Data.Set as Set import qualified Data.Map as Map import CSL.Sign import CSL.Morphism -- | Datatype for symbols newtype Symbol = Symbol {Symbol -> Id symName :: Id} deriving (Int -> Symbol -> ShowS [Symbol] -> ShowS Symbol -> String (Int -> Symbol -> ShowS) -> (Symbol -> String) -> ([Symbol] -> ShowS) -> Show Symbol forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Symbol] -> ShowS $cshowList :: [Symbol] -> ShowS show :: Symbol -> String $cshow :: Symbol -> String showsPrec :: Int -> Symbol -> ShowS $cshowsPrec :: Int -> Symbol -> ShowS Show, Symbol -> Symbol -> Bool (Symbol -> Symbol -> Bool) -> (Symbol -> Symbol -> Bool) -> Eq Symbol forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Symbol -> Symbol -> Bool $c/= :: Symbol -> Symbol -> Bool == :: Symbol -> Symbol -> Bool $c== :: Symbol -> Symbol -> Bool Eq, Eq Symbol Eq Symbol => (Symbol -> Symbol -> Ordering) -> (Symbol -> Symbol -> Bool) -> (Symbol -> Symbol -> Bool) -> (Symbol -> Symbol -> Bool) -> (Symbol -> Symbol -> Bool) -> (Symbol -> Symbol -> Symbol) -> (Symbol -> Symbol -> Symbol) -> Ord Symbol Symbol -> Symbol -> Bool Symbol -> Symbol -> Ordering Symbol -> Symbol -> Symbol forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: Symbol -> Symbol -> Symbol $cmin :: Symbol -> Symbol -> Symbol max :: Symbol -> Symbol -> Symbol $cmax :: Symbol -> Symbol -> Symbol >= :: Symbol -> Symbol -> Bool $c>= :: Symbol -> Symbol -> Bool > :: Symbol -> Symbol -> Bool $c> :: Symbol -> Symbol -> Bool <= :: Symbol -> Symbol -> Bool $c<= :: Symbol -> Symbol -> Bool < :: Symbol -> Symbol -> Bool $c< :: Symbol -> Symbol -> Bool compare :: Symbol -> Symbol -> Ordering $ccompare :: Symbol -> Symbol -> Ordering $cp1Ord :: Eq Symbol Ord, Typeable, Typeable Symbol Constr DataType Typeable Symbol => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Symbol -> c Symbol) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Symbol) -> (Symbol -> Constr) -> (Symbol -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Symbol)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol)) -> ((forall b. Data b => b -> b) -> Symbol -> Symbol) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r) -> (forall u. (forall d. Data d => d -> u) -> Symbol -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol) -> Data Symbol Symbol -> Constr Symbol -> DataType (forall b. Data b => b -> b) -> Symbol -> Symbol (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Symbol -> c Symbol (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Symbol forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u forall u. (forall d. Data d => d -> u) -> Symbol -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Symbol forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Symbol -> c Symbol forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Symbol) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol) $cSymbol :: Constr $tSymbol :: DataType gmapMo :: (forall d. Data d => d -> m d) -> Symbol -> m Symbol $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol gmapMp :: (forall d. Data d => d -> m d) -> Symbol -> m Symbol $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol gmapM :: (forall d. Data d => d -> m d) -> Symbol -> m Symbol $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol gmapQi :: Int -> (forall d. Data d => d -> u) -> Symbol -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u gmapQ :: (forall d. Data d => d -> u) -> Symbol -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Symbol -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r gmapT :: (forall b. Data b => b -> b) -> Symbol -> Symbol $cgmapT :: (forall b. Data b => b -> b) -> Symbol -> Symbol dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Symbol) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Symbol) dataTypeOf :: Symbol -> DataType $cdataTypeOf :: Symbol -> DataType toConstr :: Symbol -> Constr $ctoConstr :: Symbol -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Symbol $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Symbol gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Symbol -> c Symbol $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Symbol -> c Symbol $cp1Data :: Typeable Symbol Data) instance GetRange Symbol where getRange :: Symbol -> Range getRange = Id -> Range forall a. GetRange a => a -> Range getRange (Id -> Range) -> (Symbol -> Id) -> Symbol -> Range forall b c a. (b -> c) -> (a -> b) -> a -> c . Symbol -> Id symName instance Pretty Symbol where pretty :: Symbol -> Doc pretty = Symbol -> Doc printSymbol printSymbol :: Symbol -> Doc printSymbol :: Symbol -> Doc printSymbol x :: Symbol x = Id -> Doc forall a. Pretty a => a -> Doc pretty (Id -> Doc) -> Id -> Doc forall a b. (a -> b) -> a -> b $ Symbol -> Id symName Symbol x -- | Extraction of symbols from a signature symOf :: Sign -> Set.Set Symbol symOf :: Sign -> Set Symbol symOf = (Id -> Symbol) -> Set Id -> Set Symbol forall b a. Ord b => (a -> b) -> Set a -> Set b Set.map Id -> Symbol Symbol (Set Id -> Set Symbol) -> (Sign -> Set Id) -> Sign -> Set Symbol forall b c a. (b -> c) -> (a -> b) -> a -> c . Sign -> Set Id opIds -- | Determines the symbol map of a morhpism getSymbolMap :: Morphism -> Map.Map Symbol Symbol getSymbolMap :: Morphism -> Map Symbol Symbol getSymbolMap f :: Morphism f = (Id -> Map Symbol Symbol -> Map Symbol Symbol) -> Map Symbol Symbol -> Set Id -> Map Symbol Symbol forall a b. (a -> b -> b) -> b -> Set a -> b Set.fold (\ x :: Id x -> Symbol -> Symbol -> Map Symbol Symbol -> Map Symbol Symbol forall k a. Ord k => k -> a -> Map k a -> Map k a Map.insert (Id -> Symbol Symbol Id x) (Id -> Symbol Symbol (Id -> Symbol) -> Id -> Symbol forall a b. (a -> b) -> a -> b $ Map Id Id -> Id -> Id applyMap (Morphism -> Map Id Id operatorMap Morphism f) Id x)) Map Symbol Symbol forall k a. Map k a Map.empty (Set Id -> Map Symbol Symbol) -> Set Id -> Map Symbol Symbol forall a b. (a -> b) -> a -> b $ Sign -> Set Id opIds (Sign -> Set Id) -> Sign -> Set Id forall a b. (a -> b) -> a -> b $ Morphism -> Sign source Morphism f -- | Determines the name of a symbol getSymbolName :: Symbol -> Id getSymbolName :: Symbol -> Id getSymbolName = Symbol -> Id symName -- | make a raw_symbol idToRaw :: Id -> Symbol idToRaw :: Id -> Symbol idToRaw mid :: Id mid = Symbol :: Id -> Symbol Symbol {symName :: Id symName = Id mid} -- | convert to raw symbol symbolToRaw :: Symbol -> Symbol symbolToRaw :: Symbol -> Symbol symbolToRaw = Symbol -> Symbol forall a. a -> a id -- | does a smybol match a raw symbol? matches :: Symbol -> Symbol -> Bool matches :: Symbol -> Symbol -> Bool matches s1 :: Symbol s1 s2 :: Symbol s2 = Symbol s1 Symbol -> Symbol -> Bool forall a. Eq a => a -> a -> Bool == Symbol s2 -- | application function for Symbol Maps applySymMap :: Map.Map Symbol Symbol -> Symbol -> Symbol applySymMap :: Map Symbol Symbol -> Symbol -> Symbol applySymMap smap :: Map Symbol Symbol smap idt :: Symbol idt = Symbol -> Symbol -> Map Symbol Symbol -> Symbol forall k a. Ord k => a -> k -> Map k a -> a Map.findWithDefault Symbol idt Symbol idt Map Symbol Symbol smap