{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./CSL/Sign.hs
Description :  Signatures for the EnCL logic
Copyright   :  (c) Dominik Dietrich, DFKI Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  dominik.dietrich@dfki.de
Stability   :  experimental
Portability :  portable

Types and functions for EnCL logic signatures
-}

module CSL.Sign
    ( Sign (Sign)                   -- EnCL Signatures
    , opIds
    , OpType (..)                   -- Operator Information attached to ids
    , pretty                        -- pretty printing
    , isLegalSignature              -- is a signature ok?
    , addToSig                      -- adds an id to the given Signature
    , unite                         -- union of signatures
    , emptySig                      -- empty signature
    , isSubSigOf                    -- is subsiganture?
    , sigDiff                       -- Difference of Signatures
    , sigUnion                      -- Union for Logic.Logic
    , lookupSym
    , optypeFromArity
    , addEPDefValToSig
    , addEPDeclToSig
    , addEPDomVarDeclToSig
    ) where

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

import Common.Id
import Common.Result
import Common.Doc
import Common.DocUtils

import CSL.TreePO (ClosedInterval (ClosedInterval))
import CSL.AS_BASIC_CSL
import CSL.Print_AS ()

data OpType = OpType { OpType -> Int
opArity :: Int
                     } deriving (Int -> OpType -> ShowS
[OpType] -> ShowS
OpType -> String
(Int -> OpType -> ShowS)
-> (OpType -> String) -> ([OpType] -> ShowS) -> Show OpType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OpType] -> ShowS
$cshowList :: [OpType] -> ShowS
show :: OpType -> String
$cshow :: OpType -> String
showsPrec :: Int -> OpType -> ShowS
$cshowsPrec :: Int -> OpType -> ShowS
Show, OpType -> OpType -> Bool
(OpType -> OpType -> Bool)
-> (OpType -> OpType -> Bool) -> Eq OpType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OpType -> OpType -> Bool
$c/= :: OpType -> OpType -> Bool
== :: OpType -> OpType -> Bool
$c== :: OpType -> OpType -> Bool
Eq, Eq OpType
Eq OpType =>
(OpType -> OpType -> Ordering)
-> (OpType -> OpType -> Bool)
-> (OpType -> OpType -> Bool)
-> (OpType -> OpType -> Bool)
-> (OpType -> OpType -> Bool)
-> (OpType -> OpType -> OpType)
-> (OpType -> OpType -> OpType)
-> Ord OpType
OpType -> OpType -> Bool
OpType -> OpType -> Ordering
OpType -> OpType -> OpType
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 :: OpType -> OpType -> OpType
$cmin :: OpType -> OpType -> OpType
max :: OpType -> OpType -> OpType
$cmax :: OpType -> OpType -> OpType
>= :: OpType -> OpType -> Bool
$c>= :: OpType -> OpType -> Bool
> :: OpType -> OpType -> Bool
$c> :: OpType -> OpType -> Bool
<= :: OpType -> OpType -> Bool
$c<= :: OpType -> OpType -> Bool
< :: OpType -> OpType -> Bool
$c< :: OpType -> OpType -> Bool
compare :: OpType -> OpType -> Ordering
$ccompare :: OpType -> OpType -> Ordering
$cp1Ord :: Eq OpType
Ord, Typeable, Typeable OpType
Constr
DataType
Typeable OpType =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> OpType -> c OpType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c OpType)
-> (OpType -> Constr)
-> (OpType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c OpType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpType))
-> ((forall b. Data b => b -> b) -> OpType -> OpType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> OpType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> OpType -> r)
-> (forall u. (forall d. Data d => d -> u) -> OpType -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> OpType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> OpType -> m OpType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OpType -> m OpType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OpType -> m OpType)
-> Data OpType
OpType -> Constr
OpType -> DataType
(forall b. Data b => b -> b) -> OpType -> OpType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OpType -> c OpType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OpType
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) -> OpType -> u
forall u. (forall d. Data d => d -> u) -> OpType -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpType -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OpType -> m OpType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OpType -> m OpType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OpType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OpType -> c OpType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OpType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpType)
$cOpType :: Constr
$tOpType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> OpType -> m OpType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OpType -> m OpType
gmapMp :: (forall d. Data d => d -> m d) -> OpType -> m OpType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OpType -> m OpType
gmapM :: (forall d. Data d => d -> m d) -> OpType -> m OpType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OpType -> m OpType
gmapQi :: Int -> (forall d. Data d => d -> u) -> OpType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> OpType -> u
gmapQ :: (forall d. Data d => d -> u) -> OpType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> OpType -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpType -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpType -> r
gmapT :: (forall b. Data b => b -> b) -> OpType -> OpType
$cgmapT :: (forall b. Data b => b -> b) -> OpType -> OpType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c OpType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OpType)
dataTypeOf :: OpType -> DataType
$cdataTypeOf :: OpType -> DataType
toConstr :: OpType -> Constr
$ctoConstr :: OpType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OpType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OpType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OpType -> c OpType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OpType -> c OpType
$cp1Data :: Typeable OpType
Data)

defaultType :: OpType
defaultType :: OpType
defaultType = OpType :: Int -> OpType
OpType { opArity :: Int
opArity = 0 }

optypeFromArity :: Int -> OpType
optypeFromArity :: Int -> OpType
optypeFromArity i :: Int
i = OpType
defaultType { opArity :: Int
opArity = Int
i }

{- | Datatype for EnCL Signatures
Signatures are just sets of Tokens for the operators -}
data Sign = Sign { Sign -> Map Token OpType
items :: Map.Map Token OpType
                 , Sign -> Map Token (Maybe APInt)
epvars :: Map.Map Token (Maybe APInt)
                 , Sign -> Map Token EPDecl
epdecls :: Map.Map Token EPDecl
                 } deriving (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, 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, Typeable, Typeable Sign
Constr
DataType
Typeable Sign =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Sign -> c Sign)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Sign)
-> (Sign -> Constr)
-> (Sign -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Sign))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign))
-> ((forall b. Data b => b -> b) -> Sign -> Sign)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r)
-> (forall u. (forall d. Data d => d -> u) -> Sign -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Sign -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Sign -> m Sign)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sign -> m Sign)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sign -> m Sign)
-> Data Sign
Sign -> Constr
Sign -> DataType
(forall b. Data b => b -> b) -> Sign -> Sign
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign -> c Sign
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sign
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) -> Sign -> u
forall u. (forall d. Data d => d -> u) -> Sign -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sign -> m Sign
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sign -> m Sign
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sign
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign -> c Sign
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sign)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign)
$cSign :: Constr
$tSign :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Sign -> m Sign
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sign -> m Sign
gmapMp :: (forall d. Data d => d -> m d) -> Sign -> m Sign
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sign -> m Sign
gmapM :: (forall d. Data d => d -> m d) -> Sign -> m Sign
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sign -> m Sign
gmapQi :: Int -> (forall d. Data d => d -> u) -> Sign -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sign -> u
gmapQ :: (forall d. Data d => d -> u) -> Sign -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Sign -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
gmapT :: (forall b. Data b => b -> b) -> Sign -> Sign
$cgmapT :: (forall b. Data b => b -> b) -> Sign -> Sign
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Sign)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sign)
dataTypeOf :: Sign -> DataType
$cdataTypeOf :: Sign -> DataType
toConstr :: Sign -> Constr
$ctoConstr :: Sign -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sign
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sign
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign -> c Sign
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign -> c Sign
$cp1Data :: Typeable Sign
Data)

opIds :: Sign -> Set.Set Id
opIds :: Sign -> Set Id
opIds = (Token -> Id) -> Set Token -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Token -> Id
simpleIdToId (Set Token -> Set Id) -> (Sign -> Set Token) -> Sign -> Set Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Token OpType -> Set Token
forall k a. Map k a -> Set k
Map.keysSet (Map Token OpType -> Set Token)
-> (Sign -> Map Token OpType) -> Sign -> Set Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Map Token OpType
items

-- | The empty signature, use this one to create new signatures
emptySig :: Sign
emptySig :: Sign
emptySig = Sign :: Map Token OpType
-> Map Token (Maybe APInt) -> Map Token EPDecl -> Sign
Sign { items :: Map Token OpType
items = Map Token OpType
forall k a. Map k a
Map.empty
                , epvars :: Map Token (Maybe APInt)
epvars = Map Token (Maybe APInt)
forall k a. Map k a
Map.empty
                , epdecls :: Map Token EPDecl
epdecls = Map Token EPDecl
forall k a. Map k a
Map.empty
                }

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

-- | pretty printer for EnCL signatures
printSign :: Sign -> Doc
printSign :: Sign -> Doc
printSign s :: Sign
s = [Doc] -> Doc
vcat [ [(Token, Maybe APInt)] -> Doc
printEPVars ([(Token, Maybe APInt)] -> Doc) -> [(Token, Maybe APInt)] -> Doc
forall a b. (a -> b) -> a -> b
$ Map Token (Maybe APInt) -> [(Token, Maybe APInt)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Token (Maybe APInt) -> [(Token, Maybe APInt)])
-> Map Token (Maybe APInt) -> [(Token, Maybe APInt)]
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token (Maybe APInt)
epvars Sign
s
                   , [EPDecl] -> Doc
printEPDecls ([EPDecl] -> Doc) -> [EPDecl] -> Doc
forall a b. (a -> b) -> a -> b
$ Map Token EPDecl -> [EPDecl]
forall k a. Map k a -> [a]
Map.elems (Map Token EPDecl -> [EPDecl]) -> Map Token EPDecl -> [EPDecl]
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token EPDecl
epdecls Sign
s]

printEPVars :: [(Token, Maybe APInt)] -> Doc
printEPVars :: [(Token, Maybe APInt)] -> Doc
printEPVars [] = Doc
empty
printEPVars l :: [(Token, Maybe APInt)]
l = [Doc] -> Doc
hsep [String -> Doc
text "set", [Doc] -> Doc
sepBySemis ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((Token, Maybe APInt) -> Doc) -> [(Token, Maybe APInt)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Token, Maybe APInt) -> Doc
forall a a. (Pretty a, Pretty a) => (a, Maybe a) -> Doc
f [(Token, Maybe APInt)]
l] where
    f :: (a, Maybe a) -> Doc
f (x :: a
x, Nothing) = a -> Doc
forall a. Pretty a => a -> Doc
pretty a
x
    f (x :: a
x, Just y :: a
y) = [Doc] -> Doc
hcat [a -> Doc
forall a. Pretty a => a -> Doc
pretty a
x, String -> Doc
text "=", a -> Doc
forall a. Pretty a => a -> Doc
pretty a
y]

printEPDecls :: [EPDecl] -> Doc
printEPDecls :: [EPDecl] -> Doc
printEPDecls l :: [EPDecl]
l = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (EPDecl -> Doc) -> [EPDecl] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map EPDecl -> Doc
forall a. Pretty a => a -> Doc
f [EPDecl]
l where
    f :: a -> Doc
f x :: a
x = [Doc] -> Doc
hsep [String -> Doc
text "ep", a -> Doc
forall a. Pretty a => a -> Doc
pretty a
x]


-- | checks whether a Id is declared in the signature
lookupSym :: Sign -> Id -> Bool
lookupSym :: Sign -> Id -> Bool
lookupSym sig :: Sign
sig item :: Id
item = Token -> Map Token OpType -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member (Id -> Token
idToSimpleId Id
item) (Map Token OpType -> Bool) -> Map Token OpType -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token OpType
items Sign
sig

-- TODO: adapt the operations to new signature components


-- | determines whether a signature is valid. all sets are ok, so glued to true
isLegalSignature :: Sign -> Bool
isLegalSignature :: Sign -> Bool
isLegalSignature _ = Bool
True

-- | Basic function to extend a given signature by adding an item (id) to it
addToSig :: Sign -> Token -> OpType -> Sign
addToSig :: Sign -> Token -> OpType -> Sign
addToSig sig :: Sign
sig tok :: Token
tok ot :: OpType
ot = Sign
sig {items :: Map Token OpType
items = Token -> OpType -> Map Token OpType -> Map Token OpType
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Token
tok OpType
ot (Map Token OpType -> Map Token OpType)
-> Map Token OpType -> Map Token OpType
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token OpType
items Sign
sig}


addEPDefValToSig :: Sign -> Token -> APInt -> Sign
addEPDefValToSig :: Sign -> Token -> APInt -> Sign
addEPDefValToSig sig :: Sign
sig tok :: Token
tok i :: APInt
i
    | Maybe EPDecl -> Bool
forall a. Maybe a -> Bool
isNothing Maybe EPDecl
mD = String -> Sign
forall a. HasCallStack => String -> a
error (String -> Sign) -> String -> Sign
forall a b. (a -> b) -> a -> b
$ "addEPDefValToSig: The extended parameter"
                      String -> ShowS
forall a. [a] -> [a] -> [a]
++ " declaration for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
tok String -> ShowS
forall a. [a] -> [a] -> [a]
++ " is missing"
    | Bool
otherwise = Sign
sig {epdecls :: Map Token EPDecl
epdecls = Map Token EPDecl
ed'}
    where (mD :: Maybe EPDecl
mD, ed' :: Map Token EPDecl
ed') = (Token -> EPDecl -> EPDecl -> EPDecl)
-> Token
-> EPDecl
-> Map Token EPDecl
-> (Maybe EPDecl, Map Token EPDecl)
forall k a.
Ord k =>
(k -> a -> a -> a) -> k -> a -> Map k a -> (Maybe a, Map k a)
Map.insertLookupWithKey Token -> EPDecl -> EPDecl -> EPDecl
forall p p. p -> p -> EPDecl -> EPDecl
f Token
tok EPDecl
forall a. a
err (Map Token EPDecl -> (Maybe EPDecl, Map Token EPDecl))
-> Map Token EPDecl -> (Maybe EPDecl, Map Token EPDecl)
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token EPDecl
epdecls Sign
sig
          err :: a
err = String -> a
forall a. HasCallStack => String -> a
error "addEPDefValToSig: dummyval"
          f :: p -> p -> EPDecl -> EPDecl
f _ _ (EPDecl _ dom :: EPDomain
dom Nothing) = Token -> EPDomain -> Maybe APInt -> EPDecl
EPDecl Token
tok EPDomain
dom (Maybe APInt -> EPDecl) -> Maybe APInt -> EPDecl
forall a b. (a -> b) -> a -> b
$ APInt -> Maybe APInt
forall a. a -> Maybe a
Just APInt
i
          f _ _ (EPDecl _ _ (Just j :: APInt
j)) =
              String -> EPDecl
forall a. HasCallStack => String -> a
error (String -> EPDecl) -> String -> EPDecl
forall a b. (a -> b) -> a -> b
$ "addEPDefValToSig: default value already set to "
                        String -> ShowS
forall a. [a] -> [a] -> [a]
++ APInt -> String
forall a. Show a => a -> String
show APInt
j

addEmptyEPDomVarDeclToSig :: Sign -> Token -> Sign
addEmptyEPDomVarDeclToSig :: Sign -> Token -> Sign
addEmptyEPDomVarDeclToSig sig :: Sign
sig tok :: Token
tok = Sign
sig {epvars :: Map Token (Maybe APInt)
epvars = Map Token (Maybe APInt)
ev'}
    where ev' :: Map Token (Maybe APInt)
ev' = (Maybe APInt -> Maybe APInt -> Maybe APInt)
-> Token
-> Maybe APInt
-> Map Token (Maybe APInt)
-> Map Token (Maybe APInt)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Maybe APInt -> Maybe APInt -> Maybe APInt
forall p p. p -> p -> p
f Token
tok Maybe APInt
forall a. Maybe a
Nothing (Map Token (Maybe APInt) -> Map Token (Maybe APInt))
-> Map Token (Maybe APInt) -> Map Token (Maybe APInt)
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token (Maybe APInt)
epvars Sign
sig
          f :: p -> p -> p
f _ v :: p
v = p
v

addEPDomVarDeclToSig :: Sign -> Token -> APInt -> Sign
addEPDomVarDeclToSig :: Sign -> Token -> APInt -> Sign
addEPDomVarDeclToSig sig :: Sign
sig tok :: Token
tok i :: APInt
i = Sign
sig {epvars :: Map Token (Maybe APInt)
epvars = Map Token (Maybe APInt)
ev'}
    where ev' :: Map Token (Maybe APInt)
ev' = (Maybe APInt -> Maybe APInt -> Maybe APInt)
-> Token
-> Maybe APInt
-> Map Token (Maybe APInt)
-> Map Token (Maybe APInt)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Maybe APInt -> Maybe APInt -> Maybe APInt
forall p. p -> Maybe APInt -> p
f Token
tok (APInt -> Maybe APInt
forall a. a -> Maybe a
Just APInt
i) (Map Token (Maybe APInt) -> Map Token (Maybe APInt))
-> Map Token (Maybe APInt) -> Map Token (Maybe APInt)
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token (Maybe APInt)
epvars Sign
sig
          f :: p -> Maybe APInt -> p
f _ (Just x :: APInt
x)
              | APInt
x APInt -> APInt -> Bool
forall a. Eq a => a -> a -> Bool
== APInt
i = String -> p
forall a. HasCallStack => String -> a
error (String -> p) -> String -> p
forall a b. (a -> b) -> a -> b
$ "addEPDomVarDeclToSig: equal values for "
                         String -> ShowS
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
tok
              | Bool
otherwise = String -> p
forall a. HasCallStack => String -> a
error (String -> p) -> String -> p
forall a b. (a -> b) -> a -> b
$ "addEPDomVarDeclToSig: variable already"
                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ " set to different value " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
tok String -> ShowS
forall a. [a] -> [a] -> [a]
++ "="
                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ APInt -> String
forall a. Show a => a -> String
show APInt
x
          f n :: p
n _ = p
n

{- | Adds an extended parameter declaration for a given domain and
eventually implicitly defined EP domain vars, e.g., for 'I = [0, n]'
'n' is implicitly added -}
addEPDeclToSig :: Sign -> Token -> EPDomain -> Sign
addEPDeclToSig :: Sign -> Token -> EPDomain -> Sign
addEPDeclToSig sig :: Sign
sig tok :: Token
tok dom :: EPDomain
dom = Sign -> Sign
g (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ Sign
sig {epdecls :: Map Token EPDecl
epdecls = Map Token EPDecl
ed'}
    where (mD :: Maybe EPDecl
mD, ed' :: Map Token EPDecl
ed') = (Token -> EPDecl -> EPDecl -> EPDecl)
-> Token
-> EPDecl
-> Map Token EPDecl
-> (Maybe EPDecl, Map Token EPDecl)
forall k a.
Ord k =>
(k -> a -> a -> a) -> k -> a -> Map k a -> (Maybe a, Map k a)
Map.insertLookupWithKey Token -> EPDecl -> EPDecl -> EPDecl
forall p p. p -> p -> EPDecl -> EPDecl
f Token
tok EPDecl
epd (Map Token EPDecl -> (Maybe EPDecl, Map Token EPDecl))
-> Map Token EPDecl -> (Maybe EPDecl, Map Token EPDecl)
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token EPDecl
epdecls Sign
sig
          epd :: EPDecl
epd = Token -> EPDomain -> Maybe APInt -> EPDecl
EPDecl Token
tok EPDomain
dom Maybe APInt
forall a. Maybe a
Nothing
          f :: p -> p -> EPDecl -> EPDecl
f _ _ v :: EPDecl
v@(EPDecl _ dom' :: EPDomain
dom' _)
              | EPDomain
dom' EPDomain -> EPDomain -> Bool
forall a. Eq a => a -> a -> Bool
== EPDomain
dom = EPDecl
v
              | Bool
otherwise = String -> EPDecl
forall a. HasCallStack => String -> a
error (String -> EPDecl) -> String -> EPDecl
forall a b. (a -> b) -> a -> b
$ "addEPDeclToSig: EP already"
                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ " assigned another domain: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
tok String -> ShowS
forall a. [a] -> [a] -> [a]
++ "in"
                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ EPDomain -> String
forall a. Show a => a -> String
show EPDomain
dom'
          g :: Sign -> Sign
g s :: Sign
s =
              case (Maybe EPDecl
mD, EPDomain
dom) of
                (Nothing, ClosedInterval a :: EPVal
a b :: EPVal
b) ->
                    case (EPVal -> Maybe Token) -> [EPVal] -> [Token]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe EPVal -> Maybe Token
getEPVarRef [EPVal
a, EPVal
b] of
                      [] -> Sign
s
                      l :: [Token]
l -> (Sign -> Token -> Sign) -> Sign -> [Token] -> Sign
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Sign -> Token -> Sign
addEmptyEPDomVarDeclToSig Sign
s [Token]
l
                _ -> Sign
s


-- TODO: add support for epdecls and report errors if they do not match!

{- Two signatures s1 and s2 are compatible if the common part has the
   following properties:

   * if the default value of an extparam is defined in s1 and s2 it has to be the same
   * if the domains (of extparams or vars) are both given, they must not be disjoint
   * the arities must conincide for the same operator

-}

-- | Union of signatures
unite :: Sign -> Sign -> Sign
unite :: Sign -> Sign -> Sign
unite sig1 :: Sign
sig1 sig2 :: Sign
sig2 =
    Sign
sig1 { items :: Map Token OpType
items = Map Token OpType -> Map Token OpType -> Map Token OpType
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Sign -> Map Token OpType
items Sign
sig1) (Map Token OpType -> Map Token OpType)
-> Map Token OpType -> Map Token OpType
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token OpType
items Sign
sig2
         }

-- | Determines if sig1 is subsignature of sig2
isSubSigOf :: Sign -> Sign -> Bool
isSubSigOf :: Sign -> Sign -> Bool
isSubSigOf sig1 :: Sign
sig1 sig2 :: Sign
sig2 = Map Token OpType -> Map Token OpType -> Bool
forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
Map.isSubmapOf (Sign -> Map Token OpType
items Sign
sig1) (Map Token OpType -> Bool) -> Map Token OpType -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token OpType
items Sign
sig2

-- | difference of Signatures
sigDiff :: Sign -> Sign -> Sign
sigDiff :: Sign -> Sign -> Sign
sigDiff sig1 :: Sign
sig1 sig2 :: Sign
sig2 = Sign
sig1 {items :: Map Token OpType
items = Map Token OpType -> Map Token OpType -> Map Token OpType
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference (Sign -> Map Token OpType
items Sign
sig1) (Map Token OpType -> Map Token OpType)
-> Map Token OpType -> Map Token OpType
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token OpType
items Sign
sig2}

{- | union of Signatures
or do I have to care about more things here? -}
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