{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./HasCASL/Le.hs
Description :  the abstract syntax for analysis and final signature instance
Copyright   :  (c) Christian Maeder and Uni Bremen 2003-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

abstract syntax during static analysis
-}

module HasCASL.Le where

import HasCASL.As
import HasCASL.FoldType
import HasCASL.AsUtils

import qualified Common.Lib.State as State
import Common.Result
import Common.Id
import Common.AS_Annotation (Named)
import Common.GlobalAnnotations
import Common.Prec

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

-- * class info

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

-- | mapping class identifiers to their definition
type ClassMap = Map.Map Id ClassInfo

-- * type info

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

-- | an analysed alternative with a list of (product) types
data AltDefn =
    Construct (Maybe Id) [Type] Partiality [[Selector]]
    -- only argument types
    deriving (Int -> AltDefn -> ShowS
[AltDefn] -> ShowS
AltDefn -> String
(Int -> AltDefn -> ShowS)
-> (AltDefn -> String) -> ([AltDefn] -> ShowS) -> Show AltDefn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AltDefn] -> ShowS
$cshowList :: [AltDefn] -> ShowS
show :: AltDefn -> String
$cshow :: AltDefn -> String
showsPrec :: Int -> AltDefn -> ShowS
$cshowsPrec :: Int -> AltDefn -> ShowS
Show, AltDefn -> AltDefn -> Bool
(AltDefn -> AltDefn -> Bool)
-> (AltDefn -> AltDefn -> Bool) -> Eq AltDefn
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AltDefn -> AltDefn -> Bool
$c/= :: AltDefn -> AltDefn -> Bool
== :: AltDefn -> AltDefn -> Bool
$c== :: AltDefn -> AltDefn -> Bool
Eq, Eq AltDefn
Eq AltDefn =>
(AltDefn -> AltDefn -> Ordering)
-> (AltDefn -> AltDefn -> Bool)
-> (AltDefn -> AltDefn -> Bool)
-> (AltDefn -> AltDefn -> Bool)
-> (AltDefn -> AltDefn -> Bool)
-> (AltDefn -> AltDefn -> AltDefn)
-> (AltDefn -> AltDefn -> AltDefn)
-> Ord AltDefn
AltDefn -> AltDefn -> Bool
AltDefn -> AltDefn -> Ordering
AltDefn -> AltDefn -> AltDefn
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 :: AltDefn -> AltDefn -> AltDefn
$cmin :: AltDefn -> AltDefn -> AltDefn
max :: AltDefn -> AltDefn -> AltDefn
$cmax :: AltDefn -> AltDefn -> AltDefn
>= :: AltDefn -> AltDefn -> Bool
$c>= :: AltDefn -> AltDefn -> Bool
> :: AltDefn -> AltDefn -> Bool
$c> :: AltDefn -> AltDefn -> Bool
<= :: AltDefn -> AltDefn -> Bool
$c<= :: AltDefn -> AltDefn -> Bool
< :: AltDefn -> AltDefn -> Bool
$c< :: AltDefn -> AltDefn -> Bool
compare :: AltDefn -> AltDefn -> Ordering
$ccompare :: AltDefn -> AltDefn -> Ordering
$cp1Ord :: Eq AltDefn
Ord, Typeable, Typeable AltDefn
Constr
DataType
Typeable AltDefn =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> AltDefn -> c AltDefn)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c AltDefn)
-> (AltDefn -> Constr)
-> (AltDefn -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c AltDefn))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AltDefn))
-> ((forall b. Data b => b -> b) -> AltDefn -> AltDefn)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> AltDefn -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> AltDefn -> r)
-> (forall u. (forall d. Data d => d -> u) -> AltDefn -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> AltDefn -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> AltDefn -> m AltDefn)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> AltDefn -> m AltDefn)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> AltDefn -> m AltDefn)
-> Data AltDefn
AltDefn -> Constr
AltDefn -> DataType
(forall b. Data b => b -> b) -> AltDefn -> AltDefn
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AltDefn -> c AltDefn
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AltDefn
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) -> AltDefn -> u
forall u. (forall d. Data d => d -> u) -> AltDefn -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AltDefn -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AltDefn -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AltDefn -> m AltDefn
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AltDefn -> m AltDefn
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AltDefn
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AltDefn -> c AltDefn
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AltDefn)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AltDefn)
$cConstruct :: Constr
$tAltDefn :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> AltDefn -> m AltDefn
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AltDefn -> m AltDefn
gmapMp :: (forall d. Data d => d -> m d) -> AltDefn -> m AltDefn
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AltDefn -> m AltDefn
gmapM :: (forall d. Data d => d -> m d) -> AltDefn -> m AltDefn
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AltDefn -> m AltDefn
gmapQi :: Int -> (forall d. Data d => d -> u) -> AltDefn -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> AltDefn -> u
gmapQ :: (forall d. Data d => d -> u) -> AltDefn -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> AltDefn -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AltDefn -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AltDefn -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AltDefn -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AltDefn -> r
gmapT :: (forall b. Data b => b -> b) -> AltDefn -> AltDefn
$cgmapT :: (forall b. Data b => b -> b) -> AltDefn -> AltDefn
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AltDefn)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AltDefn)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c AltDefn)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AltDefn)
dataTypeOf :: AltDefn -> DataType
$cdataTypeOf :: AltDefn -> DataType
toConstr :: AltDefn -> Constr
$ctoConstr :: AltDefn -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AltDefn
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AltDefn
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AltDefn -> c AltDefn
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AltDefn -> c AltDefn
$cp1Data :: Typeable AltDefn
Data)

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

-- | a mapping of type (and disjoint class) identifiers
type IdMap = Map.Map Id Id

{- | data entries are produced from possibly mutual recursive data types. The
top-level identifiers of these types are never renamed but there renaming is
stored in the identifier map. This identifier map must never be empty (even
without renamings) because (the domain of) this map is used to store the
other (recursively dependent) top-level identifiers. -}
data DataEntry =
    DataEntry IdMap Id GenKind [TypeArg] RawKind (Set.Set AltDefn)
    deriving (Int -> DataEntry -> ShowS
[DataEntry] -> ShowS
DataEntry -> String
(Int -> DataEntry -> ShowS)
-> (DataEntry -> String)
-> ([DataEntry] -> ShowS)
-> Show DataEntry
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DataEntry] -> ShowS
$cshowList :: [DataEntry] -> ShowS
show :: DataEntry -> String
$cshow :: DataEntry -> String
showsPrec :: Int -> DataEntry -> ShowS
$cshowsPrec :: Int -> DataEntry -> ShowS
Show, DataEntry -> DataEntry -> Bool
(DataEntry -> DataEntry -> Bool)
-> (DataEntry -> DataEntry -> Bool) -> Eq DataEntry
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DataEntry -> DataEntry -> Bool
$c/= :: DataEntry -> DataEntry -> Bool
== :: DataEntry -> DataEntry -> Bool
$c== :: DataEntry -> DataEntry -> Bool
Eq, Eq DataEntry
Eq DataEntry =>
(DataEntry -> DataEntry -> Ordering)
-> (DataEntry -> DataEntry -> Bool)
-> (DataEntry -> DataEntry -> Bool)
-> (DataEntry -> DataEntry -> Bool)
-> (DataEntry -> DataEntry -> Bool)
-> (DataEntry -> DataEntry -> DataEntry)
-> (DataEntry -> DataEntry -> DataEntry)
-> Ord DataEntry
DataEntry -> DataEntry -> Bool
DataEntry -> DataEntry -> Ordering
DataEntry -> DataEntry -> DataEntry
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 :: DataEntry -> DataEntry -> DataEntry
$cmin :: DataEntry -> DataEntry -> DataEntry
max :: DataEntry -> DataEntry -> DataEntry
$cmax :: DataEntry -> DataEntry -> DataEntry
>= :: DataEntry -> DataEntry -> Bool
$c>= :: DataEntry -> DataEntry -> Bool
> :: DataEntry -> DataEntry -> Bool
$c> :: DataEntry -> DataEntry -> Bool
<= :: DataEntry -> DataEntry -> Bool
$c<= :: DataEntry -> DataEntry -> Bool
< :: DataEntry -> DataEntry -> Bool
$c< :: DataEntry -> DataEntry -> Bool
compare :: DataEntry -> DataEntry -> Ordering
$ccompare :: DataEntry -> DataEntry -> Ordering
$cp1Ord :: Eq DataEntry
Ord, Typeable, Typeable DataEntry
Constr
DataType
Typeable DataEntry =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> DataEntry -> c DataEntry)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DataEntry)
-> (DataEntry -> Constr)
-> (DataEntry -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DataEntry))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataEntry))
-> ((forall b. Data b => b -> b) -> DataEntry -> DataEntry)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DataEntry -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DataEntry -> r)
-> (forall u. (forall d. Data d => d -> u) -> DataEntry -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> DataEntry -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DataEntry -> m DataEntry)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DataEntry -> m DataEntry)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DataEntry -> m DataEntry)
-> Data DataEntry
DataEntry -> Constr
DataEntry -> DataType
(forall b. Data b => b -> b) -> DataEntry -> DataEntry
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataEntry -> c DataEntry
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataEntry
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) -> DataEntry -> u
forall u. (forall d. Data d => d -> u) -> DataEntry -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataEntry -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataEntry -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataEntry -> m DataEntry
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataEntry -> m DataEntry
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataEntry
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataEntry -> c DataEntry
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataEntry)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataEntry)
$cDataEntry :: Constr
$tDataEntry :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> DataEntry -> m DataEntry
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataEntry -> m DataEntry
gmapMp :: (forall d. Data d => d -> m d) -> DataEntry -> m DataEntry
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataEntry -> m DataEntry
gmapM :: (forall d. Data d => d -> m d) -> DataEntry -> m DataEntry
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataEntry -> m DataEntry
gmapQi :: Int -> (forall d. Data d => d -> u) -> DataEntry -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataEntry -> u
gmapQ :: (forall d. Data d => d -> u) -> DataEntry -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DataEntry -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataEntry -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataEntry -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataEntry -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataEntry -> r
gmapT :: (forall b. Data b => b -> b) -> DataEntry -> DataEntry
$cgmapT :: (forall b. Data b => b -> b) -> DataEntry -> DataEntry
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataEntry)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataEntry)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c DataEntry)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataEntry)
dataTypeOf :: DataEntry -> DataType
$cdataTypeOf :: DataEntry -> DataType
toConstr :: DataEntry -> Constr
$ctoConstr :: DataEntry -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataEntry
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataEntry
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataEntry -> c DataEntry
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataEntry -> c DataEntry
$cp1Data :: Typeable DataEntry
Data)

-- | possible definitions for type identifiers
data TypeDefn =
    NoTypeDefn
  | PreDatatype     -- auxiliary entry for DatatypeDefn
  | DatatypeDefn DataEntry
  | AliasTypeDefn Type
    deriving (Int -> TypeDefn -> ShowS
[TypeDefn] -> ShowS
TypeDefn -> String
(Int -> TypeDefn -> ShowS)
-> (TypeDefn -> String) -> ([TypeDefn] -> ShowS) -> Show TypeDefn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeDefn] -> ShowS
$cshowList :: [TypeDefn] -> ShowS
show :: TypeDefn -> String
$cshow :: TypeDefn -> String
showsPrec :: Int -> TypeDefn -> ShowS
$cshowsPrec :: Int -> TypeDefn -> ShowS
Show, TypeDefn -> TypeDefn -> Bool
(TypeDefn -> TypeDefn -> Bool)
-> (TypeDefn -> TypeDefn -> Bool) -> Eq TypeDefn
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeDefn -> TypeDefn -> Bool
$c/= :: TypeDefn -> TypeDefn -> Bool
== :: TypeDefn -> TypeDefn -> Bool
$c== :: TypeDefn -> TypeDefn -> Bool
Eq, Eq TypeDefn
Eq TypeDefn =>
(TypeDefn -> TypeDefn -> Ordering)
-> (TypeDefn -> TypeDefn -> Bool)
-> (TypeDefn -> TypeDefn -> Bool)
-> (TypeDefn -> TypeDefn -> Bool)
-> (TypeDefn -> TypeDefn -> Bool)
-> (TypeDefn -> TypeDefn -> TypeDefn)
-> (TypeDefn -> TypeDefn -> TypeDefn)
-> Ord TypeDefn
TypeDefn -> TypeDefn -> Bool
TypeDefn -> TypeDefn -> Ordering
TypeDefn -> TypeDefn -> TypeDefn
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 :: TypeDefn -> TypeDefn -> TypeDefn
$cmin :: TypeDefn -> TypeDefn -> TypeDefn
max :: TypeDefn -> TypeDefn -> TypeDefn
$cmax :: TypeDefn -> TypeDefn -> TypeDefn
>= :: TypeDefn -> TypeDefn -> Bool
$c>= :: TypeDefn -> TypeDefn -> Bool
> :: TypeDefn -> TypeDefn -> Bool
$c> :: TypeDefn -> TypeDefn -> Bool
<= :: TypeDefn -> TypeDefn -> Bool
$c<= :: TypeDefn -> TypeDefn -> Bool
< :: TypeDefn -> TypeDefn -> Bool
$c< :: TypeDefn -> TypeDefn -> Bool
compare :: TypeDefn -> TypeDefn -> Ordering
$ccompare :: TypeDefn -> TypeDefn -> Ordering
$cp1Ord :: Eq TypeDefn
Ord, Typeable, Typeable TypeDefn
Constr
DataType
Typeable TypeDefn =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TypeDefn -> c TypeDefn)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TypeDefn)
-> (TypeDefn -> Constr)
-> (TypeDefn -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TypeDefn))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeDefn))
-> ((forall b. Data b => b -> b) -> TypeDefn -> TypeDefn)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TypeDefn -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TypeDefn -> r)
-> (forall u. (forall d. Data d => d -> u) -> TypeDefn -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TypeDefn -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn)
-> Data TypeDefn
TypeDefn -> Constr
TypeDefn -> DataType
(forall b. Data b => b -> b) -> TypeDefn -> TypeDefn
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeDefn -> c TypeDefn
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypeDefn
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) -> TypeDefn -> u
forall u. (forall d. Data d => d -> u) -> TypeDefn -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeDefn -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeDefn -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypeDefn
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeDefn -> c TypeDefn
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TypeDefn)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeDefn)
$cAliasTypeDefn :: Constr
$cDatatypeDefn :: Constr
$cPreDatatype :: Constr
$cNoTypeDefn :: Constr
$tTypeDefn :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn
gmapMp :: (forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn
gmapM :: (forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn
gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeDefn -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TypeDefn -> u
gmapQ :: (forall d. Data d => d -> u) -> TypeDefn -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TypeDefn -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeDefn -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeDefn -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeDefn -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeDefn -> r
gmapT :: (forall b. Data b => b -> b) -> TypeDefn -> TypeDefn
$cgmapT :: (forall b. Data b => b -> b) -> TypeDefn -> TypeDefn
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeDefn)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeDefn)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TypeDefn)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TypeDefn)
dataTypeOf :: TypeDefn -> DataType
$cdataTypeOf :: TypeDefn -> DataType
toConstr :: TypeDefn -> Constr
$ctoConstr :: TypeDefn -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypeDefn
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypeDefn
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeDefn -> c TypeDefn
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeDefn -> c TypeDefn
$cp1Data :: Typeable TypeDefn
Data)

-- | for type identifiers also store the raw kind, instances and supertypes
data TypeInfo = TypeInfo
    { TypeInfo -> RawKind
typeKind :: RawKind
    , TypeInfo -> Set Kind
otherTypeKinds :: Set.Set Kind
    , TypeInfo -> Set Id
superTypes :: Set.Set Id -- only declared or direct supertypes?
    , TypeInfo -> TypeDefn
typeDefn :: TypeDefn
    } 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)

instance Eq TypeInfo where
    a :: TypeInfo
a == :: TypeInfo -> TypeInfo -> Bool
== b :: TypeInfo
b = TypeInfo -> TypeInfo -> Ordering
forall a. Ord a => a -> a -> Ordering
compare TypeInfo
a TypeInfo
b Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance Ord TypeInfo where
   compare :: TypeInfo -> TypeInfo -> Ordering
compare t1 :: TypeInfo
t1 t2 :: TypeInfo
t2 = (RawKind, Set Kind, Set Id)
-> (RawKind, Set Kind, Set Id) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare
     (TypeInfo -> RawKind
typeKind TypeInfo
t1, TypeInfo -> Set Kind
otherTypeKinds TypeInfo
t1, TypeInfo -> Set Id
superTypes TypeInfo
t1)
     (TypeInfo -> RawKind
typeKind TypeInfo
t2, TypeInfo -> Set Kind
otherTypeKinds TypeInfo
t2, TypeInfo -> Set Id
superTypes TypeInfo
t2)

-- | mapping type identifiers to their definition
type TypeMap = Map.Map Id TypeInfo

-- | the minimal information for a sort
starTypeInfo :: TypeInfo
starTypeInfo :: TypeInfo
starTypeInfo = RawKind -> Set Kind -> Set Id -> TypeDefn -> TypeInfo
TypeInfo RawKind
rStar (Kind -> Set Kind
forall a. a -> Set a
Set.singleton Kind
universe) Set Id
forall a. Set a
Set.empty TypeDefn
NoTypeDefn

-- | rename the type according to identifier map (for comorphisms)
mapType :: IdMap -> Type -> Type
mapType :: IdMap -> Type -> Type
mapType m :: IdMap
m = if IdMap -> Bool
forall k a. Map k a -> Bool
Map.null IdMap
m then Type -> Type
forall a. a -> a
id else
    FoldTypeRec Type -> Type -> Type
forall a. FoldTypeRec a -> Type -> a
foldType FoldTypeRec Type
mapTypeRec
    { foldTypeName :: Type -> Id -> RawKind -> Int -> Type
foldTypeName = \ t :: Type
t i :: Id
i k :: RawKind
k n :: Int
n -> if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= 0 then Type
t else
        case Id -> IdMap -> Maybe Id
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i IdMap
m of
          Just j :: Id
j -> Id -> RawKind -> Int -> Type
TypeName Id
j RawKind
k 0
          Nothing -> Type
t }

-- * sentences

-- | data types are also special sentences because of their properties
data Sentence =
    Formula Term
  | DatatypeSen [DataEntry]
  | ProgEqSen Id TypeScheme ProgEq
    deriving (Int -> Sentence -> ShowS
[Sentence] -> ShowS
Sentence -> String
(Int -> Sentence -> ShowS)
-> (Sentence -> String) -> ([Sentence] -> ShowS) -> Show Sentence
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sentence] -> ShowS
$cshowList :: [Sentence] -> ShowS
show :: Sentence -> String
$cshow :: Sentence -> String
showsPrec :: Int -> Sentence -> ShowS
$cshowsPrec :: Int -> Sentence -> ShowS
Show, Sentence -> Sentence -> Bool
(Sentence -> Sentence -> Bool)
-> (Sentence -> Sentence -> Bool) -> Eq Sentence
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sentence -> Sentence -> Bool
$c/= :: Sentence -> Sentence -> Bool
== :: Sentence -> Sentence -> Bool
$c== :: Sentence -> Sentence -> Bool
Eq, Eq Sentence
Eq Sentence =>
(Sentence -> Sentence -> Ordering)
-> (Sentence -> Sentence -> Bool)
-> (Sentence -> Sentence -> Bool)
-> (Sentence -> Sentence -> Bool)
-> (Sentence -> Sentence -> Bool)
-> (Sentence -> Sentence -> Sentence)
-> (Sentence -> Sentence -> Sentence)
-> Ord Sentence
Sentence -> Sentence -> Bool
Sentence -> Sentence -> Ordering
Sentence -> Sentence -> Sentence
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 :: Sentence -> Sentence -> Sentence
$cmin :: Sentence -> Sentence -> Sentence
max :: Sentence -> Sentence -> Sentence
$cmax :: Sentence -> Sentence -> Sentence
>= :: Sentence -> Sentence -> Bool
$c>= :: Sentence -> Sentence -> Bool
> :: Sentence -> Sentence -> Bool
$c> :: Sentence -> Sentence -> Bool
<= :: Sentence -> Sentence -> Bool
$c<= :: Sentence -> Sentence -> Bool
< :: Sentence -> Sentence -> Bool
$c< :: Sentence -> Sentence -> Bool
compare :: Sentence -> Sentence -> Ordering
$ccompare :: Sentence -> Sentence -> Ordering
$cp1Ord :: Eq Sentence
Ord, Typeable, Typeable Sentence
Constr
DataType
Typeable Sentence =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Sentence -> c Sentence)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Sentence)
-> (Sentence -> Constr)
-> (Sentence -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Sentence))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sentence))
-> ((forall b. Data b => b -> b) -> Sentence -> Sentence)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Sentence -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Sentence -> r)
-> (forall u. (forall d. Data d => d -> u) -> Sentence -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Sentence -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Sentence -> m Sentence)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sentence -> m Sentence)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sentence -> m Sentence)
-> Data Sentence
Sentence -> Constr
Sentence -> DataType
(forall b. Data b => b -> b) -> Sentence -> Sentence
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sentence -> c Sentence
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sentence
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) -> Sentence -> u
forall u. (forall d. Data d => d -> u) -> Sentence -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sentence -> m Sentence
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sentence -> m Sentence
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sentence
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sentence -> c Sentence
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sentence)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sentence)
$cProgEqSen :: Constr
$cDatatypeSen :: Constr
$cFormula :: Constr
$tSentence :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Sentence -> m Sentence
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sentence -> m Sentence
gmapMp :: (forall d. Data d => d -> m d) -> Sentence -> m Sentence
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sentence -> m Sentence
gmapM :: (forall d. Data d => d -> m d) -> Sentence -> m Sentence
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sentence -> m Sentence
gmapQi :: Int -> (forall d. Data d => d -> u) -> Sentence -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sentence -> u
gmapQ :: (forall d. Data d => d -> u) -> Sentence -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Sentence -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
gmapT :: (forall b. Data b => b -> b) -> Sentence -> Sentence
$cgmapT :: (forall b. Data b => b -> b) -> Sentence -> Sentence
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sentence)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sentence)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Sentence)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sentence)
dataTypeOf :: Sentence -> DataType
$cdataTypeOf :: Sentence -> DataType
toConstr :: Sentence -> Constr
$ctoConstr :: Sentence -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sentence
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sentence
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sentence -> c Sentence
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sentence -> c Sentence
$cp1Data :: Typeable Sentence
Data)

instance GetRange Sentence where
  getRange :: Sentence -> Range
getRange s :: Sentence
s = case Sentence
s of
    Formula t :: Term
t -> Term -> Range
forall a. GetRange a => a -> Range
getRange Term
t
    _ -> Range
nullRange

-- * variables

-- | type variable are kept separately
data TypeVarDefn = TypeVarDefn Variance VarKind RawKind Int
  deriving (Int -> TypeVarDefn -> ShowS
[TypeVarDefn] -> ShowS
TypeVarDefn -> String
(Int -> TypeVarDefn -> ShowS)
-> (TypeVarDefn -> String)
-> ([TypeVarDefn] -> ShowS)
-> Show TypeVarDefn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeVarDefn] -> ShowS
$cshowList :: [TypeVarDefn] -> ShowS
show :: TypeVarDefn -> String
$cshow :: TypeVarDefn -> String
showsPrec :: Int -> TypeVarDefn -> ShowS
$cshowsPrec :: Int -> TypeVarDefn -> ShowS
Show, Typeable, Typeable TypeVarDefn
Constr
DataType
Typeable TypeVarDefn =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TypeVarDefn -> c TypeVarDefn)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TypeVarDefn)
-> (TypeVarDefn -> Constr)
-> (TypeVarDefn -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TypeVarDefn))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c TypeVarDefn))
-> ((forall b. Data b => b -> b) -> TypeVarDefn -> TypeVarDefn)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TypeVarDefn -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TypeVarDefn -> r)
-> (forall u. (forall d. Data d => d -> u) -> TypeVarDefn -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> TypeVarDefn -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn)
-> Data TypeVarDefn
TypeVarDefn -> Constr
TypeVarDefn -> DataType
(forall b. Data b => b -> b) -> TypeVarDefn -> TypeVarDefn
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeVarDefn -> c TypeVarDefn
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypeVarDefn
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) -> TypeVarDefn -> u
forall u. (forall d. Data d => d -> u) -> TypeVarDefn -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeVarDefn -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeVarDefn -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypeVarDefn
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeVarDefn -> c TypeVarDefn
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TypeVarDefn)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TypeVarDefn)
$cTypeVarDefn :: Constr
$tTypeVarDefn :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn
gmapMp :: (forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn
gmapM :: (forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn
gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeVarDefn -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TypeVarDefn -> u
gmapQ :: (forall d. Data d => d -> u) -> TypeVarDefn -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TypeVarDefn -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeVarDefn -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeVarDefn -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeVarDefn -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeVarDefn -> r
gmapT :: (forall b. Data b => b -> b) -> TypeVarDefn -> TypeVarDefn
$cgmapT :: (forall b. Data b => b -> b) -> TypeVarDefn -> TypeVarDefn
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TypeVarDefn)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TypeVarDefn)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TypeVarDefn)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TypeVarDefn)
dataTypeOf :: TypeVarDefn -> DataType
$cdataTypeOf :: TypeVarDefn -> DataType
toConstr :: TypeVarDefn -> Constr
$ctoConstr :: TypeVarDefn -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypeVarDefn
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypeVarDefn
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeVarDefn -> c TypeVarDefn
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeVarDefn -> c TypeVarDefn
$cp1Data :: Typeable TypeVarDefn
Data)

-- | mapping type variables to their definition
type LocalTypeVars = Map.Map Id TypeVarDefn

-- | the type of a local variable
data VarDefn = VarDefn Type deriving (Int -> VarDefn -> ShowS
[VarDefn] -> ShowS
VarDefn -> String
(Int -> VarDefn -> ShowS)
-> (VarDefn -> String) -> ([VarDefn] -> ShowS) -> Show VarDefn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VarDefn] -> ShowS
$cshowList :: [VarDefn] -> ShowS
show :: VarDefn -> String
$cshow :: VarDefn -> String
showsPrec :: Int -> VarDefn -> ShowS
$cshowsPrec :: Int -> VarDefn -> ShowS
Show, Typeable, Typeable VarDefn
Constr
DataType
Typeable VarDefn =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> VarDefn -> c VarDefn)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c VarDefn)
-> (VarDefn -> Constr)
-> (VarDefn -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c VarDefn))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarDefn))
-> ((forall b. Data b => b -> b) -> VarDefn -> VarDefn)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> VarDefn -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> VarDefn -> r)
-> (forall u. (forall d. Data d => d -> u) -> VarDefn -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> VarDefn -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> VarDefn -> m VarDefn)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> VarDefn -> m VarDefn)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> VarDefn -> m VarDefn)
-> Data VarDefn
VarDefn -> Constr
VarDefn -> DataType
(forall b. Data b => b -> b) -> VarDefn -> VarDefn
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VarDefn -> c VarDefn
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c VarDefn
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) -> VarDefn -> u
forall u. (forall d. Data d => d -> u) -> VarDefn -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VarDefn -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VarDefn -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> VarDefn -> m VarDefn
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> VarDefn -> m VarDefn
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c VarDefn
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VarDefn -> c VarDefn
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c VarDefn)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarDefn)
$cVarDefn :: Constr
$tVarDefn :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> VarDefn -> m VarDefn
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> VarDefn -> m VarDefn
gmapMp :: (forall d. Data d => d -> m d) -> VarDefn -> m VarDefn
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> VarDefn -> m VarDefn
gmapM :: (forall d. Data d => d -> m d) -> VarDefn -> m VarDefn
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> VarDefn -> m VarDefn
gmapQi :: Int -> (forall d. Data d => d -> u) -> VarDefn -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> VarDefn -> u
gmapQ :: (forall d. Data d => d -> u) -> VarDefn -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> VarDefn -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VarDefn -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VarDefn -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VarDefn -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VarDefn -> r
gmapT :: (forall b. Data b => b -> b) -> VarDefn -> VarDefn
$cgmapT :: (forall b. Data b => b -> b) -> VarDefn -> VarDefn
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarDefn)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarDefn)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c VarDefn)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c VarDefn)
dataTypeOf :: VarDefn -> DataType
$cdataTypeOf :: VarDefn -> DataType
toConstr :: VarDefn -> Constr
$ctoConstr :: VarDefn -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c VarDefn
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c VarDefn
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VarDefn -> c VarDefn
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VarDefn -> c VarDefn
$cp1Data :: Typeable VarDefn
Data)

-- * assumptions

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

-- | possible definitions of functions
data OpDefn =
    NoOpDefn OpBrand
  | ConstructData Id     -- ^ target type
  | SelectData (Set.Set ConstrInfo) Id   -- ^ constructors of source type
  | Definition OpBrand Term
    deriving (Int -> OpDefn -> ShowS
[OpDefn] -> ShowS
OpDefn -> String
(Int -> OpDefn -> ShowS)
-> (OpDefn -> String) -> ([OpDefn] -> ShowS) -> Show OpDefn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OpDefn] -> ShowS
$cshowList :: [OpDefn] -> ShowS
show :: OpDefn -> String
$cshow :: OpDefn -> String
showsPrec :: Int -> OpDefn -> ShowS
$cshowsPrec :: Int -> OpDefn -> ShowS
Show, OpDefn -> OpDefn -> Bool
(OpDefn -> OpDefn -> Bool)
-> (OpDefn -> OpDefn -> Bool) -> Eq OpDefn
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OpDefn -> OpDefn -> Bool
$c/= :: OpDefn -> OpDefn -> Bool
== :: OpDefn -> OpDefn -> Bool
$c== :: OpDefn -> OpDefn -> Bool
Eq, Eq OpDefn
Eq OpDefn =>
(OpDefn -> OpDefn -> Ordering)
-> (OpDefn -> OpDefn -> Bool)
-> (OpDefn -> OpDefn -> Bool)
-> (OpDefn -> OpDefn -> Bool)
-> (OpDefn -> OpDefn -> Bool)
-> (OpDefn -> OpDefn -> OpDefn)
-> (OpDefn -> OpDefn -> OpDefn)
-> Ord OpDefn
OpDefn -> OpDefn -> Bool
OpDefn -> OpDefn -> Ordering
OpDefn -> OpDefn -> OpDefn
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 :: OpDefn -> OpDefn -> OpDefn
$cmin :: OpDefn -> OpDefn -> OpDefn
max :: OpDefn -> OpDefn -> OpDefn
$cmax :: OpDefn -> OpDefn -> OpDefn
>= :: OpDefn -> OpDefn -> Bool
$c>= :: OpDefn -> OpDefn -> Bool
> :: OpDefn -> OpDefn -> Bool
$c> :: OpDefn -> OpDefn -> Bool
<= :: OpDefn -> OpDefn -> Bool
$c<= :: OpDefn -> OpDefn -> Bool
< :: OpDefn -> OpDefn -> Bool
$c< :: OpDefn -> OpDefn -> Bool
compare :: OpDefn -> OpDefn -> Ordering
$ccompare :: OpDefn -> OpDefn -> Ordering
$cp1Ord :: Eq OpDefn
Ord, Typeable, Typeable OpDefn
Constr
DataType
Typeable OpDefn =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> OpDefn -> c OpDefn)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c OpDefn)
-> (OpDefn -> Constr)
-> (OpDefn -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c OpDefn))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpDefn))
-> ((forall b. Data b => b -> b) -> OpDefn -> OpDefn)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> OpDefn -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> OpDefn -> r)
-> (forall u. (forall d. Data d => d -> u) -> OpDefn -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> OpDefn -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> OpDefn -> m OpDefn)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OpDefn -> m OpDefn)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OpDefn -> m OpDefn)
-> Data OpDefn
OpDefn -> Constr
OpDefn -> DataType
(forall b. Data b => b -> b) -> OpDefn -> OpDefn
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OpDefn -> c OpDefn
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OpDefn
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) -> OpDefn -> u
forall u. (forall d. Data d => d -> u) -> OpDefn -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpDefn -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpDefn -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OpDefn -> m OpDefn
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OpDefn -> m OpDefn
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OpDefn
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OpDefn -> c OpDefn
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OpDefn)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpDefn)
$cDefinition :: Constr
$cSelectData :: Constr
$cConstructData :: Constr
$cNoOpDefn :: Constr
$tOpDefn :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> OpDefn -> m OpDefn
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OpDefn -> m OpDefn
gmapMp :: (forall d. Data d => d -> m d) -> OpDefn -> m OpDefn
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OpDefn -> m OpDefn
gmapM :: (forall d. Data d => d -> m d) -> OpDefn -> m OpDefn
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OpDefn -> m OpDefn
gmapQi :: Int -> (forall d. Data d => d -> u) -> OpDefn -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> OpDefn -> u
gmapQ :: (forall d. Data d => d -> u) -> OpDefn -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> OpDefn -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpDefn -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpDefn -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpDefn -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpDefn -> r
gmapT :: (forall b. Data b => b -> b) -> OpDefn -> OpDefn
$cgmapT :: (forall b. Data b => b -> b) -> OpDefn -> OpDefn
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpDefn)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpDefn)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c OpDefn)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OpDefn)
dataTypeOf :: OpDefn -> DataType
$cdataTypeOf :: OpDefn -> DataType
toConstr :: OpDefn -> Constr
$ctoConstr :: OpDefn -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OpDefn
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OpDefn
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OpDefn -> c OpDefn
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OpDefn -> c OpDefn
$cp1Data :: Typeable OpDefn
Data)

-- | scheme, attributes and definition for function identifiers
data OpInfo = OpInfo
    { OpInfo -> TypeScheme
opType :: TypeScheme
    , OpInfo -> Set OpAttr
opAttrs :: Set.Set OpAttr
    , OpInfo -> OpDefn
opDefn :: OpDefn
    } deriving (Int -> OpInfo -> ShowS
[OpInfo] -> ShowS
OpInfo -> String
(Int -> OpInfo -> ShowS)
-> (OpInfo -> String) -> ([OpInfo] -> ShowS) -> Show OpInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OpInfo] -> ShowS
$cshowList :: [OpInfo] -> ShowS
show :: OpInfo -> String
$cshow :: OpInfo -> String
showsPrec :: Int -> OpInfo -> ShowS
$cshowsPrec :: Int -> OpInfo -> ShowS
Show, Typeable, Typeable OpInfo
Constr
DataType
Typeable OpInfo =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> OpInfo -> c OpInfo)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c OpInfo)
-> (OpInfo -> Constr)
-> (OpInfo -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c OpInfo))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpInfo))
-> ((forall b. Data b => b -> b) -> OpInfo -> OpInfo)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> OpInfo -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> OpInfo -> r)
-> (forall u. (forall d. Data d => d -> u) -> OpInfo -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> OpInfo -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo)
-> Data OpInfo
OpInfo -> Constr
OpInfo -> DataType
(forall b. Data b => b -> b) -> OpInfo -> OpInfo
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OpInfo -> c OpInfo
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OpInfo
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) -> OpInfo -> u
forall u. (forall d. Data d => d -> u) -> OpInfo -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpInfo -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpInfo -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OpInfo -> m OpInfo
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OpInfo -> m OpInfo
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OpInfo
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OpInfo -> c OpInfo
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OpInfo)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpInfo)
$cOpInfo :: Constr
$tOpInfo :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OpInfo -> m OpInfo
gmapMp :: (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OpInfo -> m OpInfo
gmapM :: (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OpInfo -> m OpInfo
gmapQi :: Int -> (forall d. Data d => d -> u) -> OpInfo -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> OpInfo -> u
gmapQ :: (forall d. Data d => d -> u) -> OpInfo -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> OpInfo -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpInfo -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpInfo -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpInfo -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpInfo -> r
gmapT :: (forall b. Data b => b -> b) -> OpInfo -> OpInfo
$cgmapT :: (forall b. Data b => b -> b) -> OpInfo -> OpInfo
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpInfo)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c OpInfo)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OpInfo)
dataTypeOf :: OpInfo -> DataType
$cdataTypeOf :: OpInfo -> DataType
toConstr :: OpInfo -> Constr
$ctoConstr :: OpInfo -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OpInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OpInfo
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OpInfo -> c OpInfo
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OpInfo -> c OpInfo
$cp1Data :: Typeable OpInfo
Data)

instance Eq OpInfo where
    o1 :: OpInfo
o1 == :: OpInfo -> OpInfo -> Bool
== o2 :: OpInfo
o2 = OpInfo -> OpInfo -> Ordering
forall a. Ord a => a -> a -> Ordering
compare OpInfo
o1 OpInfo
o2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance Ord OpInfo where
    compare :: OpInfo -> OpInfo -> Ordering
compare = (OpInfo -> TypeScheme) -> OpInfo -> OpInfo -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing OpInfo -> TypeScheme
opType

-- | test for constructor
isConstructor :: OpInfo -> Bool
isConstructor :: OpInfo -> Bool
isConstructor o :: OpInfo
o = case OpInfo -> OpDefn
opDefn OpInfo
o of
    ConstructData _ -> Bool
True
    _ -> Bool
False

-- | mapping operation identifiers to their definition
type Assumps = Map.Map Id (Set.Set OpInfo)

-- * the local environment and final signature

-- | the signature is established by the classes, types and assumptions
data Env = Env
    { Env -> ClassMap
classMap :: ClassMap
    , Env -> TypeMap
typeMap :: TypeMap
    , Env -> LocalTypeVars
localTypeVars :: LocalTypeVars
    , Env -> Assumps
assumps :: Assumps
    , Env -> IdMap
binders :: Map.Map Id Id -- binder with associated op-id
    , Env -> Map Id VarDefn
localVars :: Map.Map Id VarDefn
    , Env -> [Named Sentence]
sentences :: [Named Sentence]
    , Env -> Set Symbol
declSymbs :: Set.Set Symbol
    , Env -> [Diagnosis]
envDiags :: [Diagnosis]
    , Env -> (PrecMap, Set Id)
preIds :: (PrecMap, Set.Set Id)
    , Env -> GlobalAnnos
globAnnos :: GlobalAnnos
    , Env -> Int
counter :: Int
    } deriving (Int -> Env -> ShowS
[Env] -> ShowS
Env -> String
(Int -> Env -> ShowS)
-> (Env -> String) -> ([Env] -> ShowS) -> Show Env
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Env] -> ShowS
$cshowList :: [Env] -> ShowS
show :: Env -> String
$cshow :: Env -> String
showsPrec :: Int -> Env -> ShowS
$cshowsPrec :: Int -> Env -> ShowS
Show, Typeable, Typeable Env
Constr
DataType
Typeable Env =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Env -> c Env)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Env)
-> (Env -> Constr)
-> (Env -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Env))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Env))
-> ((forall b. Data b => b -> b) -> Env -> Env)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Env -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Env -> r)
-> (forall u. (forall d. Data d => d -> u) -> Env -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Env -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Env -> m Env)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Env -> m Env)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Env -> m Env)
-> Data Env
Env -> Constr
Env -> DataType
(forall b. Data b => b -> b) -> Env -> Env
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Env -> c Env
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Env
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) -> Env -> u
forall u. (forall d. Data d => d -> u) -> Env -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Env -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Env -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Env -> m Env
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Env -> m Env
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Env
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Env -> c Env
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Env)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Env)
$cEnv :: Constr
$tEnv :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Env -> m Env
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Env -> m Env
gmapMp :: (forall d. Data d => d -> m d) -> Env -> m Env
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Env -> m Env
gmapM :: (forall d. Data d => d -> m d) -> Env -> m Env
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Env -> m Env
gmapQi :: Int -> (forall d. Data d => d -> u) -> Env -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Env -> u
gmapQ :: (forall d. Data d => d -> u) -> Env -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Env -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Env -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Env -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Env -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Env -> r
gmapT :: (forall b. Data b => b -> b) -> Env -> Env
$cgmapT :: (forall b. Data b => b -> b) -> Env -> Env
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Env)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Env)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Env)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Env)
dataTypeOf :: Env -> DataType
$cdataTypeOf :: Env -> DataType
toConstr :: Env -> Constr
$ctoConstr :: Env -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Env
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Env
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Env -> c Env
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Env -> c Env
$cp1Data :: Typeable Env
Data)

instance Eq Env where
    a :: Env
a == :: Env -> Env -> Bool
== b :: Env
b = Env -> Env -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Env
a Env
b Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance Ord Env where
  compare :: Env -> Env -> Ordering
compare e1 :: Env
e1 e2 :: Env
e2 = (ClassMap, TypeMap, Assumps)
-> (ClassMap, TypeMap, Assumps) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare
    (Env -> ClassMap
classMap Env
e1, Env -> TypeMap
typeMap Env
e1, Env -> Assumps
assumps Env
e1)
    (Env -> ClassMap
classMap Env
e2, Env -> TypeMap
typeMap Env
e2, Env -> Assumps
assumps Env
e2)

-- | the empty environment (fresh variables start with 1)
initialEnv :: Env
initialEnv :: Env
initialEnv = Env :: ClassMap
-> TypeMap
-> LocalTypeVars
-> Assumps
-> IdMap
-> Map Id VarDefn
-> [Named Sentence]
-> Set Symbol
-> [Diagnosis]
-> (PrecMap, Set Id)
-> GlobalAnnos
-> Int
-> Env
Env
    { classMap :: ClassMap
classMap = ClassMap
forall k a. Map k a
Map.empty
    , typeMap :: TypeMap
typeMap = TypeMap
forall k a. Map k a
Map.empty
    , localTypeVars :: LocalTypeVars
localTypeVars = LocalTypeVars
forall k a. Map k a
Map.empty
    , assumps :: Assumps
assumps = Assumps
forall k a. Map k a
Map.empty
    , binders :: IdMap
binders = IdMap
forall k a. Map k a
Map.empty
    , localVars :: Map Id VarDefn
localVars = Map Id VarDefn
forall k a. Map k a
Map.empty
    , sentences :: [Named Sentence]
sentences = []
    , declSymbs :: Set Symbol
declSymbs = Set Symbol
forall a. Set a
Set.empty
    , envDiags :: [Diagnosis]
envDiags = []
    , preIds :: (PrecMap, Set Id)
preIds = (PrecMap
emptyPrecMap, Set Id
forall a. Set a
Set.empty)
    , globAnnos :: GlobalAnnos
globAnnos = GlobalAnnos
emptyGlobalAnnos
    , counter :: Int
counter = 1 }

{- utils for singleton sets that could also be part of "Data.Set". These
functions rely on 'Data.Set.size' being computable in constant time and
would need to be rewritten for set implementations with a size
function that is only linear. -}

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

-- * accessing the environment

-- | add diagnostic messages
addDiags :: [Diagnosis] -> State.State Env ()
addDiags :: [Diagnosis] -> State Env ()
addDiags ds :: [Diagnosis]
ds = do
    Env
e <- State Env Env
forall s. State s s
State.get
    Env -> State Env ()
forall s. s -> State s ()
State.put (Env -> State Env ()) -> Env -> State Env ()
forall a b. (a -> b) -> a -> b
$ Env
e {envDiags :: [Diagnosis]
envDiags = [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a]
reverse [Diagnosis]
ds [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ Env -> [Diagnosis]
envDiags Env
e}

-- | add sentences
appendSentences :: [Named Sentence] -> State.State Env ()
appendSentences :: [Named Sentence] -> State Env ()
appendSentences fs :: [Named Sentence]
fs = do
    Env
e <- State Env Env
forall s. State s s
State.get
    Env -> State Env ()
forall s. s -> State s ()
State.put (Env -> State Env ()) -> Env -> State Env ()
forall a b. (a -> b) -> a -> b
$ Env
e {sentences :: [Named Sentence]
sentences = [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a]
reverse [Named Sentence]
fs [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ Env -> [Named Sentence]
sentences Env
e}

-- | store a class map
putClassMap :: ClassMap -> State.State Env ()
putClassMap :: ClassMap -> State Env ()
putClassMap ce :: ClassMap
ce = do
    Env
e <- State Env Env
forall s. State s s
State.get
    Env -> State Env ()
forall s. s -> State s ()
State.put Env
e { classMap :: ClassMap
classMap = ClassMap
ce }

-- | store local assumptions
putLocalVars :: Map.Map Id VarDefn -> State.State Env ()
putLocalVars :: Map Id VarDefn -> State Env ()
putLocalVars vs :: Map Id VarDefn
vs = do
    Env
e <- State Env Env
forall s. State s s
State.get
    Env -> State Env ()
forall s. s -> State s ()
State.put Env
e { localVars :: Map Id VarDefn
localVars = Map Id VarDefn
vs }

-- | converting a result to a state computation
fromResult :: (Env -> Result a) -> State.State Env (Maybe a)
fromResult :: (Env -> Result a) -> State Env (Maybe a)
fromResult f :: Env -> Result a
f = do
   Env
e <- State Env Env
forall s. State s s
State.get
   let Result ds :: [Diagnosis]
ds mr :: Maybe a
mr = Env -> Result a
f Env
e
   [Diagnosis] -> State Env ()
addDiags [Diagnosis]
ds
   Maybe a -> State Env (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
mr

-- | add the symbol to the state
addSymbol :: Symbol -> State.State Env ()
addSymbol :: Symbol -> State Env ()
addSymbol sy :: Symbol
sy = do
    Env
e <- State Env Env
forall s. State s s
State.get
    Env -> State Env ()
forall s. s -> State s ()
State.put Env
e { declSymbs :: Set Symbol
declSymbs = Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => a -> Set a -> Set a
Set.insert Symbol
sy (Set Symbol -> Set Symbol) -> Set Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Env -> Set Symbol
declSymbs Env
e }

-- | store local type variables
putLocalTypeVars :: LocalTypeVars -> State.State Env ()
putLocalTypeVars :: LocalTypeVars -> State Env ()
putLocalTypeVars tvs :: LocalTypeVars
tvs = do
    Env
e <- State Env Env
forall s. State s s
State.get
    Env -> State Env ()
forall s. s -> State s ()
State.put Env
e { localTypeVars :: LocalTypeVars
localTypeVars = LocalTypeVars
tvs }

-- | store a complete type map
putTypeMap :: TypeMap -> State.State Env ()
putTypeMap :: TypeMap -> State Env ()
putTypeMap tm :: TypeMap
tm = do
    Env
e <- State Env Env
forall s. State s s
State.get
    Env -> State Env ()
forall s. s -> State s ()
State.put Env
e { typeMap :: TypeMap
typeMap = TypeMap
tm }

-- | store assumptions
putAssumps :: Assumps -> State.State Env ()
putAssumps :: Assumps -> State Env ()
putAssumps ops :: Assumps
ops = do
    Env
e <- State Env Env
forall s. State s s
State.get
    Env -> State Env ()
forall s. s -> State s ()
State.put Env
e { assumps :: Assumps
assumps = Assumps
ops }

-- | store assumptions
putBinders :: Map.Map Id Id -> State.State Env ()
putBinders :: IdMap -> State Env ()
putBinders bs :: IdMap
bs = do
    Env
e <- State Env Env
forall s. State s s
State.get
    Env -> State Env ()
forall s. s -> State s ()
State.put Env
e { binders :: IdMap
binders = IdMap
bs }

-- | get the variable
getVar :: VarDecl -> Id
getVar :: VarDecl -> Id
getVar (VarDecl v :: Id
v _ _ _) = Id
v

-- | check uniqueness of variables
checkUniqueVars :: [VarDecl] -> State.State Env ()
checkUniqueVars :: [VarDecl] -> State Env ()
checkUniqueVars = [Diagnosis] -> State Env ()
addDiags ([Diagnosis] -> State Env ())
-> ([VarDecl] -> [Diagnosis]) -> [VarDecl] -> State Env ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Id] -> [Diagnosis]
forall a. (Pretty a, GetRange a, Ord a) => [a] -> [Diagnosis]
checkUniqueness ([Id] -> [Diagnosis])
-> ([VarDecl] -> [Id]) -> [VarDecl] -> [Diagnosis]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VarDecl -> Id) -> [VarDecl] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Id
getVar

-- * morphisms

-- mapping qualified operation identifiers (aka renamings)
type FunMap = Map.Map (Id, TypeScheme) (Id, TypeScheme)

-- | keep types and class disjoint and use a single identifier map for both
data Morphism = Morphism
    { Morphism -> Env
msource :: Env
    , Morphism -> Env
mtarget :: Env
    , Morphism -> IdMap
typeIdMap :: IdMap
    , Morphism -> IdMap
classIdMap :: IdMap
    , Morphism -> FunMap
funMap :: FunMap
    } deriving (Int -> Morphism -> ShowS
[Morphism] -> ShowS
Morphism -> String
(Int -> Morphism -> ShowS)
-> (Morphism -> String) -> ([Morphism] -> ShowS) -> Show Morphism
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Morphism] -> ShowS
$cshowList :: [Morphism] -> ShowS
show :: Morphism -> String
$cshow :: Morphism -> String
showsPrec :: Int -> Morphism -> ShowS
$cshowsPrec :: Int -> Morphism -> ShowS
Show, Morphism -> Morphism -> Bool
(Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Bool) -> Eq Morphism
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Morphism -> Morphism -> Bool
$c/= :: Morphism -> Morphism -> Bool
== :: Morphism -> Morphism -> Bool
$c== :: Morphism -> Morphism -> Bool
Eq, Eq Morphism
Eq Morphism =>
(Morphism -> Morphism -> Ordering)
-> (Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Morphism)
-> (Morphism -> Morphism -> Morphism)
-> Ord Morphism
Morphism -> Morphism -> Bool
Morphism -> Morphism -> Ordering
Morphism -> Morphism -> Morphism
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 :: Morphism -> Morphism -> Morphism
$cmin :: Morphism -> Morphism -> Morphism
max :: Morphism -> Morphism -> Morphism
$cmax :: Morphism -> Morphism -> Morphism
>= :: Morphism -> Morphism -> Bool
$c>= :: Morphism -> Morphism -> Bool
> :: Morphism -> Morphism -> Bool
$c> :: Morphism -> Morphism -> Bool
<= :: Morphism -> Morphism -> Bool
$c<= :: Morphism -> Morphism -> Bool
< :: Morphism -> Morphism -> Bool
$c< :: Morphism -> Morphism -> Bool
compare :: Morphism -> Morphism -> Ordering
$ccompare :: Morphism -> Morphism -> Ordering
$cp1Ord :: Eq Morphism
Ord, Typeable, Typeable Morphism
Constr
DataType
Typeable Morphism =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Morphism -> c Morphism)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Morphism)
-> (Morphism -> Constr)
-> (Morphism -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Morphism))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Morphism))
-> ((forall b. Data b => b -> b) -> Morphism -> Morphism)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Morphism -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Morphism -> r)
-> (forall u. (forall d. Data d => d -> u) -> Morphism -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Morphism -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Morphism -> m Morphism)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Morphism -> m Morphism)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Morphism -> m Morphism)
-> Data Morphism
Morphism -> Constr
Morphism -> DataType
(forall b. Data b => b -> b) -> Morphism -> Morphism
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Morphism -> c Morphism
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Morphism
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) -> Morphism -> u
forall u. (forall d. Data d => d -> u) -> Morphism -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Morphism -> m Morphism
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Morphism -> m Morphism
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Morphism
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Morphism -> c Morphism
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Morphism)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Morphism)
$cMorphism :: Constr
$tMorphism :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Morphism -> m Morphism
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Morphism -> m Morphism
gmapMp :: (forall d. Data d => d -> m d) -> Morphism -> m Morphism
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Morphism -> m Morphism
gmapM :: (forall d. Data d => d -> m d) -> Morphism -> m Morphism
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Morphism -> m Morphism
gmapQi :: Int -> (forall d. Data d => d -> u) -> Morphism -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Morphism -> u
gmapQ :: (forall d. Data d => d -> u) -> Morphism -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Morphism -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism -> r
gmapT :: (forall b. Data b => b -> b) -> Morphism -> Morphism
$cgmapT :: (forall b. Data b => b -> b) -> Morphism -> Morphism
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Morphism)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Morphism)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Morphism)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Morphism)
dataTypeOf :: Morphism -> DataType
$cdataTypeOf :: Morphism -> DataType
toConstr :: Morphism -> Constr
$ctoConstr :: Morphism -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Morphism
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Morphism
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Morphism -> c Morphism
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Morphism -> c Morphism
$cp1Data :: Typeable Morphism
Data)

-- | construct morphism for subsignatures
mkMorphism :: Env -> Env -> Morphism
mkMorphism :: Env -> Env -> Morphism
mkMorphism e1 :: Env
e1 e2 :: Env
e2 = Morphism :: Env -> Env -> IdMap -> IdMap -> FunMap -> Morphism
Morphism
    { msource :: Env
msource = Env
e1
    , mtarget :: Env
mtarget = Env
e2
    , typeIdMap :: IdMap
typeIdMap = IdMap
forall k a. Map k a
Map.empty
    , classIdMap :: IdMap
classIdMap = IdMap
forall k a. Map k a
Map.empty
    , funMap :: FunMap
funMap = FunMap
forall k a. Map k a
Map.empty }

isInclMor :: Morphism -> Bool
isInclMor :: Morphism -> Bool
isInclMor m :: Morphism
m =
   IdMap -> Bool
forall k a. Map k a -> Bool
Map.null (Morphism -> IdMap
typeIdMap Morphism
m) Bool -> Bool -> Bool
&& IdMap -> Bool
forall k a. Map k a -> Bool
Map.null (Morphism -> IdMap
classIdMap Morphism
m) Bool -> Bool -> Bool
&& FunMap -> Bool
forall k a. Map k a -> Bool
Map.null (Morphism -> FunMap
funMap Morphism
m)

-- * symbol stuff

-- | the type or kind of an identifier
data SymbolType =
    OpAsItemType TypeScheme
  | TypeAsItemType RawKind
  | ClassAsItemType RawKind
  | SuperClassSymbol Kind
  | TypeKindInstance Kind
  | SuperTypeSymbol Id
  | TypeAliasSymbol Type
  | PredAsItemType TypeScheme
    deriving (Int -> SymbolType -> ShowS
[SymbolType] -> ShowS
SymbolType -> String
(Int -> SymbolType -> ShowS)
-> (SymbolType -> String)
-> ([SymbolType] -> ShowS)
-> Show SymbolType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SymbolType] -> ShowS
$cshowList :: [SymbolType] -> ShowS
show :: SymbolType -> String
$cshow :: SymbolType -> String
showsPrec :: Int -> SymbolType -> ShowS
$cshowsPrec :: Int -> SymbolType -> ShowS
Show, SymbolType -> SymbolType -> Bool
(SymbolType -> SymbolType -> Bool)
-> (SymbolType -> SymbolType -> Bool) -> Eq SymbolType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SymbolType -> SymbolType -> Bool
$c/= :: SymbolType -> SymbolType -> Bool
== :: SymbolType -> SymbolType -> Bool
$c== :: SymbolType -> SymbolType -> Bool
Eq, Eq SymbolType
Eq SymbolType =>
(SymbolType -> SymbolType -> Ordering)
-> (SymbolType -> SymbolType -> Bool)
-> (SymbolType -> SymbolType -> Bool)
-> (SymbolType -> SymbolType -> Bool)
-> (SymbolType -> SymbolType -> Bool)
-> (SymbolType -> SymbolType -> SymbolType)
-> (SymbolType -> SymbolType -> SymbolType)
-> Ord SymbolType
SymbolType -> SymbolType -> Bool
SymbolType -> SymbolType -> Ordering
SymbolType -> SymbolType -> SymbolType
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 :: SymbolType -> SymbolType -> SymbolType
$cmin :: SymbolType -> SymbolType -> SymbolType
max :: SymbolType -> SymbolType -> SymbolType
$cmax :: SymbolType -> SymbolType -> SymbolType
>= :: SymbolType -> SymbolType -> Bool
$c>= :: SymbolType -> SymbolType -> Bool
> :: SymbolType -> SymbolType -> Bool
$c> :: SymbolType -> SymbolType -> Bool
<= :: SymbolType -> SymbolType -> Bool
$c<= :: SymbolType -> SymbolType -> Bool
< :: SymbolType -> SymbolType -> Bool
$c< :: SymbolType -> SymbolType -> Bool
compare :: SymbolType -> SymbolType -> Ordering
$ccompare :: SymbolType -> SymbolType -> Ordering
$cp1Ord :: Eq SymbolType
Ord, Typeable, Typeable SymbolType
Constr
DataType
Typeable SymbolType =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> SymbolType -> c SymbolType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SymbolType)
-> (SymbolType -> Constr)
-> (SymbolType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SymbolType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c SymbolType))
-> ((forall b. Data b => b -> b) -> SymbolType -> SymbolType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SymbolType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SymbolType -> r)
-> (forall u. (forall d. Data d => d -> u) -> SymbolType -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SymbolType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType)
-> Data SymbolType
SymbolType -> Constr
SymbolType -> DataType
(forall b. Data b => b -> b) -> SymbolType -> SymbolType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymbolType -> c SymbolType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymbolType
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) -> SymbolType -> u
forall u. (forall d. Data d => d -> u) -> SymbolType -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymbolType -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SymbolType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymbolType -> m SymbolType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymbolType -> m SymbolType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymbolType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymbolType -> c SymbolType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymbolType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbolType)
$cPredAsItemType :: Constr
$cTypeAliasSymbol :: Constr
$cSuperTypeSymbol :: Constr
$cTypeKindInstance :: Constr
$cSuperClassSymbol :: Constr
$cClassAsItemType :: Constr
$cTypeAsItemType :: Constr
$cOpAsItemType :: Constr
$tSymbolType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymbolType -> m SymbolType
gmapMp :: (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymbolType -> m SymbolType
gmapM :: (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymbolType -> m SymbolType
gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbolType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SymbolType -> u
gmapQ :: (forall d. Data d => d -> u) -> SymbolType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SymbolType -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SymbolType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SymbolType -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymbolType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymbolType -> r
gmapT :: (forall b. Data b => b -> b) -> SymbolType -> SymbolType
$cgmapT :: (forall b. Data b => b -> b) -> SymbolType -> SymbolType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbolType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbolType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SymbolType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymbolType)
dataTypeOf :: SymbolType -> DataType
$cdataTypeOf :: SymbolType -> DataType
toConstr :: SymbolType -> Constr
$ctoConstr :: SymbolType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymbolType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymbolType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymbolType -> c SymbolType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymbolType -> c SymbolType
$cp1Data :: Typeable SymbolType
Data)

-- | symbols with their type
data Symbol =
    Symbol { Symbol -> Id
symName :: Id, Symbol -> SymbolType
symType :: SymbolType }
    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, 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 Eq Symbol where
    s1 :: Symbol
s1 == :: Symbol -> Symbol -> Bool
== s2 :: Symbol
s2 = Symbol -> Symbol -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Symbol
s1 Symbol
s2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance Ord Symbol where
    compare :: Symbol -> Symbol -> Ordering
compare s1 :: Symbol
s1 s2 :: Symbol
s2 = (Id, SymbolType) -> (Id, SymbolType) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Symbol -> Id
symName Symbol
s1, Symbol -> SymbolType
symType Symbol
s1) (Symbol -> Id
symName Symbol
s2, Symbol -> SymbolType
symType Symbol
s2)

-- | mapping symbols to symbols
type SymbolMap = Map.Map Symbol Symbol

-- | a set of symbols
type SymbolSet = Set.Set Symbol

-- | create a type symbol
idToTypeSymbol :: Id -> RawKind -> Symbol
idToTypeSymbol :: Id -> RawKind -> Symbol
idToTypeSymbol idt :: Id
idt k :: RawKind
k = Id -> SymbolType -> Symbol
Symbol Id
idt (RawKind -> SymbolType
TypeAsItemType (RawKind -> SymbolType) -> RawKind -> SymbolType
forall a b. (a -> b) -> a -> b
$ RawKind -> RawKind
nonVarRawKind RawKind
k)

-- | create a class symbol
idToClassSymbol :: Id -> RawKind -> Symbol
idToClassSymbol :: Id -> RawKind -> Symbol
idToClassSymbol idt :: Id
idt k :: RawKind
k = Id -> SymbolType -> Symbol
Symbol Id
idt (RawKind -> SymbolType
ClassAsItemType (RawKind -> SymbolType) -> RawKind -> SymbolType
forall a b. (a -> b) -> a -> b
$ RawKind -> RawKind
nonVarRawKind RawKind
k)

-- | create an operation symbol
idToOpSymbol :: Id -> TypeScheme -> Symbol
idToOpSymbol :: Id -> TypeScheme -> Symbol
idToOpSymbol idt :: Id
idt typ :: TypeScheme
typ = Id -> SymbolType -> Symbol
Symbol Id
idt (TypeScheme -> SymbolType
OpAsItemType TypeScheme
typ)

{- | raw symbols where the type of a qualified raw symbol can be a type scheme
and also be a kind if the symbol kind is unknown. -}
data RawSymbol =
    AnID Id
  | AKindedId SymbKind Id
  | ASymbol Symbol
    deriving (Int -> RawSymbol -> ShowS
[RawSymbol] -> ShowS
RawSymbol -> String
(Int -> RawSymbol -> ShowS)
-> (RawSymbol -> String)
-> ([RawSymbol] -> ShowS)
-> Show RawSymbol
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RawSymbol] -> ShowS
$cshowList :: [RawSymbol] -> ShowS
show :: RawSymbol -> String
$cshow :: RawSymbol -> String
showsPrec :: Int -> RawSymbol -> ShowS
$cshowsPrec :: Int -> RawSymbol -> ShowS
Show, RawSymbol -> RawSymbol -> Bool
(RawSymbol -> RawSymbol -> Bool)
-> (RawSymbol -> RawSymbol -> Bool) -> Eq RawSymbol
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RawSymbol -> RawSymbol -> Bool
$c/= :: RawSymbol -> RawSymbol -> Bool
== :: RawSymbol -> RawSymbol -> Bool
$c== :: RawSymbol -> RawSymbol -> Bool
Eq, Eq RawSymbol
Eq RawSymbol =>
(RawSymbol -> RawSymbol -> Ordering)
-> (RawSymbol -> RawSymbol -> Bool)
-> (RawSymbol -> RawSymbol -> Bool)
-> (RawSymbol -> RawSymbol -> Bool)
-> (RawSymbol -> RawSymbol -> Bool)
-> (RawSymbol -> RawSymbol -> RawSymbol)
-> (RawSymbol -> RawSymbol -> RawSymbol)
-> Ord RawSymbol
RawSymbol -> RawSymbol -> Bool
RawSymbol -> RawSymbol -> Ordering
RawSymbol -> RawSymbol -> RawSymbol
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 :: RawSymbol -> RawSymbol -> RawSymbol
$cmin :: RawSymbol -> RawSymbol -> RawSymbol
max :: RawSymbol -> RawSymbol -> RawSymbol
$cmax :: RawSymbol -> RawSymbol -> RawSymbol
>= :: RawSymbol -> RawSymbol -> Bool
$c>= :: RawSymbol -> RawSymbol -> Bool
> :: RawSymbol -> RawSymbol -> Bool
$c> :: RawSymbol -> RawSymbol -> Bool
<= :: RawSymbol -> RawSymbol -> Bool
$c<= :: RawSymbol -> RawSymbol -> Bool
< :: RawSymbol -> RawSymbol -> Bool
$c< :: RawSymbol -> RawSymbol -> Bool
compare :: RawSymbol -> RawSymbol -> Ordering
$ccompare :: RawSymbol -> RawSymbol -> Ordering
$cp1Ord :: Eq RawSymbol
Ord, Typeable, Typeable RawSymbol
Constr
DataType
Typeable RawSymbol =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> RawSymbol -> c RawSymbol)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c RawSymbol)
-> (RawSymbol -> Constr)
-> (RawSymbol -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c RawSymbol))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RawSymbol))
-> ((forall b. Data b => b -> b) -> RawSymbol -> RawSymbol)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> RawSymbol -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> RawSymbol -> r)
-> (forall u. (forall d. Data d => d -> u) -> RawSymbol -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> RawSymbol -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol)
-> Data RawSymbol
RawSymbol -> Constr
RawSymbol -> DataType
(forall b. Data b => b -> b) -> RawSymbol -> RawSymbol
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RawSymbol -> c RawSymbol
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RawSymbol
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) -> RawSymbol -> u
forall u. (forall d. Data d => d -> u) -> RawSymbol -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RawSymbol -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RawSymbol -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RawSymbol
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RawSymbol -> c RawSymbol
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RawSymbol)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RawSymbol)
$cASymbol :: Constr
$cAKindedId :: Constr
$cAnID :: Constr
$tRawSymbol :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
gmapMp :: (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
gmapM :: (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
gmapQi :: Int -> (forall d. Data d => d -> u) -> RawSymbol -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RawSymbol -> u
gmapQ :: (forall d. Data d => d -> u) -> RawSymbol -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> RawSymbol -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RawSymbol -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RawSymbol -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RawSymbol -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RawSymbol -> r
gmapT :: (forall b. Data b => b -> b) -> RawSymbol -> RawSymbol
$cgmapT :: (forall b. Data b => b -> b) -> RawSymbol -> RawSymbol
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RawSymbol)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RawSymbol)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c RawSymbol)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RawSymbol)
dataTypeOf :: RawSymbol -> DataType
$cdataTypeOf :: RawSymbol -> DataType
toConstr :: RawSymbol -> Constr
$ctoConstr :: RawSymbol -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RawSymbol
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RawSymbol
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RawSymbol -> c RawSymbol
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RawSymbol -> c RawSymbol
$cp1Data :: Typeable RawSymbol
Data)

-- | mapping raw symbols to raw symbols
type RawSymbolMap = Map.Map RawSymbol RawSymbol

-- | create a raw symbol from an identifier
idToRaw :: Id -> RawSymbol
idToRaw :: Id -> RawSymbol
idToRaw = Id -> RawSymbol
AnID

-- | extract the top identifer from a raw symbol
rawSymName :: RawSymbol -> Id
rawSymName :: RawSymbol -> Id
rawSymName r :: RawSymbol
r = case RawSymbol
r of
    AnID i :: Id
i -> Id
i
    AKindedId _ i :: Id
i -> Id
i
    ASymbol s :: Symbol
s -> Symbol -> Id
symName Symbol
s

-- | convert a symbol type to a symbol kind
symbTypeToKind :: SymbolType -> SymbKind
symbTypeToKind :: SymbolType -> SymbKind
symbTypeToKind s :: SymbolType
s = case SymbolType
s of
    OpAsItemType _ -> SymbKind
SyKop
    TypeAsItemType _ -> SymbKind
SyKtype
    SuperTypeSymbol _ -> SymbKind
SyKtype
    TypeKindInstance _ -> SymbKind
SyKtype
    TypeAliasSymbol _ -> SymbKind
SyKtype
    ClassAsItemType _ -> SymbKind
SyKclass
    SuperClassSymbol _ -> SymbKind
SyKclass
    PredAsItemType _ -> SymbKind
SyKpred

-- | wrap a symbol as raw symbol (is 'ASymbol')
symbolToRaw :: Symbol -> RawSymbol
symbolToRaw :: Symbol -> RawSymbol
symbolToRaw = Symbol -> RawSymbol
ASymbol

-- | create a raw symbol from a symbol kind and an identifier
symbKindToRaw :: SymbKind -> Id -> RawSymbol
symbKindToRaw :: SymbKind -> Id -> RawSymbol
symbKindToRaw sk :: SymbKind
sk = case SymbKind
sk of
    Implicit -> Id -> RawSymbol
AnID
    _ -> SymbKind -> Id -> RawSymbol
AKindedId (SymbKind -> Id -> RawSymbol) -> SymbKind -> Id -> RawSymbol
forall a b. (a -> b) -> a -> b
$ case SymbKind
sk of
        SyKpred -> SymbKind
SyKop
        SyKfun -> SymbKind
SyKop
        SyKsort -> SymbKind
SyKtype
        _ -> SymbKind
sk

getCompoundLists :: Env -> Set.Set [Id]
getCompoundLists :: Env -> Set [Id]
getCompoundLists e :: Env
e = [Id] -> Set [Id] -> Set [Id]
forall a. Ord a => a -> Set a -> Set a
Set.delete [] (Set [Id] -> Set [Id]) -> Set [Id] -> Set [Id]
forall a b. (a -> b) -> a -> b
$ (Id -> [Id]) -> Set Id -> Set [Id]
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Id -> [Id]
getCompound (Set Id -> Set [Id]) -> Set Id -> Set [Id]
forall a b. (a -> b) -> a -> b
$ Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union
    (Assumps -> Set Id
forall k a. Map k a -> Set k
Map.keysSet (Assumps -> Set Id) -> Assumps -> Set Id
forall a b. (a -> b) -> a -> b
$ Env -> Assumps
assumps Env
e) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ TypeMap -> Set Id
forall k a. Map k a -> Set k
Map.keysSet (TypeMap -> Set Id) -> TypeMap -> Set Id
forall a b. (a -> b) -> a -> b
$ Env -> TypeMap
typeMap Env
e
    where getCompound :: Id -> [Id]
getCompound (Id _ cs :: [Id]
cs _) = [Id]
cs