{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./CommonLogic/Symbol.hs
Description :  Symbols of common logic
Copyright   :  (c) Karl Luc, DFKI Bremen 2010, Eugen Kuksa, Uni Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  eugenk@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

Definition of symbols for common logic
-}

module CommonLogic.Symbol (
        Symbol (..)
       , printSymbol
       , symOf
       , getSymbolMap
       , getSymbolName
       , symbolToRaw
       , idToRaw
       , matches
       , addSymbToSign
       , symKind
       )
       where

import qualified Common.Id as Id
import Common.Doc
import Common.DocUtils
import Common.Result

import Data.Data
import qualified Data.Set as Set
import qualified Data.Map as Map

import qualified CommonLogic.Sign as Sign
import CommonLogic.Morphism as Morphism

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

instance Pretty Symbol where
    pretty :: Symbol -> Doc
pretty = Symbol -> Doc
printSymbol

-- | Pretty prints the symbol @x@
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

-- | Converts a signature to a set of symbols
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.allItems 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 -> Map Symbol Symbol -> Map Symbol Symbol)
-> Map Symbol Symbol -> [Id] -> Map Symbol Symbol
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ x :: Id
x -> Symbol -> Symbol -> Map Symbol Symbol -> Map Symbol Symbol
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id -> Symbol
Symbol Id
x) (Id -> Symbol
Symbol (Id -> Symbol) -> Id -> Symbol
forall a b. (a -> b) -> a -> b
$ Map Id Id -> Id -> Id
applyMap (Morphism -> Map Id Id
propMap Morphism
f) Id
x))
  Map Symbol Symbol
forall k a. Map k a
Map.empty ([Id] -> Map Symbol Symbol) -> [Id] -> Map Symbol Symbol
forall a b. (a -> b) -> a -> b
$ Set Id -> [Id]
forall a. Set a -> [a]
Set.toList (Set Id -> [Id]) -> Set Id -> [Id]
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
Sign.allItems (Sign -> Set Id) -> Sign -> Set Id
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
source Morphism
f

-- | Determines the name of a symbol
getSymbolName :: Symbol -> Id.Id
getSymbolName :: Symbol -> Id
getSymbolName = Symbol -> Id
symName

symbolToRaw :: Symbol -> Symbol
symbolToRaw :: Symbol -> Symbol
symbolToRaw = Symbol -> Symbol
forall a. a -> a
id

idToRaw :: Id.Id -> Symbol
idToRaw :: Id -> Symbol
idToRaw mid :: Id
mid = Symbol :: Id -> Symbol
Symbol {symName :: Id
symName = Id
mid}

-- | Checks two symbols on equality
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

-- | Adds a symbol to a signature
addSymbToSign :: Sign.Sign -> Symbol -> Result Sign.Sign
addSymbToSign :: Sign -> Symbol -> Result Sign
addSymbToSign sig :: Sign
sig symb :: Symbol
symb = [Diagnosis] -> Maybe Sign -> Result Sign
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] (Maybe Sign -> Result Sign) -> Maybe Sign -> Result Sign
forall a b. (a -> b) -> a -> b
$ Sign -> Maybe Sign
forall a. a -> Maybe a
Just (Sign -> Maybe Sign) -> Sign -> Maybe Sign
forall a b. (a -> b) -> a -> b
$
  if Id -> Bool
Sign.isSeqMark (Id -> Bool) -> Id -> Bool
forall a b. (a -> b) -> a -> b
$ Symbol -> Id
symName Symbol
symb
  then Sign
sig { sequenceMarkers :: Set Id
Sign.sequenceMarkers =
                    Id -> Set Id -> Set Id
forall a. Ord a => a -> Set a -> Set a
Set.insert (Symbol -> Id
symName Symbol
symb) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
Sign.sequenceMarkers Sign
sig
           }
  else Sign
sig { discourseNames :: Set Id
Sign.discourseNames =
                    Id -> Set Id -> Set Id
forall a. Ord a => a -> Set a -> Set a
Set.insert (Symbol -> Id
symName Symbol
symb) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
Sign.discourseNames Sign
sig
           }

-- | Returns a string classifying the symbol as name or sequence marker
symKind :: Symbol -> String
symKind :: Symbol -> String
symKind s :: Symbol
s = if Id -> Bool
Sign.isSeqMark (Id -> Bool) -> Id -> Bool
forall a b. (a -> b) -> a -> b
$ Symbol -> Id
symName Symbol
s then String
symKindSeqMark else String
symKindName

symKindName :: String
symKindName :: String
symKindName = "Name"

symKindSeqMark :: String
symKindSeqMark :: String
symKindSeqMark = "SequenceMarker"