{-# LANGUAGE DeriveDataTypeable #-} {- | Module : ./QBF/Symbol.hs Description : Symbols of propositional logic Copyright : (c) Jonathan von Schroeder, DFKI GmbH 2010 License : GPLv2 or higher, see LICENSE.txt Maintainer : <jonathan.von_schroeder@dfki.de> Stability : experimental Portability : portable Definition of symbols for propositional logic -} module QBF.Symbol ( Symbol (..) -- Symbol type , pretty -- pretty printing for Symbols , symOf -- Extracts the symbols out of a signature , getSymbolMap -- Determines the symbol map , getSymbolName -- Determines the name of a symbol , idToRaw -- Creates a raw symbol , symbolToRaw -- Convert symbol to raw symbol , matches -- does a symbol match a raw symbol? , applySymMap -- application function for symbol maps ) where import qualified Common.Id as Id import Common.Doc import Common.DocUtils import Data.Data import qualified Data.Set as Set import qualified Data.Map as Map import qualified Propositional.Sign as Sign import QBF.Morphism as Morphism -- | Datatype for symbols newtype Symbol = Symbol {Symbol -> Id symName :: Id.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 Id.GetRange Symbol where getRange :: Symbol -> Range getRange = Id -> Range forall a. GetRange a => a -> Range Id.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 = Id -> Doc forall a. Pretty a => a -> Doc pretty (Id -> Doc) -> (Symbol -> Id) -> Symbol -> Doc forall b c a. (b -> c) -> (a -> b) -> a -> c . Symbol -> Id symName -- | Extraction of symbols from a signature symOf :: Sign.Sign -> Set.Set Symbol symOf :: Sign -> Set Symbol symOf = (Id -> Set Symbol -> Set Symbol) -> Set Symbol -> Set Id -> Set Symbol forall a b. (a -> b -> b) -> b -> Set a -> b Set.fold (\ y :: Id y -> Symbol -> Set Symbol -> Set Symbol forall a. Ord a => a -> Set a -> Set a Set.insert Symbol :: Id -> Symbol Symbol {symName :: Id symName = Id y}) Set Symbol forall a. Set a Set.empty (Set Id -> Set Symbol) -> (Sign -> Set Id) -> Sign -> Set Symbol forall b c a. (b -> c) -> (a -> b) -> a -> c . Sign -> Set Id Sign.items -- | Determines the symbol map of a morhpism getSymbolMap :: Morphism.Morphism -> Map.Map Symbol Symbol getSymbolMap :: Morphism -> Map Symbol Symbol getSymbolMap f :: Morphism f = (Id -> Map Symbol Symbol -> Map Symbol Symbol) -> Map Symbol Symbol -> [Id] -> Map Symbol Symbol forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr (\ 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 propMap Morphism f) Id x)) Map Symbol Symbol forall k a. Map k a Map.empty ([Id] -> Map Symbol Symbol) -> [Id] -> Map Symbol Symbol forall a b. (a -> b) -> a -> b $ Set Id -> [Id] forall a. Set a -> [a] Set.toList (Set Id -> [Id]) -> Set Id -> [Id] forall a b. (a -> b) -> a -> b $ Sign -> Set Id Sign.items (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.Id getSymbolName :: Symbol -> Id getSymbolName = Symbol -> Id symName -- | make a raw_symbol idToRaw :: Id.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 = Symbol -> Symbol -> Bool forall a. Eq a => a -> a -> Bool (==) -- | 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