4169N/A{- |

1178N/AModule : $Header$

1178N/ADescription : Symbols of propositional logic

1178N/ACopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010

1178N/ALicense : GPLv2 or higher

1178N/A

1178N/AMaintainer : <jonathan.von_schroeder@dfki.de>

1178N/AStability : experimental

1178N/APortability : portable

1178N/A

1178N/ADefinition of symbols for propositional logic

1178N/A-}

1178N/A

1178N/A

1178N/Amodule QBF.Symbol

1178N/A (

1178N/A Symbol (..) -- Symbol type

2362N/A , pretty -- pretty printing for Symbols

2362N/A , symOf -- Extracts the symbols out of a signature

2362N/A , getSymbolMap -- Determines the symbol map

1178N/A , getSymbolName -- Determines the name of a symbol

4169N/A , idToRaw -- Creates a raw symbol

1178N/A , symbolToRaw -- Convert symbol to raw symbol

0N/A , matches -- does a symbol match a raw symbol?

4033N/A , applySymMap -- application function for symbol maps

4033N/A ) where

0N/A

4033N/Aimport qualified Common.Id as Id

4033N/Aimport Common.Doc

0N/Aimport Common.DocUtils

1178N/Aimport qualified Data.Set as Set

1178N/Aimport qualified Data.Map as Map

1178N/Aimport qualified Propositional.Sign as Sign

1178N/Aimport QBF.Morphism as Morphism

1178N/A

1178N/A-- | Datatype for symbols

1178N/Anewtype Symbol = Symbol {symName :: Id.Id}

1178N/A deriving (Show, Eq, Ord)

1178N/A

0N/Ainstance Id.GetRange Symbol where

4033N/A getRange = Id.getRange . symName

1178N/A

1178N/Ainstance Pretty Symbol where

4033N/A pretty = printSymbol

1178N/A

1178N/AprintSymbol :: Symbol -> Doc

4033N/AprintSymbol = pretty . symName

1178N/A

4033N/A-- | Extraction of symbols from a signature

0N/AsymOf :: Sign.Sign -> Set.Set Symbol

1178N/AsymOf = Set.fold (\ y -> Set.insert Symbol {symName = y}) Set.empty .

4033N/A Sign.items

1178N/A

4033N/A-- | Determines the symbol map of a morhpism

1178N/AgetSymbolMap :: Morphism.Morphism -> Map.Map Symbol Symbol

1178N/AgetSymbolMap f =

1178N/A foldr (\ x -> Map.insert (Symbol x) (Symbol $ applyMap (propMap f) x))

1178N/A Map.empty $ Set.toList $ Sign.items $ source f

4033N/A

1178N/A-- | Determines the name of a symbol

1178N/AgetSymbolName :: Symbol -> Id.Id

4033N/AgetSymbolName = symName

1178N/A

1178N/A-- | make a raw_symbol

1178N/AidToRaw :: Id.Id -> Symbol

4033N/AidToRaw mid = Symbol {symName = mid}

1178N/A

1178N/A-- | convert to raw symbol

1178N/AsymbolToRaw :: Symbol -> Symbol

1178N/AsymbolToRaw = id

4033N/A

1178N/A-- | does a smybol match a raw symbol?

1178N/Amatches :: Symbol -> Symbol -> Bool

4033N/Amatches = (==)

1178N/A

1178N/A-- | application function for Symbol Maps

4033N/AapplySymMap :: Map.Map Symbol Symbol -> Symbol -> Symbol

1178N/AapplySymMap smap idt = Map.findWithDefault idt idt smap

1178N/A