Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Types.Bounds

Documentation

data Bound t e Source #

Constructors

Bound
Fields bname :: LocSymbol The name of the bound tyvars :: [t] Type variables that appear in the bounds bparams :: [(LocSymbol, t)] These are abstract refinements, for now bargs :: [(LocSymbol, t)] These are value variables bbody :: e The body of the bound

Instances

Instances details

Bifunctor Bound Source #
Instance details Defined in Language.Haskell.Liquid.Types.Bounds Methods bimap :: (a -> b) -> (c -> d) -> Bound a c -> Bound b d # first :: (a -> b) -> Bound a c -> Bound b c # second :: (b -> c) -> Bound a b -> Bound a c #
Eq (Bound t e) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Bounds Methods (==) :: Bound t e -> Bound t e -> Bool # (/=) :: Bound t e -> Bound t e -> Bool #
(Data t, Data e) => Data (Bound t e) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Bounds Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Bound t e -> c (Bound t e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Bound t e) # toConstr :: Bound t e -> Constr # dataTypeOf :: Bound t e -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Bound t e)) # dataCast2 :: Typeable t0 => (forall d e0. (Data d, Data e0) => c (t0 d e0)) -> Maybe (c (Bound t e)) # gmapT :: (forall b. Data b => b -> b) -> Bound t e -> Bound t e # gmapQl :: (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 # gmapQ :: (forall d. Data d => d -> u) -> Bound t e -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Bound t e -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e) #
(PPrint e, PPrint t) => Show (Bound t e) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Bounds Methods showsPrec :: Int -> Bound t e -> ShowS # show :: Bound t e -> String # showList :: [Bound t e] -> ShowS #
Generic (Bound t e) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Bounds Associated Types type Rep (Bound t e) :: Type -> Type # Methods from :: Bound t e -> Rep (Bound t e) x # to :: Rep (Bound t e) x -> Bound t e #
(Binary t, Binary e) => Binary (Bound t e) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Bounds Methods put :: Bound t e -> Put # get :: Get (Bound t e) # putList :: [Bound t e] -> Put #
Hashable (Bound t e) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Bounds Methods hashWithSalt :: Int -> Bound t e -> Int # hash :: Bound t e -> Int #
(PPrint e, PPrint t) => PPrint (Bound t e) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Bounds Methods pprintTidy :: Tidy -> Bound t e -> Doc # pprintPrec :: Int -> Tidy -> Bound t e -> Doc #
type Rep (Bound t e) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Bounds type Rep (Bound t e) = D1 ('MetaData "Bound" "Language.Haskell.Liquid.Types.Bounds" "liquidhaskell-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" 'False) (C1 ('MetaCons "Bound" 'PrefixI 'True) ((S1 ('MetaSel ('Just "bname") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocSymbol) :: S1 ('MetaSel ('Just "tyvars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [t])) :: (S1 ('MetaSel ('Just "bparams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(LocSymbol, t)]) :: (S1 ('MetaSel ('Just "bargs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(LocSymbol, t)]) :: S1 ('MetaSel ('Just "bbody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 e)))))

type RBound = RRBound RSort Source #

type RRBound tv = Bound tv Expr Source #

type RBEnv = HashMap LocSymbol RBound Source #

type RRBEnv tv = HashMap LocSymbol (RRBound tv) Source #

makeBound :: (PPrint r, UReftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r) => RRBound RSort -> [RRType r] -> [Symbol] -> RRType r -> RRType r Source #