liquidhaskell-boot-0.9.2.5.0: Liquid Types for Haskell
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Haskell.Liquid.Types.Types

Description

This module should contain all the global type definitions and basic instances.

Synopsis

Options

Ghc Information

data TargetVars Source #

Which Top-Level Binders Should be Verified

Constructors

AllVars 
Only ![Var] 

Instances

Instances details
PPrint TargetVars Source # 
Instance details

Defined in Language.Haskell.Liquid.GHC.Interface

data TyConMap Source #

Information about Type Constructors

Constructors

TyConMap 

Fields

Instances

Instances details
Qualify TyConMap Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

F.Located Things

data Located a #

Constructors

Loc 

Fields

Instances

Instances details
Foldable Located 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

fold :: Monoid m => Located m -> m #

foldMap :: Monoid m => (a -> m) -> Located a -> m #

foldMap' :: Monoid m => (a -> m) -> Located a -> m #

foldr :: (a -> b -> b) -> b -> Located a -> b #

foldr' :: (a -> b -> b) -> b -> Located a -> b #

foldl :: (b -> a -> b) -> b -> Located a -> b #

foldl' :: (b -> a -> b) -> b -> Located a -> b #

foldr1 :: (a -> a -> a) -> Located a -> a #

foldl1 :: (a -> a -> a) -> Located a -> a #

toList :: Located a -> [a] #

null :: Located a -> Bool #

length :: Located a -> Int #

elem :: Eq a => a -> Located a -> Bool #

maximum :: Ord a => Located a -> a #

minimum :: Ord a => Located a -> a #

sum :: Num a => Located a -> a #

product :: Num a => Located a -> a #

Traversable Located 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

traverse :: Applicative f => (a -> f b) -> Located a -> f (Located b) #

sequenceA :: Applicative f => Located (f a) -> f (Located a) #

mapM :: Monad m => (a -> m b) -> Located a -> m (Located b) #

sequence :: Monad m => Located (m a) -> m (Located a) #

Functor Located 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

fmap :: (a -> b) -> Located a -> Located b #

(<$) :: a -> Located b -> Located a #

Qualify ModSpecs Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareMeasure Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

TyConable LocSymbol Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Data a => Data (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Located a -> c (Located a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Located a) #

toConstr :: Located a -> Constr #

dataTypeOf :: Located a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Located a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Located a)) #

gmapT :: (forall b. Data b => b -> b) -> Located a -> Located a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Located a -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Located a -> r #

gmapQ :: (forall d. Data d => d -> u) -> Located a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Located a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Located a -> m (Located a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Located a -> m (Located a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Located a -> m (Located a) #

IsString a => IsString (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

fromString :: String -> Located a #

Generic (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Associated Types

type Rep (Located a) :: Type -> Type #

Methods

from :: Located a -> Rep (Located a) x #

to :: Rep (Located a) x -> Located a #

Show a => Show (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

showsPrec :: Int -> Located a -> ShowS #

show :: Located a -> String #

showList :: [Located a] -> ShowS #

Binary a => Binary (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

put :: Located a -> Put #

get :: Get (Located a) #

putList :: [Located a] -> Put #

NFData a => NFData (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

rnf :: Located a -> () #

Eq a => Eq (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

(==) :: Located a -> Located a -> Bool #

(/=) :: Located a -> Located a -> Bool #

Ord a => Ord (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

compare :: Located a -> Located a -> Ordering #

(<) :: Located a -> Located a -> Bool #

(<=) :: Located a -> Located a -> Bool #

(>) :: Located a -> Located a -> Bool #

(>=) :: Located a -> Located a -> Bool #

max :: Located a -> Located a -> Located a #

min :: Located a -> Located a -> Located a #

Hashable a => Hashable (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

hashWithSalt :: Int -> Located a -> Int #

hash :: Located a -> Int #

Symbolic a => Symbolic (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Located a -> Symbol #

Fixpoint a => Fixpoint (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

toFix :: Located a -> Doc #

simplify :: Located a -> Located a #

PPrint a => PPrint (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

pprintTidy :: Tidy -> Located a -> Doc #

pprintPrec :: Int -> Tidy -> Located a -> Doc #

Expression a => Expression (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Located a -> Expr #

Subable a => Subable (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

syms :: Located a -> [Symbol] #

substa :: (Symbol -> Symbol) -> Located a -> Located a #

substf :: (Symbol -> Expr) -> Located a -> Located a #

subst :: Subst -> Located a -> Located a #

subst1 :: Located a -> (Symbol, Expr) -> Located a #

Loc (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

srcSpan :: Located a -> SrcSpan #

Qualify a => Qualify (Located a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Located a -> Located a Source #

REq r => REq (Located r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Equality

Methods

(=*=) :: Located r -> Located r -> Bool Source #

Store a => Store (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

size :: Size (Located a) #

poke :: Located a -> Poke () #

peek :: Peek (Located a) #

Binary (Spec LocBareType LocSymbol) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

type Rep (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

type Rep (Located a) = D1 ('MetaData "Located" "Language.Fixpoint.Types.Spans" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "Loc" 'PrefixI 'True) (S1 ('MetaSel ('Just "loc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SourcePos) :*: (S1 ('MetaSel ('Just "locE") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SourcePos) :*: S1 ('MetaSel ('Just "val") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a))))

dummyLoc :: a -> Located a #

Symbols

type LocSymbol = Located Symbol #

Located Symbols -----------------------------------------------------

Default unknown name

isDummy :: Symbolic a => a -> Bool #

Bare Type Constructors and Variables

data BTyCon Source #

Constructors

BTyCon 

Fields

Instances

Instances details
Data BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BTyCon -> c BTyCon #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BTyCon #

toConstr :: BTyCon -> Constr #

dataTypeOf :: BTyCon -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BTyCon) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BTyCon) #

gmapT :: (forall b. Data b => b -> b) -> BTyCon -> BTyCon #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BTyCon -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BTyCon -> r #

gmapQ :: (forall d. Data d => d -> u) -> BTyCon -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> BTyCon -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BTyCon -> m BTyCon #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BTyCon -> m BTyCon #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BTyCon -> m BTyCon #

Generic BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep BTyCon :: Type -> Type #

Methods

from :: BTyCon -> Rep BTyCon x #

to :: Rep BTyCon x -> BTyCon #

Show BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Binary BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: BTyCon -> Put #

get :: Get BTyCon #

putList :: [BTyCon] -> Put #

NFData BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: BTyCon -> () #

Eq BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: BTyCon -> BTyCon -> Bool #

(/=) :: BTyCon -> BTyCon -> Bool #

Ord BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Hashable BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> BTyCon -> Int #

hash :: BTyCon -> Int #

Symbolic BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

symbol :: BTyCon -> Symbol #

Fixpoint BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

toFix :: BTyCon -> Doc #

simplify :: BTyCon -> BTyCon #

PPrint BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> BTyCon -> Doc #

pprintPrec :: Int -> Tidy -> BTyCon -> Doc #

Loc BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: BTyCon -> SrcSpan #

Qualify ModSpecs Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareMeasure Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

TyConable BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

FreeVar BTyCon BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

freeVars :: BTyCon -> [BTyVar]

SubsTy BTyVar BSort BSort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, BSort) -> BSort -> BSort Source #

SubsTy BTyVar BSort BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, BSort) -> BTyCon -> BTyCon Source #

SubsTy Symbol Symbol (BRType r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (Symbol, Symbol) -> BRType r -> BRType r Source #

SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

SubsTy BTyVar (RType BTyCon BTyVar ()) Sort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, RType BTyCon BTyVar ()) -> Sort -> Sort Source #

Binary (Spec LocBareType LocSymbol) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Reftable (RTProp BTyCon BTyVar (UReft Reft)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp BTyCon BTyVar ()) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RType BTyCon BTyVar (UReft Reft)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

type Rep BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep BTyCon = D1 ('MetaData "BTyCon" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "BTyCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "btc_tc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LocSymbol) :*: (S1 ('MetaSel ('Just "btc_class") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool) :*: S1 ('MetaSel ('Just "btc_prom") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool))))

newtype BTyVar Source #

Constructors

BTV Symbol 

Instances

Instances details
Data BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BTyVar -> c BTyVar #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BTyVar #

toConstr :: BTyVar -> Constr #

dataTypeOf :: BTyVar -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BTyVar) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BTyVar) #

gmapT :: (forall b. Data b => b -> b) -> BTyVar -> BTyVar #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BTyVar -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BTyVar -> r #

gmapQ :: (forall d. Data d => d -> u) -> BTyVar -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> BTyVar -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BTyVar -> m BTyVar #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BTyVar -> m BTyVar #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BTyVar -> m BTyVar #

IsString BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fromString :: String -> BTyVar #

Generic BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep BTyVar :: Type -> Type #

Methods

from :: BTyVar -> Rep BTyVar x #

to :: Rep BTyVar x -> BTyVar #

Show BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Binary BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: BTyVar -> Put #

get :: Get BTyVar #

putList :: [BTyVar] -> Put #

NFData BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: BTyVar -> () #

Eq BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: BTyVar -> BTyVar -> Bool #

(/=) :: BTyVar -> BTyVar -> Bool #

Ord BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Hashable BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> BTyVar -> Int #

hash :: BTyVar -> Int #

Symbolic BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

symbol :: BTyVar -> Symbol #

PPrint BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> BTyVar -> Doc #

pprintPrec :: Int -> Tidy -> BTyVar -> Doc #

Qualify ModSpecs Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareMeasure Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

FreeVar BTyCon BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

freeVars :: BTyCon -> [BTyVar]

SubsTy BTyVar BSort BSort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, BSort) -> BSort -> BSort Source #

SubsTy BTyVar BSort BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, BSort) -> BTyCon -> BTyCon Source #

SubsTy Symbol Symbol (BRType r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (Symbol, Symbol) -> BRType r -> BRType r Source #

SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

SubsTy BTyVar (RType BTyCon BTyVar ()) Sort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, RType BTyCon BTyVar ()) -> Sort -> Sort Source #

SubsTy BTyVar (RType c BTyVar ()) BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, RType c BTyVar ()) -> BTyVar -> BTyVar Source #

SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) Source #

Binary (Spec LocBareType LocSymbol) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Reftable (RTProp BTyCon BTyVar (UReft Reft)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp BTyCon BTyVar ()) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RType BTyCon BTyVar (UReft Reft)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

type Rep BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep BTyVar

Refined Type Constructors

data RTyCon Source #

Constructors

RTyCon TyCon ![RPVar] !TyConInfo 

Instances

Instances details
Data RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTyCon -> c RTyCon #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RTyCon #

toConstr :: RTyCon -> Constr #

dataTypeOf :: RTyCon -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RTyCon) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RTyCon) #

gmapT :: (forall b. Data b => b -> b) -> RTyCon -> RTyCon #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTyCon -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTyCon -> r #

gmapQ :: (forall d. Data d => d -> u) -> RTyCon -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RTyCon -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTyCon -> m RTyCon #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTyCon -> m RTyCon #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTyCon -> m RTyCon #

Monoid REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: REnv #

mappend :: REnv -> REnv -> REnv #

mconcat :: [REnv] -> REnv #

Semigroup REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(<>) :: REnv -> REnv -> REnv #

sconcat :: NonEmpty REnv -> REnv #

stimes :: Integral b => b -> REnv -> REnv #

Exception Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Generic RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep RTyCon :: Type -> Type #

Methods

from :: RTyCon -> Rep RTyCon x #

to :: Rep RTyCon x -> RTyCon #

Show Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

showsPrec :: Int -> Error -> ShowS #

show :: Error -> String #

showList :: [Error] -> ShowS #

Show RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

NFData REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: REnv -> () #

NFData RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: RTyCon -> () #

Eq RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: RTyCon -> RTyCon -> Bool #

(/=) :: RTyCon -> RTyCon -> Bool #

Hashable RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

hashWithSalt :: Int -> RTyCon -> Int #

hash :: RTyCon -> Int #

Symbolic RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

symbol :: RTyCon -> Symbol #

Fixpoint RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

toFix :: RTyCon -> Doc #

simplify :: RTyCon -> RTyCon #

PPrint Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

pprintTidy :: Tidy -> Error -> Doc #

pprintPrec :: Int -> Tidy -> Error -> Doc #

PPrint RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RTyCon -> Doc #

pprintPrec :: Int -> Tidy -> RTyCon -> Doc #

Qualify RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> RTyCon -> RTyCon Source #

Qualify SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

REq SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Equality

TyConable RTyCon Source #

TyConable Instances -------------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.Types

Result Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

FreeVar RTyCon RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

freeVars :: RTyCon -> [RTyVar]

SubsTy TyVar Type SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (TyVar, Type) -> SpecType -> SpecType Source #

SubsTy Symbol RSort Sort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (Symbol, RSort) -> Sort -> Sort Source #

SubsTy RTyVar RSort Sort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> Sort -> Sort Source #

SubsTy RTyVar RSort PrType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> PrType -> PrType Source #

SubsTy RTyVar RSort RSort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> RSort -> RSort Source #

SubsTy RTyVar RSort RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> RTyCon -> RTyCon Source #

SubsTy RTyVar RSort SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

SubsTy RTyVar RTyVar SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

SubsTy tv RSort Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, RSort) -> Predicate -> Predicate Source #

(Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Fresh

Methods

fresh :: m (RRType r) Source #

true :: Bool -> RRType r -> m (RRType r) Source #

refresh :: Bool -> RRType r -> m (RRType r) Source #

SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Exception [Error] Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

PPrint (CtxError SpecType) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Subable (RRProp Reft) Source #

Subable Instances -----------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Result [Error] Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Qualify (Measure SpecType DataCon) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Reftable (RTProp RTyCon RTyVar Reft) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp RTyCon RTyVar (UReft Reft)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp RTyCon RTyVar ()) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => Reftable (RType RTyCon RTyVar r) Source #

Reftable Instances -------------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.RefType

type Rep RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep RTyCon = D1 ('MetaData "RTyCon" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "RTyCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "rtc_tc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TyCon) :*: (S1 ('MetaSel ('Just "rtc_pvars") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RPVar]) :*: S1 ('MetaSel ('Just "rtc_info") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TyConInfo))))

data TyConInfo Source #

Co- and Contra-variance for TyCon --------------------------------

Indexes start from 0 and type or predicate arguments can be both covariant and contravaariant e.g., for the below Foo dataType

data Foo a b c d :: b - Prop, q :: Int -> Prop, r :: a -> Prop> = F (ar -> bp) | Q (c -> a) | G (Intq -> ar)

there will be:

varianceTyArgs = [Bivariant , Covariant, Contravatiant, Invariant] variancePsArgs = [Covariant, Contravatiant, Bivariant]

Constructors

TyConInfo 

Fields

Instances

Instances details
Data TyConInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TyConInfo -> c TyConInfo #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TyConInfo #

toConstr :: TyConInfo -> Constr #

dataTypeOf :: TyConInfo -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TyConInfo) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyConInfo) #

gmapT :: (forall b. Data b => b -> b) -> TyConInfo -> TyConInfo #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyConInfo -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyConInfo -> r #

gmapQ :: (forall d. Data d => d -> u) -> TyConInfo -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TyConInfo -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TyConInfo -> m TyConInfo #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TyConInfo -> m TyConInfo #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TyConInfo -> m TyConInfo #

Generic TyConInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep TyConInfo :: Type -> Type #

Show TyConInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Default TyConInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

def :: TyConInfo #

NFData TyConInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: TyConInfo -> () #

Qualify TyConInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

type Rep TyConInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep TyConInfo = D1 ('MetaData "TyConInfo" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "TyConInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "varianceTyArgs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 VarianceInfo) :*: (S1 ('MetaSel ('Just "variancePsArgs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 VarianceInfo) :*: S1 ('MetaSel ('Just "sizeFunction") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe SizeFun)))))

isEqType :: TyConable c => RType c t t1 -> Bool Source #

isRVar :: RType c tv r -> Bool Source #

isBool :: RType RTyCon t t1 -> Bool Source #

Accessors for RTyCon

Refinement Types

data RType c tv r Source #

Constructors

RVar 

Fields

RFun 

Fields

RAllT 

Fields

RAllP

"forall x y :: Nat, w :: Int . TYPE" ^^^^^^^^^^^^^^^^^^^ (rt_pvbind)

Fields

RApp

For example, in [a]- v > h}>, we apply (via RApp) * the RProp denoted by `{h -> v > h}` to * the RTyCon denoted by `[]`.

Fields

RAllE 

Fields

REx 

Fields

RExprArg (Located Expr)

For expression arguments to type aliases see testsposvector2.hs

RAppTy 

Fields

RRTy 

Fields

RHole r

let LH match against the Haskell type and add k-vars, e.g. `x:_` see testsposHoles.hs

Instances

Instances details
Monoid REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: REnv #

mappend :: REnv -> REnv -> REnv #

mconcat :: [REnv] -> REnv #

Semigroup REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(<>) :: REnv -> REnv -> REnv #

sconcat :: NonEmpty REnv -> REnv #

stimes :: Integral b => b -> REnv -> REnv #

Exception Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Show Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

showsPrec :: Int -> Error -> ShowS #

show :: Error -> String #

showList :: [Error] -> ShowS #

NFData REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: REnv -> () #

PPrint Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

pprintTidy :: Tidy -> Error -> Doc #

pprintPrec :: Int -> Tidy -> Error -> Doc #

Qualify ModSpecs Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareMeasure Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

REq SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Equality

Result Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

SubsTy TyVar Type SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (TyVar, Type) -> SpecType -> SpecType Source #

SubsTy Symbol RSort Sort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (Symbol, RSort) -> Sort -> Sort Source #

SubsTy BTyVar BSort BSort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, BSort) -> BSort -> BSort Source #

SubsTy BTyVar BSort BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, BSort) -> BTyCon -> BTyCon Source #

SubsTy RTyVar RSort Sort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> Sort -> Sort Source #

SubsTy RTyVar RSort PrType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> PrType -> PrType Source #

SubsTy RTyVar RSort RSort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> RSort -> RSort Source #

SubsTy RTyVar RSort RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> RTyCon -> RTyCon Source #

SubsTy RTyVar RSort SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

SubsTy RTyVar RTyVar SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

SubsTy tv RSort Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, RSort) -> Predicate -> Predicate Source #

SubsTy Symbol Symbol (BRType r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (Symbol, Symbol) -> BRType r -> BRType r Source #

SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, ty) -> RTProp c tv (UReft r) -> RTProp c tv (UReft r) Source #

(Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Fresh

Methods

fresh :: m (RRType r) Source #

true :: Bool -> RRType r -> m (RRType r) Source #

refresh :: Bool -> RRType r -> m (RRType r) Source #

SubsTy BTyVar (RType BTyCon BTyVar ()) Sort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, RType BTyCon BTyVar ()) -> Sort -> Sort Source #

SubsTy BTyVar (RType c BTyVar ()) BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, RType c BTyVar ()) -> BTyVar -> BTyVar Source #

SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) Source #

SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Exception [Error] Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

PPrint (CtxError SpecType) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Subable (RRProp Reft) Source #

Subable Instances -----------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Result [Error] Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Functor (RType c tv) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> RType c tv a -> RType c tv b #

(<$) :: a -> RType c tv b -> RType c tv a #

Show tv => Show (RTVU c tv) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> RTVU c tv -> ShowS #

show :: RTVU c tv -> String #

showList :: [RTVU c tv] -> ShowS #

Binary (Spec LocBareType LocSymbol) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

(PPrint r, Reftable r, PPrint t, PPrint (RType c tv r)) => PPrint (Ref t (RType c tv r)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Ref t (RType c tv r) -> Doc #

pprintPrec :: Int -> Tidy -> Ref t (RType c tv r) -> Doc #

Qualify (Measure SpecType DataCon) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

(Data c, Data tv, Data r) => Data (RType c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c0 (d -> b) -> d -> c0 b) -> (forall g. g -> c0 g) -> RType c tv r -> c0 (RType c tv r) #

gunfold :: (forall b r0. Data b => c0 (b -> r0) -> c0 r0) -> (forall r1. r1 -> c0 r1) -> Constr -> c0 (RType c tv r) #

toConstr :: RType c tv r -> Constr #

dataTypeOf :: RType c tv r -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (RType c tv r)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (RType c tv r)) #

gmapT :: (forall b. Data b => b -> b) -> RType c tv r -> RType c tv r #

gmapQl :: (r0 -> r' -> r0) -> r0 -> (forall d. Data d => d -> r') -> RType c tv r -> r0 #

gmapQr :: forall r0 r'. (r' -> r0 -> r0) -> r0 -> (forall d. Data d => d -> r') -> RType c tv r -> r0 #

gmapQ :: (forall d. Data d => d -> u) -> RType c tv r -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RType c tv r -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RType c tv r -> m (RType c tv r) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RType c tv r -> m (RType c tv r) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RType c tv r -> m (RType c tv r) #

(SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Monoid (RTProp c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

mempty :: RTProp c tv r #

mappend :: RTProp c tv r -> RTProp c tv r -> RTProp c tv r #

mconcat :: [RTProp c tv r] -> RTProp c tv r #

(SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Monoid (RType c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

mempty :: RType c tv r #

mappend :: RType c tv r -> RType c tv r -> RType c tv r #

mconcat :: [RType c tv r] -> RType c tv r #

(SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Semigroup (RTProp c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

(<>) :: RTProp c tv r -> RTProp c tv r -> RTProp c tv r #

sconcat :: NonEmpty (RTProp c tv r) -> RTProp c tv r #

stimes :: Integral b => b -> RTProp c tv r -> RTProp c tv r #

(SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Semigroup (RType c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

(<>) :: RType c tv r -> RType c tv r -> RType c tv r #

sconcat :: NonEmpty (RType c tv r) -> RType c tv r #

stimes :: Integral b => b -> RType c tv r -> RType c tv r #

Generic (RType c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (RType c tv r) :: Type -> Type #

Methods

from :: RType c tv r -> Rep (RType c tv r) x #

to :: Rep (RType c tv r) x -> RType c tv r #

PPrint (RTProp c tv r) => Show (RTProp c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

showsPrec :: Int -> RTProp c tv r -> ShowS #

show :: RTProp c tv r -> String #

showList :: [RTProp c tv r] -> ShowS #

PPrint (RType c tv r) => Show (RType c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

showsPrec :: Int -> RType c tv r -> ShowS #

show :: RType c tv r -> String #

showList :: [RType c tv r] -> ShowS #

(Binary c, Binary tv, Binary r) => Binary (RType c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: RType c tv r -> Put #

get :: Get (RType c tv r) #

putList :: [RType c tv r] -> Put #

(NFData c, NFData tv, NFData r) => NFData (RType c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: RType c tv r -> () #

(Eq c, Eq tv, Hashable tv, PPrint tv, TyConable c, PPrint c, Reftable (RTProp c tv ())) => Eq (RType c tv ()) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

(==) :: RType c tv () -> RType c tv () -> Bool #

(/=) :: RType c tv () -> RType c tv () -> Bool #

(Eq tv, Eq r, Eq c) => Eq (RType c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: RType c tv r -> RType c tv r -> Bool #

(/=) :: RType c tv r -> RType c tv r -> Bool #

(Hashable tv, Hashable r, Hashable c) => Hashable (RType c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> RType c tv r -> Int #

hash :: RType c tv r -> Int #

OkRT c tv r => PPrint (RType c tv r) Source #

Pretty Printing RefType ---------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> RType c tv r -> Doc #

pprintPrec :: Int -> Tidy -> RType c tv r -> Doc #

Reftable (RTProp BTyCon BTyVar (UReft Reft)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp BTyCon BTyVar ()) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp RTyCon RTyVar Reft) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp RTyCon RTyVar (UReft Reft)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp RTyCon RTyVar ()) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RType BTyCon BTyVar (UReft Reft)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => Reftable (RType RTyCon RTyVar r) Source #

Reftable Instances -------------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.RefType

(Reftable r, TyConable c) => Subable (RTProp c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

syms :: RTProp c tv r -> [Symbol] #

substa :: (Symbol -> Symbol) -> RTProp c tv r -> RTProp c tv r #

substf :: (Symbol -> Expr) -> RTProp c tv r -> RTProp c tv r #

subst :: Subst -> RTProp c tv r -> RTProp c tv r #

subst1 :: RTProp c tv r -> (Symbol, Expr) -> RTProp c tv r #

(Subable r, Reftable r, TyConable c) => Subable (RType c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

syms :: RType c tv r -> [Symbol] #

substa :: (Symbol -> Symbol) -> RType c tv r -> RType c tv r #

substf :: (Symbol -> Expr) -> RType c tv r -> RType c tv r #

subst :: Subst -> RType c tv r -> RType c tv r #

subst1 :: RType c tv r -> (Symbol, Expr) -> RType c tv r #

Corecursive (RType c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Elaborate

Methods

embed :: Base (RType c tv r) (RType c tv r) -> RType c tv r #

ana :: (a -> Base (RType c tv r) a) -> a -> RType c tv r #

apo :: (a -> Base (RType c tv r) (Either (RType c tv r) a)) -> a -> RType c tv r #

postpro :: Recursive (RType c tv r) => (forall b. Base (RType c tv r) b -> Base (RType c tv r) b) -> (a -> Base (RType c tv r) a) -> a -> RType c tv r #

gpostpro :: (Recursive (RType c tv r), Monad m) => (forall b. m (Base (RType c tv r) b) -> Base (RType c tv r) (m b)) -> (forall c0. Base (RType c tv r) c0 -> Base (RType c tv r) c0) -> (a -> Base (RType c tv r) (m a)) -> a -> RType c tv r #

Recursive (RType c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Elaborate

Methods

project :: RType c tv r -> Base (RType c tv r) (RType c tv r) #

cata :: (Base (RType c tv r) a -> a) -> RType c tv r -> a #

para :: (Base (RType c tv r) (RType c tv r, a) -> a) -> RType c tv r -> a #

gpara :: (Corecursive (RType c tv r), Comonad w) => (forall b. Base (RType c tv r) (w b) -> w (Base (RType c tv r) b)) -> (Base (RType c tv r) (EnvT (RType c tv r) w a) -> a) -> RType c tv r -> a #

prepro :: Corecursive (RType c tv r) => (forall b. Base (RType c tv r) b -> Base (RType c tv r) b) -> (Base (RType c tv r) a -> a) -> RType c tv r -> a #

gprepro :: (Corecursive (RType c tv r), Comonad w) => (forall b. Base (RType c tv r) (w b) -> w (Base (RType c tv r) b)) -> (forall c0. Base (RType c tv r) c0 -> Base (RType c tv r) c0) -> (Base (RType c tv r) (w a) -> a) -> RType c tv r -> a #

type Rep (RType c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (RType c tv r)
type Base (RType c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Elaborate

type Base (RType c tv r)

data Ref τ t Source #

Ref describes `Prop τ` and HProp arguments applied to type constructors. For example, in [a]- v > h}>, we apply (via RApp) * the RProp denoted by `{h -> v > h}` to * the RTyCon denoted by `[]`. Thus, Ref is used for abstract-predicate (arguments) that are associated with _type constructors_ i.e. whose semantics are _dependent upon_ the data-type. In contrast, the Predicate argument in ur_pred in the UReft applies directly to any type and has semantics _independent of_ the data-type.

Constructors

RProp 

Fields

Instances

Instances details
SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, ty) -> RTProp c tv (UReft r) -> RTProp c tv (UReft r) Source #

Functor (Ref τ) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> Ref τ a -> Ref τ b #

(<$) :: a -> Ref τ b -> Ref τ a #

Subable (RRProp Reft) Source #

Subable Instances -----------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.RefType

(Data τ, Data t) => Data (Ref τ t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ref τ t -> c (Ref τ t) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Ref τ t) #

toConstr :: Ref τ t -> Constr #

dataTypeOf :: Ref τ t -> DataType #

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Ref τ t)) #

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Ref τ t)) #

gmapT :: (forall b. Data b => b -> b) -> Ref τ t -> Ref τ t #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ref τ t -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ref τ t -> r #

gmapQ :: (forall d. Data d => d -> u) -> Ref τ t -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Ref τ t -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ref τ t -> m (Ref τ t) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ref τ t -> m (Ref τ t) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ref τ t -> m (Ref τ t) #

Generic (Ref τ t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (Ref τ t) :: Type -> Type #

Methods

from :: Ref τ t -> Rep (Ref τ t) x #

to :: Rep (Ref τ t) x -> Ref τ t #

(Binary τ, Binary t) => Binary (Ref τ t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: Ref τ t -> Put #

get :: Get (Ref τ t) #

putList :: [Ref τ t] -> Put #

(NFData τ, NFData t) => NFData (Ref τ t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: Ref τ t -> () #

(Eq τ, Eq t) => Eq (Ref τ t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: Ref τ t -> Ref τ t -> Bool #

(/=) :: Ref τ t -> Ref τ t -> Bool #

(Hashable τ, Hashable t) => Hashable (Ref τ t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> Ref τ t -> Int #

hash :: Ref τ t -> Int #

(PPrint r, Reftable r, PPrint t, PPrint (RType c tv r)) => PPrint (Ref t (RType c tv r)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Ref t (RType c tv r) -> Doc #

pprintPrec :: Int -> Tidy -> Ref t (RType c tv r) -> Doc #

REq t2 => REq (Ref t1 t2) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Equality

Methods

(=*=) :: Ref t1 t2 -> Ref t1 t2 -> Bool Source #

(SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Monoid (RTProp c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

mempty :: RTProp c tv r #

mappend :: RTProp c tv r -> RTProp c tv r -> RTProp c tv r #

mconcat :: [RTProp c tv r] -> RTProp c tv r #

(SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Semigroup (RTProp c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

(<>) :: RTProp c tv r -> RTProp c tv r -> RTProp c tv r #

sconcat :: NonEmpty (RTProp c tv r) -> RTProp c tv r #

stimes :: Integral b => b -> RTProp c tv r -> RTProp c tv r #

PPrint (RTProp c tv r) => Show (RTProp c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

showsPrec :: Int -> RTProp c tv r -> ShowS #

show :: RTProp c tv r -> String #

showList :: [RTProp c tv r] -> ShowS #

Reftable (RTProp BTyCon BTyVar (UReft Reft)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp BTyCon BTyVar ()) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp RTyCon RTyVar Reft) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp RTyCon RTyVar (UReft Reft)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp RTyCon RTyVar ()) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

(Reftable r, TyConable c) => Subable (RTProp c tv r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

syms :: RTProp c tv r -> [Symbol] #

substa :: (Symbol -> Symbol) -> RTProp c tv r -> RTProp c tv r #

substf :: (Symbol -> Expr) -> RTProp c tv r -> RTProp c tv r #

subst :: Subst -> RTProp c tv r -> RTProp c tv r #

subst1 :: RTProp c tv r -> (Symbol, Expr) -> RTProp c tv r #

type Rep (Ref τ t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (Ref τ t)

type RTProp c tv r = Ref (RType c tv ()) (RType c tv r) Source #

RTProp is a convenient alias for Ref that will save a bunch of typing. In general, perhaps we need not expose Ref directly at all.

rPropP :: [(Symbol, τ)] -> r -> Ref τ (RType c tv r) Source #

newtype RTyVar Source #

Constructors

RTV TyVar 

Instances

Instances details
Data RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTyVar -> c RTyVar #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RTyVar #

toConstr :: RTyVar -> Constr #

dataTypeOf :: RTyVar -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RTyVar) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RTyVar) #

gmapT :: (forall b. Data b => b -> b) -> RTyVar -> RTyVar #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTyVar -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTyVar -> r #

gmapQ :: (forall d. Data d => d -> u) -> RTyVar -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RTyVar -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTyVar -> m RTyVar #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTyVar -> m RTyVar #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTyVar -> m RTyVar #

Monoid REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: REnv #

mappend :: REnv -> REnv -> REnv #

mconcat :: [REnv] -> REnv #

Semigroup REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(<>) :: REnv -> REnv -> REnv #

sconcat :: NonEmpty REnv -> REnv #

stimes :: Integral b => b -> REnv -> REnv #

Exception Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Generic RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep RTyVar :: Type -> Type #

Methods

from :: RTyVar -> Rep RTyVar x #

to :: Rep RTyVar x -> RTyVar #

Show Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

showsPrec :: Int -> Error -> ShowS #

show :: Error -> String #

showList :: [Error] -> ShowS #

Show RTyVar Source #

Printing Refinement Types -------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.RefType

NFData REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: REnv -> () #

NFData RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: RTyVar -> () #

Eq RTyVar Source #

Wrappers for GHC Type Elements --------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

(==) :: RTyVar -> RTyVar -> Bool #

(/=) :: RTyVar -> RTyVar -> Bool #

Ord RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Hashable RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

hashWithSalt :: Int -> RTyVar -> Int #

hash :: RTyVar -> Int #

Symbolic RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

symbol :: RTyVar -> Symbol #

PPrint Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

pprintTidy :: Tidy -> Error -> Doc #

pprintPrec :: Int -> Tidy -> Error -> Doc #

PPrint RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RTyVar -> Doc #

pprintPrec :: Int -> Tidy -> RTyVar -> Doc #

Qualify SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

REq SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Equality

Result Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

FreeVar RTyCon RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

freeVars :: RTyCon -> [RTyVar]

SubsTy TyVar Type SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (TyVar, Type) -> SpecType -> SpecType Source #

SubsTy Symbol RSort Sort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (Symbol, RSort) -> Sort -> Sort Source #

SubsTy RTyVar RSort Sort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> Sort -> Sort Source #

SubsTy RTyVar RSort PrType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> PrType -> PrType Source #

SubsTy RTyVar RSort RSort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> RSort -> RSort Source #

SubsTy RTyVar RSort RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> RTyCon -> RTyCon Source #

SubsTy RTyVar RSort SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

SubsTy RTyVar RTyVar SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

SubsTy tv RSort Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, RSort) -> Predicate -> Predicate Source #

(Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Fresh

Methods

fresh :: m (RRType r) Source #

true :: Bool -> RRType r -> m (RRType r) Source #

refresh :: Bool -> RRType r -> m (RRType r) Source #

SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Exception [Error] Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

PPrint (CtxError SpecType) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Subable (RRProp Reft) Source #

Subable Instances -----------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Result [Error] Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Qualify (Measure SpecType DataCon) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Reftable (RTProp RTyCon RTyVar Reft) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp RTyCon RTyVar (UReft Reft)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp RTyCon RTyVar ()) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => Reftable (RType RTyCon RTyVar r) Source #

Reftable Instances -------------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.RefType

type Rep RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep RTyVar = D1 ('MetaData "RTyVar" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'True) (C1 ('MetaCons "RTV" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TyVar)))

data RTAlias x a Source #

Refinement Type Aliases

Constructors

RTA 

Fields

  • rtName :: Symbol

    name of the alias

  • rtTArgs :: [x]

    type parameters

  • rtVArgs :: [Symbol]

    value parameters

  • rtBody :: a

    what the alias expands to , rtMod :: !ModName -- ^ module where alias was defined

Instances

Instances details
Functor (RTAlias x) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> RTAlias x a -> RTAlias x b #

(<$) :: a -> RTAlias x b -> RTAlias x a #

(Data x, Data a) => Data (RTAlias x a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTAlias x a -> c (RTAlias x a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RTAlias x a) #

toConstr :: RTAlias x a -> Constr #

dataTypeOf :: RTAlias x a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RTAlias x a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RTAlias x a)) #

gmapT :: (forall b. Data b => b -> b) -> RTAlias x a -> RTAlias x a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTAlias x a -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTAlias x a -> r #

gmapQ :: (forall d. Data d => d -> u) -> RTAlias x a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RTAlias x a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTAlias x a -> m (RTAlias x a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTAlias x a -> m (RTAlias x a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTAlias x a -> m (RTAlias x a) #

Generic (RTAlias x a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (RTAlias x a) :: Type -> Type #

Methods

from :: RTAlias x a -> Rep (RTAlias x a) x0 #

to :: Rep (RTAlias x a) x0 -> RTAlias x a #

(Show tv, Show ty) => Show (RTAlias tv ty) Source #

Auxiliary Stuff Used Elsewhere ---------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

showsPrec :: Int -> RTAlias tv ty -> ShowS #

show :: RTAlias tv ty -> String #

showList :: [RTAlias tv ty] -> ShowS #

(Binary x, Binary a) => Binary (RTAlias x a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: RTAlias x a -> Put #

get :: Get (RTAlias x a) #

putList :: [RTAlias x a] -> Put #

(Eq x, Eq a) => Eq (RTAlias x a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: RTAlias x a -> RTAlias x a -> Bool #

(/=) :: RTAlias x a -> RTAlias x a -> Bool #

(Hashable x, Hashable a) => Hashable (RTAlias x a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> RTAlias x a -> Int #

hash :: RTAlias x a -> Int #

(PPrint tv, PPrint ty) => PPrint (RTAlias tv ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> RTAlias tv ty -> Doc #

pprintPrec :: Int -> Tidy -> RTAlias tv ty -> Doc #

Qualify a => Qualify (RTAlias Symbol a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

type Rep (RTAlias x a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (RTAlias x a)

type OkRT c tv r = (TyConable c, PPrint tv, PPrint c, PPrint r, Reftable r, Reftable (RTProp c tv ()), Reftable (RTProp c tv r), Eq c, Eq tv, Hashable tv) Source #

lmapEAlias :: LMap -> Located (RTAlias Symbol Expr) Source #

Worlds

data HSeg t Source #

Constructors

HBind 

Fields

HVar UsedPVar 

Instances

Instances details
Data t => Data (HSeg t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HSeg t -> c (HSeg t) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (HSeg t) #

toConstr :: HSeg t -> Constr #

dataTypeOf :: HSeg t -> DataType #

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (HSeg t)) #

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (HSeg t)) #

gmapT :: (forall b. Data b => b -> b) -> HSeg t -> HSeg t #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HSeg t -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HSeg t -> r #

gmapQ :: (forall d. Data d => d -> u) -> HSeg t -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> HSeg t -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HSeg t -> m (HSeg t) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HSeg t -> m (HSeg t) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HSeg t -> m (HSeg t) #

Generic (HSeg t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (HSeg t) :: Type -> Type #

Methods

from :: HSeg t -> Rep (HSeg t) x #

to :: Rep (HSeg t) x -> HSeg t #

type Rep (HSeg t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (HSeg t)

newtype World t Source #

A World is a Separation Logic predicate that is essentially a sequence of binders that satisfies two invariants (TODO:LIQUID): 1. Each `hs_addr :: Symbol` appears at most once, 2. There is at most one HVar in a list.

Constructors

World [HSeg t] 

Instances

Instances details
Data t => Data (World t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> World t -> c (World t) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (World t) #

toConstr :: World t -> Constr #

dataTypeOf :: World t -> DataType #

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (World t)) #

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (World t)) #

gmapT :: (forall b. Data b => b -> b) -> World t -> World t #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> World t -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> World t -> r #

gmapQ :: (forall d. Data d => d -> u) -> World t -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> World t -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> World t -> m (World t) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> World t -> m (World t) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> World t -> m (World t) #

Generic (World t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (World t) :: Type -> Type #

Methods

from :: World t -> Rep (World t) x #

to :: Rep (World t) x -> World t #

type Rep (World t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (World t) = D1 ('MetaData "World" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'True) (C1 ('MetaCons "World" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [HSeg t])))

Classes describing operations on RTypes

class Eq c => TyConable c where Source #

Minimal complete definition

isFun, isList, isTuple, ppTycon

Instances

Instances details
TyConable TyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

TyConable LocSymbol Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

TyConable BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

TyConable RTyCon Source #

TyConable Instances -------------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.Types

class SubsTy tv ty a where Source #

Methods

subt :: (tv, ty) -> a -> a Source #

Instances

Instances details
SubsTy TyVar Type SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (TyVar, Type) -> SpecType -> SpecType Source #

SubsTy Symbol RSort Sort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (Symbol, RSort) -> Sort -> Sort Source #

SubsTy BTyVar BSort BSort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, BSort) -> BSort -> BSort Source #

SubsTy BTyVar BSort BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, BSort) -> BTyCon -> BTyCon Source #

SubsTy RTyVar RSort Sort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> Sort -> Sort Source #

SubsTy RTyVar RSort PrType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> PrType -> PrType Source #

SubsTy RTyVar RSort RSort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> RSort -> RSort Source #

SubsTy RTyVar RSort RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> RTyCon -> RTyCon Source #

SubsTy RTyVar RSort SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

SubsTy RTyVar RTyVar SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

SubsTy tv RSort Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, RSort) -> Predicate -> Predicate Source #

SubsTy tv ty Symbol Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, ty) -> Symbol -> Symbol Source #

SubsTy tv ty Sort => SubsTy tv ty Expr Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, ty) -> Expr -> Expr Source #

SubsTy tv ty Expr => SubsTy tv ty Reft Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, ty) -> Reft -> Reft Source #

SubsTy tv ty () Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, ty) -> () -> () Source #

SubsTy Symbol Symbol (BRType r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (Symbol, Symbol) -> BRType r -> BRType r Source #

SubsTy tv ty ty => SubsTy tv ty (PVKind ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, ty) -> PVKind ty -> PVKind ty Source #

SubsTy tv ty ty => SubsTy tv ty (PVar ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, ty) -> PVar ty -> PVar ty Source #

SubsTy tv ty r => SubsTy tv ty (UReft r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, ty) -> UReft r -> UReft r Source #

(SubsTy tv ty a, SubsTy tv ty b) => SubsTy tv ty (a, b) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, ty) -> (a, b) -> (a, b) Source #

SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, ty) -> RTProp c tv (UReft r) -> RTProp c tv (UReft r) Source #

SubsTy BTyVar (RType BTyCon BTyVar ()) Sort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, RType BTyCon BTyVar ()) -> Sort -> Sort Source #

SubsTy BTyVar (RType c BTyVar ()) BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, RType c BTyVar ()) -> BTyVar -> BTyVar Source #

SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) Source #

SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Type Variables

data RTVar tv s Source #

Constructors

RTVar 

Fields

Instances

Instances details
SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (BTyVar, RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) Source #

SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

(Data tv, Data s) => Data (RTVar tv s) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTVar tv s -> c (RTVar tv s) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RTVar tv s) #

toConstr :: RTVar tv s -> Constr #

dataTypeOf :: RTVar tv s -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RTVar tv s)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RTVar tv s)) #

gmapT :: (forall b. Data b => b -> b) -> RTVar tv s -> RTVar tv s #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTVar tv s -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTVar tv s -> r #

gmapQ :: (forall d. Data d => d -> u) -> RTVar tv s -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RTVar tv s -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTVar tv s -> m (RTVar tv s) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTVar tv s -> m (RTVar tv s) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTVar tv s -> m (RTVar tv s) #

Generic (RTVar tv s) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (RTVar tv s) :: Type -> Type #

Methods

from :: RTVar tv s -> Rep (RTVar tv s) x #

to :: Rep (RTVar tv s) x -> RTVar tv s #

Show tv => Show (RTVU c tv) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> RTVU c tv -> ShowS #

show :: RTVU c tv -> String #

showList :: [RTVU c tv] -> ShowS #

(Binary tv, Binary s) => Binary (RTVar tv s) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: RTVar tv s -> Put #

get :: Get (RTVar tv s) #

putList :: [RTVar tv s] -> Put #

(NFData tv, NFData s) => NFData (RTVar tv s) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: RTVar tv s -> () #

Eq tv => Eq (RTVar tv s) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: RTVar tv s -> RTVar tv s -> Bool #

(/=) :: RTVar tv s -> RTVar tv s -> Bool #

(Hashable tv, Hashable s) => Hashable (RTVar tv s) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> RTVar tv s -> Int #

hash :: RTVar tv s -> Int #

PPrint v => PPrint (RTVar v s) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RTVar v s -> Doc #

pprintPrec :: Int -> Tidy -> RTVar v s -> Doc #

type Rep (RTVar tv s) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (RTVar tv s) = D1 ('MetaData "RTVar" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "RTVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "ty_var_value") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 tv) :*: S1 ('MetaSel ('Just "ty_var_info") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RTVInfo s))))

data RTVInfo s Source #

Constructors

RTVNoInfo 

Fields

RTVInfo 

Fields

Instances

Instances details
Functor RTVInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> RTVInfo a -> RTVInfo b #

(<$) :: a -> RTVInfo b -> RTVInfo a #

Data s => Data (RTVInfo s) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTVInfo s -> c (RTVInfo s) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RTVInfo s) #

toConstr :: RTVInfo s -> Constr #

dataTypeOf :: RTVInfo s -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RTVInfo s)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RTVInfo s)) #

gmapT :: (forall b. Data b => b -> b) -> RTVInfo s -> RTVInfo s #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTVInfo s -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTVInfo s -> r #

gmapQ :: (forall d. Data d => d -> u) -> RTVInfo s -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RTVInfo s -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTVInfo s -> m (RTVInfo s) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTVInfo s -> m (RTVInfo s) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTVInfo s -> m (RTVInfo s) #

Generic (RTVInfo s) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (RTVInfo s) :: Type -> Type #

Methods

from :: RTVInfo s -> Rep (RTVInfo s) x #

to :: Rep (RTVInfo s) x -> RTVInfo s #

Binary s => Binary (RTVInfo s) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: RTVInfo s -> Put #

get :: Get (RTVInfo s) #

putList :: [RTVInfo s] -> Put #

NFData s => NFData (RTVInfo s) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: RTVInfo s -> () #

Eq s => Eq (RTVInfo s) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: RTVInfo s -> RTVInfo s -> Bool #

(/=) :: RTVInfo s -> RTVInfo s -> Bool #

Hashable s => Hashable (RTVInfo s) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> RTVInfo s -> Int #

hash :: RTVInfo s -> Int #

type Rep (RTVInfo s) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (RTVInfo s)

makeRTVar :: tv -> RTVar tv s Source #

mapTyVarValue :: (tv1 -> tv2) -> RTVar tv1 s -> RTVar tv2 s Source #

dropTyVarInfo :: RTVar tv s1 -> RTVar tv s2 Source #

rTVarToBind :: RTVar RTyVar s -> Maybe (Symbol, s) Source #

setRtvPol :: RTVar tv a -> Bool -> RTVar tv a Source #

Predicate Variables

data PVar t Source #

Abstract Predicate Variables ----------------------------------

Constructors

PV 

Fields

Instances

Instances details
Functor PVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> PVar a -> PVar b #

(<$) :: a -> PVar b -> PVar a #

Subable UsedPVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

SubsTy tv ty ty => SubsTy tv ty (PVar ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, ty) -> PVar ty -> PVar ty Source #

Data t => Data (PVar t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PVar t -> c (PVar t) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (PVar t) #

toConstr :: PVar t -> Constr #

dataTypeOf :: PVar t -> DataType #

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (PVar t)) #

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (PVar t)) #

gmapT :: (forall b. Data b => b -> b) -> PVar t -> PVar t #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PVar t -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PVar t -> r #

gmapQ :: (forall d. Data d => d -> u) -> PVar t -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PVar t -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PVar t -> m (PVar t) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PVar t -> m (PVar t) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PVar t -> m (PVar t) #

Generic (PVar t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (PVar t) :: Type -> Type #

Methods

from :: PVar t -> Rep (PVar t) x #

to :: Rep (PVar t) x -> PVar t #

Show t => Show (PVar t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> PVar t -> ShowS #

show :: PVar t -> String #

showList :: [PVar t] -> ShowS #

Binary t => Binary (PVar t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: PVar t -> Put #

get :: Get (PVar t) #

putList :: [PVar t] -> Put #

NFData t => NFData (PVar t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: PVar t -> () #

Eq (PVar t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: PVar t -> PVar t -> Bool #

(/=) :: PVar t -> PVar t -> Bool #

Ord (PVar t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

compare :: PVar t -> PVar t -> Ordering #

(<) :: PVar t -> PVar t -> Bool #

(<=) :: PVar t -> PVar t -> Bool #

(>) :: PVar t -> PVar t -> Bool #

(>=) :: PVar t -> PVar t -> Bool #

max :: PVar t -> PVar t -> PVar t #

min :: PVar t -> PVar t -> PVar t #

Hashable (PVar a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> PVar a -> Int #

hash :: PVar a -> Int #

PPrint (PVar a) Source #

F.PPrint -----------------------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> PVar a -> Doc #

pprintPrec :: Int -> Tidy -> PVar a -> Doc #

type Rep (PVar t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (PVar t)

pvType :: PVar t -> t Source #

data PVKind t Source #

Constructors

PVProp t 
PVHProp 

Instances

Instances details
Foldable PVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fold :: Monoid m => PVKind m -> m #

foldMap :: Monoid m => (a -> m) -> PVKind a -> m #

foldMap' :: Monoid m => (a -> m) -> PVKind a -> m #

foldr :: (a -> b -> b) -> b -> PVKind a -> b #

foldr' :: (a -> b -> b) -> b -> PVKind a -> b #

foldl :: (b -> a -> b) -> b -> PVKind a -> b #

foldl' :: (b -> a -> b) -> b -> PVKind a -> b #

foldr1 :: (a -> a -> a) -> PVKind a -> a #

foldl1 :: (a -> a -> a) -> PVKind a -> a #

toList :: PVKind a -> [a] #

null :: PVKind a -> Bool #

length :: PVKind a -> Int #

elem :: Eq a => a -> PVKind a -> Bool #

maximum :: Ord a => PVKind a -> a #

minimum :: Ord a => PVKind a -> a #

sum :: Num a => PVKind a -> a #

product :: Num a => PVKind a -> a #

Traversable PVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

traverse :: Applicative f => (a -> f b) -> PVKind a -> f (PVKind b) #

sequenceA :: Applicative f => PVKind (f a) -> f (PVKind a) #

mapM :: Monad m => (a -> m b) -> PVKind a -> m (PVKind b) #

sequence :: Monad m => PVKind (m a) -> m (PVKind a) #

Functor PVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> PVKind a -> PVKind b #

(<$) :: a -> PVKind b -> PVKind a #

SubsTy tv ty ty => SubsTy tv ty (PVKind ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, ty) -> PVKind ty -> PVKind ty Source #

Data t => Data (PVKind t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PVKind t -> c (PVKind t) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (PVKind t) #

toConstr :: PVKind t -> Constr #

dataTypeOf :: PVKind t -> DataType #

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (PVKind t)) #

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (PVKind t)) #

gmapT :: (forall b. Data b => b -> b) -> PVKind t -> PVKind t #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PVKind t -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PVKind t -> r #

gmapQ :: (forall d. Data d => d -> u) -> PVKind t -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PVKind t -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PVKind t -> m (PVKind t) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PVKind t -> m (PVKind t) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PVKind t -> m (PVKind t) #

Generic (PVKind t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (PVKind t) :: Type -> Type #

Methods

from :: PVKind t -> Rep (PVKind t) x #

to :: Rep (PVKind t) x -> PVKind t #

Show t => Show (PVKind t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> PVKind t -> ShowS #

show :: PVKind t -> String #

showList :: [PVKind t] -> ShowS #

Binary a => Binary (PVKind a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: PVKind a -> Put #

get :: Get (PVKind a) #

putList :: [PVKind a] -> Put #

NFData a => NFData (PVKind a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: PVKind a -> () #

type Rep (PVKind t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (PVKind t) = D1 ('MetaData "PVKind" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "PVProp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "PVHProp" 'PrefixI 'False) (U1 :: Type -> Type))

newtype Predicate Source #

Constructors

Pr [UsedPVar] 

Instances

Instances details
Data Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Predicate -> c Predicate #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Predicate #

toConstr :: Predicate -> Constr #

dataTypeOf :: Predicate -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Predicate) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Predicate) #

gmapT :: (forall b. Data b => b -> b) -> Predicate -> Predicate #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Predicate -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Predicate -> r #

gmapQ :: (forall d. Data d => d -> u) -> Predicate -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Predicate -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Predicate -> m Predicate #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Predicate -> m Predicate #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Predicate -> m Predicate #

Monoid Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Semigroup Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Generic Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep Predicate :: Type -> Type #

Show Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Binary Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

NFData Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: Predicate -> () #

Eq Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Hashable Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

PPrint Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Reftable Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Subable Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

SubsTy RTyVar RSort PrType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> PrType -> PrType Source #

SubsTy tv RSort Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, RSort) -> Predicate -> Predicate Source #

type Rep Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep Predicate = D1 ('MetaData "Predicate" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'True) (C1 ('MetaCons "Pr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [UsedPVar])))

Refinements

data UReft r Source #

Constructors

MkUReft 

Fields

Instances

Instances details
Foldable UReft Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fold :: Monoid m => UReft m -> m #

foldMap :: Monoid m => (a -> m) -> UReft a -> m #

foldMap' :: Monoid m => (a -> m) -> UReft a -> m #

foldr :: (a -> b -> b) -> b -> UReft a -> b #

foldr' :: (a -> b -> b) -> b -> UReft a -> b #

foldl :: (b -> a -> b) -> b -> UReft a -> b #

foldl' :: (b -> a -> b) -> b -> UReft a -> b #

foldr1 :: (a -> a -> a) -> UReft a -> a #

foldl1 :: (a -> a -> a) -> UReft a -> a #

toList :: UReft a -> [a] #

null :: UReft a -> Bool #

length :: UReft a -> Int #

elem :: Eq a => a -> UReft a -> Bool #

maximum :: Ord a => UReft a -> a #

minimum :: Ord a => UReft a -> a #

sum :: Num a => UReft a -> a #

product :: Num a => UReft a -> a #

Traversable UReft Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

traverse :: Applicative f => (a -> f b) -> UReft a -> f (UReft b) #

sequenceA :: Applicative f => UReft (f a) -> f (UReft a) #

mapM :: Monad m => (a -> m b) -> UReft a -> m (UReft b) #

sequence :: Monad m => UReft (m a) -> m (UReft a) #

Functor UReft Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> UReft a -> UReft b #

(<$) :: a -> UReft b -> UReft a #

Monoid REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: REnv #

mappend :: REnv -> REnv -> REnv #

mconcat :: [REnv] -> REnv #

Semigroup REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(<>) :: REnv -> REnv -> REnv #

sconcat :: NonEmpty REnv -> REnv #

stimes :: Integral b => b -> REnv -> REnv #

Exception Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Show Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

showsPrec :: Int -> Error -> ShowS #

show :: Error -> String #

showList :: [Error] -> ShowS #

NFData REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: REnv -> () #

PPrint Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

pprintTidy :: Tidy -> Error -> Doc #

pprintPrec :: Int -> Tidy -> Error -> Doc #

Qualify ModSpecs Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareMeasure Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify RReft Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> RReft -> RReft Source #

Qualify SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

REq SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Equality

Result Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Freshable m Integer => Freshable m RReft Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Fresh

Methods

fresh :: m RReft Source #

true :: Bool -> RReft -> m RReft Source #

refresh :: Bool -> RReft -> m RReft Source #

SubsTy TyVar Type SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (TyVar, Type) -> SpecType -> SpecType Source #

SubsTy RTyVar RSort SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

SubsTy RTyVar RTyVar SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

SubsTy tv ty r => SubsTy tv ty (UReft r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, ty) -> UReft r -> UReft r Source #

(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, ty) -> RTProp c tv (UReft r) -> RTProp c tv (UReft r) Source #

Data r => Data (UReft r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UReft r -> c (UReft r) #

gunfold :: (forall b r0. Data b => c (b -> r0) -> c r0) -> (forall r1. r1 -> c r1) -> Constr -> c (UReft r) #

toConstr :: UReft r -> Constr #

dataTypeOf :: UReft r -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (UReft r)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (UReft r)) #

gmapT :: (forall b. Data b => b -> b) -> UReft r -> UReft r #

gmapQl :: (r0 -> r' -> r0) -> r0 -> (forall d. Data d => d -> r') -> UReft r -> r0 #

gmapQr :: forall r0 r'. (r' -> r0 -> r0) -> r0 -> (forall d. Data d => d -> r') -> UReft r -> r0 #

gmapQ :: (forall d. Data d => d -> u) -> UReft r -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> UReft r -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UReft r -> m (UReft r) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UReft r -> m (UReft r) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UReft r -> m (UReft r) #

Monoid a => Monoid (UReft a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: UReft a #

mappend :: UReft a -> UReft a -> UReft a #

mconcat :: [UReft a] -> UReft a #

Semigroup a => Semigroup (UReft a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(<>) :: UReft a -> UReft a -> UReft a #

sconcat :: NonEmpty (UReft a) -> UReft a #

stimes :: Integral b => b -> UReft a -> UReft a #

Exception [Error] Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Generic (UReft r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (UReft r) :: Type -> Type #

Methods

from :: UReft r -> Rep (UReft r) x #

to :: Rep (UReft r) x -> UReft r #

Show (UReft Reft) Source # 
Instance details

Defined in Language.Haskell.Liquid.Transforms.RefSplit

PPrint (UReft r) => Show (UReft r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

showsPrec :: Int -> UReft r -> ShowS #

show :: UReft r -> String #

showList :: [UReft r] -> ShowS #

Binary r => Binary (UReft r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: UReft r -> Put #

get :: Get (UReft r) #

putList :: [UReft r] -> Put #

NFData r => NFData (UReft r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: UReft r -> () #

Eq r => Eq (UReft r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: UReft r -> UReft r -> Bool #

(/=) :: UReft r -> UReft r -> Bool #

Hashable r => Hashable (UReft r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> UReft r -> Int #

hash :: UReft r -> Int #

PPrint (CtxError SpecType) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

(PPrint r, Reftable r) => PPrint (UReft r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> UReft r -> Doc #

pprintPrec :: Int -> Tidy -> UReft r -> Doc #

Expression (UReft ()) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

expr :: UReft () -> Expr #

(PPrint r, Reftable r) => Reftable (UReft r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

isTauto :: UReft r -> Bool #

ppTy :: UReft r -> Doc -> Doc #

top :: UReft r -> UReft r #

bot :: UReft r -> UReft r #

meet :: UReft r -> UReft r -> UReft r #

toReft :: UReft r -> Reft #

ofReft :: Reft -> UReft r #

params :: UReft r -> [Symbol] #

Subable r => Subable (UReft r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

syms :: UReft r -> [Symbol] #

substa :: (Symbol -> Symbol) -> UReft r -> UReft r #

substf :: (Symbol -> Expr) -> UReft r -> UReft r #

subst :: Subst -> UReft r -> UReft r #

subst1 :: UReft r -> (Symbol, Expr) -> UReft r #

REq (UReft Reft) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Equality

Methods

(=*=) :: UReft Reft -> UReft Reft -> Bool Source #

UReftable (UReft Reft) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Result [Error] Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Binary (Spec LocBareType LocSymbol) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Qualify (Measure SpecType DataCon) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Reftable (RTProp BTyCon BTyVar (UReft Reft)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp RTyCon RTyVar (UReft Reft)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RType BTyCon BTyVar (UReft Reft)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

type Rep (UReft r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (UReft r) = D1 ('MetaData "UReft" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "MkUReft" 'PrefixI 'True) (S1 ('MetaSel ('Just "ur_reft") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 r) :*: S1 ('MetaSel ('Just "ur_pred") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Predicate)))

Relational predicates

data RelExpr Source #

Constructors

ERBasic Expr 
ERChecked Expr RelExpr 
ERUnChecked Expr RelExpr 

Instances

Instances details
Data RelExpr Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RelExpr -> c RelExpr #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RelExpr #

toConstr :: RelExpr -> Constr #

dataTypeOf :: RelExpr -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RelExpr) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RelExpr) #

gmapT :: (forall b. Data b => b -> b) -> RelExpr -> RelExpr #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RelExpr -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RelExpr -> r #

gmapQ :: (forall d. Data d => d -> u) -> RelExpr -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RelExpr -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RelExpr -> m RelExpr #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RelExpr -> m RelExpr #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RelExpr -> m RelExpr #

Generic RelExpr Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep RelExpr :: Type -> Type #

Methods

from :: RelExpr -> Rep RelExpr x #

to :: Rep RelExpr x -> RelExpr #

Show RelExpr Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Binary RelExpr Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: RelExpr -> Put #

get :: Get RelExpr #

putList :: [RelExpr] -> Put #

Eq RelExpr Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: RelExpr -> RelExpr -> Bool #

(/=) :: RelExpr -> RelExpr -> Bool #

PPrint RelExpr Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RelExpr -> Doc #

pprintPrec :: Int -> Tidy -> RelExpr -> Doc #

type Rep RelExpr Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Parse-time entities describing refined data types

data SizeFun Source #

Termination expressions

Constructors

IdSizeFun

x -> F.EVar x

SymSizeFun LocSymbol

x -> f x

Instances

Instances details
Data SizeFun Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SizeFun -> c SizeFun #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SizeFun #

toConstr :: SizeFun -> Constr #

dataTypeOf :: SizeFun -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SizeFun) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SizeFun) #

gmapT :: (forall b. Data b => b -> b) -> SizeFun -> SizeFun #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SizeFun -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SizeFun -> r #

gmapQ :: (forall d. Data d => d -> u) -> SizeFun -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> SizeFun -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SizeFun -> m SizeFun #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SizeFun -> m SizeFun #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SizeFun -> m SizeFun #

Generic SizeFun Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep SizeFun :: Type -> Type #

Methods

from :: SizeFun -> Rep SizeFun x #

to :: Rep SizeFun x -> SizeFun #

Show SizeFun Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Binary SizeFun Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: SizeFun -> Put #

get :: Get SizeFun #

putList :: [SizeFun] -> Put #

NFData SizeFun Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: SizeFun -> () #

Eq SizeFun Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: SizeFun -> SizeFun -> Bool #

(/=) :: SizeFun -> SizeFun -> Bool #

Hashable SizeFun Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> SizeFun -> Int #

hash :: SizeFun -> Int #

PPrint SizeFun Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> SizeFun -> Doc #

pprintPrec :: Int -> Tidy -> SizeFun -> Doc #

Qualify SizeFun Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

type Rep SizeFun Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep SizeFun = D1 ('MetaData "SizeFun" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "IdSizeFun" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SymSizeFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocSymbol)))

szFun :: SizeFun -> Symbol -> Expr Source #

data DataDecl Source #

Data type refinements

Constructors

DataDecl 

Fields

Instances

Instances details
Data DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataDecl -> c DataDecl #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataDecl #

toConstr :: DataDecl -> Constr #

dataTypeOf :: DataDecl -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataDecl) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataDecl) #

gmapT :: (forall b. Data b => b -> b) -> DataDecl -> DataDecl #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataDecl -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataDecl -> r #

gmapQ :: (forall d. Data d => d -> u) -> DataDecl -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DataDecl -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataDecl -> m DataDecl #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDecl -> m DataDecl #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDecl -> m DataDecl #

Generic DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep DataDecl :: Type -> Type #

Methods

from :: DataDecl -> Rep DataDecl x #

to :: Rep DataDecl x -> DataDecl #

Show DataDecl Source #

For debugging.

Instance details

Defined in Language.Haskell.Liquid.Types.Types

Binary DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: DataDecl -> Put #

get :: Get DataDecl #

putList :: [DataDecl] -> Put #

Eq DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Ord DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Hashable DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> DataDecl -> Int #

hash :: DataDecl -> Int #

Symbolic DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

symbol :: DataDecl -> Symbol #

PPrint DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

pprintTidy :: Tidy -> DataDecl -> Doc #

pprintPrec :: Int -> Tidy -> DataDecl -> Doc #

Loc DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: DataDecl -> SrcSpan #

Qualify DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

type Rep DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

data DataName Source #

The name of the TyCon corresponding to a DataDecl

Constructors

DnName !LocSymbol

for isVanillyAlgTyCon we can directly use the TyCon name

DnCon !LocSymbol

for FamInst TyCon we save some DataCon name

Instances

Instances details
Data DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataName -> c DataName #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataName #

toConstr :: DataName -> Constr #

dataTypeOf :: DataName -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataName) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataName) #

gmapT :: (forall b. Data b => b -> b) -> DataName -> DataName #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataName -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataName -> r #

gmapQ :: (forall d. Data d => d -> u) -> DataName -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DataName -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataName -> m DataName #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataName -> m DataName #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataName -> m DataName #

Generic DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep DataName :: Type -> Type #

Methods

from :: DataName -> Rep DataName x #

to :: Rep DataName x -> DataName #

Show DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Binary DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: DataName -> Put #

get :: Get DataName #

putList :: [DataName] -> Put #

Eq DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Ord DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Hashable DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> DataName -> Int #

hash :: DataName -> Int #

Symbolic DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

symbol :: DataName -> Symbol #

PPrint DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> DataName -> Doc #

pprintPrec :: Int -> Tidy -> DataName -> Doc #

Loc DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: DataName -> SrcSpan #

type Rep DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep DataName = D1 ('MetaData "DataName" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "DnName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LocSymbol)) :+: C1 ('MetaCons "DnCon" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LocSymbol)))

data DataCtor Source #

Data Constructor

Constructors

DataCtor 

Fields

Instances

Instances details
Data DataCtor Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataCtor -> c DataCtor #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataCtor #

toConstr :: DataCtor -> Constr #

dataTypeOf :: DataCtor -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataCtor) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataCtor) #

gmapT :: (forall b. Data b => b -> b) -> DataCtor -> DataCtor #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataCtor -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataCtor -> r #

gmapQ :: (forall d. Data d => d -> u) -> DataCtor -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DataCtor -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataCtor -> m DataCtor #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataCtor -> m DataCtor #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataCtor -> m DataCtor #

Generic DataCtor Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep DataCtor :: Type -> Type #

Methods

from :: DataCtor -> Rep DataCtor x #

to :: Rep DataCtor x -> DataCtor #

Binary DataCtor Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: DataCtor -> Put #

get :: Get DataCtor #

putList :: [DataCtor] -> Put #

Eq DataCtor Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Hashable DataCtor Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> DataCtor -> Int #

hash :: DataCtor -> Int #

PPrint DataCtor Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

pprintTidy :: Tidy -> DataCtor -> Doc #

pprintPrec :: Int -> Tidy -> DataCtor -> Doc #

Loc DataCtor Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: DataCtor -> SrcSpan #

Qualify DataCtor Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

type Rep DataCtor Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

data DataConP Source #

Constructors

DataConP 

Fields

Instances

Instances details
Data DataConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataConP -> c DataConP #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataConP #

toConstr :: DataConP -> Constr #

dataTypeOf :: DataConP -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataConP) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataConP) #

gmapT :: (forall b. Data b => b -> b) -> DataConP -> DataConP #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataConP -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataConP -> r #

gmapQ :: (forall d. Data d => d -> u) -> DataConP -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DataConP -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataConP -> m DataConP #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataConP -> m DataConP #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataConP -> m DataConP #

Generic DataConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep DataConP :: Type -> Type #

Methods

from :: DataConP -> Rep DataConP x #

to :: Rep DataConP x -> DataConP #

Show DataConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PredType

PPrint DataConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PredType

Methods

pprintTidy :: Tidy -> DataConP -> Doc #

pprintPrec :: Int -> Tidy -> DataConP -> Doc #

Loc DataConP Source #
NOTE:DataCon-Data
for each DataConP we also store the type of the constructed data. This is *the same as* tyRes for *vanilla* ADTs (e.g. List, Maybe etc.) but may differ for GADTs. For example,

data Thing a where X :: Thing Int Y :: Thing Bool

Here the DataConP associated with X (resp. Y) has tyRes corresponding to 'Thing Int' (resp. 'Thing Bool'), but in both cases, the tyData should be 'Thing a'.

Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: DataConP -> SrcSpan #

type Rep DataConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

data HasDataDecl Source #

Constructors

NoDecl (Maybe SizeFun) 
HasDecl 

Instances

Instances details
Show HasDataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

PPrint HasDataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

data DataDeclKind Source #

What kind of DataDecl is it?

Constructors

DataUser

User defined data-definitions (should have refined fields)

DataReflected

Automatically lifted data-definitions (do not have refined fields)

Instances

Instances details
Data DataDeclKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataDeclKind -> c DataDeclKind #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataDeclKind #

toConstr :: DataDeclKind -> Constr #

dataTypeOf :: DataDeclKind -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataDeclKind) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataDeclKind) #

gmapT :: (forall b. Data b => b -> b) -> DataDeclKind -> DataDeclKind #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataDeclKind -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataDeclKind -> r #

gmapQ :: (forall d. Data d => d -> u) -> DataDeclKind -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DataDeclKind -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataDeclKind -> m DataDeclKind #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDeclKind -> m DataDeclKind #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDeclKind -> m DataDeclKind #

Generic DataDeclKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep DataDeclKind :: Type -> Type #

Show DataDeclKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Binary DataDeclKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

NFData DataDeclKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: DataDeclKind -> () #

Eq DataDeclKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Hashable DataDeclKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep DataDeclKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep DataDeclKind = D1 ('MetaData "DataDeclKind" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "DataUser" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DataReflected" 'PrefixI 'False) (U1 :: Type -> Type))

data TyConP Source #

Instances

Instances details
Data TyConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TyConP -> c TyConP #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TyConP #

toConstr :: TyConP -> Constr #

dataTypeOf :: TyConP -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TyConP) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyConP) #

gmapT :: (forall b. Data b => b -> b) -> TyConP -> TyConP #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyConP -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyConP -> r #

gmapQ :: (forall d. Data d => d -> u) -> TyConP -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TyConP -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TyConP -> m TyConP #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TyConP -> m TyConP #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TyConP -> m TyConP #

Generic TyConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep TyConP :: Type -> Type #

Methods

from :: TyConP -> Rep TyConP x #

to :: Rep TyConP x -> TyConP #

Show TyConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PredType

PPrint TyConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PredType

Methods

pprintTidy :: Tidy -> TyConP -> Doc #

pprintPrec :: Int -> Tidy -> TyConP -> Doc #

Loc TyConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: TyConP -> SrcSpan #

Qualify TyConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConP -> TyConP Source #

type Rep TyConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep TyConP = D1 ('MetaData "TyConP" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "TyConP" 'PrefixI 'True) ((S1 ('MetaSel ('Just "tcpLoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SourcePos) :*: (S1 ('MetaSel ('Just "tcpCon") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TyCon) :*: S1 ('MetaSel ('Just "tcpFreeTyVarsTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RTyVar]))) :*: ((S1 ('MetaSel ('Just "tcpFreePredTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [PVar RSort]) :*: S1 ('MetaSel ('Just "tcpVarianceTs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 VarianceInfo)) :*: (S1 ('MetaSel ('Just "tcpVariancePs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 VarianceInfo) :*: S1 ('MetaSel ('Just "tcpSizeFun") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe SizeFun))))))

Pre-instantiated RType

type RRType Source #

Arguments

 = RType RTyCon RTyVar

Resolved version

type RRProp r = Ref RSort (RRType r) Source #

type BRType Source #

Arguments

 = RType BTyCon BTyVar

Bare parsed version

type BRProp r = Ref BSort (BRType r) Source #

type BSort = BRType () Source #

type RTVU c tv = RTVar tv (RType c tv ()) Source #

Unified Representation of Refinement Types --------------------------------

type PVU c tv = PVar (RType c tv ()) Source #

Instantiated RType

type SpecRep = RRep RReft Source #

type RSort = RRType () Source #

type UsedPVar = PVar () Source #

Predicates ----------------------------------------------------------------

type REnv = AREnv SpecType Source #

The type used during constraint generation, used also to define contexts for errors, hence in this file, and NOT in elsewhere. **DO NOT ATTEMPT TO MOVE** Am splitting into + global : many bindings, shared across all constraints + local : few bindings, relevant to particular constraints

data AREnv t Source #

Constructors

REnv 

Fields

Instances

Instances details
Functor AREnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> AREnv a -> AREnv b #

(<$) :: a -> AREnv b -> AREnv a #

Monoid REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: REnv #

mappend :: REnv -> REnv -> REnv #

mconcat :: [REnv] -> REnv #

Semigroup REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(<>) :: REnv -> REnv -> REnv #

sconcat :: NonEmpty REnv -> REnv #

stimes :: Integral b => b -> REnv -> REnv #

NFData REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: REnv -> () #

PPrint t => PPrint (AREnv t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> AREnv t -> Doc #

pprintPrec :: Int -> Tidy -> AREnv t -> Doc #

Constructing & Destructing RTypes

data RTypeRep c tv r Source #

Constructor and Destructors for RTypes ------------------------------------

Constructors

RTypeRep 

Fields

fromRTypeRep :: RTypeRep c tv r -> RType c tv r Source #

toRTypeRep :: RType c tv r -> RTypeRep c tv r Source #

mkArrow :: [(RTVar tv (RType c tv ()), r)] -> [PVar (RType c tv ())] -> [(Symbol, RFInfo, RType c tv r, r)] -> RType c tv r -> RType c tv r Source #

bkArrowDeep :: RType t t1 a -> ([Symbol], [RFInfo], [RType t t1 a], [a], RType t t1 a) Source #

bkArrow :: RType t t1 a -> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a) Source #

safeBkArrow :: PPrint (RType t t1 a) => RType t t1 a -> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a) Source #

mkUnivs :: (Foldable t, Foldable t1) => t (RTVar tv (RType c tv ()), r) -> t1 (PVar (RType c tv ())) -> RType c tv r -> RType c tv r Source #

bkUniv :: RType tv c r -> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())], RType tv c r) Source #

bkClass :: (PPrint c, TyConable c) => RType c tv r -> ([(c, [RType c tv r])], RType c tv r) Source #

rFun :: Monoid r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r Source #

rFun' :: Monoid r => RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r Source #

rCls :: Monoid r => TyCon -> [RType RTyCon tv r] -> RType RTyCon tv r Source #

rRCls :: Monoid r => c -> [RType c tv r] -> RType c tv r Source #

rFunDebug :: Monoid r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r Source #

Manipulating Predicates

pappSym :: Show a => a -> Symbol Source #

pApp :: Symbol -> [Expr] -> Expr Source #

Some tests on RTypes

isBase :: RType t t1 t2 -> Bool Source #

isFunTy :: RType t t1 t2 -> Bool Source #

isTrivial :: (Reftable r, TyConable c) => RType c tv r -> Bool Source #

Traversing RType

efoldReft :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> BScope -> (c -> [RType c tv r] -> [(Symbol, a)]) -> (RTVar tv (RType c tv ()) -> [(Symbol, a)]) -> (RType c tv r -> a) -> (SEnv a -> Maybe (RType c tv r) -> r -> b -> b) -> (PVar (RType c tv ()) -> SEnv a -> SEnv a) -> SEnv a -> b -> RType c tv r -> b Source #

foldReft :: (Reftable r, TyConable c) => BScope -> (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a Source #

foldReft' :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> BScope -> (RType c tv r -> b) -> (SEnv b -> Maybe (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a Source #

emapReft :: ([Symbol] -> r1 -> r2) -> [Symbol] -> RType c tv r1 -> RType c tv r2 Source #

mapReft :: (r1 -> r2) -> RType c tv r1 -> RType c tv r2 Source #

mapReftM :: Monad m => (r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2) Source #

mapPropM :: Monad m => (RTProp c tv r -> m (RTProp c tv r)) -> RType c tv r -> m (RType c tv r) Source #

mapExprReft :: (Symbol -> Expr -> Expr) -> RType c tv RReft -> RType c tv RReft Source #

Visitors ------------------------------------------------------------------

mapBot :: (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r Source #

mapBind :: (Symbol -> Symbol) -> RType c tv r -> RType c tv r Source #

mapRFInfo :: (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r Source #

foldRType :: (acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc Source #

???

data Oblig Source #

Different kinds of Check Obligations ------------------------------------

Constructors

OTerm

Obligation that proves termination

OInv

Obligation that proves invariants

OCons

Obligation that proves subtyping constraints

Instances

Instances details
Data Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Oblig -> c Oblig #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Oblig #

toConstr :: Oblig -> Constr #

dataTypeOf :: Oblig -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Oblig) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Oblig) #

gmapT :: (forall b. Data b => b -> b) -> Oblig -> Oblig #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Oblig -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Oblig -> r #

gmapQ :: (forall d. Data d => d -> u) -> Oblig -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Oblig -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Oblig -> m Oblig #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Oblig -> m Oblig #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Oblig -> m Oblig #

Generic Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Associated Types

type Rep Oblig :: Type -> Type #

Methods

from :: Oblig -> Rep Oblig x #

to :: Rep Oblig x -> Oblig #

Show Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

showsPrec :: Int -> Oblig -> ShowS #

show :: Oblig -> String #

showList :: [Oblig] -> ShowS #

Binary Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

put :: Oblig -> Put #

get :: Get Oblig #

putList :: [Oblig] -> Put #

NFData Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

rnf :: Oblig -> () #

Eq Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

(==) :: Oblig -> Oblig -> Bool #

(/=) :: Oblig -> Oblig -> Bool #

Hashable Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

hashWithSalt :: Int -> Oblig -> Int #

hash :: Oblig -> Int #

PPrint Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

pprintTidy :: Tidy -> Oblig -> Doc #

pprintPrec :: Int -> Tidy -> Oblig -> Doc #

type Rep Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

type Rep Oblig = D1 ('MetaData "Oblig" "Language.Haskell.Liquid.Types.Errors" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "OTerm" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OInv" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OCons" 'PrefixI 'False) (U1 :: Type -> Type)))

ignoreOblig :: RType t t1 t2 -> RType t t1 t2 Source #

Inferred Annotations

newtype AnnInfo a Source #

Annotations -------------------------------------------------------

Constructors

AI (HashMap SrcSpan [(Maybe Text, a)]) 

Instances

Instances details
Functor AnnInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> AnnInfo a -> AnnInfo b #

(<$) :: a -> AnnInfo b -> AnnInfo a #

FromJSON a => FromJSON (AnnInfo a) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.DiffCheck

ToJSON a => ToJSON (AnnInfo a) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.DiffCheck

Data a => Data (AnnInfo a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AnnInfo a -> c (AnnInfo a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (AnnInfo a) #

toConstr :: AnnInfo a -> Constr #

dataTypeOf :: AnnInfo a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (AnnInfo a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (AnnInfo a)) #

gmapT :: (forall b. Data b => b -> b) -> AnnInfo a -> AnnInfo a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AnnInfo a -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AnnInfo a -> r #

gmapQ :: (forall d. Data d => d -> u) -> AnnInfo a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> AnnInfo a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AnnInfo a -> m (AnnInfo a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AnnInfo a -> m (AnnInfo a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AnnInfo a -> m (AnnInfo a) #

Monoid (AnnInfo a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: AnnInfo a #

mappend :: AnnInfo a -> AnnInfo a -> AnnInfo a #

mconcat :: [AnnInfo a] -> AnnInfo a #

Semigroup (AnnInfo a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(<>) :: AnnInfo a -> AnnInfo a -> AnnInfo a #

sconcat :: NonEmpty (AnnInfo a) -> AnnInfo a #

stimes :: Integral b => b -> AnnInfo a -> AnnInfo a #

Generic (AnnInfo a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (AnnInfo a) :: Type -> Type #

Methods

from :: AnnInfo a -> Rep (AnnInfo a) x #

to :: Rep (AnnInfo a) x -> AnnInfo a #

PPrint a => Show (AnnInfo a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

showsPrec :: Int -> AnnInfo a -> ShowS #

show :: AnnInfo a -> String #

showList :: [AnnInfo a] -> ShowS #

NFData a => NFData (AnnInfo a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: AnnInfo a -> () #

PPrint a => PPrint (AnnInfo a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> AnnInfo a -> Doc #

pprintPrec :: Int -> Tidy -> AnnInfo a -> Doc #

type Rep (AnnInfo a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (AnnInfo a) = D1 ('MetaData "AnnInfo" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'True) (C1 ('MetaCons "AI" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap SrcSpan [(Maybe Text, a)]))))

data Annot t Source #

Constructors

AnnUse t 
AnnDef t 
AnnRDf t 
AnnLoc SrcSpan 

Instances

Instances details
Functor Annot Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> Annot a -> Annot b #

(<$) :: a -> Annot b -> Annot a #

Data t => Data (Annot t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Annot t -> c (Annot t) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Annot t) #

toConstr :: Annot t -> Constr #

dataTypeOf :: Annot t -> DataType #

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Annot t)) #

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Annot t)) #

gmapT :: (forall b. Data b => b -> b) -> Annot t -> Annot t #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annot t -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annot t -> r #

gmapQ :: (forall d. Data d => d -> u) -> Annot t -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Annot t -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Annot t -> m (Annot t) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Annot t -> m (Annot t) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Annot t -> m (Annot t) #

Generic (Annot t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (Annot t) :: Type -> Type #

Methods

from :: Annot t -> Rep (Annot t) x #

to :: Rep (Annot t) x -> Annot t #

NFData a => NFData (Annot a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: Annot a -> () #

PPrint t => PPrint (Annot t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Annot t -> Doc #

pprintPrec :: Int -> Tidy -> Annot t -> Doc #

type Rep (Annot t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (Annot t) = D1 ('MetaData "Annot" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) ((C1 ('MetaCons "AnnUse" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "AnnDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t))) :+: (C1 ('MetaCons "AnnRDf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "AnnLoc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SrcSpan))))

Hole Information

data HoleInfo i t Source #

Var Hole Info -----------------------------------------------------

Constructors

HoleInfo 

Fields

Instances

Instances details
Functor (HoleInfo i) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> HoleInfo i a -> HoleInfo i b #

(<$) :: a -> HoleInfo i b -> HoleInfo i a #

PPrint t => PPrint (HoleInfo i t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> HoleInfo i t -> Doc #

pprintPrec :: Int -> Tidy -> HoleInfo i t -> Doc #

Overall Output

data Output a Source #

Output --------------------------------------------------------------------

Constructors

O 

Fields

Instances

Instances details
Functor Output Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> Output a -> Output b #

(<$) :: a -> Output b -> Output a #

FromJSON (Output Doc) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.DiffCheck

ToJSON (Output Doc) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.DiffCheck

Monoid (Output a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: Output a #

mappend :: Output a -> Output a -> Output a #

mconcat :: [Output a] -> Output a #

Semigroup (Output a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(<>) :: Output a -> Output a -> Output a #

sconcat :: NonEmpty (Output a) -> Output a #

stimes :: Integral b => b -> Output a -> Output a #

Generic (Output a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (Output a) :: Type -> Type #

Methods

from :: Output a -> Rep (Output a) x #

to :: Rep (Output a) x -> Output a #

PPrint a => PPrint (Output a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Output a -> Doc #

pprintPrec :: Int -> Tidy -> Output a -> Doc #

type Rep (Output a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (Output a) = D1 ('MetaData "Output" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "O" 'PrefixI 'True) ((S1 ('MetaSel ('Just "o_vars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [String])) :*: S1 ('MetaSel ('Just "o_types") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (AnnInfo a))) :*: (S1 ('MetaSel ('Just "o_templs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (AnnInfo a)) :*: (S1 ('MetaSel ('Just "o_bots") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [SrcSpan]) :*: S1 ('MetaSel ('Just "o_result") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ErrorResult)))))

Refinement Hole

hole :: Expr Source #

isHole :: Expr -> Bool Source #

hasHoleTy :: RType t t1 t2 -> Bool Source #

Converting To and From Sort

ofRSort :: Reftable r => RType c tv () -> RType c tv r Source #

toRSort :: RType c tv r -> RType c tv () Source #

rTypeValueVar :: Reftable r => RType c tv r -> Symbol Source #

rTypeReft :: Reftable r => RType c tv r -> Reft Source #

topRTypeBase :: Reftable r => RType c tv r -> RType c tv r Source #

Class for values that can be pretty printed

class PPrint a where #

Implement either pprintTidy or pprintPrec

Minimal complete definition

Nothing

Methods

pprintTidy :: Tidy -> a -> Doc #

pprintPrec :: Int -> Tidy -> a -> Doc #

Instances

Instances details
PPrint Class Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Class -> Doc #

pprintPrec :: Int -> Tidy -> Class -> Doc #

PPrint DataCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> DataCon -> Doc #

pprintPrec :: Int -> Tidy -> DataCon -> Doc #

PPrint Type Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Type -> Doc #

pprintPrec :: Int -> Tidy -> Type -> Doc #

PPrint TyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> TyCon -> Doc #

pprintPrec :: Int -> Tidy -> TyCon -> Doc #

PPrint Name Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Name -> Doc #

pprintPrec :: Int -> Tidy -> Name -> Doc #

PPrint SourceError Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

PPrint SrcSpan Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

pprintTidy :: Tidy -> SrcSpan -> Doc #

pprintPrec :: Int -> Tidy -> SrcSpan -> Doc #

PPrint TyThing Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> TyThing -> Doc #

pprintPrec :: Int -> Tidy -> TyThing -> Doc #

PPrint Var Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Var -> Doc #

pprintPrec :: Int -> Tidy -> Var -> Doc #

PPrint CVertex 
Instance details

Defined in Language.Fixpoint.Graph.Types

Methods

pprintTidy :: Tidy -> CVertex -> Doc #

pprintPrec :: Int -> Tidy -> CVertex -> Doc #

PPrint KVGraph 
Instance details

Defined in Language.Fixpoint.Graph.Types

Methods

pprintTidy :: Tidy -> KVGraph -> Doc #

pprintPrec :: Int -> Tidy -> KVGraph -> Doc #

PPrint Rank 
Instance details

Defined in Language.Fixpoint.Graph.Types

Methods

pprintTidy :: Tidy -> Rank -> Doc #

pprintPrec :: Int -> Tidy -> Rank -> Doc #

PPrint TermOrigin 
Instance details

Defined in Language.Fixpoint.Solver.Rewrite

PPrint AxiomEnv 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> AxiomEnv -> Doc #

pprintPrec :: Int -> Tidy -> AxiomEnv -> Doc #

PPrint Equation 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> Equation -> Doc #

pprintPrec :: Int -> Tidy -> Equation -> Doc #

PPrint GFixSolution 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint QualParam 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint QualPattern 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint Qualifier 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint Rewrite 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> Rewrite -> Doc #

pprintPrec :: Int -> Tidy -> Rewrite -> Doc #

PPrint IBindEnv 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

pprintTidy :: Tidy -> IBindEnv -> Doc #

pprintPrec :: Int -> Tidy -> IBindEnv -> Doc #

PPrint Packs 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

pprintTidy :: Tidy -> Packs -> Doc #

pprintPrec :: Int -> Tidy -> Packs -> Doc #

PPrint Error 
Instance details

Defined in Language.Fixpoint.Types.Errors

Methods

pprintTidy :: Tidy -> Error -> Doc #

pprintPrec :: Int -> Tidy -> Error -> Doc #

PPrint Error1 
Instance details

Defined in Language.Fixpoint.Types.Errors

Methods

pprintTidy :: Tidy -> Error1 -> Doc #

pprintPrec :: Int -> Tidy -> Error1 -> Doc #

PPrint Symbol 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

pprintTidy :: Tidy -> Symbol -> Doc #

pprintPrec :: Int -> Tidy -> Symbol -> Doc #

PPrint DocTable 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> DocTable -> Doc #

pprintPrec :: Int -> Tidy -> DocTable -> Doc #

PPrint Tidy Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Tidy -> Doc #

pprintPrec :: Int -> Tidy -> Tidy -> Doc #

PPrint Bop 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Bop -> Doc #

pprintPrec :: Int -> Tidy -> Bop -> Doc #

PPrint Brel 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Brel -> Doc #

pprintPrec :: Int -> Tidy -> Brel -> Doc #

PPrint Constant 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Constant -> Doc #

pprintPrec :: Int -> Tidy -> Constant -> Doc #

PPrint Expr 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Expr -> Doc #

pprintPrec :: Int -> Tidy -> Expr -> Doc #

PPrint KVSub 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> KVSub -> Doc #

pprintPrec :: Int -> Tidy -> KVSub -> Doc #

PPrint KVar 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> KVar -> Doc #

pprintPrec :: Int -> Tidy -> KVar -> Doc #

PPrint Subst 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Subst -> Doc #

pprintPrec :: Int -> Tidy -> Subst -> Doc #

PPrint SymConst 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> SymConst -> Doc #

pprintPrec :: Int -> Tidy -> SymConst -> Doc #

PPrint BIndex 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> BIndex -> Doc #

pprintPrec :: Int -> Tidy -> BIndex -> Doc #

PPrint BindPred 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> BindPred -> Doc #

pprintPrec :: Int -> Tidy -> BindPred -> Doc #

PPrint Cube 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> Cube -> Doc #

pprintPrec :: Int -> Tidy -> Cube -> Doc #

PPrint EQual 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> EQual -> Doc #

pprintPrec :: Int -> Tidy -> EQual -> Doc #

PPrint EbindSol 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> EbindSol -> Doc #

pprintPrec :: Int -> Tidy -> EbindSol -> Doc #

PPrint KIndex 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> KIndex -> Doc #

pprintPrec :: Int -> Tidy -> KIndex -> Doc #

PPrint QBind 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> QBind -> Doc #

pprintPrec :: Int -> Tidy -> QBind -> Doc #

PPrint DataCtor 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> DataCtor -> Doc #

pprintPrec :: Int -> Tidy -> DataCtor -> Doc #

PPrint DataDecl 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> DataDecl -> Doc #

pprintPrec :: Int -> Tidy -> DataDecl -> Doc #

PPrint DataField 
Instance details

Defined in Language.Fixpoint.Types.Sorts

PPrint FTycon 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> FTycon -> Doc #

pprintPrec :: Int -> Tidy -> FTycon -> Doc #

PPrint Sort 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> Sort -> Doc #

pprintPrec :: Int -> Tidy -> Sort -> Doc #

PPrint TCArgs 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> TCArgs -> Doc #

pprintPrec :: Int -> Tidy -> TCArgs -> Doc #

PPrint SrcSpan 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

pprintTidy :: Tidy -> SrcSpan -> Doc #

pprintPrec :: Int -> Tidy -> SrcSpan -> Doc #

PPrint Templates 
Instance details

Defined in Language.Fixpoint.Types.Templates

PPrint Sem 
Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

pprintTidy :: Tidy -> Sem -> Doc #

pprintPrec :: Int -> Tidy -> Sem -> Doc #

PPrint SmtSort 
Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

pprintTidy :: Tidy -> SmtSort -> Doc #

pprintPrec :: Int -> Tidy -> SmtSort -> Doc #

PPrint TheorySymbol 
Instance details

Defined in Language.Fixpoint.Types.Theories

PPrint Trigger 
Instance details

Defined in Language.Fixpoint.Types.Triggers

Methods

pprintTidy :: Tidy -> Trigger -> Doc #

pprintPrec :: Int -> Tidy -> Trigger -> Doc #

PPrint Stats 
Instance details

Defined in Language.Fixpoint.Utils.Statistics

Methods

pprintTidy :: Tidy -> Stats -> Doc #

pprintPrec :: Int -> Tidy -> Stats -> Doc #

PPrint CGEnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

pprintTidy :: Tidy -> CGEnv -> Doc #

pprintPrec :: Int -> Tidy -> CGEnv -> Doc #

PPrint CGInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

pprintTidy :: Tidy -> CGInfo -> Doc #

pprintPrec :: Int -> Tidy -> CGInfo -> Doc #

PPrint SubC Source # 
Instance details

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

pprintTidy :: Tidy -> SubC -> Doc #

pprintPrec :: Int -> Tidy -> SubC -> Doc #

PPrint WfC Source # 
Instance details

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

pprintTidy :: Tidy -> WfC -> Doc #

pprintPrec :: Int -> Tidy -> WfC -> Doc #

PPrint Pattern Source # 
Instance details

Defined in Language.Haskell.Liquid.GHC.Resugar

Methods

pprintTidy :: Tidy -> Pattern -> Doc #

pprintPrec :: Int -> Tidy -> Pattern -> Doc #

PPrint Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

pprintTidy :: Tidy -> Oblig -> Doc #

pprintPrec :: Int -> Tidy -> Oblig -> Doc #

PPrint ParseError Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

PPrint UserError Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

PPrint TargetInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.GHC.Interface

PPrint TargetSpec Source #

Pretty Printing -----------------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.GHC.Interface

PPrint BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> BTyCon -> Doc #

pprintPrec :: Int -> Tidy -> BTyCon -> Doc #

PPrint BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> BTyVar -> Doc #

pprintPrec :: Int -> Tidy -> BTyVar -> Doc #

PPrint Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Body -> Doc #

pprintPrec :: Int -> Tidy -> Body -> Doc #

PPrint Cinfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Cinfo -> Doc #

pprintPrec :: Int -> Tidy -> Cinfo -> Doc #

PPrint DataConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PredType

Methods

pprintTidy :: Tidy -> DataConP -> Doc #

pprintPrec :: Int -> Tidy -> DataConP -> Doc #

PPrint DataCtor Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

pprintTidy :: Tidy -> DataCtor -> Doc #

pprintPrec :: Int -> Tidy -> DataCtor -> Doc #

PPrint DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

pprintTidy :: Tidy -> DataDecl -> Doc #

pprintPrec :: Int -> Tidy -> DataDecl -> Doc #

PPrint DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> DataName -> Doc #

pprintPrec :: Int -> Tidy -> DataName -> Doc #

PPrint Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

pprintTidy :: Tidy -> Error -> Doc #

pprintPrec :: Int -> Tidy -> Error -> Doc #

PPrint HasDataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

PPrint KVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> KVKind -> Doc #

pprintPrec :: Int -> Tidy -> KVKind -> Doc #

PPrint KVProf Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> KVProf -> Doc #

pprintPrec :: Int -> Tidy -> KVProf -> Doc #

PPrint LMap Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> LMap -> Doc #

pprintPrec :: Int -> Tidy -> LMap -> Doc #

PPrint LogicMap Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> LogicMap -> Doc #

pprintPrec :: Int -> Tidy -> LogicMap -> Doc #

PPrint ModName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> ModName -> Doc #

pprintPrec :: Int -> Tidy -> ModName -> Doc #

PPrint Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

PPrint RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RTyCon -> Doc #

pprintPrec :: Int -> Tidy -> RTyCon -> Doc #

PPrint RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RTyVar -> Doc #

pprintPrec :: Int -> Tidy -> RTyVar -> Doc #

PPrint RelExpr Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RelExpr -> Doc #

pprintPrec :: Int -> Tidy -> RelExpr -> Doc #

PPrint SizeFun Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> SizeFun -> Doc #

pprintPrec :: Int -> Tidy -> SizeFun -> Doc #

PPrint TargetVars Source # 
Instance details

Defined in Language.Haskell.Liquid.GHC.Interface

PPrint TyConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PredType

Methods

pprintTidy :: Tidy -> TyConP -> Doc #

pprintPrec :: Int -> Tidy -> TyConP -> Doc #

PPrint Variance Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Variance

Methods

pprintTidy :: Tidy -> Variance -> Doc #

pprintPrec :: Int -> Tidy -> Variance -> Doc #

PPrint Def Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.DiffCheck

Methods

pprintTidy :: Tidy -> Def -> Doc #

pprintPrec :: Int -> Tidy -> Def -> Doc #

PPrint DiffCheck Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.DiffCheck

PPrint Doc 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Doc -> Doc #

pprintPrec :: Int -> Tidy -> Doc -> Doc #

PPrint Text 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Text -> Doc #

pprintPrec :: Int -> Tidy -> Text -> Doc #

PPrint Integer 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Integer -> Doc #

pprintPrec :: Int -> Tidy -> Integer -> Doc #

PPrint () 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> () -> Doc #

pprintPrec :: Int -> Tidy -> () -> Doc #

PPrint Bool 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Bool -> Doc #

pprintPrec :: Int -> Tidy -> Bool -> Doc #

PPrint Char 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Char -> Doc #

pprintPrec :: Int -> Tidy -> Char -> Doc #

PPrint Float 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Float -> Doc #

pprintPrec :: Int -> Tidy -> Float -> Doc #

PPrint Int 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Int -> Doc #

pprintPrec :: Int -> Tidy -> Int -> Doc #

PPrint (Bind Var) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Bind Var -> Doc #

pprintPrec :: Int -> Tidy -> Bind Var -> Doc #

PPrint (Expr Var) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Expr Var -> Doc #

pprintPrec :: Int -> Tidy -> Expr Var -> Doc #

PPrint (MsgEnvelope DecoratedSDoc) Source #

A whole bunch of PPrint instances follow ----------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Fixpoint a => PPrint (SimpC a) 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> SimpC a -> Doc #

pprintPrec :: Int -> Tidy -> SimpC a -> Doc #

Fixpoint a => PPrint (SubC a) 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> SubC a -> Doc #

pprintPrec :: Int -> Tidy -> SubC a -> Doc #

Fixpoint a => PPrint (WfC a) 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> WfC a -> Doc #

pprintPrec :: Int -> Tidy -> WfC a -> Doc #

PPrint a => PPrint (SEnv a) 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

pprintTidy :: Tidy -> SEnv a -> Doc #

pprintPrec :: Int -> Tidy -> SEnv a -> Doc #

PPrint a => PPrint (SizedEnv a) 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

pprintTidy :: Tidy -> SizedEnv a -> Doc #

pprintPrec :: Int -> Tidy -> SizedEnv a -> Doc #

Fixpoint a => PPrint (FixResult a) 
Instance details

Defined in Language.Fixpoint.Types.Errors

Methods

pprintTidy :: Tidy -> FixResult a -> Doc #

pprintPrec :: Int -> Tidy -> FixResult a -> Doc #

PPrint a => PPrint (TCEmb a) 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> TCEmb a -> Doc #

pprintPrec :: Int -> Tidy -> TCEmb a -> Doc #

PPrint a => PPrint (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

pprintTidy :: Tidy -> Located a -> Doc #

pprintPrec :: Int -> Tidy -> Located a -> Doc #

PPrint a => PPrint (Triggered a) 
Instance details

Defined in Language.Fixpoint.Types.Triggers

Methods

pprintTidy :: Tidy -> Triggered a -> Doc #

pprintPrec :: Int -> Tidy -> Triggered a -> Doc #

(Show v, PPrint v) => PPrint (PlugTV v) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Types

Methods

pprintTidy :: Tidy -> PlugTV v -> Doc #

pprintPrec :: Int -> Tidy -> PlugTV v -> Doc #

PPrint a => PPrint (Template a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Constraint.Template

Methods

pprintTidy :: Tidy -> Template a -> Doc #

pprintPrec :: Int -> Tidy -> Template a -> Doc #

PPrint (CtxError SpecType) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

PPrint (CtxError Doc) Source #

Pretty Printing Error Messages --------------------------------------------

Need to put PPrint Error instance here (instead of in Types), as it depends on PPrint SpecTypes, which lives in this module.

Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

PPrint t => PPrint (AREnv t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> AREnv t -> Doc #

pprintPrec :: Int -> Tidy -> AREnv t -> Doc #

PPrint a => PPrint (AnnInfo a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> AnnInfo a -> Doc #

pprintPrec :: Int -> Tidy -> AnnInfo a -> Doc #

PPrint t => PPrint (Annot t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Annot t -> Doc #

pprintPrec :: Int -> Tidy -> Annot t -> Doc #

PPrint t => PPrint (CMeasure t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> CMeasure t -> Doc #

pprintPrec :: Int -> Tidy -> CMeasure t -> Doc #

PPrint a => PPrint (Output a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Output a -> Doc #

pprintPrec :: Int -> Tidy -> Output a -> Doc #

PPrint (PVar a) Source #

F.PPrint -----------------------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> PVar a -> Doc #

pprintPrec :: Int -> Tidy -> PVar a -> Doc #

PPrint t => PPrint (RClass t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RClass t -> Doc #

pprintPrec :: Int -> Tidy -> RClass t -> Doc #

PPrint t => PPrint (RILaws t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RILaws t -> Doc #

pprintPrec :: Int -> Tidy -> RILaws t -> Doc #

PPrint t => PPrint (RISig t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RISig t -> Doc #

pprintPrec :: Int -> Tidy -> RISig t -> Doc #

PPrint t => PPrint (RInstance t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RInstance t -> Doc #

pprintPrec :: Int -> Tidy -> RInstance t -> Doc #

(PPrint r, Reftable r) => PPrint (UReft r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> UReft r -> Doc #

pprintPrec :: Int -> Tidy -> UReft r -> Doc #

(Ord a, PPrint a) => PPrint (HashSet a) 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> HashSet a -> Doc #

pprintPrec :: Int -> Tidy -> HashSet a -> Doc #

PPrint a => PPrint (Maybe a) 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Maybe a -> Doc #

pprintPrec :: Int -> Tidy -> Maybe a -> Doc #

PPrint a => PPrint [a] 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> [a] -> Doc #

pprintPrec :: Int -> Tidy -> [a] -> Doc #

(PPrint a, PPrint b) => PPrint (Either a b) 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Either a b -> Doc #

pprintPrec :: Int -> Tidy -> Either a b -> Doc #

(PPrint a, PPrint b) => PPrint (Sol a b) 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> Sol a b -> Doc #

pprintPrec :: Int -> Tidy -> Sol a b -> Doc #

(PPrint ty, PPrint ctor) => PPrint (Pspec ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Parse

Methods

pprintTidy :: Tidy -> Pspec ty ctor -> Doc #

pprintPrec :: Int -> Tidy -> Pspec ty ctor -> Doc #

(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 #

(Show ty, Show bndr, PPrint ty, PPrint bndr) => PPrint (Spec ty bndr) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

pprintTidy :: Tidy -> Spec ty bndr -> Doc #

pprintPrec :: Int -> Tidy -> Spec ty bndr -> Doc #

PPrint a => PPrint (Def t a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Def t a -> Doc #

pprintPrec :: Int -> Tidy -> Def t a -> Doc #

PPrint t => PPrint (HoleInfo i t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> HoleInfo i t -> Doc #

pprintPrec :: Int -> Tidy -> HoleInfo i t -> Doc #

(PPrint t, PPrint a) => PPrint (MSpec t a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> MSpec t a -> Doc #

pprintPrec :: Int -> Tidy -> MSpec t a -> Doc #

(PPrint t, PPrint a) => PPrint (Measure t a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Measure t a -> Doc #

pprintPrec :: Int -> Tidy -> Measure t a -> Doc #

(PPrint tv, PPrint ty) => PPrint (RTAlias tv ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> RTAlias tv ty -> Doc #

pprintPrec :: Int -> Tidy -> RTAlias tv ty -> Doc #

(PPrint tv, PPrint t) => PPrint (RTEnv tv t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> RTEnv tv t -> Doc #

pprintPrec :: Int -> Tidy -> RTEnv tv t -> Doc #

PPrint v => PPrint (RTVar v s) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RTVar v s -> Doc #

pprintPrec :: Int -> Tidy -> RTVar v s -> Doc #

(PPrint r, Reftable r, PPrint t, PPrint (RType c tv r)) => PPrint (Ref t (RType c tv r)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Ref t (RType c tv r) -> Doc #

pprintPrec :: Int -> Tidy -> Ref t (RType c tv r) -> Doc #

(Ord a, PPrint a, PPrint b) => PPrint (HashMap a b) 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> HashMap a b -> Doc #

pprintPrec :: Int -> Tidy -> HashMap a b -> Doc #

(PPrint a, PPrint b) => PPrint (a, b) 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> (a, b) -> Doc #

pprintPrec :: Int -> Tidy -> (a, b) -> Doc #

OkRT c tv r => PPrint (RType c tv r) Source #

Pretty Printing RefType ---------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> RType c tv r -> Doc #

pprintPrec :: Int -> Tidy -> RType c tv r -> Doc #

(PPrint a, PPrint b, PPrint c) => PPrint (a, b, c) 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> (a, b, c) -> Doc #

pprintPrec :: Int -> Tidy -> (a, b, c) -> Doc #

(PPrint a, PPrint b, PPrint c, PPrint d) => PPrint (a, b, c, d) 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> (a, b, c, d) -> Doc #

pprintPrec :: Int -> Tidy -> (a, b, c, d) -> Doc #

(PPrint a, PPrint b, PPrint c, PPrint d, PPrint e) => PPrint (a, b, c, d, e) 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> (a, b, c, d, e) -> Doc #

pprintPrec :: Int -> Tidy -> (a, b, c, d, e) -> Doc #

pprint :: PPrint a => a -> Doc #

Top-level pretty printer

showpp :: PPrint a => a -> String #

Printer Configuration

data PPEnv Source #

Printer ----------------------------------------------------------------

Constructors

PP 

Fields

Instances

Instances details
Show PPEnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> PPEnv -> ShowS #

show :: PPEnv -> String #

showList :: [PPEnv] -> ShowS #

Modules and Imports

data ModName Source #

Module Names --------------------------------------------------------------

Constructors

ModName !ModType !ModuleName 

Instances

Instances details
Data ModName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModName -> c ModName #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModName #

toConstr :: ModName -> Constr #

dataTypeOf :: ModName -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModName) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModName) #

gmapT :: (forall b. Data b => b -> b) -> ModName -> ModName #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModName -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModName -> r #

gmapQ :: (forall d. Data d => d -> u) -> ModName -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ModName -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModName -> m ModName #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModName -> m ModName #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModName -> m ModName #

Generic ModName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep ModName :: Type -> Type #

Methods

from :: ModName -> Rep ModName x #

to :: Rep ModName x -> ModName #

Show ModName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Eq ModName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: ModName -> ModName -> Bool #

(/=) :: ModName -> ModName -> Bool #

Ord ModName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Hashable ModName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> ModName -> Int #

hash :: ModName -> Int #

Symbolic ModName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

symbol :: ModName -> Symbol #

PPrint ModName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> ModName -> Doc #

pprintPrec :: Int -> Tidy -> ModName -> Doc #

Qualify ModSpecs Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

type Rep ModName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep ModName = D1 ('MetaData "ModName" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "ModName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModType) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModuleName)))

data ModType Source #

Constructors

Target 
SrcImport 
SpecImport 

Instances

Instances details
Data ModType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModType -> c ModType #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModType #

toConstr :: ModType -> Constr #

dataTypeOf :: ModType -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModType) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModType) #

gmapT :: (forall b. Data b => b -> b) -> ModType -> ModType #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModType -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModType -> r #

gmapQ :: (forall d. Data d => d -> u) -> ModType -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ModType -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModType -> m ModType #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModType -> m ModType #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModType -> m ModType #

Generic ModType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep ModType :: Type -> Type #

Methods

from :: ModType -> Rep ModType x #

to :: Rep ModType x -> ModType #

Show ModType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Eq ModType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: ModType -> ModType -> Bool #

(/=) :: ModType -> ModType -> Bool #

Ord ModType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Hashable ModType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> ModType -> Int #

hash :: ModType -> Int #

type Rep ModType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep ModType = D1 ('MetaData "ModType" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "Target" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SrcImport" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SpecImport" 'PrefixI 'False) (U1 :: Type -> Type)))

qualifyModName :: ModName -> Symbol -> Symbol Source #

Refinement Type Aliases

data RTEnv tv t Source #

Refinement Type Aliases ---------------------------------------------------

Constructors

RTE 

Fields

Instances

Instances details
Monoid (RTEnv tv t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: RTEnv tv t #

mappend :: RTEnv tv t -> RTEnv tv t -> RTEnv tv t #

mconcat :: [RTEnv tv t] -> RTEnv tv t #

Semigroup (RTEnv tv t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(<>) :: RTEnv tv t -> RTEnv tv t -> RTEnv tv t #

sconcat :: NonEmpty (RTEnv tv t) -> RTEnv tv t #

stimes :: Integral b => b -> RTEnv tv t -> RTEnv tv t #

(PPrint tv, PPrint t) => PPrint (RTEnv tv t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> RTEnv tv t -> Doc #

pprintPrec :: Int -> Tidy -> RTEnv tv t -> Doc #

Diagnostics, Warnings, Errors and Error Messages

type ErrorResult = FixResult UserError Source #

Error Data Type -----------------------------------------------------------

data Warning Source #

Diagnostic info -----------------------------------------------------------

Instances

Instances details
Show Warning Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Eq Warning Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: Warning -> Warning -> Bool #

(/=) :: Warning -> Warning -> Bool #

printWarning :: Logger -> DynFlags -> Warning -> IO () Source #

Printing Warnings ---------------------------------------------------------

Source information (associated with constraints)

data Cinfo Source #

Source Information Associated With Constraints ----------------------------

Constructors

Ci 

Fields

Instances

Instances details
Generic Cinfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep Cinfo :: Type -> Type #

Methods

from :: Cinfo -> Rep Cinfo x #

to :: Rep Cinfo x -> Cinfo #

Show Cinfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> Cinfo -> ShowS #

show :: Cinfo -> String #

showList :: [Cinfo] -> ShowS #

NFData Cinfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: Cinfo -> () #

Eq Cinfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: Cinfo -> Cinfo -> Bool #

(/=) :: Cinfo -> Cinfo -> Bool #

Fixpoint Cinfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

toFix :: Cinfo -> Doc #

simplify :: Cinfo -> Cinfo #

PPrint Cinfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Cinfo -> Doc #

pprintPrec :: Int -> Tidy -> Cinfo -> Doc #

Loc Cinfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: Cinfo -> SrcSpan #

Result (FixResult Cinfo) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

type Rep Cinfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep Cinfo = D1 ('MetaData "Cinfo" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "Ci" 'PrefixI 'True) (S1 ('MetaSel ('Just "ci_loc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "ci_err") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Error)) :*: S1 ('MetaSel ('Just "ci_var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Var)))))

Measures

data Measure ty ctor Source #

Constructors

M 

Fields

Instances

Instances details
Bifunctor Measure Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

bimap :: (a -> b) -> (c -> d) -> Measure a c -> Measure b d #

first :: (a -> b) -> Measure a c -> Measure b c #

second :: (b -> c) -> Measure a b -> Measure a c #

Qualify BareMeasure Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Functor (Measure ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> Measure ty a -> Measure ty b #

(<$) :: a -> Measure ty b -> Measure ty a #

(Data ty, Data ctor) => Data (Measure ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Measure ty ctor -> c (Measure ty ctor) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Measure ty ctor) #

toConstr :: Measure ty ctor -> Constr #

dataTypeOf :: Measure ty ctor -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Measure ty ctor)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Measure ty ctor)) #

gmapT :: (forall b. Data b => b -> b) -> Measure ty ctor -> Measure ty ctor #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Measure ty ctor -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Measure ty ctor -> r #

gmapQ :: (forall d. Data d => d -> u) -> Measure ty ctor -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Measure ty ctor -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Measure ty ctor -> m (Measure ty ctor) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Measure ty ctor -> m (Measure ty ctor) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Measure ty ctor -> m (Measure ty ctor) #

Generic (Measure ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (Measure ty ctor) :: Type -> Type #

Methods

from :: Measure ty ctor -> Rep (Measure ty ctor) x #

to :: Rep (Measure ty ctor) x -> Measure ty ctor #

PPrint (Measure t a) => Show (Measure t a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> Measure t a -> ShowS #

show :: Measure t a -> String #

showList :: [Measure t a] -> ShowS #

(Binary t, Binary c) => Binary (Measure t c) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: Measure t c -> Put #

get :: Get (Measure t c) #

putList :: [Measure t c] -> Put #

(Eq ty, Eq ctor) => Eq (Measure ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: Measure ty ctor -> Measure ty ctor -> Bool #

(/=) :: Measure ty ctor -> Measure ty ctor -> Bool #

(Hashable ty, Hashable ctor) => Hashable (Measure ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> Measure ty ctor -> Int #

hash :: Measure ty ctor -> Int #

(PPrint t, PPrint a) => PPrint (Measure t a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Measure t a -> Doc #

pprintPrec :: Int -> Tidy -> Measure t a -> Doc #

Subable (Measure ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

syms :: Measure ty ctor -> [Symbol] #

substa :: (Symbol -> Symbol) -> Measure ty ctor -> Measure ty ctor #

substf :: (Symbol -> Expr) -> Measure ty ctor -> Measure ty ctor #

subst :: Subst -> Measure ty ctor -> Measure ty ctor #

subst1 :: Measure ty ctor -> (Symbol, Expr) -> Measure ty ctor #

Loc (Measure a b) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: Measure a b -> SrcSpan #

Qualify (Measure SpecType DataCon) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

type Rep (Measure ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (Measure ty ctor) = D1 ('MetaData "Measure" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "M" 'PrefixI 'True) ((S1 ('MetaSel ('Just "msName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocSymbol) :*: S1 ('MetaSel ('Just "msSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ty)) :*: (S1 ('MetaSel ('Just "msEqns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Def ty ctor]) :*: (S1 ('MetaSel ('Just "msKind") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 MeasureKind) :*: S1 ('MetaSel ('Just "msUnSorted") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 UnSortedExprs)))))

data MeasureKind Source #

Constructors

MsReflect

due to `reflect foo`

MsMeasure

due to `measure foo` with old-style (non-haskell) equations

MsLifted

due to `measure foo` with new-style haskell equations

MsClass

due to `class measure` definition

MsAbsMeasure

due to `measure foo` without equations c.f. testsposT1223.hs

MsSelector

due to selector-fields e.g. `data Foo = Foo { fld :: Int }`

MsChecker

due to checkers e.g. `is-F` for `data Foo = F ... | G ...`

Instances

Instances details
Data MeasureKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MeasureKind -> c MeasureKind #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MeasureKind #

toConstr :: MeasureKind -> Constr #

dataTypeOf :: MeasureKind -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MeasureKind) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MeasureKind) #

gmapT :: (forall b. Data b => b -> b) -> MeasureKind -> MeasureKind #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MeasureKind -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MeasureKind -> r #

gmapQ :: (forall d. Data d => d -> u) -> MeasureKind -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> MeasureKind -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MeasureKind -> m MeasureKind #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MeasureKind -> m MeasureKind #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MeasureKind -> m MeasureKind #

Generic MeasureKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep MeasureKind :: Type -> Type #

Show MeasureKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Binary MeasureKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Eq MeasureKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Ord MeasureKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Hashable MeasureKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep MeasureKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep MeasureKind = D1 ('MetaData "MeasureKind" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) ((C1 ('MetaCons "MsReflect" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MsMeasure" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MsLifted" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "MsClass" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MsAbsMeasure" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "MsSelector" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MsChecker" 'PrefixI 'False) (U1 :: Type -> Type))))

data CMeasure ty Source #

Constructors

CM 

Fields

Instances

Instances details
Functor CMeasure Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> CMeasure a -> CMeasure b #

(<$) :: a -> CMeasure b -> CMeasure a #

Data ty => Data (CMeasure ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CMeasure ty -> c (CMeasure ty) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (CMeasure ty) #

toConstr :: CMeasure ty -> Constr #

dataTypeOf :: CMeasure ty -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (CMeasure ty)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (CMeasure ty)) #

gmapT :: (forall b. Data b => b -> b) -> CMeasure ty -> CMeasure ty #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CMeasure ty -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CMeasure ty -> r #

gmapQ :: (forall d. Data d => d -> u) -> CMeasure ty -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> CMeasure ty -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CMeasure ty -> m (CMeasure ty) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CMeasure ty -> m (CMeasure ty) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CMeasure ty -> m (CMeasure ty) #

Generic (CMeasure ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (CMeasure ty) :: Type -> Type #

Methods

from :: CMeasure ty -> Rep (CMeasure ty) x #

to :: Rep (CMeasure ty) x -> CMeasure ty #

PPrint (CMeasure t) => Show (CMeasure t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> CMeasure t -> ShowS #

show :: CMeasure t -> String #

showList :: [CMeasure t] -> ShowS #

PPrint t => PPrint (CMeasure t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> CMeasure t -> Doc #

pprintPrec :: Int -> Tidy -> CMeasure t -> Doc #

type Rep (CMeasure ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (CMeasure ty) = D1 ('MetaData "CMeasure" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "CM" 'PrefixI 'True) (S1 ('MetaSel ('Just "cName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocSymbol) :*: S1 ('MetaSel ('Just "cSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ty)))

data Def ty ctor Source #

Constructors

Def 

Fields

Instances

Instances details
Bifunctor Def Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

bimap :: (a -> b) -> (c -> d) -> Def a c -> Def b d #

first :: (a -> b) -> Def a c -> Def b c #

second :: (b -> c) -> Def a b -> Def a c #

Functor (Def ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> Def ty a -> Def ty b #

(<$) :: a -> Def ty b -> Def ty a #

(Data ty, Data ctor) => Data (Def ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Def ty ctor -> c (Def ty ctor) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Def ty ctor) #

toConstr :: Def ty ctor -> Constr #

dataTypeOf :: Def ty ctor -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Def ty ctor)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Def ty ctor)) #

gmapT :: (forall b. Data b => b -> b) -> Def ty ctor -> Def ty ctor #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Def ty ctor -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Def ty ctor -> r #

gmapQ :: (forall d. Data d => d -> u) -> Def ty ctor -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Def ty ctor -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Def ty ctor -> m (Def ty ctor) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Def ty ctor -> m (Def ty ctor) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Def ty ctor -> m (Def ty ctor) #

Generic (Def ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (Def ty ctor) :: Type -> Type #

Methods

from :: Def ty ctor -> Rep (Def ty ctor) x #

to :: Rep (Def ty ctor) x -> Def ty ctor #

(Show ctor, Show ty) => Show (Def ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> Def ty ctor -> ShowS #

show :: Def ty ctor -> String #

showList :: [Def ty ctor] -> ShowS #

(Binary t, Binary c) => Binary (Def t c) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: Def t c -> Put #

get :: Get (Def t c) #

putList :: [Def t c] -> Put #

(Eq ctor, Eq ty) => Eq (Def ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: Def ty ctor -> Def ty ctor -> Bool #

(/=) :: Def ty ctor -> Def ty ctor -> Bool #

(Hashable ctor, Hashable ty) => Hashable (Def ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> Def ty ctor -> Int #

hash :: Def ty ctor -> Int #

PPrint a => PPrint (Def t a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Def t a -> Doc #

pprintPrec :: Int -> Tidy -> Def t a -> Doc #

Subable (Def ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

syms :: Def ty ctor -> [Symbol] #

substa :: (Symbol -> Symbol) -> Def ty ctor -> Def ty ctor #

substf :: (Symbol -> Expr) -> Def ty ctor -> Def ty ctor #

subst :: Subst -> Def ty ctor -> Def ty ctor #

subst1 :: Def ty ctor -> (Symbol, Expr) -> Def ty ctor #

Qualify (Def ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Def ty ctor -> Def ty ctor Source #

type Rep (Def ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (Def ty ctor)

data Body Source #

Measures

Constructors

E Expr

Measure Refinement: {v | v = e }

P Expr

Measure Refinement: {v | (? v) = p }

R Symbol Expr

Measure Refinement: {v | p}

Instances

Instances details
Data Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Body -> c Body #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Body #

toConstr :: Body -> Constr #

dataTypeOf :: Body -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Body) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Body) #

gmapT :: (forall b. Data b => b -> b) -> Body -> Body #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Body -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Body -> r #

gmapQ :: (forall d. Data d => d -> u) -> Body -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Body -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Body -> m Body #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Body -> m Body #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Body -> m Body #

Generic Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep Body :: Type -> Type #

Methods

from :: Body -> Rep Body x #

to :: Rep Body x -> Body #

Show Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> Body -> ShowS #

show :: Body -> String #

showList :: [Body] -> ShowS #

Binary Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: Body -> Put #

get :: Get Body #

putList :: [Body] -> Put #

Eq Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: Body -> Body -> Bool #

(/=) :: Body -> Body -> Bool #

Hashable Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> Body -> Int #

hash :: Body -> Int #

PPrint Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Body -> Doc #

pprintPrec :: Int -> Tidy -> Body -> Doc #

Subable Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

syms :: Body -> [Symbol] #

substa :: (Symbol -> Symbol) -> Body -> Body #

substf :: (Symbol -> Expr) -> Body -> Body #

subst :: Subst -> Body -> Body #

subst1 :: Body -> (Symbol, Expr) -> Body #

Qualify Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Body -> Body Source #

type Rep Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep Body

data MSpec ty ctor Source #

Constructors

MSpec 

Fields

Instances

Instances details
Bifunctor MSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

bimap :: (a -> b) -> (c -> d) -> MSpec a c -> MSpec b d #

first :: (a -> b) -> MSpec a c -> MSpec b c #

second :: (b -> c) -> MSpec a b -> MSpec a c #

Functor (MSpec ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> MSpec ty a -> MSpec ty b #

(<$) :: a -> MSpec ty b -> MSpec ty a #

(Data ty, Data ctor) => Data (MSpec ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MSpec ty ctor -> c (MSpec ty ctor) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (MSpec ty ctor) #

toConstr :: MSpec ty ctor -> Constr #

dataTypeOf :: MSpec ty ctor -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (MSpec ty ctor)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (MSpec ty ctor)) #

gmapT :: (forall b. Data b => b -> b) -> MSpec ty ctor -> MSpec ty ctor #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MSpec ty ctor -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MSpec ty ctor -> r #

gmapQ :: (forall d. Data d => d -> u) -> MSpec ty ctor -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> MSpec ty ctor -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) #

Eq ctor => Monoid (MSpec ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: MSpec ty ctor #

mappend :: MSpec ty ctor -> MSpec ty ctor -> MSpec ty ctor #

mconcat :: [MSpec ty ctor] -> MSpec ty ctor #

Eq ctor => Semigroup (MSpec ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(<>) :: MSpec ty ctor -> MSpec ty ctor -> MSpec ty ctor #

sconcat :: NonEmpty (MSpec ty ctor) -> MSpec ty ctor #

stimes :: Integral b => b -> MSpec ty ctor -> MSpec ty ctor #

Generic (MSpec ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (MSpec ty ctor) :: Type -> Type #

Methods

from :: MSpec ty ctor -> Rep (MSpec ty ctor) x #

to :: Rep (MSpec ty ctor) x -> MSpec ty ctor #

(Show ty, Show ctor, PPrint ctor, PPrint ty) => Show (MSpec ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> MSpec ty ctor -> ShowS #

show :: MSpec ty ctor -> String #

showList :: [MSpec ty ctor] -> ShowS #

(PPrint t, PPrint a) => PPrint (MSpec t a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> MSpec t a -> Doc #

pprintPrec :: Int -> Tidy -> MSpec t a -> Doc #

type Rep (MSpec ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (MSpec ty ctor)

Scoping Info

type BScope = Bool Source #

Information about scope Binders Scope in

Type Classes

data RClass ty Source #

Constructors

RClass 

Fields

Instances

Instances details
Functor RClass Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> RClass a -> RClass b #

(<$) :: a -> RClass b -> RClass a #

Data ty => Data (RClass ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RClass ty -> c (RClass ty) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RClass ty) #

toConstr :: RClass ty -> Constr #

dataTypeOf :: RClass ty -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RClass ty)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RClass ty)) #

gmapT :: (forall b. Data b => b -> b) -> RClass ty -> RClass ty #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RClass ty -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RClass ty -> r #

gmapQ :: (forall d. Data d => d -> u) -> RClass ty -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RClass ty -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RClass ty -> m (RClass ty) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RClass ty -> m (RClass ty) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RClass ty -> m (RClass ty) #

Generic (RClass ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (RClass ty) :: Type -> Type #

Methods

from :: RClass ty -> Rep (RClass ty) x #

to :: Rep (RClass ty) x -> RClass ty #

Show ty => Show (RClass ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> RClass ty -> ShowS #

show :: RClass ty -> String #

showList :: [RClass ty] -> ShowS #

Binary ty => Binary (RClass ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: RClass ty -> Put #

get :: Get (RClass ty) #

putList :: [RClass ty] -> Put #

Eq ty => Eq (RClass ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: RClass ty -> RClass ty -> Bool #

(/=) :: RClass ty -> RClass ty -> Bool #

Hashable ty => Hashable (RClass ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> RClass ty -> Int #

hash :: RClass ty -> Int #

PPrint t => PPrint (RClass t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RClass t -> Doc #

pprintPrec :: Int -> Tidy -> RClass t -> Doc #

type Rep (RClass ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (RClass ty) = D1 ('MetaData "RClass" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "RClass" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rcName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BTyCon) :*: S1 ('MetaSel ('Just "rcSupers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ty])) :*: (S1 ('MetaSel ('Just "rcTyVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [BTyVar]) :*: S1 ('MetaSel ('Just "rcMethods") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(LocSymbol, ty)]))))

KV Profiling

data KVKind Source #

KVar Profile --------------------------------------------------------------

Constructors

RecBindE Var

Recursive binder letrec x = ...

NonRecBindE Var

Non recursive binder let x = ...

TypeInstE 
PredInstE 
LamE 
CaseE Int

Int is the number of cases

LetE 
ProjectE

Projecting out field of

Instances

Instances details
Data KVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> KVKind -> c KVKind #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c KVKind #

toConstr :: KVKind -> Constr #

dataTypeOf :: KVKind -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c KVKind) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVKind) #

gmapT :: (forall b. Data b => b -> b) -> KVKind -> KVKind #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVKind -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVKind -> r #

gmapQ :: (forall d. Data d => d -> u) -> KVKind -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> KVKind -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> KVKind -> m KVKind #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> KVKind -> m KVKind #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> KVKind -> m KVKind #

Generic KVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep KVKind :: Type -> Type #

Methods

from :: KVKind -> Rep KVKind x #

to :: Rep KVKind x -> KVKind #

Show KVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

NFData KVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: KVKind -> () #

Eq KVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: KVKind -> KVKind -> Bool #

(/=) :: KVKind -> KVKind -> Bool #

Ord KVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Hashable KVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> KVKind -> Int #

hash :: KVKind -> Int #

PPrint KVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> KVKind -> Doc #

pprintPrec :: Int -> Tidy -> KVKind -> Doc #

type Rep KVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep KVKind = D1 ('MetaData "KVKind" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (((C1 ('MetaCons "RecBindE" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Var)) :+: C1 ('MetaCons "NonRecBindE" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Var))) :+: (C1 ('MetaCons "TypeInstE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PredInstE" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "LamE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CaseE" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :+: (C1 ('MetaCons "LetE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ProjectE" 'PrefixI 'False) (U1 :: Type -> Type))))

data KVProf Source #

Instances

Instances details
Generic KVProf Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep KVProf :: Type -> Type #

Methods

from :: KVProf -> Rep KVProf x #

to :: Rep KVProf x -> KVProf #

NFData KVProf Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: KVProf -> () #

PPrint KVProf Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> KVProf -> Doc #

pprintPrec :: Int -> Tidy -> KVProf -> Doc #

type Rep KVProf Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep KVProf = D1 ('MetaData "KVProf" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'True) (C1 ('MetaCons "KVP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap KVKind Int))))

Misc

mapRTAVars :: (a -> b) -> RTAlias a ty -> RTAlias b ty Source #

insertsSEnv :: SEnv a -> [(Symbol, a)] -> SEnv a Source #

CoreToLogic

data LogicMap Source #

Constructors

LM 

Fields

toLogicMap :: [(LocSymbol, [Symbol], Expr)] -> LogicMap Source #

eAppWithMap :: LogicMap -> Located Symbol -> [Expr] -> Expr -> Expr Source #

data LMap Source #

Constructors

LMap 

Fields

Instances

Instances details
Show LMap Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> LMap -> ShowS #

show :: LMap -> String #

showList :: [LMap] -> ShowS #

PPrint LMap Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> LMap -> Doc #

pprintPrec :: Int -> Tidy -> LMap -> Doc #

Refined Instances

newtype DEnv x ty Source #

Constructors

DEnv (HashMap x (HashMap Symbol (RISig ty))) 

Instances

Instances details
Functor (DEnv x) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> DEnv x a -> DEnv x b #

(<$) :: a -> DEnv x b -> DEnv x a #

Hashable x => Monoid (DEnv x ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: DEnv x ty #

mappend :: DEnv x ty -> DEnv x ty -> DEnv x ty #

mconcat :: [DEnv x ty] -> DEnv x ty #

Hashable x => Semigroup (DEnv x ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(<>) :: DEnv x ty -> DEnv x ty -> DEnv x ty #

sconcat :: NonEmpty (DEnv x ty) -> DEnv x ty #

stimes :: Integral b => b -> DEnv x ty -> DEnv x ty #

(Show x, Show ty) => Show (DEnv x ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> DEnv x ty -> ShowS #

show :: DEnv x ty -> String #

showList :: [DEnv x ty] -> ShowS #

data RInstance t Source #

Refined Instances ---------------------------------------------------------

Constructors

RI 

Fields

Instances

Instances details
Functor RInstance Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> RInstance a -> RInstance b #

(<$) :: a -> RInstance b -> RInstance a #

Data t => Data (RInstance t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RInstance t -> c (RInstance t) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RInstance t) #

toConstr :: RInstance t -> Constr #

dataTypeOf :: RInstance t -> DataType #

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (RInstance t)) #

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (RInstance t)) #

gmapT :: (forall b. Data b => b -> b) -> RInstance t -> RInstance t #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RInstance t -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RInstance t -> r #

gmapQ :: (forall d. Data d => d -> u) -> RInstance t -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RInstance t -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RInstance t -> m (RInstance t) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RInstance t -> m (RInstance t) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RInstance t -> m (RInstance t) #

Generic (RInstance t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (RInstance t) :: Type -> Type #

Methods

from :: RInstance t -> Rep (RInstance t) x #

to :: Rep (RInstance t) x -> RInstance t #

Show t => Show (RInstance t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Binary t => Binary (RInstance t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: RInstance t -> Put #

get :: Get (RInstance t) #

putList :: [RInstance t] -> Put #

Eq t => Eq (RInstance t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: RInstance t -> RInstance t -> Bool #

(/=) :: RInstance t -> RInstance t -> Bool #

Hashable t => Hashable (RInstance t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> RInstance t -> Int #

hash :: RInstance t -> Int #

PPrint t => PPrint (RInstance t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RInstance t -> Doc #

pprintPrec :: Int -> Tidy -> RInstance t -> Doc #

type Rep (RInstance t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (RInstance t) = D1 ('MetaData "RInstance" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "RI" 'PrefixI 'True) (S1 ('MetaSel ('Just "riclass") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BTyCon) :*: (S1 ('MetaSel ('Just "ritype") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [t]) :*: S1 ('MetaSel ('Just "risigs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(LocSymbol, RISig t)]))))

data RISig t Source #

Constructors

RIAssumed t 
RISig t 

Instances

Instances details
Functor RISig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> RISig a -> RISig b #

(<$) :: a -> RISig b -> RISig a #

Data t => Data (RISig t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RISig t -> c (RISig t) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RISig t) #

toConstr :: RISig t -> Constr #

dataTypeOf :: RISig t -> DataType #

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (RISig t)) #

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (RISig t)) #

gmapT :: (forall b. Data b => b -> b) -> RISig t -> RISig t #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RISig t -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RISig t -> r #

gmapQ :: (forall d. Data d => d -> u) -> RISig t -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RISig t -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RISig t -> m (RISig t) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RISig t -> m (RISig t) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RISig t -> m (RISig t) #

Generic (RISig t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (RISig t) :: Type -> Type #

Methods

from :: RISig t -> Rep (RISig t) x #

to :: Rep (RISig t) x -> RISig t #

Show t => Show (RISig t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> RISig t -> ShowS #

show :: RISig t -> String #

showList :: [RISig t] -> ShowS #

Binary t => Binary (RISig t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: RISig t -> Put #

get :: Get (RISig t) #

putList :: [RISig t] -> Put #

Eq t => Eq (RISig t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: RISig t -> RISig t -> Bool #

(/=) :: RISig t -> RISig t -> Bool #

Hashable t => Hashable (RISig t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> RISig t -> Int #

hash :: RISig t -> Int #

PPrint t => PPrint (RISig t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RISig t -> Doc #

pprintPrec :: Int -> Tidy -> RISig t -> Doc #

type Rep (RISig t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (RISig t) = D1 ('MetaData "RISig" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "RIAssumed" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "RISig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)))

data RILaws ty Source #

Constructors

RIL 

Fields

Instances

Instances details
Functor RILaws Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> RILaws a -> RILaws b #

(<$) :: a -> RILaws b -> RILaws a #

Data ty => Data (RILaws ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RILaws ty -> c (RILaws ty) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RILaws ty) #

toConstr :: RILaws ty -> Constr #

dataTypeOf :: RILaws ty -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RILaws ty)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RILaws ty)) #

gmapT :: (forall b. Data b => b -> b) -> RILaws ty -> RILaws ty #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RILaws ty -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RILaws ty -> r #

gmapQ :: (forall d. Data d => d -> u) -> RILaws ty -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RILaws ty -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RILaws ty -> m (RILaws ty) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RILaws ty -> m (RILaws ty) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RILaws ty -> m (RILaws ty) #

Generic (RILaws ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (RILaws ty) :: Type -> Type #

Methods

from :: RILaws ty -> Rep (RILaws ty) x #

to :: Rep (RILaws ty) x -> RILaws ty #

Show ty => Show (RILaws ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> RILaws ty -> ShowS #

show :: RILaws ty -> String #

showList :: [RILaws ty] -> ShowS #

Binary t => Binary (RILaws t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: RILaws t -> Put #

get :: Get (RILaws t) #

putList :: [RILaws t] -> Put #

Eq ty => Eq (RILaws ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: RILaws ty -> RILaws ty -> Bool #

(/=) :: RILaws ty -> RILaws ty -> Bool #

Hashable ty => Hashable (RILaws ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> RILaws ty -> Int #

hash :: RILaws ty -> Int #

PPrint t => PPrint (RILaws t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RILaws t -> Doc #

pprintPrec :: Int -> Tidy -> RILaws t -> Doc #

type Rep (RILaws ty) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (RILaws ty) = D1 ('MetaData "RILaws" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "RIL" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rilName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BTyCon) :*: S1 ('MetaSel ('Just "rilSupers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ty])) :*: (S1 ('MetaSel ('Just "rilTyArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ty]) :*: (S1 ('MetaSel ('Just "rilEqus") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(LocSymbol, LocSymbol)]) :*: S1 ('MetaSel ('Just "rilPos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located ()))))))

data MethodType t Source #

Constructors

MT 

Fields

Instances

Instances details
Show t => Show (MethodType t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Ureftable Instances

class Reftable r => UReftable r where Source #

Minimal complete definition

Nothing

Methods

ofUReft :: UReft Reft -> r Source #

Instances

Instances details
UReftable () Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

ofUReft :: UReft Reft -> () Source #

UReftable (UReft Reft) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

String Literals

data Axiom b s e Source #

Values Related to Specifications ------------------------------------

Constructors

Axiom 

Fields

Instances

Instances details
Show (Axiom Var Type CoreExpr) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Refined Function Info

newtype RFInfo Source #

Constructors

RFInfo 

Fields

Instances

Instances details
Data RFInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RFInfo -> c RFInfo #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RFInfo #

toConstr :: RFInfo -> Constr #

dataTypeOf :: RFInfo -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RFInfo) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RFInfo) #

gmapT :: (forall b. Data b => b -> b) -> RFInfo -> RFInfo #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RFInfo -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RFInfo -> r #

gmapQ :: (forall d. Data d => d -> u) -> RFInfo -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RFInfo -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RFInfo -> m RFInfo #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RFInfo -> m RFInfo #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RFInfo -> m RFInfo #

Generic RFInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep RFInfo :: Type -> Type #

Methods

from :: RFInfo -> Rep RFInfo x #

to :: Rep RFInfo x -> RFInfo #

Show RFInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Binary RFInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: RFInfo -> Put #

get :: Get RFInfo #

putList :: [RFInfo] -> Put #

NFData RFInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: RFInfo -> () #

Eq RFInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: RFInfo -> RFInfo -> Bool #

(/=) :: RFInfo -> RFInfo -> Bool #

Hashable RFInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> RFInfo -> Int #

hash :: RFInfo -> Int #

type Rep RFInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep RFInfo = D1 ('MetaData "RFInfo" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'True) (C1 ('MetaCons "RFInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "permitTC") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool))))

classRFInfoType :: Bool -> RType c tv r -> RType c tv r Source #

Orphan instances

Show DataCon Source # 
Instance details

Ord DataCon Source # 
Instance details

Ord TyCon Source # 
Instance details

Methods

compare :: TyCon -> TyCon -> Ordering #

(<) :: TyCon -> TyCon -> Bool #

(<=) :: TyCon -> TyCon -> Bool #

(>) :: TyCon -> TyCon -> Bool #

(>=) :: TyCon -> TyCon -> Bool #

max :: TyCon -> TyCon -> TyCon #

min :: TyCon -> TyCon -> TyCon #

Symbolic DataCon Source # 
Instance details

Methods

symbol :: DataCon -> Symbol #

Symbolic ModuleName Source # 
Instance details

Methods

symbol :: ModuleName -> Symbol #

PPrint DataCon Source # 
Instance details

Methods

pprintTidy :: Tidy -> DataCon -> Doc #

pprintPrec :: Int -> Tidy -> DataCon -> Doc #

PPrint TyThing Source # 
Instance details

Methods

pprintTidy :: Tidy -> TyThing -> Doc #

pprintPrec :: Int -> Tidy -> TyThing -> Doc #

NFData a => NFData (TError a) Source # 
Instance details

Methods

rnf :: TError a -> () #

Subable t => Subable (WithModel t) Source # 
Instance details

Methods

syms :: WithModel t -> [Symbol] #

substa :: (Symbol -> Symbol) -> WithModel t -> WithModel t #

substf :: (Symbol -> Expr) -> WithModel t -> WithModel t #

subst :: Subst -> WithModel t -> WithModel t #

subst1 :: WithModel t -> (Symbol, Expr) -> WithModel t #