{-# LANGUAGE FlexibleContexts   #-}
{-# LANGUAGE TupleSections      #-}
{-# LANGUAGE OverloadedStrings  #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveTraversable  #-}
{-# LANGUAGE DeriveGeneric      #-}
{-# LANGUAGE DerivingVia        #-}
{-# LANGUAGE NamedFieldPuns     #-}

{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module Language.Haskell.Liquid.Types.Bounds (

    Bound(..),

    RBound, RRBound, RRBoundV,

    RBEnv, RRBEnv, RRBEnvV,

    emapBoundM,
    mapBoundTy

    ) where

import Prelude hiding (error)
import Text.PrettyPrint.HughesPJ
import GHC.Generics
import Data.Hashable
import Data.Bifunctor as Bifunctor
import Data.Data
import qualified Data.Binary         as B
import Data.Traversable
import qualified Data.HashMap.Strict as M

import qualified Language.Fixpoint.Types as F
import Language.Haskell.Liquid.Types.RefType ()
import Language.Haskell.Liquid.Types.RType
import Language.Haskell.Liquid.Types.Types


data Bound t e = Bound
  { forall t e. Bound t e -> LocSymbol
bname   :: LocSymbol         -- ^ The name of the bound
  , forall t e. Bound t e -> [t]
tyvars  :: [t]               -- ^ Type variables that appear in the bounds
  , forall t e. Bound t e -> [(LocSymbol, t)]
bparams :: [(LocSymbol, t)]  -- ^ These are abstract refinements, for now
  , forall t e. Bound t e -> [(LocSymbol, t)]
bargs   :: [(LocSymbol, t)]  -- ^ These are value variables
  , forall t e. Bound t e -> e
bbody   :: e                 -- ^ The body of the bound
  } deriving (Typeable (Bound t e)
Typeable (Bound t e) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Bound t e -> c (Bound t e))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Bound t e))
-> (Bound t e -> Constr)
-> (Bound t e -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Bound t e)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Bound t e)))
-> ((forall b. Data b => b -> b) -> Bound t e -> Bound t e)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Bound t e -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Bound t e -> r)
-> (forall u. (forall d. Data d => d -> u) -> Bound t e -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Bound t e -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e))
-> Data (Bound t e)
Bound t e -> Constr
Bound t e -> DataType
(forall b. Data b => b -> b) -> Bound t e -> Bound t e
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) -> Bound t e -> u
forall u. (forall d. Data d => d -> u) -> Bound t e -> [u]
forall t e. (Data t, Data e) => Typeable (Bound t e)
forall t e. (Data t, Data e) => Bound t e -> Constr
forall t e. (Data t, Data e) => Bound t e -> DataType
forall t e.
(Data t, Data e) =>
(forall b. Data b => b -> b) -> Bound t e -> Bound t e
forall t e u.
(Data t, Data e) =>
Int -> (forall d. Data d => d -> u) -> Bound t e -> u
forall t e u.
(Data t, Data e) =>
(forall d. Data d => d -> u) -> Bound t e -> [u]
forall t e r r'.
(Data t, Data e) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
forall t e r r'.
(Data t, Data e) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
forall t e (m :: * -> *).
(Data t, Data e, Monad m) =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
forall t e (m :: * -> *).
(Data t, Data e, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
forall t e (c :: * -> *).
(Data t, Data e) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Bound t e)
forall t e (c :: * -> *).
(Data t, Data e) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bound t e -> c (Bound t e)
forall t e (t :: * -> *) (c :: * -> *).
(Data t, Data e, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Bound t e))
forall t e (t :: * -> * -> *) (c :: * -> *).
(Data t, Data e, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Bound t e))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Bound t e)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bound t e -> c (Bound t e)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Bound t e))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Bound t e))
$cgfoldl :: forall t e (c :: * -> *).
(Data t, Data e) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bound t e -> c (Bound t e)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bound t e -> c (Bound t e)
$cgunfold :: forall t e (c :: * -> *).
(Data t, Data e) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Bound t e)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Bound t e)
$ctoConstr :: forall t e. (Data t, Data e) => Bound t e -> Constr
toConstr :: Bound t e -> Constr
$cdataTypeOf :: forall t e. (Data t, Data e) => Bound t e -> DataType
dataTypeOf :: Bound t e -> DataType
$cdataCast1 :: forall t e (t :: * -> *) (c :: * -> *).
(Data t, Data e, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Bound t e))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Bound t e))
$cdataCast2 :: forall t e (t :: * -> * -> *) (c :: * -> *).
(Data t, Data e, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Bound t e))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Bound t e))
$cgmapT :: forall t e.
(Data t, Data e) =>
(forall b. Data b => b -> b) -> Bound t e -> Bound t e
gmapT :: (forall b. Data b => b -> b) -> Bound t e -> Bound t e
$cgmapQl :: forall t e r r'.
(Data t, Data e) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
$cgmapQr :: forall t e r r'.
(Data t, Data e) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
$cgmapQ :: forall t e u.
(Data t, Data e) =>
(forall d. Data d => d -> u) -> Bound t e -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Bound t e -> [u]
$cgmapQi :: forall t e u.
(Data t, Data e) =>
Int -> (forall d. Data d => d -> u) -> Bound t e -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Bound t e -> u
$cgmapM :: forall t e (m :: * -> *).
(Data t, Data e, Monad m) =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
$cgmapMp :: forall t e (m :: * -> *).
(Data t, Data e, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
$cgmapMo :: forall t e (m :: * -> *).
(Data t, Data e, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
Data, (forall x. Bound t e -> Rep (Bound t e) x)
-> (forall x. Rep (Bound t e) x -> Bound t e)
-> Generic (Bound t e)
forall x. Rep (Bound t e) x -> Bound t e
forall x. Bound t e -> Rep (Bound t e) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t e x. Rep (Bound t e) x -> Bound t e
forall t e x. Bound t e -> Rep (Bound t e) x
$cfrom :: forall t e x. Bound t e -> Rep (Bound t e) x
from :: forall x. Bound t e -> Rep (Bound t e) x
$cto :: forall t e x. Rep (Bound t e) x -> Bound t e
to :: forall x. Rep (Bound t e) x -> Bound t e
Generic, (forall a b. (a -> b) -> Bound t a -> Bound t b)
-> (forall a b. a -> Bound t b -> Bound t a) -> Functor (Bound t)
forall a b. a -> Bound t b -> Bound t a
forall a b. (a -> b) -> Bound t a -> Bound t b
forall t a b. a -> Bound t b -> Bound t a
forall t a b. (a -> b) -> Bound t a -> Bound t b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall t a b. (a -> b) -> Bound t a -> Bound t b
fmap :: forall a b. (a -> b) -> Bound t a -> Bound t b
$c<$ :: forall t a b. a -> Bound t b -> Bound t a
<$ :: forall a b. a -> Bound t b -> Bound t a
Functor, (forall m. Monoid m => Bound t m -> m)
-> (forall m a. Monoid m => (a -> m) -> Bound t a -> m)
-> (forall m a. Monoid m => (a -> m) -> Bound t a -> m)
-> (forall a b. (a -> b -> b) -> b -> Bound t a -> b)
-> (forall a b. (a -> b -> b) -> b -> Bound t a -> b)
-> (forall b a. (b -> a -> b) -> b -> Bound t a -> b)
-> (forall b a. (b -> a -> b) -> b -> Bound t a -> b)
-> (forall a. (a -> a -> a) -> Bound t a -> a)
-> (forall a. (a -> a -> a) -> Bound t a -> a)
-> (forall a. Bound t a -> [a])
-> (forall a. Bound t a -> Bool)
-> (forall a. Bound t a -> Int)
-> (forall a. Eq a => a -> Bound t a -> Bool)
-> (forall a. Ord a => Bound t a -> a)
-> (forall a. Ord a => Bound t a -> a)
-> (forall a. Num a => Bound t a -> a)
-> (forall a. Num a => Bound t a -> a)
-> Foldable (Bound t)
forall a. Eq a => a -> Bound t a -> Bool
forall a. Num a => Bound t a -> a
forall a. Ord a => Bound t a -> a
forall m. Monoid m => Bound t m -> m
forall a. Bound t a -> Bool
forall a. Bound t a -> Int
forall a. Bound t a -> [a]
forall a. (a -> a -> a) -> Bound t a -> a
forall t a. Eq a => a -> Bound t a -> Bool
forall t a. Num a => Bound t a -> a
forall t a. Ord a => Bound t a -> a
forall t m. Monoid m => Bound t m -> m
forall m a. Monoid m => (a -> m) -> Bound t a -> m
forall t a. Bound t a -> Bool
forall t a. Bound t a -> Int
forall t a. Bound t a -> [a]
forall b a. (b -> a -> b) -> b -> Bound t a -> b
forall a b. (a -> b -> b) -> b -> Bound t a -> b
forall t a. (a -> a -> a) -> Bound t a -> a
forall t m a. Monoid m => (a -> m) -> Bound t a -> m
forall t b a. (b -> a -> b) -> b -> Bound t a -> b
forall t a b. (a -> b -> b) -> b -> Bound t a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall t m. Monoid m => Bound t m -> m
fold :: forall m. Monoid m => Bound t m -> m
$cfoldMap :: forall t m a. Monoid m => (a -> m) -> Bound t a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Bound t a -> m
$cfoldMap' :: forall t m a. Monoid m => (a -> m) -> Bound t a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Bound t a -> m
$cfoldr :: forall t a b. (a -> b -> b) -> b -> Bound t a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Bound t a -> b
$cfoldr' :: forall t a b. (a -> b -> b) -> b -> Bound t a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Bound t a -> b
$cfoldl :: forall t b a. (b -> a -> b) -> b -> Bound t a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Bound t a -> b
$cfoldl' :: forall t b a. (b -> a -> b) -> b -> Bound t a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Bound t a -> b
$cfoldr1 :: forall t a. (a -> a -> a) -> Bound t a -> a
foldr1 :: forall a. (a -> a -> a) -> Bound t a -> a
$cfoldl1 :: forall t a. (a -> a -> a) -> Bound t a -> a
foldl1 :: forall a. (a -> a -> a) -> Bound t a -> a
$ctoList :: forall t a. Bound t a -> [a]
toList :: forall a. Bound t a -> [a]
$cnull :: forall t a. Bound t a -> Bool
null :: forall a. Bound t a -> Bool
$clength :: forall t a. Bound t a -> Int
length :: forall a. Bound t a -> Int
$celem :: forall t a. Eq a => a -> Bound t a -> Bool
elem :: forall a. Eq a => a -> Bound t a -> Bool
$cmaximum :: forall t a. Ord a => Bound t a -> a
maximum :: forall a. Ord a => Bound t a -> a
$cminimum :: forall t a. Ord a => Bound t a -> a
minimum :: forall a. Ord a => Bound t a -> a
$csum :: forall t a. Num a => Bound t a -> a
sum :: forall a. Num a => Bound t a -> a
$cproduct :: forall t a. Num a => Bound t a -> a
product :: forall a. Num a => Bound t a -> a
Foldable, Functor (Bound t)
Foldable (Bound t)
(Functor (Bound t), Foldable (Bound t)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Bound t a -> f (Bound t b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Bound t (f a) -> f (Bound t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Bound t a -> m (Bound t b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Bound t (m a) -> m (Bound t a))
-> Traversable (Bound t)
forall t. Functor (Bound t)
forall t. Foldable (Bound t)
forall t (m :: * -> *) a. Monad m => Bound t (m a) -> m (Bound t a)
forall t (f :: * -> *) a.
Applicative f =>
Bound t (f a) -> f (Bound t a)
forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bound t a -> m (Bound t b)
forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Bound t a -> f (Bound t b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Bound t (m a) -> m (Bound t a)
forall (f :: * -> *) a.
Applicative f =>
Bound t (f a) -> f (Bound t a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bound t a -> m (Bound t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Bound t a -> f (Bound t b)
$ctraverse :: forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Bound t a -> f (Bound t b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Bound t a -> f (Bound t b)
$csequenceA :: forall t (f :: * -> *) a.
Applicative f =>
Bound t (f a) -> f (Bound t a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Bound t (f a) -> f (Bound t a)
$cmapM :: forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bound t a -> m (Bound t b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bound t a -> m (Bound t b)
$csequence :: forall t (m :: * -> *) a. Monad m => Bound t (m a) -> m (Bound t a)
sequence :: forall (m :: * -> *) a. Monad m => Bound t (m a) -> m (Bound t a)
Traversable)
  deriving Get (Bound t e)
[Bound t e] -> Put
Bound t e -> Put
(Bound t e -> Put)
-> Get (Bound t e) -> ([Bound t e] -> Put) -> Binary (Bound t e)
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
forall t e. (Binary t, Binary e) => Get (Bound t e)
forall t e. (Binary t, Binary e) => [Bound t e] -> Put
forall t e. (Binary t, Binary e) => Bound t e -> Put
$cput :: forall t e. (Binary t, Binary e) => Bound t e -> Put
put :: Bound t e -> Put
$cget :: forall t e. (Binary t, Binary e) => Get (Bound t e)
get :: Get (Bound t e)
$cputList :: forall t e. (Binary t, Binary e) => [Bound t e] -> Put
putList :: [Bound t e] -> Put
B.Binary via Generically (Bound t e)

type RBound        = RRBound RSort
type RRBound tv    = RRBoundV F.Symbol tv
type RRBoundV v tv = Bound tv (F.ExprV v)
type RBEnv         = M.HashMap LocSymbol RBound
type RRBEnv tv     = M.HashMap LocSymbol (RRBound tv)
type RRBEnvV v tv     = M.HashMap LocSymbol (RRBoundV v tv)

emapBoundM
  :: Monad m
  => ([F.Symbol] -> t0 -> m t1)
  -> ([F.Symbol] -> e0 -> m e1)
  -> Bound t0 e0
  -> m (Bound t1 e1)
emapBoundM :: forall (m :: * -> *) t0 t1 e0 e1.
Monad m =>
([Symbol] -> t0 -> m t1)
-> ([Symbol] -> e0 -> m e1) -> Bound t0 e0 -> m (Bound t1 e1)
emapBoundM [Symbol] -> t0 -> m t1
f [Symbol] -> e0 -> m e1
g Bound t0 e0
b = do
    tyvars <- (t0 -> m t1) -> [t0] -> m [t1]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([Symbol] -> t0 -> m t1
f []) ([t0] -> m [t1]) -> [t0] -> m [t1]
forall a b. (a -> b) -> a -> b
$ Bound t0 e0 -> [t0]
forall t e. Bound t e -> [t]
tyvars Bound t0 e0
b
    (e1, bparams) <- mapAccumM (\[Symbol]
e -> ((LocSymbol, t1) -> ([Symbol], (LocSymbol, t1)))
-> m (LocSymbol, t1) -> m ([Symbol], (LocSymbol, t1))
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Symbol]
e,) (m (LocSymbol, t1) -> m ([Symbol], (LocSymbol, t1)))
-> ((LocSymbol, t0) -> m (LocSymbol, t1))
-> (LocSymbol, t0)
-> m ([Symbol], (LocSymbol, t1))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t0 -> m t1) -> (LocSymbol, t0) -> m (LocSymbol, t1)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (LocSymbol, a) -> f (LocSymbol, b)
traverse ([Symbol] -> t0 -> m t1
f [Symbol]
e)) [] (bparams b)
    (e2, bargs) <- mapAccumM (\[Symbol]
e -> ((LocSymbol, t1) -> ([Symbol], (LocSymbol, t1)))
-> m (LocSymbol, t1) -> m ([Symbol], (LocSymbol, t1))
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Symbol]
e,) (m (LocSymbol, t1) -> m ([Symbol], (LocSymbol, t1)))
-> ((LocSymbol, t0) -> m (LocSymbol, t1))
-> (LocSymbol, t0)
-> m ([Symbol], (LocSymbol, t1))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t0 -> m t1) -> (LocSymbol, t0) -> m (LocSymbol, t1)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (LocSymbol, a) -> f (LocSymbol, b)
traverse ([Symbol] -> t0 -> m t1
f [Symbol]
e)) e1 (bargs b)
    bbody <- g e2 (bbody b)
    return b{tyvars, bparams, bargs, bbody}

mapBoundTy :: (t0 -> t1) -> Bound t0 e -> Bound t1 e
mapBoundTy :: forall t0 t1 e. (t0 -> t1) -> Bound t0 e -> Bound t1 e
mapBoundTy t0 -> t1
f Bound{e
[t0]
[(LocSymbol, t0)]
LocSymbol
bname :: forall t e. Bound t e -> LocSymbol
tyvars :: forall t e. Bound t e -> [t]
bparams :: forall t e. Bound t e -> [(LocSymbol, t)]
bargs :: forall t e. Bound t e -> [(LocSymbol, t)]
bbody :: forall t e. Bound t e -> e
bname :: LocSymbol
tyvars :: [t0]
bparams :: [(LocSymbol, t0)]
bargs :: [(LocSymbol, t0)]
bbody :: e
..} = do
    Bound
      { tyvars :: [t1]
tyvars = (t0 -> t1) -> [t0] -> [t1]
forall a b. (a -> b) -> [a] -> [b]
map t0 -> t1
f [t0]
tyvars
      , bparams :: [(LocSymbol, t1)]
bparams = ((LocSymbol, t0) -> (LocSymbol, t1))
-> [(LocSymbol, t0)] -> [(LocSymbol, t1)]
forall a b. (a -> b) -> [a] -> [b]
map ((t0 -> t1) -> (LocSymbol, t0) -> (LocSymbol, t1)
forall a b. (a -> b) -> (LocSymbol, a) -> (LocSymbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap t0 -> t1
f) [(LocSymbol, t0)]
bparams
      , bargs :: [(LocSymbol, t1)]
bargs = ((LocSymbol, t0) -> (LocSymbol, t1))
-> [(LocSymbol, t0)] -> [(LocSymbol, t1)]
forall a b. (a -> b) -> [a] -> [b]
map ((t0 -> t1) -> (LocSymbol, t0) -> (LocSymbol, t1)
forall a b. (a -> b) -> (LocSymbol, a) -> (LocSymbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap t0 -> t1
f) [(LocSymbol, t0)]
bargs
      , e
LocSymbol
bname :: LocSymbol
bbody :: e
bname :: LocSymbol
bbody :: e
..
      }

instance Hashable (Bound t e) where
  hashWithSalt :: Int -> Bound t e -> Int
hashWithSalt Int
i = Int -> LocSymbol -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
i (LocSymbol -> Int) -> (Bound t e -> LocSymbol) -> Bound t e -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bound t e -> LocSymbol
forall t e. Bound t e -> LocSymbol
bname

instance Eq (Bound t e) where
  Bound t e
b1 == :: Bound t e -> Bound t e -> Bool
== Bound t e
b2 = Bound t e -> LocSymbol
forall t e. Bound t e -> LocSymbol
bname Bound t e
b1 LocSymbol -> LocSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== Bound t e -> LocSymbol
forall t e. Bound t e -> LocSymbol
bname Bound t e
b2

instance (PPrint e, PPrint t) => (Show (Bound t e)) where
  show :: Bound t e -> String
show = Bound t e -> String
forall a. PPrint a => a -> String
showpp


instance (PPrint e, PPrint t) => (PPrint (Bound t e)) where
  pprintTidy :: Tidy -> Bound t e -> Doc
pprintTidy Tidy
k (Bound LocSymbol
s [t]
vs [(LocSymbol, t)]
ps [(LocSymbol, t)]
ys e
e) = Doc
"bound" Doc -> Doc -> Doc
<+> Tidy -> LocSymbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k LocSymbol
s Doc -> Doc -> Doc
<+>
                                      Doc
"forall" Doc -> Doc -> Doc
<+> Tidy -> [t] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k [t]
vs Doc -> Doc -> Doc
<+> Doc
"." Doc -> Doc -> Doc
<+>
                                      Tidy -> [LocSymbol] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k ((LocSymbol, t) -> LocSymbol
forall a b. (a, b) -> a
fst ((LocSymbol, t) -> LocSymbol) -> [(LocSymbol, t)] -> [LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, t)]
ps) Doc -> Doc -> Doc
<+> Doc
"=" Doc -> Doc -> Doc
<+>
                                      Tidy -> [LocSymbol] -> Doc
forall {a}. PPrint a => Tidy -> [a] -> Doc
ppBsyms Tidy
k ((LocSymbol, t) -> LocSymbol
forall a b. (a, b) -> a
fst ((LocSymbol, t) -> LocSymbol) -> [(LocSymbol, t)] -> [LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, t)]
ys) Doc -> Doc -> Doc
<+> Tidy -> e -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k e
e
    where
      ppBsyms :: Tidy -> [a] -> Doc
ppBsyms Tidy
_ [] = Doc
""
      ppBsyms Tidy
k' [a]
xs = Doc
"\\" Doc -> Doc -> Doc
<+> Tidy -> [a] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k' [a]
xs Doc -> Doc -> Doc
<+> Doc
"->"

instance Bifunctor Bound where
  first :: forall t0 t1 e. (t0 -> t1) -> Bound t0 e -> Bound t1 e
first  a -> b
f (Bound LocSymbol
s [a]
vs [(LocSymbol, a)]
ps [(LocSymbol, a)]
xs c
e) = LocSymbol
-> [b] -> [(LocSymbol, b)] -> [(LocSymbol, b)] -> c -> Bound b c
forall t e.
LocSymbol
-> [t] -> [(LocSymbol, t)] -> [(LocSymbol, t)] -> e -> Bound t e
Bound LocSymbol
s (a -> b
f (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
vs) ((a -> b) -> (LocSymbol, a) -> (LocSymbol, b)
forall a b. (a -> b) -> (LocSymbol, a) -> (LocSymbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f ((LocSymbol, a) -> (LocSymbol, b))
-> [(LocSymbol, a)] -> [(LocSymbol, b)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, a)]
ps) ((a -> b) -> (LocSymbol, a) -> (LocSymbol, b)
forall a b. (a -> b) -> (LocSymbol, a) -> (LocSymbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f ((LocSymbol, a) -> (LocSymbol, b))
-> [(LocSymbol, a)] -> [(LocSymbol, b)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, a)]
xs) c
e
  second :: forall b c a. (b -> c) -> Bound a b -> Bound a c
second = (b -> c) -> Bound a b -> Bound a c
forall a b. (a -> b) -> Bound a a -> Bound a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap