Symbol.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
5645e0c82a55b05abb975bd91b9566823dc5efb0Evan Hunt{-# LANGUAGE DeriveDataTypeable #-}
87708bde16713bc02ff2598f4a82f98c699a2f2dMark AndrewsDescription : Symbols of propositional logic
87708bde16713bc02ff2598f4a82f98c699a2f2dMark AndrewsCopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
87708bde16713bc02ff2598f4a82f98c699a2f2dMark AndrewsLicense : GPLv2 or higher, see LICENSE.txt
87708bde16713bc02ff2598f4a82f98c699a2f2dMark AndrewsMaintainer : <jonathan.von_schroeder@dfki.de>
87708bde16713bc02ff2598f4a82f98c699a2f2dMark AndrewsStability : experimental
87708bde16713bc02ff2598f4a82f98c699a2f2dMark AndrewsPortability : portable
87708bde16713bc02ff2598f4a82f98c699a2f2dMark AndrewsDefinition of symbols for propositional logic
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver Symbol (..) -- Symbol type
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver , pretty -- pretty printing for Symbols
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver , symOf -- Extracts the symbols out of a signature
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver , getSymbolMap -- Determines the symbol map
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver , getSymbolName -- Determines the name of a symbol
87708bde16713bc02ff2598f4a82f98c699a2f2dMark Andrews , idToRaw -- Creates a raw symbol
87708bde16713bc02ff2598f4a82f98c699a2f2dMark Andrews , symbolToRaw -- Convert symbol to raw symbol
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver , matches -- does a symbol match a raw symbol?
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver , applySymMap -- application function for symbol maps
87708bde16713bc02ff2598f4a82f98c699a2f2dMark Andrewsimport qualified Common.Id as Id
afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryverimport qualified Data.Set as Set
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverimport qualified Data.Map as Map
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverimport qualified Propositional.Sign as Sign
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverimport QBF.Morphism as Morphism
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver-- | Datatype for symbols
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryvernewtype Symbol = Symbol {symName :: Id.Id}
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver deriving (Show, Eq, Ord, Typeable, Data)
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverinstance Id.GetRange Symbol where
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver getRange = Id.getRange . symName
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryverinstance Pretty Symbol where
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver pretty = printSymbol
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon SchryverprintSymbol :: Symbol -> Doc
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon SchryverprintSymbol = pretty . symName
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver-- | Extraction of symbols from a signature
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon SchryversymOf = Set.fold (\ y -> Set.insert Symbol {symName = y}) Set.empty .
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver-- | Determines the symbol map of a morhpism
afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon SchryvergetSymbolMap :: Morphism.Morphism -> Map.Map Symbol Symbol
afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon SchryvergetSymbolMap f =
afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryver foldr (\ x -> Map.insert (Symbol x) (Symbol $ applyMap (propMap f) x))
afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryver Map.empty $ Set.toList $ Sign.items $ source f
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver-- | Determines the name of a symbol
afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon SchryvergetSymbolName :: Symbol -> Id.Id
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon SchryvergetSymbolName = symName
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver-- | make a raw_symbol
afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon SchryveridToRaw :: Id.Id -> Symbol
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon SchryveridToRaw mid = Symbol {symName = mid}
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryver-- | convert to raw symbol
afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon SchryversymbolToRaw :: Symbol -> Symbol
afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon SchryversymbolToRaw = id
afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryver-- | does a smybol match a raw symbol?
afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryvermatches :: Symbol -> Symbol -> Bool
9fee08f655527a5dd849b171daeeee1dbbccca76Vernon Schryvermatches = (==)
afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon Schryver-- | application function for Symbol Maps
afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon SchryverapplySymMap :: Map.Map Symbol Symbol -> Symbol -> Symbol
afaa290bb6acc504e93a0adbf20b6dd6c64e6d63Vernon SchryverapplySymMap smap idt = Map.findWithDefault idt idt smap