{-# LANGUAGE DeriveDataTypeable #-} {- | Module : ./DFOL/Symbol.hs Description : Symbol definition for first-order logic with dependent types Copyright : (c) Kristina Sojakova, DFKI Bremen 2010 License : GPLv2 or higher, see LICENSE.txt Maintainer : k.sojakova@jacobs-university.de Stability : experimental Portability : portable -} module DFOL.Symbol where import DFOL.AS_DFOL import Common.Id import Common.Doc import Common.DocUtils import Data.Data import qualified Data.Map as Map -- a symbol is just a name data Symbol = Symbol {Symbol -> NAME name :: NAME} 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) -- pretty printing instance Pretty Symbol where pretty :: Symbol -> Doc pretty = Symbol -> Doc printSymbol instance GetRange Symbol where getRange :: Symbol -> Range getRange = NAME -> Range forall a. GetRange a => a -> Range getRange (NAME -> Range) -> (Symbol -> NAME) -> Symbol -> Range forall b c a. (b -> c) -> (a -> b) -> a -> c . Symbol -> NAME name printSymbol :: Symbol -> Doc printSymbol :: Symbol -> Doc printSymbol (Symbol s :: NAME s) = NAME -> Doc forall a. Pretty a => a -> Doc pretty NAME s -- interface to name maps toSymMap :: Map.Map NAME NAME -> Map.Map Symbol Symbol toSymMap :: Map NAME NAME -> Map Symbol Symbol toSymMap map1 :: Map NAME NAME map1 = [(Symbol, Symbol)] -> Map Symbol Symbol forall k a. Ord k => [(k, a)] -> Map k a Map.fromList ([(Symbol, Symbol)] -> Map Symbol Symbol) -> [(Symbol, Symbol)] -> Map Symbol Symbol forall a b. (a -> b) -> a -> b $ ((NAME, NAME) -> (Symbol, Symbol)) -> [(NAME, NAME)] -> [(Symbol, Symbol)] forall a b. (a -> b) -> [a] -> [b] map (\ (k :: NAME k, a :: NAME a) -> (NAME -> Symbol Symbol NAME k, NAME -> Symbol Symbol NAME a)) ([(NAME, NAME)] -> [(Symbol, Symbol)]) -> [(NAME, NAME)] -> [(Symbol, Symbol)] forall a b. (a -> b) -> a -> b $ Map NAME NAME -> [(NAME, NAME)] forall k a. Map k a -> [(k, a)] Map.toList Map NAME NAME map1 toNameMap :: Map.Map Symbol Symbol -> Map.Map NAME NAME toNameMap :: Map Symbol Symbol -> Map NAME NAME toNameMap map1 :: Map Symbol Symbol map1 = [(NAME, NAME)] -> Map NAME NAME forall k a. Ord k => [(k, a)] -> Map k a Map.fromList ([(NAME, NAME)] -> Map NAME NAME) -> [(NAME, NAME)] -> Map NAME NAME forall a b. (a -> b) -> a -> b $ ((Symbol, Symbol) -> (NAME, NAME)) -> [(Symbol, Symbol)] -> [(NAME, NAME)] forall a b. (a -> b) -> [a] -> [b] map (\ (Symbol k :: NAME k, Symbol a :: NAME a) -> (NAME k, NAME a)) ([(Symbol, Symbol)] -> [(NAME, NAME)]) -> [(Symbol, Symbol)] -> [(NAME, NAME)] forall a b. (a -> b) -> a -> b $ Map Symbol Symbol -> [(Symbol, Symbol)] forall k a. Map k a -> [(k, a)] Map.toList Map Symbol Symbol map1 -- interface to Id toId :: Symbol -> Id toId :: Symbol -> Id toId sym :: Symbol sym = [NAME] -> Id mkId [Symbol -> NAME name Symbol sym] fromId :: Id -> Symbol fromId :: Id -> Symbol fromId (Id toks :: [NAME] toks _ _) = NAME -> Symbol Symbol (NAME -> Symbol) -> NAME -> Symbol forall a b. (a -> b) -> a -> b $ String -> Range -> NAME Token ((NAME -> String) -> [NAME] -> String forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap NAME -> String tokStr [NAME] toks) Range nullRange