liquidhaskell-0.8.10.2: Liquid Types for Haskell
Safe HaskellNone
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
Functor Located 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

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

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

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) #

TyConable LocSymbol Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Qualify BareMeasure Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify ModSpecs Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Eq a => Eq (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

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

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

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) #

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 #

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 #

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 #

NFData a => NFData (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

rnf :: Located a -> () #

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 #

Hashable a => Hashable (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

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

hash :: Located a -> Int #

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 #

Symbolic a => Symbolic (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Located a -> Symbol #

Loc (Located a) 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

srcSpan :: Located a -> SrcSpan #

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 #

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 #

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.8.10.2-9LffrKqL5487RhcCeFJUHY" '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
Eq BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

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 #

Ord BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Show BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

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 #

NFData BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: BTyCon -> () #

Binary BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: BTyCon -> Put #

get :: Get BTyCon #

putList :: [BTyCon] -> Put #

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 #

Loc BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: BTyCon -> SrcSpan #

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 #

TyConable BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Qualify BareType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareMeasure Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify ModSpecs 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 #

Binary (Spec LocBareType LocSymbol) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

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

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp BTyCon BTyVar (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 BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep BTyCon = D1 ('MetaData "BTyCon" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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
Eq BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

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 #

Ord BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Show BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

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 #

NFData BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: BTyVar -> () #

Binary BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: BTyVar -> Put #

get :: Get BTyVar #

putList :: [BTyVar] -> Put #

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 BareType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareMeasure Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify ModSpecs 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 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 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 ()) (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 ()) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp BTyCon BTyVar (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 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
Eq RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

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 #

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

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 #

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 #

Monoid REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: REnv #

mappend :: REnv -> REnv -> REnv #

mconcat :: [REnv] -> REnv #

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 -> () #

Hashable RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

hashWithSalt :: Int -> RTyCon -> Int #

hash :: RTyCon -> Int #

Exception Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

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 #

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

Qualify SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

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

REq SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Equality

FreeVar RTyCon RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

freeVars :: RTyCon -> [RTyVar]

SubsTy tv RSort Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

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 SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

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 RTyVar SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

(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 :: RRType r -> m (RRType r) Source #

refresh :: 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

Subable (RRProp Reft) Source #

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

Instance details

Defined in Language.Haskell.Liquid.Types.RefType

PPrint (CtxError SpecType) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

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 ()) 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

(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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 #

Show TyConInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Generic TyConInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep TyConInfo :: Type -> Type #

NFData TyConInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: TyConInfo -> () #

Default TyConInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

def :: 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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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

RImpF 

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
Show Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

showsPrec :: Int -> Error -> ShowS #

show :: Error -> String #

showList :: [Error] -> ShowS #

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 #

Monoid REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: REnv #

mappend :: REnv -> REnv -> REnv #

mconcat :: [REnv] -> REnv #

NFData REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: REnv -> () #

Exception Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

PPrint Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

pprintTidy :: Tidy -> Error -> Doc #

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

Result Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Qualify SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareMeasure Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify ModSpecs Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

REq SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Equality

SubsTy tv RSort Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

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 SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

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 RTyVar SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

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 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 Symbol Symbol (RTProp BTyCon BTyVar r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

(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 :: RRType r -> m (RRType r) Source #

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

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

Defined in Language.Haskell.Liquid.Types.RefType

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 BTyCon BTyVar ()) Sort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon 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 #

Exception [Error] 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

PPrint (CtxError SpecType) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

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

(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 #

(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 #

(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) #

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 #

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 #

(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 #

(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 #

(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 -> () #

(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 #

(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 #

(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 #

Reftable (RTProp RTyCon RTyVar ()) 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 BTyCon BTyVar ()) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp 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 (RType BTyCon BTyVar (UReft Reft)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

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 #

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

Defined in Language.Haskell.Liquid.Types.Types

type Rep (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 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 Symbol Symbol (RTProp BTyCon BTyVar r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

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

(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 #

(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 #

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: 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 #

(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 #

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 #

(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 ()) 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 #

(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 #

Reftable (RTProp RTyCon RTyVar ()) 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 BTyCon BTyVar ()) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

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

Defined in Language.Haskell.Liquid.Types.RefType

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
Eq RTyVar Source #

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

Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

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

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 #

Ord RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

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

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 #

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 #

Monoid REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: REnv #

mappend :: REnv -> REnv -> REnv #

mconcat :: [REnv] -> REnv #

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 -> () #

Hashable RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

hashWithSalt :: Int -> RTyVar -> Int #

hash :: RTyVar -> Int #

Exception Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

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 #

Result Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Qualify SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

REq SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Equality

FreeVar RTyCon RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

freeVars :: RTyCon -> [RTyVar]

SubsTy tv RSort Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

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 SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

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 RTyVar SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

(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 :: RRType r -> m (RRType r) Source #

refresh :: 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

Subable (RRProp Reft) Source #

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

Instance details

Defined in Language.Haskell.Liquid.Types.RefType

PPrint (CtxError SpecType) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

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 ()) 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

(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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 #

(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 #

(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) #

(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 #

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 #

(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 #

(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 #

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 #

dropImplicits :: RType c tv r -> RType c tv r 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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 RTyCon Source #

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

Instance details

Defined in Language.Haskell.Liquid.Types.Types

TyConable BTyCon Source # 
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 tv RSort Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (tv, RSort) -> Predicate -> Predicate 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 Symbol Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy tv ty () Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

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 SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

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 RTyVar SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

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 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 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 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 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 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 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 Symbol Symbol (RTProp BTyCon BTyVar r) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

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

Defined in Language.Haskell.Liquid.Types.RefType

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 BTyCon BTyVar ()) Sort Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon 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 #

Type Variables

data RTVar tv s Source #

Constructors

RTVar 

Fields

Instances

Instances details
SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon 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 #

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 #

(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) #

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 #

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 #

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: RTVar tv s -> () #

(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 #

(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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 #

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: 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 #

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 #

Eq (PVar t) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

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) #

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 #

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 #

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 #

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: PVar t -> () #

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 #

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
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 #

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) #

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) #

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 #

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 #

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: PVKind a -> () #

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 #

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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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
Eq Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

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 #

Show Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Generic Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep Predicate :: Type -> Type #

Semigroup Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Monoid 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 -> () #

Binary Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Hashable Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Subable Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Reftable Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

PPrint Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

SubsTy tv RSort Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy RTyVar RSort PrType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

subt :: (RTyVar, RSort) -> PrType -> PrType 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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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
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 #

Show Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

showsPrec :: Int -> Error -> ShowS #

show :: Error -> String #

showList :: [Error] -> ShowS #

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) #

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 #

Monoid REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: REnv #

mappend :: REnv -> REnv -> REnv #

mconcat :: [REnv] -> REnv #

NFData REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: REnv -> () #

Exception Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

PPrint Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

pprintTidy :: Tidy -> Error -> Doc #

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

Result Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Qualify SpecType 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 BareMeasure Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify ModSpecs Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

REq SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Equality

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

Defined in Language.Haskell.Liquid.Types.Fresh

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 #

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 #

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) #

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 #

Show (UReft Reft) Source # 
Instance details

Defined in Language.Haskell.Liquid.Transforms.RefSplit

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 #

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 #

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 #

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: UReft r -> () #

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 #

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 #

Exception [Error] Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Expression (UReft ()) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

expr :: UReft () -> Expr #

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 #

(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] #

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 #

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

REq (UReft Reft) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Equality

Methods

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

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 RTyCon RTyVar (UReft Reft)) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Reftable (RTProp BTyCon BTyVar (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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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)))

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 #

Show SizeFun Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

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 #

NFData SizeFun Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: SizeFun -> () #

Binary SizeFun Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: SizeFun -> Put #

get :: Get SizeFun #

putList :: [SizeFun] -> Put #

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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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
Eq DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

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 #

Ord DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Show DataDecl Source #

For debugging.

Instance details

Defined in Language.Haskell.Liquid.Types.Types

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 #

Binary DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: DataDecl -> Put #

get :: Get DataDecl #

putList :: [DataDecl] -> Put #

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 #

Loc DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: DataDecl -> SrcSpan #

PPrint DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

pprintTidy :: Tidy -> DataDecl -> Doc #

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

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
Eq DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

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 #

Ord DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Show DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

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 #

Binary DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: DataName -> Put #

get :: Get DataName #

putList :: [DataName] -> Put #

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 #

Loc DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: DataName -> SrcSpan #

PPrint DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> DataName -> Doc #

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

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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 #

Hashable DataCtor Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> DataCtor -> Int #

hash :: DataCtor -> Int #

Loc DataCtor Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: DataCtor -> SrcSpan #

PPrint DataCtor Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

pprintTidy :: Tidy -> DataCtor -> Doc #

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

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 #

Show DataConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PredType

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 #

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 #

PPrint DataConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PredType

Methods

pprintTidy :: Tidy -> DataConP -> Doc #

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

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
Eq DataDeclKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

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 #

Show DataDeclKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Generic DataDeclKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep DataDeclKind :: Type -> Type #

NFData DataDeclKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: DataDeclKind -> () #

Binary 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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 #

Show TyConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PredType

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 #

Loc TyConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: TyConP -> SrcSpan #

PPrint TyConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PredType

Methods

pprintTidy :: Tidy -> TyConP -> Doc #

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

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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 #

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 #

Monoid REnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: REnv #

mappend :: REnv -> REnv -> REnv #

mconcat :: [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, RType c tv r, r)] -> [(Symbol, RType c tv r, r)] -> RType c tv r -> RType c tv r Source #

bkArrowDeep :: RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a) Source #

bkArrow :: RType t t1 a -> (([Symbol], [RType t t1 a], [a]), ([Symbol], [RType t t1 a], [a]), RType t t1 a) Source #

safeBkArrow :: PPrint (RType t t1 a) => RType t t1 a -> (([Symbol], [RType t t1 a], [a]), ([Symbol], [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 #

rImpF :: Monoid r => Symbol -> RType c tv r -> 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 #

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 #

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 #

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
Eq Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

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

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

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 #

Show Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

showsPrec :: Int -> Oblig -> ShowS #

show :: Oblig -> String #

showList :: [Oblig] -> ShowS #

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 #

NFData Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

rnf :: Oblig -> () #

Binary Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

put :: Oblig -> Put #

get :: Get Oblig #

putList :: [Oblig] -> Put #

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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 #

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) #

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 #

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 #

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 #

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 #

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: AnnInfo a -> () #

ToJSON a => ToJSON (AnnInfo a) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.DiffCheck

FromJSON a => FromJSON (AnnInfo a) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.DiffCheck

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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 #

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 #

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 #

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 #

ToJSON (Output Doc) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.DiffCheck

FromJSON (Output Doc) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.DiffCheck

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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 Bool 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Bool -> Doc #

pprintPrec :: Int -> Tidy -> Bool -> 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 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 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 SourceError Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

PPrint AltCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Synthesize.Misc

Methods

pprintTidy :: Tidy -> AltCon -> Doc #

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

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 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 ErrMsg Source #

A whole bunch of PPrint instances follow ----------------------------------

Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> ErrMsg -> Doc #

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

PPrint SrcSpan Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

pprintTidy :: Tidy -> SrcSpan -> Doc #

pprintPrec :: Int -> Tidy -> SrcSpan -> 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 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 QBind 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> QBind -> Doc #

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

PPrint EbindSol 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> EbindSol -> Doc #

pprintPrec :: Int -> Tidy -> EbindSol -> 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 KIndex 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> KIndex -> Doc #

pprintPrec :: Int -> Tidy -> KIndex -> 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 Command 
Instance details

Defined in Language.Fixpoint.Smt.Types

Methods

pprintTidy :: Tidy -> Command -> Doc #

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

PPrint GFixSolution 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint Qualifier 
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 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 Rewrite 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> Rewrite -> Doc #

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

PPrint TheorySymbol 
Instance details

Defined in Language.Fixpoint.Types.Theories

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 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 Templates 
Instance details

Defined in Language.Fixpoint.Types.Templates

PPrint Trigger 
Instance details

Defined in Language.Fixpoint.Types.Triggers

Methods

pprintTidy :: Tidy -> Trigger -> Doc #

pprintPrec :: Int -> Tidy -> Trigger -> 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 KVSub 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> KVSub -> Doc #

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

PPrint SymConst 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> SymConst -> Doc #

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

PPrint Constant 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Constant -> Doc #

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

PPrint Brel 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Brel -> Doc #

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

PPrint Bop 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Bop -> Doc #

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

PPrint Expr 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Expr -> Doc #

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

PPrint FTycon 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> FTycon -> Doc #

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

PPrint DataField 
Instance details

Defined in Language.Fixpoint.Types.Sorts

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 TCArgs 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> TCArgs -> Doc #

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

PPrint Symbol 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

pprintTidy :: Tidy -> Symbol -> Doc #

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

PPrint SrcSpan 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

pprintTidy :: Tidy -> SrcSpan -> Doc #

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

PPrint Tidy Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Tidy -> Doc #

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

PPrint DocTable 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> DocTable -> Doc #

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

PPrint ParseError Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

PPrint Variance Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Variance

Methods

pprintTidy :: Tidy -> Variance -> Doc #

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

PPrint UserError Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

PPrint Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

pprintTidy :: Tidy -> Oblig -> Doc #

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

PPrint KVProf Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> KVProf -> Doc #

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

PPrint KVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> KVKind -> Doc #

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

PPrint Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Body -> Doc #

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

PPrint ModName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> ModName -> Doc #

pprintPrec :: Int -> Tidy -> ModName -> 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 SizeFun Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> SizeFun -> Doc #

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

PPrint DataCtor Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

pprintTidy :: Tidy -> DataCtor -> Doc #

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

PPrint DataName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> DataName -> Doc #

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

PPrint DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

pprintTidy :: Tidy -> DataDecl -> Doc #

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

PPrint RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RTyCon -> Doc #

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

PPrint BTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> BTyCon -> Doc #

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

PPrint RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RTyVar -> Doc #

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

PPrint BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> BTyVar -> Doc #

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

PPrint Predicate Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

PPrint TargetVars Source # 
Instance details

Defined in Language.Haskell.Liquid.GHC.Interface

PPrint DataConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PredType

Methods

pprintTidy :: Tidy -> DataConP -> Doc #

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

PPrint TyConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PredType

Methods

pprintTidy :: Tidy -> TyConP -> Doc #

pprintPrec :: Int -> Tidy -> TyConP -> 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 Pattern Source # 
Instance details

Defined in Language.Haskell.Liquid.GHC.Resugar

Methods

pprintTidy :: Tidy -> Pattern -> Doc #

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

PPrint TargetSpec Source #

Pretty Printing -----------------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.GHC.Interface

PPrint TargetInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.GHC.Interface

PPrint DiffCheck Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.DiffCheck

PPrint CGInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

pprintTidy :: Tidy -> CGInfo -> Doc #

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

PPrint WfC Source # 
Instance details

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

pprintTidy :: Tidy -> WfC -> Doc #

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

PPrint SubC Source # 
Instance details

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

pprintTidy :: Tidy -> SubC -> Doc #

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

PPrint CGEnv Source # 
Instance details

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

pprintTidy :: Tidy -> CGEnv -> Doc #

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

PPrint Stats 
Instance details

Defined in Language.Fixpoint.Utils.Statistics

Methods

pprintTidy :: Tidy -> Stats -> Doc #

pprintPrec :: Int -> Tidy -> Stats -> 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 (Maybe a) 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

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

pprintPrec :: Int -> Tidy -> Maybe a -> 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 (Bind Var) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Bind Var -> Doc #

pprintPrec :: Int -> Tidy -> Bind Var -> 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 #

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 (SimpC a) 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

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

pprintPrec :: Int -> Tidy -> SimpC 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 (Triggered a) 
Instance details

Defined in Language.Fixpoint.Types.Triggers

Methods

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

pprintPrec :: Int -> Tidy -> Triggered 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 (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 (SizedEnv a) 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

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

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

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 (CtxError SpecType) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

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 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 (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 (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 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 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 (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 (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 #

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 #

(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 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 (a, b) 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> (a, b) -> Doc #

pprintPrec :: Int -> Tidy -> (a, b) -> Doc #

(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 (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 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 (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 (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 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 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 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 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 #

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 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 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 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 #

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 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
Eq ModName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

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 #

Ord ModName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Show ModName Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

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 #

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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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
Eq ModType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

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 #

Ord ModType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Show ModType Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

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 #

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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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
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 #

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 #

(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
Eq Warning Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Show Warning Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

printWarning :: 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
Eq Cinfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Ord Cinfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

compare :: Cinfo -> Cinfo -> Ordering #

(<) :: Cinfo -> Cinfo -> Bool #

(<=) :: Cinfo -> Cinfo -> Bool #

(>) :: Cinfo -> Cinfo -> Bool #

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

max :: Cinfo -> Cinfo -> Cinfo #

min :: Cinfo -> Cinfo -> Cinfo #

Show Cinfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> Cinfo -> ShowS #

show :: Cinfo -> String #

showList :: [Cinfo] -> ShowS #

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 #

NFData Cinfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: Cinfo -> () #

Loc Cinfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: Cinfo -> SrcSpan #

Fixpoint Cinfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

toFix :: Cinfo -> Doc #

simplify :: Cinfo -> Cinfo #

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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 #

(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 #

(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) #

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 #

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 #

(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 #

(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 #

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 #

(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 #

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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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
Eq MeasureKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

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 #

Ord MeasureKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Show MeasureKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Generic MeasureKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep MeasureKind :: Type -> Type #

Binary 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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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) #

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 #

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 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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 #

(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 #

(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) #

(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 #

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 #

(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 #

(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 #

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 #

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 #

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
Eq Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

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 #

Show Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> Body -> ShowS #

show :: Body -> String #

showList :: [Body] -> ShowS #

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 #

Binary Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: Body -> Put #

get :: Get Body #

putList :: [Body] -> Put #

Hashable Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> Body -> Int #

hash :: Body -> Int #

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 #

PPrint Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Body -> Doc #

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

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) #

(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 #

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 #

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 #

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 #

(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 #

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 #

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) #

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 #

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 #

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 #

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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 
ImplictE 
ProjectE

Projecting out field of

Instances

Instances details
Eq KVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

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 #

Ord KVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Show KVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

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 #

NFData KVKind Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: KVKind -> () #

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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 "ImplictE" '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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 #

(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 #

(Eq x, 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 #

(Eq x, 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 #

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 #

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 #

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) #

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

Defined in Language.Haskell.Liquid.Types.Types

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 #

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 #

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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 #

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 #

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) #

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 #

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 #

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 #

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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 #

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 #

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) #

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 #

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 #

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 #

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-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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

Orphan instances

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 #

Show DataCon Source # 
Instance details

Show ModuleName Source # 
Instance details

Hashable ModuleName Source # 
Instance details

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 #