{-# 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