{-# LANGUAGE DeriveDataTypeable #-} {- | Module : ./Temporal/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 Temporal.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 Temporal.Sign as Sign import qualified Temporal.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) instance Pretty Symbol where pretty :: Symbol -> Doc pretty = Symbol -> Doc printSymbol 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 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.Sign -> Set.Set Symbol symOf :: Sign -> Set Symbol symOf x :: Sign x = (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) -> Set Id -> Set Symbol forall a b. (a -> b) -> a -> b $ Sign -> Set Id Sign.items Sign x -- | Determines the symbol map of a morhpism getSymbolMap :: Morphism.Morphism -> Map.Map Symbol Symbol getSymbolMap :: Morphism -> Map Symbol Symbol getSymbolMap f :: Morphism f = (Id -> Id -> Map Symbol Symbol -> Map Symbol Symbol) -> Map Symbol Symbol -> Map Id Id -> Map Symbol Symbol forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b Map.foldrWithKey (\ k :: Id k a :: Id a -> Symbol -> Symbol -> Map Symbol Symbol -> Map Symbol Symbol forall k a. Ord k => k -> a -> Map k a -> Map k a Map.insert Symbol :: Id -> Symbol Symbol {symName :: Id symName = Id k} Symbol :: Id -> Symbol Symbol {symName :: Id symName = Id a}) Map Symbol Symbol forall k a. Map k a Map.empty (Map Id Id -> Map Symbol Symbol) -> Map Id Id -> Map Symbol Symbol forall a b. (a -> b) -> a -> b $ Morphism -> Map Id Id Morphism.propMap 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 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