{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./CommonLogic/Sign.hs
Description :  Signature for common logic
Copyright   :  (c) Karl Luc, DFKI Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

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

Definition of signatures for common logic
-}

module CommonLogic.Sign
    (Sign (..)
    , pretty                        -- pretty printing
    , allItems                      -- union of all signature-fields
    , emptySig                      -- empty signature
    , isSubSigOf                    -- sub signature of signature
    , sigDiff                       -- Difference of Signatures
    , unite                         -- union of signatures
    , uniteL                        -- union of a list ofsignatures
    , sigUnion                      -- Union for Logic.Logic
    , sigUnionL                     -- union of a list ofsignatures
    , isSeqMark                     -- is an Id a sequence marker?
    ) where

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

import Data.Data
import Data.List (isPrefixOf)

-- | Datatype for common logic Signatures

data Sign = Sign { Sign -> Set Id
discourseNames :: Set.Set Id
                 , Sign -> Set Id
nondiscourseNames :: Set.Set Id
                 , Sign -> Set Id
sequenceMarkers :: Set.Set Id
                 } deriving (Sign -> Sign -> Bool
(Sign -> Sign -> Bool) -> (Sign -> Sign -> Bool) -> Eq Sign
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sign -> Sign -> Bool
$c/= :: Sign -> Sign -> Bool
== :: Sign -> Sign -> Bool
$c== :: Sign -> Sign -> Bool
Eq, Eq Sign
Eq Sign =>
(Sign -> Sign -> Ordering)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Sign)
-> (Sign -> Sign -> Sign)
-> Ord Sign
Sign -> Sign -> Bool
Sign -> Sign -> Ordering
Sign -> Sign -> Sign
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 :: Sign -> Sign -> Sign
$cmin :: Sign -> Sign -> Sign
max :: Sign -> Sign -> Sign
$cmax :: Sign -> Sign -> Sign
>= :: Sign -> Sign -> Bool
$c>= :: Sign -> Sign -> Bool
> :: Sign -> Sign -> Bool
$c> :: Sign -> Sign -> Bool
<= :: Sign -> Sign -> Bool
$c<= :: Sign -> Sign -> Bool
< :: Sign -> Sign -> Bool
$c< :: Sign -> Sign -> Bool
compare :: Sign -> Sign -> Ordering
$ccompare :: Sign -> Sign -> Ordering
$cp1Ord :: Eq Sign
Ord, Int -> Sign -> ShowS
[Sign] -> ShowS
Sign -> String
(Int -> Sign -> ShowS)
-> (Sign -> String) -> ([Sign] -> ShowS) -> Show Sign
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sign] -> ShowS
$cshowList :: [Sign] -> ShowS
show :: Sign -> String
$cshow :: Sign -> String
showsPrec :: Int -> Sign -> ShowS
$cshowsPrec :: Int -> Sign -> ShowS
Show, Typeable)

instance Pretty Sign where
    pretty :: Sign -> Doc
pretty = Sign -> Doc
printSign

-- | union of all signature-fields
allItems :: Sign -> Set.Set Id
allItems :: Sign -> Set Id
allItems s :: Sign
s = [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Id] -> Set Id) -> [Set Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ ((Sign -> Set Id) -> Set Id) -> [Sign -> Set Id] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map (\ f :: Sign -> Set Id
f -> Sign -> Set Id
f Sign
s) [ Sign -> Set Id
discourseNames
                                          , Sign -> Set Id
nondiscourseNames
                                          , Sign -> Set Id
sequenceMarkers
                                          ]

-- | The empty signature
emptySig :: Sign
emptySig :: Sign
emptySig = Sign :: Set Id -> Set Id -> Set Id -> Sign
Sign { discourseNames :: Set Id
discourseNames = Set Id
forall a. Set a
Set.empty
                , nondiscourseNames :: Set Id
nondiscourseNames = Set Id
forall a. Set a
Set.empty
                , sequenceMarkers :: Set Id
sequenceMarkers = Set Id
forall a. Set a
Set.empty
                }

-- | pretty printing for Signatures
printSign :: Sign -> Doc
printSign :: Sign -> Doc
printSign s :: Sign
s =
  [Doc] -> Doc
vsep [ String -> Doc
text "%{"
       , String -> Doc
text "discourseNames: "
          Doc -> Doc -> Doc
<+> [Doc] -> Doc
sepByCommas ((Id -> Doc) -> [Id] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Doc
forall a. Pretty a => a -> Doc
pretty ([Id] -> [Doc]) -> [Id] -> [Doc]
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
discourseNames Sign
s)
       , String -> Doc
text "nondiscourseNames: "
          Doc -> Doc -> Doc
<+> [Doc] -> Doc
sepByCommas ((Id -> Doc) -> [Id] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Doc
forall a. Pretty a => a -> Doc
pretty ([Id] -> [Doc]) -> [Id] -> [Doc]
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
nondiscourseNames Sign
s)
       , String -> Doc
text "sequenceMarkers: "
          Doc -> Doc -> Doc
<+> [Doc] -> Doc
sepByCommas ((Id -> Doc) -> [Id] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Doc
forall a. Pretty a => a -> Doc
pretty ([Id] -> [Doc]) -> [Id] -> [Doc]
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
sequenceMarkers Sign
s)
       , String -> Doc
text "}%"]

-- | Determines if sig1 is subsignature of sig2
isSubSigOf :: Sign -> Sign -> Bool
isSubSigOf :: Sign -> Sign -> Bool
isSubSigOf sig1 :: Sign
sig1 sig2 :: Sign
sig2 =
  Set Id -> Set Id -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (Sign -> Set Id
discourseNames Sign
sig1) (Sign -> Set Id
discourseNames Sign
sig2)
  Bool -> Bool -> Bool
&& Set Id -> Set Id -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (Sign -> Set Id
nondiscourseNames Sign
sig1) (Sign -> Set Id
nondiscourseNames Sign
sig2)
  Bool -> Bool -> Bool
&& Set Id -> Set Id -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (Sign -> Set Id
sequenceMarkers Sign
sig1) (Sign -> Set Id
sequenceMarkers Sign
sig2)

-- | difference of Signatures
sigDiff :: Sign -> Sign -> Sign
sigDiff :: Sign -> Sign -> Sign
sigDiff sig1 :: Sign
sig1 sig2 :: Sign
sig2 = Sign :: Set Id -> Set Id -> Set Id -> Sign
Sign {
  discourseNames :: Set Id
discourseNames = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign -> Set Id
discourseNames Sign
sig1) (Sign -> Set Id
discourseNames Sign
sig2),
  nondiscourseNames :: Set Id
nondiscourseNames = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign -> Set Id
nondiscourseNames Sign
sig1) (Sign -> Set Id
nondiscourseNames Sign
sig2),
  sequenceMarkers :: Set Id
sequenceMarkers = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign -> Set Id
sequenceMarkers Sign
sig1) (Sign -> Set Id
sequenceMarkers Sign
sig2)
}

-- | Unite Signatures
sigUnion :: Sign -> Sign -> Result Sign
sigUnion :: Sign -> Sign -> Result Sign
sigUnion s1 :: Sign
s1 = [Diagnosis] -> Maybe Sign -> Result Sign
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Debug "All fine sigUnion" Range
nullRange]
      (Maybe Sign -> Result Sign)
-> (Sign -> Maybe Sign) -> Sign -> Result Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Maybe Sign
forall a. a -> Maybe a
Just (Sign -> Maybe Sign) -> (Sign -> Sign) -> Sign -> Maybe Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Sign -> Sign
unite Sign
s1

-- | Unite Signature in a list
sigUnionL :: [Sign] -> Result Sign
sigUnionL :: [Sign] -> Result Sign
sigUnionL (sig :: Sign
sig : sigL :: [Sign]
sigL) = Sign -> Sign -> Result Sign
sigUnion Sign
sig ([Sign] -> Sign
uniteL [Sign]
sigL)
sigUnionL [] = Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return Sign
emptySig

-- | Union of two signatures. Behaves like Set.union, i.e. is fast with @bigsig `union` smallsig@.
unite :: Sign -> Sign -> Sign
unite :: Sign -> Sign -> Sign
unite sig1 :: Sign
sig1 sig2 :: Sign
sig2 = Sign :: Set Id -> Set Id -> Set Id -> Sign
Sign
  { discourseNames :: Set Id
discourseNames = Sign -> Set Id
discourseNames Sign
sig1 Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Sign -> Set Id
discourseNames Sign
sig2
  , nondiscourseNames :: Set Id
nondiscourseNames = Sign -> Set Id
nondiscourseNames Sign
sig1 Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Sign -> Set Id
nondiscourseNames Sign
sig2
  , sequenceMarkers :: Set Id
sequenceMarkers = Sign -> Set Id
sequenceMarkers Sign
sig1 Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Sign -> Set Id
sequenceMarkers Sign
sig2
  }

-- | Union of a list of signatures.
uniteL :: [Sign] -> Sign
uniteL :: [Sign] -> Sign
uniteL = (Sign -> Sign -> Sign) -> Sign -> [Sign] -> Sign
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Sign -> Sign -> Sign
unite Sign
emptySig

isSeqMark :: Id -> Bool
isSeqMark :: Id -> Bool
isSeqMark = String -> Bool
isStringSeqMark (String -> Bool) -> (Id -> String) -> Id -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> String
tokStr (Token -> String) -> (Id -> Token) -> Id -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Token
idToSimpleId

-- | Checks whether a String is a sequence marker
isStringSeqMark :: String -> Bool
isStringSeqMark :: String -> Bool
isStringSeqMark s :: String
s = "..." String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
s