{-# LANGUAGE DeriveDataTypeable #-} {- | Module : ./Propositional/Symbol.hs Description : Symbols of propositional logic Copyright : (c) Dominik Luecke, Uni Bremen 2007 License : GPLv2 or higher, see LICENSE.txt Maintainer : luecke@informatik.uni-bremen.de Stability : experimental Portability : portable Definition of symbols for propositional logic -} module NeSyPatterns.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 Common.IRI 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 NeSyPatterns.Sign as Sign import NeSyPatterns.Morphism as Morphism import NeSyPatterns.Sign (ResolvedNode) -- | Datatype for symbols newtype Symbol = Symbol { Symbol -> ResolvedNode node :: ResolvedNode } 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 = ResolvedNode -> Range forall a. GetRange a => a -> Range Id.getRange (ResolvedNode -> Range) -> (Symbol -> ResolvedNode) -> Symbol -> Range forall b c a. (b -> c) -> (a -> b) -> a -> c . Symbol -> ResolvedNode node instance Pretty Symbol where pretty :: Symbol -> Doc pretty = Symbol -> Doc printSymbol printSymbol :: Symbol -> Doc printSymbol :: Symbol -> Doc printSymbol = ResolvedNode -> Doc forall a. Pretty a => a -> Doc pretty (ResolvedNode -> Doc) -> (Symbol -> ResolvedNode) -> Symbol -> Doc forall b c a. (b -> c) -> (a -> b) -> a -> c . Symbol -> ResolvedNode node -- | Extraction of symbols from a signature symOf :: Sign.Sign -> Set.Set Symbol symOf :: Sign -> Set Symbol symOf = (ResolvedNode -> Symbol) -> Set ResolvedNode -> Set Symbol forall b a. Ord b => (a -> b) -> Set a -> Set b Set.map ResolvedNode -> Symbol Symbol (Set ResolvedNode -> Set Symbol) -> (Sign -> Set ResolvedNode) -> Sign -> Set Symbol forall b c a. (b -> c) -> (a -> b) -> a -> c . Sign -> Set ResolvedNode Sign.nodes -- | Determines the symbol map of a morhpism getSymbolMap :: Morphism.Morphism -> Map.Map Symbol Symbol getSymbolMap :: Morphism -> Map Symbol Symbol getSymbolMap f :: Morphism f = (ResolvedNode -> Map Symbol Symbol -> Map Symbol Symbol) -> Map Symbol Symbol -> Set ResolvedNode -> Map Symbol Symbol forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr (\n :: ResolvedNode n -> Symbol -> Symbol -> Map Symbol Symbol -> Map Symbol Symbol forall k a. Ord k => k -> a -> Map k a -> Map k a Map.insert (ResolvedNode -> Symbol Symbol ResolvedNode n) (ResolvedNode -> Symbol Symbol (ResolvedNode -> Symbol) -> ResolvedNode -> Symbol forall a b. (a -> b) -> a -> b $ Map ResolvedNode ResolvedNode -> ResolvedNode -> ResolvedNode Morphism.applyMap (Morphism -> Map ResolvedNode ResolvedNode Morphism.nodeMap Morphism f) ResolvedNode n)) (Map Symbol Symbol forall k a. Map k a Map.empty :: Map.Map Symbol Symbol) (Sign -> Set ResolvedNode Sign.nodes (Morphism -> Sign source Morphism f)) -- | Determines the name of a symbol getSymbolName :: Symbol -> Id.Id getSymbolName :: Symbol -> Id getSymbolName (Symbol ( Sign.ResolvedNode o :: IRI o i :: IRI i _)) = Id -> Id -> Id Id.appendId (IRI -> Id uriToCaslId IRI o) (IRI -> Id uriToCaslId IRI i) -- | make a raw_symbol idToRaw :: Id.Id -> Symbol idToRaw :: Id -> Symbol idToRaw mid :: Id mid = case Id -> [Token] Id.getPlainTokenList Id mid of [o :: Token o, i :: Token i] -> case (String -> Maybe IRI parseIRI (String -> Maybe IRI) -> String -> Maybe IRI forall a b. (a -> b) -> a -> b $ Token -> String forall a. Show a => a -> String show Token o, String -> Maybe IRI parseIRI (String -> Maybe IRI) -> String -> Maybe IRI forall a b. (a -> b) -> a -> b $ Token -> String forall a. Show a => a -> String show Token i) of (Just o' :: IRI o', Just i' :: IRI i') -> ResolvedNode -> Symbol Symbol (ResolvedNode -> Symbol) -> ResolvedNode -> Symbol forall a b. (a -> b) -> a -> b $ IRI -> IRI -> Range -> ResolvedNode Sign.ResolvedNode IRI o' IRI i' (Id -> Range Id.posOfId Id mid) _ -> String -> Symbol forall a. HasCallStack => String -> a error "NeSyPatterns.Symbol.idToRaw: Invalid iri" _ -> String -> Symbol forall a. HasCallStack => String -> a error "NeSyPatterns.Symbol.idToRaw: Invalid number of tokens" -- | 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 n1 :: Symbol n1 n2 :: Symbol n2 = let a :: ResolvedNode a = Symbol -> ResolvedNode node Symbol n1 b :: ResolvedNode b = Symbol -> ResolvedNode node Symbol n2 o :: ResolvedNode -> IRI o = ResolvedNode -> IRI Sign.resolvedOTerm i :: ResolvedNode -> IRI i = ResolvedNode -> IRI Sign.resolvedNeSyId in ResolvedNode -> IRI o ResolvedNode a IRI -> IRI -> Bool forall a. Eq a => a -> a -> Bool == ResolvedNode -> IRI o ResolvedNode b Bool -> Bool -> Bool && ResolvedNode -> IRI i ResolvedNode a IRI -> IRI -> Bool forall a. Eq a => a -> a -> Bool == ResolvedNode -> IRI i ResolvedNode b -- | 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