liquidhaskell-0.8.2.2: Liquid Types for Haskell

Safe HaskellNone
LanguageHaskell98

Language.Haskell.Liquid.Types

Contents

Description

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

Synopsis

Options

data Config Source #

Constructors

Config 

Fields

Instances

Eq Config Source # 

Methods

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

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

Data Config Source # 

Methods

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

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

toConstr :: Config -> Constr #

dataTypeOf :: Config -> DataType #

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

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

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

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

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

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

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

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

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

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

Show Config Source # 
Generic Config Source # 

Associated Types

type Rep Config :: * -> * #

Methods

from :: Config -> Rep Config x #

to :: Rep Config x -> Config #

Serialize Config Source # 
HasConfig Config Source # 
type Rep Config Source # 
type Rep Config

class HasConfig t where Source #

Minimal complete definition

getConfig

Instances

HasConfig Config Source # 
HasConfig GhcSpec Source # 
HasConfig GhcInfo Source # 
HasConfig BareEnv Source # 
HasConfig CGEnv Source # 

Ghc Information

data GhcInfo Source #

GHC Information : Code & Spec ------------------------------

Constructors

GI 

Fields

data GhcSpec Source #

The following is the overall type for specifications obtained from parsing the target source and dependent libraries

Constructors

SP 

Fields

data TargetVars Source #

Which Top-Level Binders Should be Verified

Constructors

AllVars 
Only ![Var] 

F.Located Things

data Located a :: * -> * #

Constructors

Loc 

Fields

Instances

Functor Located 

Methods

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

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

Foldable Located 

Methods

fold :: Monoid m => Located m -> 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 

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

Binary BareSpec # 

Methods

put :: BareSpec -> Put #

get :: Get BareSpec #

putList :: [BareSpec] -> Put #

TyConable LocSymbol Source # 
Resolvable LocSymbol Source # 
Eq a => Eq (Located a) 

Methods

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

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

Data a => Data (Located a) 

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

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) 

Methods

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

show :: Located a -> String #

showList :: [Located a] -> ShowS #

IsString a => IsString (Located a) 

Methods

fromString :: String -> Located a #

Generic (Located a) 

Associated Types

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

Methods

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

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

Binary a => Binary (Located a) 

Methods

put :: Located a -> Put #

get :: Get (Located a) #

putList :: [Located a] -> Put #

NFData a => NFData (Located a) 

Methods

rnf :: Located a -> () #

Hashable a => Hashable (Located a) 

Methods

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

hash :: Located a -> Int #

Expression a => Expression (Located a) 

Methods

expr :: Located a -> Expr #

Subable a => Subable (Located a) 

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) 

Methods

symbol :: Located a -> Symbol #

Loc (Located a) 

Methods

srcSpan :: Located a -> SrcSpan #

Fixpoint a => Fixpoint (Located a) 

Methods

toFix :: Located a -> Doc #

simplify :: Located a -> Located a #

PPrint a => PPrint (Located a) 

Methods

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

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

GhcLookup (Located Symbol) Source # 
ExpandAliases a => ExpandAliases (Located a) Source # 

Methods

expand :: SourcePos -> Located a -> BareM (Located a) Source #

type Rep (Located a) 
type Rep (Located a) = D1 * (MetaData "Located" "Language.Fixpoint.Types.Spans" "liquid-fixpoint-0.7.0.6-7ekgo2vNzFQLD9cAgffOsC" False) (C1 * (MetaCons "Loc" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "loc") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * SourcePos)) ((:*:) * (S1 * (MetaSel (Just Symbol "locE") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * SourcePos)) (S1 * (MetaSel (Just Symbol "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

Eq BTyCon Source # 

Methods

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

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

Data BTyCon Source # 

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

Show BTyCon Source # 
Generic BTyCon Source # 

Associated Types

type Rep BTyCon :: * -> * #

Methods

from :: BTyCon -> Rep BTyCon x #

to :: Rep BTyCon x -> BTyCon #

Binary BTyCon Source # 

Methods

put :: BTyCon -> Put #

get :: Get BTyCon #

putList :: [BTyCon] -> Put #

Binary BareSpec # 

Methods

put :: BareSpec -> Put #

get :: Get BareSpec #

putList :: [BareSpec] -> Put #

NFData BTyCon Source # 

Methods

rnf :: BTyCon -> () #

Symbolic BTyCon Source # 

Methods

symbol :: BTyCon -> Symbol #

Fixpoint BTyCon Source # 

Methods

toFix :: BTyCon -> Doc #

simplify :: BTyCon -> BTyCon #

PPrint BTyCon Source # 

Methods

pprintTidy :: Tidy -> BTyCon -> Doc #

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

TyConable BTyCon Source # 
FreeVar BTyCon BTyVar Source # 

Methods

freeVars :: BTyCon -> [BTyVar]

type Rep BTyCon Source # 
type Rep BTyCon = D1 * (MetaData "BTyCon" "Language.Haskell.Liquid.Types" "liquidhaskell-0.8.2.2-CpzODPl6eK730bIB0y0Im0" False) (C1 * (MetaCons "BTyCon" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "btc_tc") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * LocSymbol)) ((:*:) * (S1 * (MetaSel (Just Symbol "btc_class") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Bool)) (S1 * (MetaSel (Just Symbol "btc_prom") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Bool)))))

newtype BTyVar Source #

Constructors

BTV Symbol 

Instances

Eq BTyVar Source # 

Methods

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

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

Data BTyVar Source # 

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 :: (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 # 
Show BTyVar Source # 
IsString BTyVar Source # 

Methods

fromString :: String -> BTyVar #

Generic BTyVar Source # 

Associated Types

type Rep BTyVar :: * -> * #

Methods

from :: BTyVar -> Rep BTyVar x #

to :: Rep BTyVar x -> BTyVar #

Binary BTyVar Source # 

Methods

put :: BTyVar -> Put #

get :: Get BTyVar #

putList :: [BTyVar] -> Put #

Binary BareSpec # 

Methods

put :: BareSpec -> Put #

get :: Get BareSpec #

putList :: [BareSpec] -> Put #

NFData BTyVar Source # 

Methods

rnf :: BTyVar -> () #

Hashable BTyVar Source # 

Methods

hashWithSalt :: Int -> BTyVar -> Int #

hash :: BTyVar -> Int #

Symbolic BTyVar Source # 

Methods

symbol :: BTyVar -> Symbol #

PPrint BTyVar Source # 

Methods

pprintTidy :: Tidy -> BTyVar -> Doc #

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

FreeVar BTyCon BTyVar Source # 

Methods

freeVars :: BTyCon -> [BTyVar]

type Rep BTyVar Source # 
type Rep BTyVar

Refined Type Constructors

data RTyCon Source #

Constructors

RTyCon TyCon ![RPVar] !TyConInfo 

Instances

Eq RTyCon Source # 

Methods

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

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

Data RTyCon Source # 

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 :: (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 RTyCon Source # 
Generic RTyCon Source # 

Associated Types

type Rep RTyCon :: * -> * #

Methods

from :: RTyCon -> Rep RTyCon x #

to :: Rep RTyCon x -> RTyCon #

NFData RTyCon Source # 

Methods

rnf :: RTyCon -> () #

Fixpoint RTyCon Source # 

Methods

toFix :: RTyCon -> Doc #

simplify :: RTyCon -> RTyCon #

PPrint RTyCon Source # 

Methods

pprintTidy :: Tidy -> RTyCon -> Doc #

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

TyConable RTyCon Source #

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

SubStratum SpecType Source # 
Result Error Source # 
ExpandAliases SpecType Source # 
FreeVar RTyCon RTyVar Source # 

Methods

freeVars :: RTyCon -> [RTyVar]

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

Methods

fresh :: m (RRType r) Source #

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

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

SubStratum (Annot SpecType) Source # 
Result [Error] Source # 
type Rep RTyCon Source # 
type Rep RTyCon = D1 * (MetaData "RTyCon" "Language.Haskell.Liquid.Types" "liquidhaskell-0.8.2.2-CpzODPl6eK730bIB0y0Im0" False) (C1 * (MetaCons "RTyCon" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "rtc_tc") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * TyCon)) ((:*:) * (S1 * (MetaSel (Just Symbol "rtc_pvars") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * [RPVar])) (S1 * (MetaSel (Just Symbol "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

Data TyConInfo Source # 

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 :: (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 # 
Generic TyConInfo Source # 

Associated Types

type Rep TyConInfo :: * -> * #

NFData TyConInfo Source # 

Methods

rnf :: TyConInfo -> () #

Default TyConInfo Source # 

Methods

def :: TyConInfo #

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

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

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

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

Accessors for RTyCon

Refinement Types

data RType c tv r Source #

Constructors

RVar 

Fields

RFun 

Fields

RAllT 

Fields

RAllP

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

Fields

RAllS

"forall w . TYPE" ^^^^^ (rt_sbind)

Fields

RApp 

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

Binary BareSpec # 

Methods

put :: BareSpec -> Put #

get :: Get BareSpec #

putList :: [BareSpec] -> Put #

SubStratum SpecType Source # 
Result Error Source # 
ExpandAliases SpecType Source # 
Freshable BareM Integer Source # 
(Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) Source # 

Methods

fresh :: m (RRType r) Source #

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

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

SubStratum (Annot SpecType) Source # 
Result [Error] Source # 
Functor (RType c tv) Source # 

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 # 

Methods

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

show :: RTVU c tv -> String #

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

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

Methods

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

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

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

Methods

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

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

toConstr :: RType c tv r -> Constr #

dataTypeOf :: RType c tv r -> DataType #

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

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

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

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

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

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

Generic (RType c tv r) Source # 

Associated Types

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

Methods

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

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

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

Methods

put :: RType c tv r -> Put #

get :: Get (RType c tv r) #

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

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

Methods

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

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

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 # 

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 #

type Rep (RType c tv r) Source # 
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

Functor (Ref τ) Source # 

Methods

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

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

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

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 (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (Ref τ t)) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t 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 :: (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 # 

Associated Types

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

Methods

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

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

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

Methods

put :: Ref τ t -> Put #

get :: Get (Ref τ t) #

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

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

Methods

rnf :: Ref τ t -> () #

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

Methods

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

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

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

Methods

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

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

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

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

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

type Rep (Ref τ t) Source # 
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

Data RTyVar Source # 

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

Generic RTyVar Source # 

Associated Types

type Rep RTyVar :: * -> * #

Methods

from :: RTyVar -> Rep RTyVar x #

to :: Rep RTyVar x -> RTyVar #

NFData RTyVar Source # 

Methods

rnf :: RTyVar -> () #

Symbolic RTyVar Source # 

Methods

symbol :: RTyVar -> Symbol #

PPrint RTyVar Source # 

Methods

pprintTidy :: Tidy -> RTyVar -> Doc #

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

SubStratum SpecType Source # 
Result Error Source # 
ExpandAliases SpecType Source # 
FreeVar RTyCon RTyVar Source # 

Methods

freeVars :: RTyCon -> [RTyVar]

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

Methods

fresh :: m (RRType r) Source #

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

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

SubStratum (Annot SpecType) Source # 
Result [Error] Source # 
type Rep RTyVar Source # 
type Rep RTyVar = D1 * (MetaData "RTyVar" "Language.Haskell.Liquid.Types" "liquidhaskell-0.8.2.2-CpzODPl6eK730bIB0y0Im0" True) (C1 * (MetaCons "RTV" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * TyVar)))

data RTAlias x a Source #

Refinement Type Aliases

Constructors

RTA 

Fields

Instances

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

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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTAlias x a -> r #

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

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

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

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

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

Generic (RTAlias x a) Source # 

Associated Types

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

Methods

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

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

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

Methods

put :: RTAlias x a -> Put #

get :: Get (RTAlias x a) #

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

type Rep (RTAlias x a) Source # 
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 -> RTAlias Symbol Expr Source #

Worlds

data HSeg t Source #

Constructors

HBind 

Fields

HVar UsedPVar 

Instances

Data t => Data (HSeg t) Source # 

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 (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (HSeg t)) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t 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 :: (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 # 

Associated Types

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

Methods

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

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

type Rep (HSeg t) Source # 
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

Data t => Data (World t) Source # 

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 (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (World t)) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t 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 :: (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 # 

Associated Types

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

Methods

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

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

type Rep (World t) Source # 
type Rep (World t) = D1 * (MetaData "World" "Language.Haskell.Liquid.Types" "liquidhaskell-0.8.2.2-CpzODPl6eK730bIB0y0Im0" True) (C1 * (MetaCons "World" PrefixI False) (S1 * (MetaSel (Nothing 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

class SubsTy tv ty a where Source #

Minimal complete definition

subt

Methods

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

Type Variables

data RTVar tv s Source #

Constructors

RTVar 

Fields

Instances

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

Methods

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

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

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

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

Methods

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

show :: RTVU c tv -> String #

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

Generic (RTVar tv s) Source # 

Associated Types

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

Methods

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

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

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

Methods

put :: RTVar tv s -> Put #

get :: Get (RTVar tv s) #

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

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

Methods

rnf :: RTVar tv s -> () #

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

Methods

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

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

type Rep (RTVar tv s) Source # 
type Rep (RTVar tv s) = D1 * (MetaData "RTVar" "Language.Haskell.Liquid.Types" "liquidhaskell-0.8.2.2-CpzODPl6eK730bIB0y0Im0" False) (C1 * (MetaCons "RTVar" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "ty_var_value") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * tv)) (S1 * (MetaSel (Just Symbol "ty_var_info") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (RTVInfo s)))))

data RTVInfo s Source #

Constructors

RTVNoInfo 
RTVInfo 

Fields

Instances

Functor RTVInfo Source # 

Methods

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

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

Data s => Data (RTVInfo s) Source # 

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

Associated Types

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

Methods

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

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

Binary s => Binary (RTVInfo s) Source # 

Methods

put :: RTVInfo s -> Put #

get :: Get (RTVInfo s) #

putList :: [RTVInfo s] -> Put #

NFData s => NFData (RTVInfo s) Source # 

Methods

rnf :: RTVInfo s -> () #

type Rep (RTVInfo s) Source # 
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 #

Predicate Variables

data PVar t Source #

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

Constructors

PV 

Fields

Instances

Functor PVar Source # 

Methods

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

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

Subable UsedPVar Source # 
Eq (PVar t) Source # 

Methods

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

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

Data t => Data (PVar t) Source # 

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 (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (PVar t)) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t 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 :: (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 # 

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 # 

Methods

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

show :: PVar t -> String #

showList :: [PVar t] -> ShowS #

Generic (PVar t) Source # 

Associated Types

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

Methods

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

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

Binary t => Binary (PVar t) Source # 

Methods

put :: PVar t -> Put #

get :: Get (PVar t) #

putList :: [PVar t] -> Put #

NFData t => NFData (PVar t) Source # 

Methods

rnf :: PVar t -> () #

Hashable (PVar a) Source # 

Methods

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

hash :: PVar a -> Int #

PPrint (PVar a) Source # 

Methods

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

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

Resolvable t => Resolvable (PVar t) Source # 

Methods

resolve :: SourcePos -> PVar t -> BareM (PVar t) Source #

type Rep (PVar t) Source # 
type Rep (PVar t)

pvType :: PVar t -> t Source #

data PVKind t Source #

Constructors

PVProp t 
PVHProp 

Instances

Functor PVKind Source # 

Methods

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

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

Foldable PVKind Source # 

Methods

fold :: Monoid m => PVKind m -> 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 # 

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

Data t => Data (PVKind t) Source # 

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 (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (PVKind t)) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t 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 :: (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 # 

Methods

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

show :: PVKind t -> String #

showList :: [PVKind t] -> ShowS #

Generic (PVKind t) Source # 

Associated Types

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

Methods

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

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

Binary a => Binary (PVKind a) Source # 

Methods

put :: PVKind a -> Put #

get :: Get (PVKind a) #

putList :: [PVKind a] -> Put #

NFData a => NFData (PVKind a) Source # 

Methods

rnf :: PVKind a -> () #

type Rep (PVKind t) Source # 
type Rep (PVKind t) = D1 * (MetaData "PVKind" "Language.Haskell.Liquid.Types" "liquidhaskell-0.8.2.2-CpzODPl6eK730bIB0y0Im0" False) ((:+:) * (C1 * (MetaCons "PVProp" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))) (C1 * (MetaCons "PVHProp" PrefixI False) (U1 *)))

newtype Predicate Source #

Constructors

Pr [UsedPVar] 

Instances

Data Predicate Source # 

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

Generic Predicate Source # 

Associated Types

type Rep Predicate :: * -> * #

Monoid Predicate Source # 
Binary Predicate Source # 
NFData Predicate Source # 

Methods

rnf :: Predicate -> () #

Subable Predicate Source # 
Reftable Predicate Source # 
PPrint Predicate Source # 
Resolvable Predicate Source # 
type Rep Predicate Source # 
type Rep Predicate = D1 * (MetaData "Predicate" "Language.Haskell.Liquid.Types" "liquidhaskell-0.8.2.2-CpzODPl6eK730bIB0y0Im0" True) (C1 * (MetaCons "Pr" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [UsedPVar])))

Refinements

data UReft r Source #

Constructors

MkUReft 

Fields

Instances

Functor UReft Source # 

Methods

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

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

Foldable UReft Source # 

Methods

fold :: Monoid m => UReft m -> 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 # 

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

Binary BareSpec # 

Methods

put :: BareSpec -> Put #

get :: Get BareSpec #

putList :: [BareSpec] -> Put #

SubStratum SpecType Source # 
Result Error Source # 
ExpandAliases SpecType Source # 
ExpandAliases RReft Source # 
Freshable m Integer => Freshable m RReft Source # 
Freshable BareM Integer Source # 
Data r => Data (UReft r) Source # 

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 a. Data b => c (b -> a) -> c a) -> (forall a. a -> c a) -> 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 :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UReft r -> r #

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

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

Generic (UReft r) Source # 

Associated Types

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

Methods

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

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

Monoid a => Monoid (UReft a) Source # 

Methods

mempty :: UReft a #

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

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

Binary r => Binary (UReft r) Source # 

Methods

put :: UReft r -> Put #

get :: Get (UReft r) #

putList :: [UReft r] -> Put #

NFData r => NFData (UReft r) Source # 

Methods

rnf :: UReft r -> () #

Expression (UReft ()) Source # 

Methods

expr :: UReft () -> Expr #

Subable r => Subable (UReft r) Source # 

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 # 

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

UReftable (UReft Reft) Source # 
SubStratum (Annot SpecType) Source # 
Result [Error] Source # 
Resolvable (UReft Reft) Source # 
type Rep (UReft r) Source # 
type Rep (UReft r) = D1 * (MetaData "UReft" "Language.Haskell.Liquid.Types" "liquidhaskell-0.8.2.2-CpzODPl6eK730bIB0y0Im0" False) (C1 * (MetaCons "MkUReft" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "ur_reft") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * r)) ((:*:) * (S1 * (MetaSel (Just Symbol "ur_pred") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Predicate)) (S1 * (MetaSel (Just Symbol "ur_strata") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Strata)))))

Parse-time entities describing refined data types

data SizeFun Source #

Termination expressions

Constructors

IdSizeFun

x -> F.EVar x

SymSizeFun LocSymbol

x -> f x

Instances

Data SizeFun Source # 

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 :: (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 # 
Generic SizeFun Source # 

Associated Types

type Rep SizeFun :: * -> * #

Methods

from :: SizeFun -> Rep SizeFun x #

to :: Rep SizeFun x -> SizeFun #

Binary SizeFun Source # 

Methods

put :: SizeFun -> Put #

get :: Get SizeFun #

putList :: [SizeFun] -> Put #

NFData SizeFun Source # 

Methods

rnf :: SizeFun -> () #

PPrint SizeFun Source # 

Methods

pprintTidy :: Tidy -> SizeFun -> Doc #

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

type Rep SizeFun Source # 
type Rep SizeFun = D1 * (MetaData "SizeFun" "Language.Haskell.Liquid.Types" "liquidhaskell-0.8.2.2-CpzODPl6eK730bIB0y0Im0" False) ((:+:) * (C1 * (MetaCons "IdSizeFun" PrefixI False) (U1 *)) (C1 * (MetaCons "SymSizeFun" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * LocSymbol))))

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

data DataDecl Source #

Data type refinements

Constructors

D 

Fields

Instances

Eq DataDecl Source # 
Data DataDecl Source # 

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 :: (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 # 
Show DataDecl Source #

For debugging.

Generic DataDecl Source # 

Associated Types

type Rep DataDecl :: * -> * #

Methods

from :: DataDecl -> Rep DataDecl x #

to :: Rep DataDecl x -> DataDecl #

Binary DataDecl Source # 

Methods

put :: DataDecl -> Put #

get :: Get DataDecl #

putList :: [DataDecl] -> Put #

Symbolic DataDecl Source # 

Methods

symbol :: DataDecl -> Symbol #

Loc DataDecl Source # 

Methods

srcSpan :: DataDecl -> SrcSpan #

type Rep DataDecl Source # 

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

Eq DataName Source # 
Data DataName Source # 

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 :: (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 # 
Show DataName Source # 
Generic DataName Source # 

Associated Types

type Rep DataName :: * -> * #

Methods

from :: DataName -> Rep DataName x #

to :: Rep DataName x -> DataName #

Binary DataName Source # 

Methods

put :: DataName -> Put #

get :: Get DataName #

putList :: [DataName] -> Put #

Hashable DataName Source # 

Methods

hashWithSalt :: Int -> DataName -> Int #

hash :: DataName -> Int #

Symbolic DataName Source # 

Methods

symbol :: DataName -> Symbol #

Loc DataName Source # 

Methods

srcSpan :: DataName -> SrcSpan #

PPrint DataName Source # 

Methods

pprintTidy :: Tidy -> DataName -> Doc #

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

GhcLookup DataName Source # 
type Rep DataName Source # 
type Rep DataName = D1 * (MetaData "DataName" "Language.Haskell.Liquid.Types" "liquidhaskell-0.8.2.2-CpzODPl6eK730bIB0y0Im0" False) ((:+:) * (C1 * (MetaCons "DnName" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * LocSymbol))) (C1 * (MetaCons "DnCon" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * LocSymbol))))

data DataCtor Source #

Data Constructor

Constructors

DataCtor 

Fields

Instances

Data DataCtor Source # 

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

Associated Types

type Rep DataCtor :: * -> * #

Methods

from :: DataCtor -> Rep DataCtor x #

to :: Rep DataCtor x -> DataCtor #

Binary DataCtor Source # 

Methods

put :: DataCtor -> Put #

get :: Get DataCtor #

putList :: [DataCtor] -> Put #

Loc DataCtor Source # 

Methods

srcSpan :: DataCtor -> SrcSpan #

type Rep DataCtor Source # 

data DataConP Source #

Constructors

DataConP 

Fields

Instances

Data DataConP Source # 

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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataConP -> r #

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

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

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

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

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

Generic DataConP Source # 

Associated Types

type Rep DataConP :: * -> * #

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'.

Methods

srcSpan :: DataConP -> SrcSpan #

ExpandAliases DataConP Source # 
type Rep DataConP Source # 

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

Eq DataDeclKind Source # 
Data DataDeclKind Source # 

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 :: (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 # 
Generic DataDeclKind Source # 

Associated Types

type Rep DataDeclKind :: * -> * #

Binary DataDeclKind Source # 
NFData DataDeclKind Source # 

Methods

rnf :: DataDeclKind -> () #

type Rep DataDeclKind Source # 
type Rep DataDeclKind = D1 * (MetaData "DataDeclKind" "Language.Haskell.Liquid.Types" "liquidhaskell-0.8.2.2-CpzODPl6eK730bIB0y0Im0" False) ((:+:) * (C1 * (MetaCons "DataUser" PrefixI False) (U1 *)) (C1 * (MetaCons "DataReflected" PrefixI False) (U1 *)))

data TyConP Source #

Instances

Data TyConP Source # 

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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyConP -> r #

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

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

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

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

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

Generic TyConP Source # 

Associated Types

type Rep TyConP :: * -> * #

Methods

from :: TyConP -> Rep TyConP x #

to :: Rep TyConP x -> TyConP #

type Rep TyConP Source # 
type Rep TyConP

Pre-instantiated RType

type RRProp r = Ref RSort (RRType r) Source #

type BRProp r = Ref BSort (BRType r) Source #

type BSort = BRType () Source #

type RTVU c tv = RTVar tv (RType c tv ()) Source #

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

data REnv 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

Constructors

REnv 

Fields

Instances

NFData REnv Source # 

Methods

rnf :: REnv -> () #

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 ())] -> [PVar (RType c tv ())] -> [Symbol] -> [(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], RType t t1 a) Source #

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

mkUnivs :: (Foldable t, Foldable t1, Foldable t2) => t (RTVar tv (RType c tv ())) -> t1 (PVar (RType c tv ())) -> t2 Symbol -> RType c tv r -> RType c tv r Source #

bkUniv :: RType t1 a t2 -> ([RTVar a (RType t1 a ())], [PVar (RType t1 a ())], [Symbol], RType t1 a t2) Source #

bkClass :: TyConable c => RType c tv r -> ([(c, [RType c tv r])], RType c tv r) Source #

rFun :: Monoid r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r Source #

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) -> (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) => (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) -> (RType c tv r -> b) -> (SEnv b -> Maybe (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a 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 #

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

Data Oblig Source # 

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

Methods

showsPrec :: Int -> Oblig -> ShowS #

show :: Oblig -> String #

showList :: [Oblig] -> ShowS #

Generic Oblig Source # 

Associated Types

type Rep Oblig :: * -> * #

Methods

from :: Oblig -> Rep Oblig x #

to :: Rep Oblig x -> Oblig #

Binary Oblig Source # 

Methods

put :: Oblig -> Put #

get :: Get Oblig #

putList :: [Oblig] -> Put #

NFData Oblig Source # 

Methods

rnf :: Oblig -> () #

PPrint Oblig Source # 

Methods

pprintTidy :: Tidy -> Oblig -> Doc #

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

type Rep Oblig Source # 
type Rep Oblig = D1 * (MetaData "Oblig" "Language.Haskell.Liquid.Types.Errors" "liquidhaskell-0.8.2.2-CpzODPl6eK730bIB0y0Im0" False) ((:+:) * (C1 * (MetaCons "OTerm" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "OInv" PrefixI False) (U1 *)) (C1 * (MetaCons "OCons" PrefixI False) (U1 *))))

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

Functor AnnInfo Source # 

Methods

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

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

Data a => Data (AnnInfo a) Source # 

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

Generic (AnnInfo a) Source # 

Associated Types

type Rep (AnnInfo a) :: * -> * #

Methods

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

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

Monoid (AnnInfo a) Source # 

Methods

mempty :: AnnInfo a #

mappend :: AnnInfo a -> AnnInfo a -> AnnInfo a #

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

NFData a => NFData (AnnInfo a) Source # 

Methods

rnf :: AnnInfo a -> () #

type Rep (AnnInfo a) Source # 
type Rep (AnnInfo a) = D1 * (MetaData "AnnInfo" "Language.Haskell.Liquid.Types" "liquidhaskell-0.8.2.2-CpzODPl6eK730bIB0y0Im0" True) (C1 * (MetaCons "AI" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (HashMap SrcSpan [(Maybe Text, a)]))))

data Annot t Source #

Constructors

AnnUse t 
AnnDef t 
AnnRDf t 
AnnLoc SrcSpan 

Instances

Functor Annot Source # 

Methods

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

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

Data t => Data (Annot t) Source # 

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 (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (Annot t)) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t 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 :: (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 # 

Associated Types

type Rep (Annot t) :: * -> * #

Methods

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

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

NFData a => NFData (Annot a) Source # 

Methods

rnf :: Annot a -> () #

SubStratum (Annot SpecType) Source # 
type Rep (Annot t) Source # 

Overall Output

data Output a Source #

Output --------------------------------------------------------------------

Constructors

O 

Fields

Instances

Functor Output Source # 

Methods

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

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

Generic (Output a) Source # 

Associated Types

type Rep (Output a) :: * -> * #

Methods

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

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

Monoid (Output a) Source # 

Methods

mempty :: Output a #

mappend :: Output a -> Output a -> Output a #

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

type Rep (Output a) Source # 

Refinement Hole

hole :: Expr Source #

isHole :: Expr -> 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

Methods

pprintTidy :: Tidy -> a -> Doc #

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

Instances

PPrint Bool 

Methods

pprintTidy :: Tidy -> Bool -> Doc #

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

PPrint Float 

Methods

pprintTidy :: Tidy -> Float -> Doc #

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

PPrint Int 

Methods

pprintTidy :: Tidy -> Int -> Doc #

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

PPrint Integer 

Methods

pprintTidy :: Tidy -> Integer -> Doc #

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

PPrint () 

Methods

pprintTidy :: Tidy -> () -> Doc #

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

PPrint Doc 

Methods

pprintTidy :: Tidy -> Doc -> Doc #

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

PPrint Text 

Methods

pprintTidy :: Tidy -> Text -> Doc #

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

PPrint Stats 

Methods

pprintTidy :: Tidy -> Stats -> Doc #

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

PPrint Error1 

Methods

pprintTidy :: Tidy -> Error1 -> Doc #

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

PPrint CVertex 

Methods

pprintTidy :: Tidy -> CVertex -> Doc #

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

PPrint KVGraph 

Methods

pprintTidy :: Tidy -> KVGraph -> Doc #

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

PPrint Rank 

Methods

pprintTidy :: Tidy -> Rank -> Doc #

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

PPrint QBind 

Methods

pprintTidy :: Tidy -> QBind -> Doc #

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

PPrint Cube 

Methods

pprintTidy :: Tidy -> Cube -> Doc #

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

PPrint EQual 

Methods

pprintTidy :: Tidy -> EQual -> Doc #

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

PPrint KIndex 

Methods

pprintTidy :: Tidy -> KIndex -> Doc #

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

PPrint BIndex 

Methods

pprintTidy :: Tidy -> BIndex -> Doc #

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

PPrint BindPred 

Methods

pprintTidy :: Tidy -> BindPred -> Doc #

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

PPrint Command 

Methods

pprintTidy :: Tidy -> Command -> Doc #

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

PPrint GFixSolution 
PPrint Qualifier 
PPrint AxiomEnv 

Methods

pprintTidy :: Tidy -> AxiomEnv -> Doc #

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

PPrint Equation 

Methods

pprintTidy :: Tidy -> Equation -> Doc #

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

PPrint Rewrite 

Methods

pprintTidy :: Tidy -> Rewrite -> Doc #

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

PPrint Trigger 

Methods

pprintTidy :: Tidy -> Trigger -> Doc #

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

PPrint TheorySymbol 
PPrint Sem 

Methods

pprintTidy :: Tidy -> Sem -> Doc #

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

PPrint SmtSort 

Methods

pprintTidy :: Tidy -> SmtSort -> Doc #

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

PPrint IBindEnv 

Methods

pprintTidy :: Tidy -> IBindEnv -> Doc #

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

PPrint Packs 

Methods

pprintTidy :: Tidy -> Packs -> Doc #

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

PPrint Error 

Methods

pprintTidy :: Tidy -> Error -> Doc #

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

PPrint KVar 

Methods

pprintTidy :: Tidy -> KVar -> Doc #

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

PPrint Subst 

Methods

pprintTidy :: Tidy -> Subst -> Doc #

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

PPrint KVSub 

Methods

pprintTidy :: Tidy -> KVSub -> Doc #

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

PPrint SymConst 

Methods

pprintTidy :: Tidy -> SymConst -> Doc #

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

PPrint Constant 

Methods

pprintTidy :: Tidy -> Constant -> Doc #

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

PPrint Brel 

Methods

pprintTidy :: Tidy -> Brel -> Doc #

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

PPrint Bop 

Methods

pprintTidy :: Tidy -> Bop -> Doc #

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

PPrint Expr 

Methods

pprintTidy :: Tidy -> Expr -> Doc #

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

PPrint FTycon 

Methods

pprintTidy :: Tidy -> FTycon -> Doc #

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

PPrint DataField 
PPrint DataCtor 

Methods

pprintTidy :: Tidy -> DataCtor -> Doc #

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

PPrint DataDecl 

Methods

pprintTidy :: Tidy -> DataDecl -> Doc #

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

PPrint Symbol 

Methods

pprintTidy :: Tidy -> Symbol -> Doc #

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

PPrint SrcSpan 

Methods

pprintTidy :: Tidy -> SrcSpan -> Doc #

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

PPrint DocTable 

Methods

pprintTidy :: Tidy -> DocTable -> Doc #

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

PPrint Variance # 

Methods

pprintTidy :: Tidy -> Variance -> Doc #

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

PPrint UserError # 
PPrint Oblig # 

Methods

pprintTidy :: Tidy -> Oblig -> Doc #

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

PPrint KVProf # 

Methods

pprintTidy :: Tidy -> KVProf -> Doc #

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

PPrint KVKind # 

Methods

pprintTidy :: Tidy -> KVKind -> Doc #

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

PPrint Body # 

Methods

pprintTidy :: Tidy -> Body -> Doc #

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

PPrint ModName # 

Methods

pprintTidy :: Tidy -> ModName -> Doc #

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

PPrint SizeFun # 

Methods

pprintTidy :: Tidy -> SizeFun -> Doc #

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

PPrint DataName # 

Methods

pprintTidy :: Tidy -> DataName -> Doc #

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

PPrint Strata # 

Methods

pprintTidy :: Tidy -> Strata -> Doc #

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

PPrint Stratum # 

Methods

pprintTidy :: Tidy -> Stratum -> Doc #

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

PPrint RTyCon # 

Methods

pprintTidy :: Tidy -> RTyCon -> Doc #

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

PPrint BTyCon # 

Methods

pprintTidy :: Tidy -> BTyCon -> Doc #

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

PPrint RTyVar # 

Methods

pprintTidy :: Tidy -> RTyVar -> Doc #

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

PPrint BTyVar # 

Methods

pprintTidy :: Tidy -> BTyVar -> Doc #

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

PPrint Predicate # 
PPrint DiffCheck # 
PPrint CGInfo # 

Methods

pprintTidy :: Tidy -> CGInfo -> Doc #

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

PPrint WfC # 

Methods

pprintTidy :: Tidy -> WfC -> Doc #

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

PPrint SubC # 

Methods

pprintTidy :: Tidy -> SubC -> Doc #

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

PPrint CGEnv # 

Methods

pprintTidy :: Tidy -> CGEnv -> Doc #

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

PPrint Val # 

Methods

pprintTidy :: Tidy -> Val -> Doc #

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

PPrint a => PPrint [a] 

Methods

pprintTidy :: Tidy -> [a] -> Doc #

pprintPrec :: Int -> Tidy -> [a] -> Doc #

PPrint a => PPrint (Maybe a) 

Methods

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

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

PPrint a => PPrint (SizedEnv a) 

Methods

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

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

Fixpoint a => PPrint (WfC a) 

Methods

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

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

Fixpoint a => PPrint (SubC a) 

Methods

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

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

Fixpoint a => PPrint (SimpC a) 

Methods

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

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

PPrint a => PPrint (Triggered a) 

Methods

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

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

PPrint a => PPrint (SEnv a) 

Methods

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

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

PPrint a => PPrint (Located a) 

Methods

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

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

PPrint a => PPrint (HashSet a) 

Methods

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

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

PPrint t => PPrint (CMeasure t) # 

Methods

pprintTidy :: Tidy -> CMeasure t -> Doc #

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

PPrint (PVar a) # 

Methods

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

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

(PPrint a, PPrint b) => PPrint (a, b) 

Methods

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

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

(PPrint a, PPrint b) => PPrint (HashMap a b) 

Methods

pprintTidy :: Tidy -> HashMap a b -> Doc #

pprintPrec :: Int -> Tidy -> HashMap a b -> Doc #

(PPrint a, PPrint b) => PPrint (Sol a b) 

Methods

pprintTidy :: Tidy -> Sol a b -> Doc #

pprintPrec :: Int -> Tidy -> Sol a b -> Doc #

(PPrint t, PPrint a) => PPrint (MSpec t a) # 

Methods

pprintTidy :: Tidy -> MSpec t a -> Doc #

pprintPrec :: Int -> Tidy -> MSpec t a -> Doc #

(PPrint t, PPrint a) => PPrint (Measure t a) # 

Methods

pprintTidy :: Tidy -> Measure t a -> Doc #

pprintPrec :: Int -> Tidy -> Measure t a -> Doc #

PPrint a => PPrint (Def t a) # 

Methods

pprintTidy :: Tidy -> Def t a -> Doc #

pprintPrec :: Int -> Tidy -> Def t a -> Doc #

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

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

Methods

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

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

(PPrint e, PPrint t) => PPrint (Bound t e) # 

Methods

pprintTidy :: Tidy -> Bound t e -> Doc #

pprintPrec :: Int -> Tidy -> Bound t e -> Doc #

(PPrint a, PPrint b, PPrint c) => PPrint (a, b, c) 

Methods

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

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

(PPrint a, PPrint b, PPrint c, PPrint d) => PPrint (a, b, c, d) 

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) 

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

Modules and Imports

data ModName Source #

Module Names --------------------------------------------------------------

Constructors

ModName !ModType !ModuleName 

Refinement Type Aliases

data RTEnv Source #

Refinement Type Aliases ---------------------------------------------------

Constructors

RTE 

Fields

Instances

mapRE :: (HashMap Symbol (RTAlias Symbol Expr) -> HashMap Symbol (RTAlias Symbol Expr)) -> RTEnv -> RTEnv Source #

Errors and Error Messages

type ErrorResult = FixResult UserError Source #

Error Data Type -----------------------------------------------------------

Source information (associated with constraints)

data Cinfo Source #

Source Information Associated With Constraints ----------------------------

Constructors

Ci 

Fields

Instances

Eq Cinfo Source # 

Methods

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

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

Ord Cinfo Source # 

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 #

Generic Cinfo Source # 

Associated Types

type Rep Cinfo :: * -> * #

Methods

from :: Cinfo -> Rep Cinfo x #

to :: Rep Cinfo x -> Cinfo #

NFData Cinfo Source # 

Methods

rnf :: Cinfo -> () #

Loc Cinfo Source # 

Methods

srcSpan :: Cinfo -> SrcSpan #

Fixpoint Cinfo Source # 

Methods

toFix :: Cinfo -> Doc #

simplify :: Cinfo -> Cinfo #

Result (FixResult Cinfo) Source # 
type Rep Cinfo Source # 
type Rep Cinfo = D1 * (MetaData "Cinfo" "Language.Haskell.Liquid.Types" "liquidhaskell-0.8.2.2-CpzODPl6eK730bIB0y0Im0" False) (C1 * (MetaCons "Ci" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "ci_loc") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * SrcSpan)) ((:*:) * (S1 * (MetaSel (Just Symbol "ci_err") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * (Maybe Error))) (S1 * (MetaSel (Just Symbol "ci_var") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * (Maybe Var))))))

Measures

data Measure ty ctor Source #

Constructors

M 

Fields

Instances

Bifunctor Measure Source # 

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 #

Functor (Measure ty) Source # 

Methods

fmap :: (a -> b) -> Measure ty a -> Measure ty b #

(<$) :: a -> Measure ty b -> Measure ty a #

(Data ctor, Data ty) => Data (Measure ty ctor) Source # 

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

Methods

showsPrec :: Int -> Measure t a -> ShowS #

show :: Measure t a -> String #

showList :: [Measure t a] -> ShowS #

Generic (Measure ty ctor) Source # 

Associated Types

type Rep (Measure ty ctor) :: * -> * #

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 # 

Methods

put :: Measure t c -> Put #

get :: Get (Measure t c) #

putList :: [Measure t c] -> Put #

Subable (Measure ty ctor) Source # 

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 #

(PPrint t, PPrint a) => PPrint (Measure t a) Source # 

Methods

pprintTidy :: Tidy -> Measure t a -> Doc #

pprintPrec :: Int -> Tidy -> Measure t a -> Doc #

ExpandAliases ty => ExpandAliases (Measure ty ctor) Source # 

Methods

expand :: SourcePos -> Measure ty ctor -> BareM (Measure ty ctor) Source #

type