{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./THF/Sign.hs
Description :  Signature for THF
Copyright   :  (c) A. Tsogias, DFKI Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Alexis.Tsogias@dfki.de
Stability   :  provisional
Portability :  portable

Data structures and functions for thf THF Signatures.
Note: Most of the implenentations support only THF0.
-}

module THF.Sign where

import THF.As
import THF.Cons

import Common.DefaultMorphism
import Common.Id hiding (typeId)
import Common.Result

import Data.Data
import qualified Data.Map as Map

{- -----------------------------------------------------------------------------
Definitions and instances of data structures
----------------------------------------------------------------------------- -}

-- We use the DefaultMorphism for THF.
type MorphismTHF = DefaultMorphism SignTHF

{- A signature is a container for types and constants. In addition they are
stored in an SymbolMap. -}
data SignTHF = Sign
    { SignTHF -> TypeMap
types :: TypeMap
    , SignTHF -> ConstMap
consts :: ConstMap
    , SignTHF -> SymbolMap
symbols :: SymbolMap
    } deriving (Int -> SignTHF -> ShowS
[SignTHF] -> ShowS
SignTHF -> String
(Int -> SignTHF -> ShowS)
-> (SignTHF -> String) -> ([SignTHF] -> ShowS) -> Show SignTHF
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SignTHF] -> ShowS
$cshowList :: [SignTHF] -> ShowS
show :: SignTHF -> String
$cshow :: SignTHF -> String
showsPrec :: Int -> SignTHF -> ShowS
$cshowsPrec :: Int -> SignTHF -> ShowS
Show, SignTHF -> SignTHF -> Bool
(SignTHF -> SignTHF -> Bool)
-> (SignTHF -> SignTHF -> Bool) -> Eq SignTHF
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SignTHF -> SignTHF -> Bool
$c/= :: SignTHF -> SignTHF -> Bool
== :: SignTHF -> SignTHF -> Bool
$c== :: SignTHF -> SignTHF -> Bool
Eq, Typeable, Typeable SignTHF
Constr
DataType
Typeable SignTHF =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> SignTHF -> c SignTHF)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SignTHF)
-> (SignTHF -> Constr)
-> (SignTHF -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SignTHF))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SignTHF))
-> ((forall b. Data b => b -> b) -> SignTHF -> SignTHF)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SignTHF -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SignTHF -> r)
-> (forall u. (forall d. Data d => d -> u) -> SignTHF -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> SignTHF -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SignTHF -> m SignTHF)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SignTHF -> m SignTHF)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SignTHF -> m SignTHF)
-> Data SignTHF
SignTHF -> Constr
SignTHF -> DataType
(forall b. Data b => b -> b) -> SignTHF -> SignTHF
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SignTHF -> c SignTHF
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SignTHF
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) -> SignTHF -> u
forall u. (forall d. Data d => d -> u) -> SignTHF -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SignTHF -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SignTHF -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SignTHF -> m SignTHF
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SignTHF -> m SignTHF
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SignTHF
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SignTHF -> c SignTHF
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SignTHF)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SignTHF)
$cSign :: Constr
$tSignTHF :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> SignTHF -> m SignTHF
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SignTHF -> m SignTHF
gmapMp :: (forall d. Data d => d -> m d) -> SignTHF -> m SignTHF
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SignTHF -> m SignTHF
gmapM :: (forall d. Data d => d -> m d) -> SignTHF -> m SignTHF
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SignTHF -> m SignTHF
gmapQi :: Int -> (forall d. Data d => d -> u) -> SignTHF -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SignTHF -> u
gmapQ :: (forall d. Data d => d -> u) -> SignTHF -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SignTHF -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SignTHF -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SignTHF -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SignTHF -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SignTHF -> r
gmapT :: (forall b. Data b => b -> b) -> SignTHF -> SignTHF
$cgmapT :: (forall b. Data b => b -> b) -> SignTHF -> SignTHF
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SignTHF)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SignTHF)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SignTHF)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SignTHF)
dataTypeOf :: SignTHF -> DataType
$cdataTypeOf :: SignTHF -> DataType
toConstr :: SignTHF -> Constr
$ctoConstr :: SignTHF -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SignTHF
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SignTHF
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SignTHF -> c SignTHF
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SignTHF -> c SignTHF
$cp1Data :: Typeable SignTHF
Data)

-- Ord instance that does not use symbols
instance Ord SignTHF where
    compare :: SignTHF -> SignTHF -> Ordering
compare s1 :: SignTHF
s1 s2 :: SignTHF
s2 = (TypeMap, ConstMap) -> (TypeMap, ConstMap) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (SignTHF -> TypeMap
types SignTHF
s1, SignTHF -> ConstMap
consts SignTHF
s1) (SignTHF -> TypeMap
types SignTHF
s2, SignTHF -> ConstMap
consts SignTHF
s2)

instance GetRange SignTHF

-- Map for Types.
type TypeMap = Map.Map Constant TypeInfo

-- Map for Constants.
type ConstMap = Map.Map Constant ConstInfo

-- Map for Symbols. These are symbols and types.
type SymbolMap = Map.Map Constant SymbolTHF

{- TypeInfo are containers for types, their name and Kind.
In addition the original Annotaions can be stored as
Annotations. -}
data TypeInfo = TypeInfo
    { TypeInfo -> Constant
typeId :: Constant
    , TypeInfo -> Name
typeName :: Name
    , TypeInfo -> Kind
typeKind :: Kind
    , TypeInfo -> Annotations
typeAnno :: Annotations }
    deriving (Int -> TypeInfo -> ShowS
[TypeInfo] -> ShowS
TypeInfo -> String
(Int -> TypeInfo -> ShowS)
-> (TypeInfo -> String) -> ([TypeInfo] -> ShowS) -> Show TypeInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeInfo] -> ShowS
$cshowList :: [TypeInfo] -> ShowS
show :: TypeInfo -> String
$cshow :: TypeInfo -> String
showsPrec :: Int -> TypeInfo -> ShowS
$cshowsPrec :: Int -> TypeInfo -> ShowS
Show, Typeable, Typeable TypeInfo
Constr
DataType
Typeable TypeInfo =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TypeInfo -> c TypeInfo)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TypeInfo)
-> (TypeInfo -> Constr)
-> (TypeInfo -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TypeInfo))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeInfo))
-> ((forall b. Data b => b -> b) -> TypeInfo -> TypeInfo)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TypeInfo -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TypeInfo -> r)
-> (forall u. (forall d. Data d => d -> u) -> TypeInfo -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TypeInfo -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo)
-> Data TypeInfo
TypeInfo -> Constr
TypeInfo -> DataType
(forall b. Data b => b -> b) -> TypeInfo -> TypeInfo
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeInfo -> c TypeInfo
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypeInfo
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) -> TypeInfo -> u
forall u. (forall d. Data d => d -> u) -> TypeInfo -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeInfo -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeInfo -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypeInfo
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeInfo -> c TypeInfo
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TypeInfo)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeInfo)
$cTypeInfo :: Constr
$tTypeInfo :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo
gmapMp :: (forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo
gmapM :: (forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo
gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeInfo -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TypeInfo -> u
gmapQ :: (forall d. Data d => d -> u) -> TypeInfo -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TypeInfo -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeInfo -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeInfo -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeInfo -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeInfo -> r
gmapT :: (forall b. Data b => b -> b) -> TypeInfo -> TypeInfo
$cgmapT :: (forall b. Data b => b -> b) -> TypeInfo -> TypeInfo
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeInfo)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TypeInfo)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TypeInfo)
dataTypeOf :: TypeInfo -> DataType
$cdataTypeOf :: TypeInfo -> DataType
toConstr :: TypeInfo -> Constr
$ctoConstr :: TypeInfo -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypeInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypeInfo
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeInfo -> c TypeInfo
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeInfo -> c TypeInfo
$cp1Data :: Typeable TypeInfo
Data)

-- Ord instance that neither uses typeDef nor typeAnno
instance Ord TypeInfo where
    compare :: TypeInfo -> TypeInfo -> Ordering
compare ti1 :: TypeInfo
ti1 ti2 :: TypeInfo
ti2 = (Constant, Name, Kind) -> (Constant, Name, Kind) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare
        (TypeInfo -> Constant
typeId TypeInfo
ti1, TypeInfo -> Name
typeName TypeInfo
ti1, TypeInfo -> Kind
typeKind TypeInfo
ti1)
        (TypeInfo -> Constant
typeId TypeInfo
ti2, TypeInfo -> Name
typeName TypeInfo
ti2, TypeInfo -> Kind
typeKind TypeInfo
ti2)

-- Eq instance that neither uses typeDef nor typeAnno
instance Eq TypeInfo where
    == :: TypeInfo -> TypeInfo -> Bool
(==) ti1 :: TypeInfo
ti1 ti2 :: TypeInfo
ti2 = (TypeInfo -> Constant
typeId TypeInfo
ti1, TypeInfo -> Name
typeName TypeInfo
ti1, TypeInfo -> Kind
typeKind TypeInfo
ti1) (Constant, Name, Kind) -> (Constant, Name, Kind) -> Bool
forall a. Eq a => a -> a -> Bool
==
                   (TypeInfo -> Constant
typeId TypeInfo
ti2, TypeInfo -> Name
typeName TypeInfo
ti2, TypeInfo -> Kind
typeKind TypeInfo
ti2)

{- ConstInfo are containers for constants, their naem and type.
In addition the original Annotaions can be stored as
Annotations. -}
data ConstInfo = ConstInfo
    { ConstInfo -> Constant
constId :: Constant
    , ConstInfo -> Name
constName :: Name
    , ConstInfo -> Type
constType :: Type
    , ConstInfo -> Annotations
constAnno :: Annotations }
    deriving (Int -> ConstInfo -> ShowS
[ConstInfo] -> ShowS
ConstInfo -> String
(Int -> ConstInfo -> ShowS)
-> (ConstInfo -> String)
-> ([ConstInfo] -> ShowS)
-> Show ConstInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ConstInfo] -> ShowS
$cshowList :: [ConstInfo] -> ShowS
show :: ConstInfo -> String
$cshow :: ConstInfo -> String
showsPrec :: Int -> ConstInfo -> ShowS
$cshowsPrec :: Int -> ConstInfo -> ShowS
Show, Typeable, Typeable ConstInfo
Constr
DataType
Typeable ConstInfo =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ConstInfo -> c ConstInfo)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ConstInfo)
-> (ConstInfo -> Constr)
-> (ConstInfo -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ConstInfo))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConstInfo))
-> ((forall b. Data b => b -> b) -> ConstInfo -> ConstInfo)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ConstInfo -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ConstInfo -> r)
-> (forall u. (forall d. Data d => d -> u) -> ConstInfo -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ConstInfo -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ConstInfo -> m ConstInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ConstInfo -> m ConstInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ConstInfo -> m ConstInfo)
-> Data ConstInfo
ConstInfo -> Constr
ConstInfo -> DataType
(forall b. Data b => b -> b) -> ConstInfo -> ConstInfo
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ConstInfo -> c ConstInfo
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ConstInfo
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) -> ConstInfo -> u
forall u. (forall d. Data d => d -> u) -> ConstInfo -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ConstInfo -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ConstInfo -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ConstInfo -> m ConstInfo
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ConstInfo -> m ConstInfo
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ConstInfo
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ConstInfo -> c ConstInfo
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ConstInfo)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConstInfo)
$cConstInfo :: Constr
$tConstInfo :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ConstInfo -> m ConstInfo
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ConstInfo -> m ConstInfo
gmapMp :: (forall d. Data d => d -> m d) -> ConstInfo -> m ConstInfo
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ConstInfo -> m ConstInfo
gmapM :: (forall d. Data d => d -> m d) -> ConstInfo -> m ConstInfo
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ConstInfo -> m ConstInfo
gmapQi :: Int -> (forall d. Data d => d -> u) -> ConstInfo -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ConstInfo -> u
gmapQ :: (forall d. Data d => d -> u) -> ConstInfo -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ConstInfo -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ConstInfo -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ConstInfo -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ConstInfo -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ConstInfo -> r
gmapT :: (forall b. Data b => b -> b) -> ConstInfo -> ConstInfo
$cgmapT :: (forall b. Data b => b -> b) -> ConstInfo -> ConstInfo
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConstInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConstInfo)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ConstInfo)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ConstInfo)
dataTypeOf :: ConstInfo -> DataType
$cdataTypeOf :: ConstInfo -> DataType
toConstr :: ConstInfo -> Constr
$ctoConstr :: ConstInfo -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ConstInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ConstInfo
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ConstInfo -> c ConstInfo
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ConstInfo -> c ConstInfo
$cp1Data :: Typeable ConstInfo
Data)

-- Ord instance that neither uses constDef nor constAnno
instance Ord ConstInfo where
    compare :: ConstInfo -> ConstInfo -> Ordering
compare ci1 :: ConstInfo
ci1 ci2 :: ConstInfo
ci2 = (Constant, Name, Type) -> (Constant, Name, Type) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare
        (ConstInfo -> Constant
constId ConstInfo
ci1, ConstInfo -> Name
constName ConstInfo
ci1, ConstInfo -> Type
constType ConstInfo
ci1)
        (ConstInfo -> Constant
constId ConstInfo
ci2, ConstInfo -> Name
constName ConstInfo
ci2, ConstInfo -> Type
constType ConstInfo
ci2)

-- Eq instance that neither uses constDef nor constAnno
instance Eq ConstInfo where
    == :: ConstInfo -> ConstInfo -> Bool
(==) ci1 :: ConstInfo
ci1 ci2 :: ConstInfo
ci2 = (ConstInfo -> Constant
constId ConstInfo
ci1, ConstInfo -> Name
constName ConstInfo
ci1, ConstInfo -> Type
constType ConstInfo
ci1) (Constant, Name, Type) -> (Constant, Name, Type) -> Bool
forall a. Eq a => a -> a -> Bool
==
                   (ConstInfo -> Constant
constId ConstInfo
ci2, ConstInfo -> Name
constName ConstInfo
ci2, ConstInfo -> Type
constType ConstInfo
ci2)

-- Creates an empty Signature.
emptySign :: SignTHF
emptySign :: SignTHF
emptySign = Sign :: TypeMap -> ConstMap -> SymbolMap -> SignTHF
Sign
    { types :: TypeMap
types = TypeMap
forall k a. Map k a
Map.empty
    , consts :: ConstMap
consts = ConstMap
forall k a. Map k a
Map.empty
    , symbols :: SymbolMap
symbols = SymbolMap
forall k a. Map k a
Map.empty }


{- -----------------------------------------------------------------------------
Some helper data structures and functions for the
union, difference and insersection methods
----------------------------------------------------------------------------- -}

type EitherMap c x = Map.Map c (Either x Diagnosis)

-- Convert a map into an EitherMap.
toEitherLeftMap :: Map.Map c x -> EitherMap c x
toEitherLeftMap :: Map c x -> EitherMap c x
toEitherLeftMap = (x -> Either x Diagnosis) -> Map c x -> EitherMap c x
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map x -> Either x Diagnosis
forall a b. a -> Either a b
Left

eitherMapHasDiagnosis :: EitherMap c x -> Bool
eitherMapHasDiagnosis :: EitherMap c x -> Bool
eitherMapHasDiagnosis = (Either x Diagnosis -> Bool -> Bool)
-> Bool -> EitherMap c x -> Bool
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (\ a :: Either x Diagnosis
a b :: Bool
b -> case Either x Diagnosis
a of
    Right _ -> Bool
True
    _ -> Bool
b ) Bool
False

-- only use after eitherMapHasDiagnosis returned true
eitherMapGetDiagnosis :: EitherMap c x -> [Diagnosis]
eitherMapGetDiagnosis :: EitherMap c x -> [Diagnosis]
eitherMapGetDiagnosis =
    (Either x Diagnosis -> [Diagnosis] -> [Diagnosis])
-> [Diagnosis] -> EitherMap c x -> [Diagnosis]
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (\ e :: Either x Diagnosis
e dl :: [Diagnosis]
dl -> (x -> [Diagnosis])
-> (Diagnosis -> [Diagnosis]) -> Either x Diagnosis -> [Diagnosis]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ([Diagnosis] -> x -> [Diagnosis]
forall a b. a -> b -> a
const [Diagnosis]
dl) (Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
dl) Either x Diagnosis
e) []

-- only use after eitherMapHasDiagnosis returned false
eitherMapGetMap :: EitherMap c x -> Map.Map c x
eitherMapGetMap :: EitherMap c x -> Map c x
eitherMapGetMap = (Either x Diagnosis -> x) -> EitherMap c x -> Map c x
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ (Left a :: x
a) -> x
a)

{- If the EitherMap contains diagnosis they will be returned in a list.
Otherwise the map will be converted back. -}
genRes :: EitherMap c x -> Either (Map.Map c x) [Diagnosis]
genRes :: EitherMap c x -> Either (Map c x) [Diagnosis]
genRes em :: EitherMap c x
em = if EitherMap c x -> Bool
forall c x. EitherMap c x -> Bool
eitherMapHasDiagnosis EitherMap c x
em
            then [Diagnosis] -> Either (Map c x) [Diagnosis]
forall a b. b -> Either a b
Right (EitherMap c x -> [Diagnosis]
forall c x. EitherMap c x -> [Diagnosis]
eitherMapGetDiagnosis EitherMap c x
em)
            else Map c x -> Either (Map c x) [Diagnosis]
forall a b. a -> Either a b
Left (EitherMap c x -> Map c x
forall c x. EitherMap c x -> Map c x
eitherMapGetMap EitherMap c x
em)


{- -----------------------------------------------------------------------------
Signature union
----------------------------------------------------------------------------- -}

-- Union of two signatures
sigUnion :: SignTHF -> SignTHF -> Result SignTHF
sigUnion :: SignTHF -> SignTHF -> Result SignTHF
sigUnion s1 :: SignTHF
s1 s2 :: SignTHF
s2 =
    let smu :: Either SymbolMap [Diagnosis]
smu = SymbolMap -> SymbolMap -> Either SymbolMap [Diagnosis]
symbolMapUnion (SignTHF -> SymbolMap
symbols SignTHF
s1) (SignTHF -> SymbolMap
symbols SignTHF
s2)
    in case Either SymbolMap [Diagnosis]
smu of
        Right d :: [Diagnosis]
d -> [Diagnosis] -> Maybe SignTHF -> Result SignTHF
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
d Maybe SignTHF
forall a. Maybe a
Nothing
        Left nsm :: SymbolMap
nsm ->
            let tmu :: Either TypeMap [Diagnosis]
tmu = TypeMap -> TypeMap -> Either TypeMap [Diagnosis]
typeMapUnion (SignTHF -> TypeMap
types SignTHF
s1) (SignTHF -> TypeMap
types SignTHF
s2)
                cmu :: Either ConstMap [Diagnosis]
cmu = ConstMap -> ConstMap -> Either ConstMap [Diagnosis]
constMapUnion (SignTHF -> ConstMap
consts SignTHF
s1) (SignTHF -> ConstMap
consts SignTHF
s2)
            in case Either TypeMap [Diagnosis]
tmu of
                Right d1 :: [Diagnosis]
d1 -> [Diagnosis] -> Maybe SignTHF -> Result SignTHF
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
d1 Maybe SignTHF
forall a. Maybe a
Nothing
                Left ntm :: TypeMap
ntm -> case Either ConstMap [Diagnosis]
cmu of
                    Right d2 :: [Diagnosis]
d2 -> [Diagnosis] -> Maybe SignTHF -> Result SignTHF
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
d2 Maybe SignTHF
forall a. Maybe a
Nothing
                    Left ncm :: ConstMap
ncm -> [Diagnosis] -> Maybe SignTHF -> Result SignTHF
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] (SignTHF -> Maybe SignTHF
forall a. a -> Maybe a
Just (SignTHF -> Maybe SignTHF) -> SignTHF -> Maybe SignTHF
forall a b. (a -> b) -> a -> b
$
                        SignTHF
s1 { types :: TypeMap
types = TypeMap
ntm, consts :: ConstMap
consts = ConstMap
ncm, symbols :: SymbolMap
symbols = SymbolMap
nsm })

typeMapUnion :: TypeMap -> TypeMap -> Either TypeMap [Diagnosis]
typeMapUnion :: TypeMap -> TypeMap -> Either TypeMap [Diagnosis]
typeMapUnion t1 :: TypeMap
t1 t2 :: TypeMap
t2 =
    let emt1 :: EitherMap Constant TypeInfo
emt1 = TypeMap -> EitherMap Constant TypeInfo
forall c x. Map c x -> EitherMap c x
toEitherLeftMap TypeMap
t1
        emt2 :: EitherMap Constant TypeInfo
emt2 = TypeMap -> EitherMap Constant TypeInfo
forall c x. Map c x -> EitherMap c x
toEitherLeftMap TypeMap
t2
    in EitherMap Constant TypeInfo -> Either TypeMap [Diagnosis]
forall c x. EitherMap c x -> Either (Map c x) [Diagnosis]
genRes (EitherMap Constant TypeInfo -> Either TypeMap [Diagnosis])
-> EitherMap Constant TypeInfo -> Either TypeMap [Diagnosis]
forall a b. (a -> b) -> a -> b
$ String
-> EitherMap Constant TypeInfo
-> EitherMap Constant TypeInfo
-> EitherMap Constant TypeInfo
forall c x.
(Ord c, Eq x, Show x) =>
String -> EitherMap c x -> EitherMap c x -> EitherMap c x
unite "Types" EitherMap Constant TypeInfo
emt1 EitherMap Constant TypeInfo
emt2

constMapUnion :: ConstMap -> ConstMap -> Either ConstMap [Diagnosis]
constMapUnion :: ConstMap -> ConstMap -> Either ConstMap [Diagnosis]
constMapUnion c1 :: ConstMap
c1 c2 :: ConstMap
c2 =
    let emc1 :: EitherMap Constant ConstInfo
emc1 = ConstMap -> EitherMap Constant ConstInfo
forall c x. Map c x -> EitherMap c x
toEitherLeftMap ConstMap
c1
        emc2 :: EitherMap Constant ConstInfo
emc2 = ConstMap -> EitherMap Constant ConstInfo
forall c x. Map c x -> EitherMap c x
toEitherLeftMap ConstMap
c2
    in EitherMap Constant ConstInfo -> Either ConstMap [Diagnosis]
forall c x. EitherMap c x -> Either (Map c x) [Diagnosis]
genRes (EitherMap Constant ConstInfo -> Either ConstMap [Diagnosis])
-> EitherMap Constant ConstInfo -> Either ConstMap [Diagnosis]
forall a b. (a -> b) -> a -> b
$ String
-> EitherMap Constant ConstInfo
-> EitherMap Constant ConstInfo
-> EitherMap Constant ConstInfo
forall c x.
(Ord c, Eq x, Show x) =>
String -> EitherMap c x -> EitherMap c x -> EitherMap c x
unite "Constants" EitherMap Constant ConstInfo
emc1 EitherMap Constant ConstInfo
emc2

symbolMapUnion :: SymbolMap -> SymbolMap -> Either SymbolMap [Diagnosis]
symbolMapUnion :: SymbolMap -> SymbolMap -> Either SymbolMap [Diagnosis]
symbolMapUnion s1 :: SymbolMap
s1 s2 :: SymbolMap
s2 =
    let ems1 :: EitherMap Constant SymbolTHF
ems1 = SymbolMap -> EitherMap Constant SymbolTHF
forall c x. Map c x -> EitherMap c x
toEitherLeftMap SymbolMap
s1
        ems2 :: EitherMap Constant SymbolTHF
ems2 = SymbolMap -> EitherMap Constant SymbolTHF
forall c x. Map c x -> EitherMap c x
toEitherLeftMap SymbolMap
s2
    in EitherMap Constant SymbolTHF -> Either SymbolMap [Diagnosis]
forall c x. EitherMap c x -> Either (Map c x) [Diagnosis]
genRes (EitherMap Constant SymbolTHF -> Either SymbolMap [Diagnosis])
-> EitherMap Constant SymbolTHF -> Either SymbolMap [Diagnosis]
forall a b. (a -> b) -> a -> b
$ String
-> EitherMap Constant SymbolTHF
-> EitherMap Constant SymbolTHF
-> EitherMap Constant SymbolTHF
forall c x.
(Ord c, Eq x, Show x) =>
String -> EitherMap c x -> EitherMap c x -> EitherMap c x
unite "Symbols" EitherMap Constant SymbolTHF
ems1 EitherMap Constant SymbolTHF
ems2

unite :: (Ord c, Eq x, Show x) => String -> EitherMap c x -> EitherMap c x
                                                          -> EitherMap c x
unite :: String -> EitherMap c x -> EitherMap c x -> EitherMap c x
unite s :: String
s = (Either x Diagnosis -> Either x Diagnosis -> Either x Diagnosis)
-> EitherMap c x -> EitherMap c x -> EitherMap c x
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith (\ (Left e1 :: x
e1) (Left e2 :: x
e2) -> if x
e1 x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== x
e2 then x -> Either x Diagnosis
forall a b. a -> Either a b
Left x
e1
            else Diagnosis -> Either x Diagnosis
forall a b. b -> Either a b
Right (DiagKind -> String -> () -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
                    (String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ x -> String
forall a. Show a => a -> String
show x
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ x -> String
forall a. Show a => a -> String
show x
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++
                    " have the same name but heve different definitions.") ()))


{- -----------------------------------------------------------------------------
Signature difference
----------------------------------------------------------------------------- -}

-- Difference of two signatures
sigDiff :: SignTHF -> SignTHF -> Result SignTHF
sigDiff :: SignTHF -> SignTHF -> Result SignTHF
sigDiff s1 :: SignTHF
s1 s2 :: SignTHF
s2 = [Diagnosis] -> Maybe SignTHF -> Result SignTHF
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] (SignTHF -> Maybe SignTHF
forall a. a -> Maybe a
Just (SignTHF -> Maybe SignTHF) -> SignTHF -> Maybe SignTHF
forall a b. (a -> b) -> a -> b
$
    SignTHF
s1 { types :: TypeMap
types = TypeMap -> TypeMap -> TypeMap
forall c x. (Ord c, Eq x) => Map c x -> Map c x -> Map c x
diff (SignTHF -> TypeMap
types SignTHF
s1) (SignTHF -> TypeMap
types SignTHF
s2)
       , consts :: ConstMap
consts = ConstMap -> ConstMap -> ConstMap
forall c x. (Ord c, Eq x) => Map c x -> Map c x -> Map c x
diff (SignTHF -> ConstMap
consts SignTHF
s1) (SignTHF -> ConstMap
consts SignTHF
s2)
       , symbols :: SymbolMap
symbols = SymbolMap -> SymbolMap -> SymbolMap
forall c x. (Ord c, Eq x) => Map c x -> Map c x -> Map c x
diff (SignTHF -> SymbolMap
symbols SignTHF
s1) (SignTHF -> SymbolMap
symbols SignTHF
s2) })

diff :: (Ord c, Eq x) => Map.Map c x -> Map.Map c x -> Map.Map c x
diff :: Map c x -> Map c x -> Map c x
diff = (x -> x -> Maybe x) -> Map c x -> Map c x -> Map c x
forall k a b.
Ord k =>
(a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWith (\ e1 :: x
e1 e2 :: x
e2 -> if x
e1 x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== x
e2 then Maybe x
forall a. Maybe a
Nothing else x -> Maybe x
forall a. a -> Maybe a
Just x
e1)

{- -----------------------------------------------------------------------------
Signature intersection
----------------------------------------------------------------------------- -}

-- Intersection of two signatures
sigIntersect :: SignTHF -> SignTHF -> Result SignTHF
sigIntersect :: SignTHF -> SignTHF -> Result SignTHF
sigIntersect s1 :: SignTHF
s1 s2 :: SignTHF
s2 =
    let smi :: Either SymbolMap [Diagnosis]
smi = SymbolMap -> SymbolMap -> Either SymbolMap [Diagnosis]
symbolMapIntersect (SignTHF -> SymbolMap
symbols SignTHF
s1) (SignTHF -> SymbolMap
symbols SignTHF
s2)
    in case Either SymbolMap [Diagnosis]
smi of
        Right d :: [Diagnosis]
d -> [Diagnosis] -> Maybe SignTHF -> Result SignTHF
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
d Maybe SignTHF
forall a. Maybe a
Nothing
        Left nsm :: SymbolMap
nsm ->
            let tmi :: Either TypeMap [Diagnosis]
tmi = TypeMap -> TypeMap -> Either TypeMap [Diagnosis]
typeMapIntersect (SignTHF -> TypeMap
types SignTHF
s1) (SignTHF -> TypeMap
types SignTHF
s2)
                cmi :: Either ConstMap [Diagnosis]
cmi = ConstMap -> ConstMap -> Either ConstMap [Diagnosis]
constMapIntersect (SignTHF -> ConstMap
consts SignTHF
s1) (SignTHF -> ConstMap
consts SignTHF
s2)
            in case Either TypeMap [Diagnosis]
tmi of
                Right d1 :: [Diagnosis]
d1 -> [Diagnosis] -> Maybe SignTHF -> Result SignTHF
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
d1 Maybe SignTHF
forall a. Maybe a
Nothing
                Left ntm :: TypeMap
ntm -> case Either ConstMap [Diagnosis]
cmi of
                    Right d2 :: [Diagnosis]
d2 -> [Diagnosis] -> Maybe SignTHF -> Result SignTHF
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
d2 Maybe SignTHF
forall a. Maybe a
Nothing
                    Left ncm :: ConstMap
ncm -> [Diagnosis] -> Maybe SignTHF -> Result SignTHF
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] (SignTHF -> Maybe SignTHF
forall a. a -> Maybe a
Just (SignTHF -> Maybe SignTHF) -> SignTHF -> Maybe SignTHF
forall a b. (a -> b) -> a -> b
$
                        SignTHF
s1 { types :: TypeMap
types = TypeMap
ntm, consts :: ConstMap
consts = ConstMap
ncm, symbols :: SymbolMap
symbols = SymbolMap
nsm })

typeMapIntersect :: TypeMap -> TypeMap -> Either TypeMap [Diagnosis]
typeMapIntersect :: TypeMap -> TypeMap -> Either TypeMap [Diagnosis]
typeMapIntersect t1 :: TypeMap
t1 t2 :: TypeMap
t2 =
    let emt1 :: EitherMap Constant TypeInfo
emt1 = TypeMap -> EitherMap Constant TypeInfo
forall c x. Map c x -> EitherMap c x
toEitherLeftMap TypeMap
t1
        emt2 :: EitherMap Constant TypeInfo
emt2 = TypeMap -> EitherMap Constant TypeInfo
forall c x. Map c x -> EitherMap c x
toEitherLeftMap TypeMap
t2
    in EitherMap Constant TypeInfo -> Either TypeMap [Diagnosis]
forall c x. EitherMap c x -> Either (Map c x) [Diagnosis]
genRes (EitherMap Constant TypeInfo -> Either TypeMap [Diagnosis])
-> EitherMap Constant TypeInfo -> Either TypeMap [Diagnosis]
forall a b. (a -> b) -> a -> b
$ String
-> EitherMap Constant TypeInfo
-> EitherMap Constant TypeInfo
-> EitherMap Constant TypeInfo
forall c x.
(Ord c, Eq x, Show x) =>
String -> EitherMap c x -> EitherMap c x -> EitherMap c x
intersect "Types" EitherMap Constant TypeInfo
emt1 EitherMap Constant TypeInfo
emt2

constMapIntersect :: ConstMap -> ConstMap -> Either ConstMap [Diagnosis]
constMapIntersect :: ConstMap -> ConstMap -> Either ConstMap [Diagnosis]
constMapIntersect c1 :: ConstMap
c1 c2 :: ConstMap
c2 =
    let emc1 :: EitherMap Constant ConstInfo
emc1 = ConstMap -> EitherMap Constant ConstInfo
forall c x. Map c x -> EitherMap c x
toEitherLeftMap ConstMap
c1
        emc2 :: EitherMap Constant ConstInfo
emc2 = ConstMap -> EitherMap Constant ConstInfo
forall c x. Map c x -> EitherMap c x
toEitherLeftMap ConstMap
c2
    in EitherMap Constant ConstInfo -> Either ConstMap [Diagnosis]
forall c x. EitherMap c x -> Either (Map c x) [Diagnosis]
genRes (EitherMap Constant ConstInfo -> Either ConstMap [Diagnosis])
-> EitherMap Constant ConstInfo -> Either ConstMap [Diagnosis]
forall a b. (a -> b) -> a -> b
$ String
-> EitherMap Constant ConstInfo
-> EitherMap Constant ConstInfo
-> EitherMap Constant ConstInfo
forall c x.
(Ord c, Eq x, Show x) =>
String -> EitherMap c x -> EitherMap c x -> EitherMap c x
intersect "Constants" EitherMap Constant ConstInfo
emc1 EitherMap Constant ConstInfo
emc2

symbolMapIntersect :: SymbolMap -> SymbolMap -> Either SymbolMap [Diagnosis]
symbolMapIntersect :: SymbolMap -> SymbolMap -> Either SymbolMap [Diagnosis]
symbolMapIntersect s1 :: SymbolMap
s1 s2 :: SymbolMap
s2 =
    let ems1 :: EitherMap Constant SymbolTHF
ems1 = SymbolMap -> EitherMap Constant SymbolTHF
forall c x. Map c x -> EitherMap c x
toEitherLeftMap SymbolMap
s1
        ems2 :: EitherMap Constant SymbolTHF
ems2 = SymbolMap -> EitherMap Constant SymbolTHF
forall c x. Map c x -> EitherMap c x
toEitherLeftMap SymbolMap
s2
    in EitherMap Constant SymbolTHF -> Either SymbolMap [Diagnosis]
forall c x. EitherMap c x -> Either (Map c x) [Diagnosis]
genRes (EitherMap Constant SymbolTHF -> Either SymbolMap [Diagnosis])
-> EitherMap Constant SymbolTHF -> Either SymbolMap [Diagnosis]
forall a b. (a -> b) -> a -> b
$ String
-> EitherMap Constant SymbolTHF
-> EitherMap Constant SymbolTHF
-> EitherMap Constant SymbolTHF
forall c x.
(Ord c, Eq x, Show x) =>
String -> EitherMap c x -> EitherMap c x -> EitherMap c x
intersect "Symbols" EitherMap Constant SymbolTHF
ems1 EitherMap Constant SymbolTHF
ems2

intersect :: (Ord c, Eq x, Show x) => String -> EitherMap c x -> EitherMap c x
                                                         -> EitherMap c x
intersect :: String -> EitherMap c x -> EitherMap c x -> EitherMap c x
intersect s :: String
s = (Either x Diagnosis -> Either x Diagnosis -> Either x Diagnosis)
-> EitherMap c x -> EitherMap c x -> EitherMap c x
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith (\ (Left e1 :: x
e1) (Left e2 :: x
e2) ->
                if x
e1 x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== x
e2 then x -> Either x Diagnosis
forall a b. a -> Either a b
Left x
e1 else Diagnosis -> Either x Diagnosis
forall a b. b -> Either a b
Right (DiagKind -> String -> () -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
                    (String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ x -> String
forall a. Show a => a -> String
show x
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ x -> String
forall a. Show a => a -> String
show x
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++
                    " have the same name but heve different definitions.") ()))